Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add round-trip-identity theorems to file class enum de/serializers #3

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Add round-trip-identity theorems to file class enum de/serializers #3

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
40 changes: 31 additions & 9 deletions ELFSage/Constants/ELFHeader.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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. -/
Expand All @@ -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 --/
Expand Down