From af8057820145677be85b99a8af69011c2c954eb4 Mon Sep 17 00:00:00 2001
From: Daniel Windham <daniel@atlascomputing.org>
Date: Fri, 12 Apr 2024 03:46:48 -0400
Subject: [PATCH] Add round-trip-identity theorems to file class enum
 de/serializers

---
 ELFSage/Constants/ELFHeader.lean | 40 +++++++++++++++++++++++++-------
 1 file changed, 31 insertions(+), 9 deletions(-)

diff --git a/ELFSage/Constants/ELFHeader.lean b/ELFSage/Constants/ELFHeader.lean
index 06976f8..b8a31cf 100644
--- a/ELFSage/Constants/ELFHeader.lean
+++ b/ELFSage/Constants/ELFHeader.lean
@@ -1,7 +1,11 @@
 import ELFSage.Util.Hex
 /- ELF File Types -/
 
-/- ELf file classes.  The file format is designed to be portable among machines
+structure NatGreaterThan (n : Nat) where
+  val  : Nat
+  isGt : LT.lt n val
+
+/- ELF file classes.  The file format is designed to be portable among machines
 of various sizes, without imposing the sizes of the largest machine on the
 smallest. The class of the file defines the basic types used by the data
 structures of the object file container itself. -/
@@ -13,26 +17,44 @@ inductive ELFHeader.ei_class.values where
   /-- 64-bit architecture --/
   | elfclass64 : ELFHeader.ei_class.values
   /-- unknown data encoding --/
-  | elfclass_other : Nat → ELFHeader.ei_class.values
+  | elfclass_other : NatGreaterThan 2 → ELFHeader.ei_class.values
 
-def ELFHeader.ei_class.fromNat : Nat → ELFHeader.ei_class.values
-  | 0 => .elfclassnone
-  | 1 => .elfclass32
-  | 2 => .elfclass64
-  | n => .elfclass_other n
+def ELFHeader.ei_class.fromNat (n: Nat) : ELFHeader.ei_class.values :=
+  if h : n ≤ 2 then
+    match n with
+    | 0 => .elfclassnone
+    | 1 => .elfclass32
+    | 2 => .elfclass64
+  else
+    .elfclass_other ⟨n, by omega⟩
 
 def ELFHeader.ei_class.toNat : ELFHeader.ei_class.values → Nat
   | .elfclassnone     => 0
   | .elfclass32       => 1
   | .elfclass64       => 2
-  | .elfclass_other n => n
+  | .elfclass_other n => n.1
 
 instance : ToString (ELFHeader.ei_class.values) where
   toString
   | .elfclassnone     => "None"
   | .elfclass32       => "32-bit"
   | .elfclass64       => "64-bit"
-  | .elfclass_other n => s!"Unrecognized ei_class: 0x{Hex.toHex n}"
+  | .elfclass_other n => s!"Unrecognized ei_class: 0x{Hex.toHex n.1}"
+
+theorem ELFHeader.ei_class.fromNat_of_toNat (n : Nat) :
+    ELFHeader.ei_class.toNat (ELFHeader.ei_class.fromNat n) = n := by
+  simp [ELFHeader.ei_class.fromNat, ELFHeader.ei_class.toNat]
+  by_cases h : n = 0; rw [h]; simp
+  by_cases h : n = 1; rw [h]; simp
+  by_cases h : n = 2; rw [h]; simp
+  have h : ¬ n ≤ 2 := (by omega); simp [h]
+
+theorem ELFHeader.ei_class.toNat_of_fromNat (v : ELFHeader.ei_class.values) :
+    ELFHeader.ei_class.fromNat (ELFHeader.ei_class.toNat v) = v := by
+  simp [ELFHeader.ei_class.toNat, ELFHeader.ei_class.fromNat]
+  cases v with
+  | elfclass_other n => let _ := n.isGt; let hn : ¬ n.val ≤ 2 := (by omega); simp [hn]
+  | _ => simp
 
 inductive ELFHeader.ei_data.values where
   /-- invalid data encoding --/