Skip to content

Update Lean to current nightly #16

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

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

Update Lean to current nightly #16

Show file tree
Hide file tree
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
8 changes: 4 additions & 4 deletions ELFSage/Types/ELFHeader.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,7 @@ def ELFHeader.ph_end [ELFHeader α] (eh : α) :=

instance [ELFHeader α] : ToString α where
toString eh :=
let ident (i : Fin 16) := (ELFHeader.e_ident eh).bytes.get ⟨ i, by simp [(ELFHeader.e_ident eh).sized] ⟩
let ident (i : Fin 16) := (ELFHeader.e_ident eh).bytes[i]'(by simp [(ELFHeader.e_ident eh).sized])
let identAsHex (i: Fin 16) := toHex (ident i).toNat
let identAsHexLength2 (i: Fin 16) := toHexMinLength (ident i).toNat 2
"ElfHeader {\n" ++
Expand Down Expand Up @@ -149,7 +149,7 @@ def mkELF64Header (bs : ByteArray) (h : bs.size ≥ 0x40) : ELF64Header := {
e_shnum := getUInt16from 0x3C (by omega),
e_shstrndx := getUInt16from 0x3E (by omega),
} where
isBigEndian := bs.get ⟨0x5,by omega⟩ == 2
isBigEndian := bs[0x5] == 2
getUInt16from := if isBigEndian then bs.getUInt16BEfrom else bs.getUInt16LEfrom
getUInt32from := if isBigEndian then bs.getUInt32BEfrom else bs.getUInt32LEfrom
getUInt64from := if isBigEndian then bs.getUInt64BEfrom else bs.getUInt64LEfrom
Expand Down Expand Up @@ -243,7 +243,7 @@ def mkELF32Header (bs : ByteArray) (h : bs.size ≥ 0x34) : ELF32Header := {
e_shnum := getUInt16from 0x30 (by omega),
e_shstrndx := getUInt16from 0x32 (by omega),
} where
isBigEndian := bs.get ⟨0x5,by omega⟩ == 2
isBigEndian := bs[0x5] == 2
getUInt16from := if isBigEndian then bs.getUInt16BEfrom else bs.getUInt16LEfrom
getUInt32from := if isBigEndian then bs.getUInt32BEfrom else bs.getUInt32LEfrom

Expand Down Expand Up @@ -311,7 +311,7 @@ instance : ELFHeader RawELFHeader where

def mkRawELFHeader? (bs : ByteArray) : Except String RawELFHeader :=
if h : bs.size < 5 then throw "Can't determine if this is a 32 or 64 bit binary (not enough bytes)."
else match bs.get ⟨0x4, by omega⟩ with
else match bs[0x4] with
| 1 => .elf32 <$> mkELF32Header? bs
| 2 => .elf64 <$> mkELF64Header? bs
| _ => throw "Can't determine if this is a 32 of 64 bit binary (byte 0x5 of the elf header is bad)"
2 changes: 1 addition & 1 deletion ELFSage/Types/File.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -125,7 +125,7 @@ inductive RawELFFile where

def mkRawELFFile? (bytes : ByteArray) : Except String RawELFFile :=
if h : bytes.size < 5 then throw "Can't determine if this is a 32 or 64 bit binary (not enough bytes)."
else match bytes.get ⟨0x4, by omega⟩ with
else match bytes[0x4] with
| 1 => .elf32 <$> mkELF32File? bytes
| 2 => .elf64 <$> mkELF64File? bytes
| _ => throw "Can't determine if this is a 32 of 64 bit binary (byte 0x5 of the elf header is bad)"
Expand Down
8 changes: 4 additions & 4 deletions ELFSage/Types/SymbolTable.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,8 +45,8 @@ def mkELF64SymbolTableEntry
(h : bs.size - offset ≥ 0x18) :
ELF64SymbolTableEntry := {
st_name := getUInt32from (offset + 0x00) (by omega),
st_info := bs.get ⟨offset + 0x4, by omega⟩,
st_other := bs.get ⟨offset + 0x5, by omega⟩,
st_info := bs[offset + 0x4]
st_other := bs[offset + 0x5]
st_shndx := getUInt16from (offset + 0x6) (by omega),
st_value := getUInt64from (offset + 0x8) (by omega),
st_size := getUInt64from (offset + 0x10) (by omega),
Expand Down Expand Up @@ -87,8 +87,8 @@ def mkELF32SymbolTableEntry
st_name := getUInt32from (offset + 0x00) (by omega),
st_value := getUInt32from (offset + 0x04) (by omega),
st_size := getUInt32from (offset + 0x08) (by omega),
st_info := bs.get ⟨offset + 0x9, by omega⟩,
st_other := bs.get ⟨offset + 0xa, by omega⟩,
st_info := bs[offset + 0x9],
st_other := bs[offset + 0xa],
st_shndx := getUInt16from (offset + 0xb) (by omega) ,
} where
getUInt16from := if isBigEndian then bs.getUInt16BEfrom else bs.getUInt16LEfrom
Expand Down
Loading