Placed.lean🔗

Placed Libraries in Linked ELF Executables (Arm64.Obj.PlacedLib.InElf)

Layer / Role: Arm64 Trusted Computing Base (Role::Spec, definitions only, 0 theorems).
Purpose & Key Exports: When a parsed static ELF executable contains a placed library (Obj.PlacedLib.InElf img lib pl): the patched text and data bytes of lib under placement pl are mapped in img's PT_LOAD segments (text executable, data readable, writable data writable), and each exported function has exactly one .symtab entry, at its placed address. Obj.PlacedLib.LinkedAt lib elfBytes pl says the raw ELF file elfBytes parses to such an image for the Placeable placement pl, and Obj.PlacedLib.LinkedIn lib elfBytes (∃ pl, LinkedAt) is the satisfiability (non-vacuity) witness for a layout-generic library contract (Obj.PlacedLib.subroutineOk) against a real linked binary. InElf constrains pl.ρ only through relocated text/data bytes and data-object placement: a spec mentioning pl.ρ x for a symbol no relocation or data object uses is not tied to the ELF's .symtab.
When to read: Read when auditing a library's precondition-satisfiability statement or when composing a library contract into a whole-binary ELF proof.

@[expose] public section

namespace Arm64.Obj

open Arm64.Process

img maps bytes at [addr, addr + bytes.length) in its PT_LOAD segments: byte i is the byte at addr + i of the first segment containing that address (as in ElfImage.loadState), with a permission satisfying ok.

def ElfMaps (img : ElfImage) (addr : BitVec 64) (bytes : List (BitVec 8)) (ok : Perm → Bool) :
    Prop :=
  ∀ (i : Nat) (hi : i < bytes.length), ∃ p,
    Snapshot.cellAt img.segments (addr + BitVec.ofNat 64 i) = some (some p, bytes[i]) ∧ ok p

3 declarations not shown (lines 48–67): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.Obj.PlacedLib.InElf.data, Arm64.Obj.PlacedLib.InElf.exports, Arm64.Obj.PlacedLib.InElf, Arm64.Obj.PlacedLib.InElf.text, Arm64.Obj.PlacedLib.LinkedAt, Arm64.Obj.PlacedLib.LinkedIn

structure MultiPlacedLib.InElfL69–85 ↗#

The parsed executable img contains multi-block library lib placed under mpl:

every block i's patched text (lib.blocks[i].patched (lib.blockPlacement mpl i)) is mapped executable (r-x) at mpl.base i;
each data object's initial bytes (lib.patchedData mpl d) are mapped at mpl.ρ d.sym, readable if d.readOnly and exactly rw- otherwise;
each exported function e of lib is defined in some block i at offset off and its raw name lib.elfSym e has exactly one .symtab entry, at mpl.base i + off.

structure MultiPlacedLib.InElf (img : ElfImage) (lib : MultiPlacedLib) (mpl : MultiPlacement) :
    Prop where
  blocks : ∀ (i : Nat) (hi : i < lib.blocks.length),
    ElfMaps img (mpl.base i) (lib.blocks[i].patched (lib.blockPlacement mpl i)) (· == Perm.rx)
  data : ∀ d ∈ lib.data,
    ElfMaps img (mpl.ρ d.sym) (lib.patchedData mpl d)
      (fun p => if d.readOnly then p.r else p == Perm.rw)
  exports : ∀ e ∈ lib.exports, ∃ i off,
    lookupBlockSym e lib.blocks = some (i, off) ∧
    lookupUnique (lib.elfSym e) img.symbols = some (mpl.base i + BitVec.ofNat 64 off)

def MultiPlacedLib.LinkedAtL87–92 ↗#

The ELF executable elfBytes links multi-block library lib at multi-block placement mpl: it parses (ElfImage.parse) to an image containing lib under mpl, and lib is Placeable at mpl.

def MultiPlacedLib.LinkedAt (lib : MultiPlacedLib) (elfBytes : List (BitVec 8))
    (mpl : MultiPlacement) : Prop :=
  ∃ img, ElfImage.parse elfBytes = .ok img ∧ lib.Placeable mpl ∧ lib.InElf img mpl

abbrev MultiPlacedLib.LinkedInL94–100 ↗#

The ELF executable elfBytes links multi-block library lib at some multi-block placement (MultiPlacedLib.LinkedAt).

abbrev MultiPlacedLib.LinkedIn (lib : MultiPlacedLib) (elfBytes : List (BitVec 8)) : Prop :=
  ∃ mpl, lib.LinkedAt elfBytes mpl

end Arm64.Obj