MultiCodeROHook.lean
Read-Only Multi-Block Subroutine Hooks
Lifts verified Obj. subroutines to state-transformer hooks (HookOk) backed by read-only byte-slice ownership lib. (↦ᵣ) in spec., without requiring PermsRX, CodeLoaded s0., or SepProp.. Defines the multi-block overlay and restoration primitives loadMultiCodeMem and restoreMultiCodeMem, the induced hook codeROSubroutineHook, and the lifting theorems subroutine, subroutine, and subroutine.
@[expose] public section
def Arm64.
Relocated byte sequence of block k of lib under placement mpl.
def Arm64.Obj.MultiPlacedLib.blockPatched (lib : Arm64.Obj.MultiPlacedLib)
(mpl : Arm64.Obj.MultiPlacement) (k : Nat) : List (BitVec 8) :=
(lib.blockLib k).text.patched (lib.blockPlacement mpl k)
def Arm64.
First block index k < lib. whose relocated code region under mpl contains a (none if a lies outside all code blocks of lib). Under lib., block regions are pairwise disjoint so at most one block contains a.
def Arm64.Obj.MultiPlacedLib.findCodeBlock (lib : Arm64.Obj.MultiPlacedLib)
(mpl : Arm64.Obj.MultiPlacement) (a : BitVec 64) : Option Nat :=
(List.range lib.blocks.length).find? fun k =>
decide (Arm64.InRegion (mpl.base k) (lib.blockPatched mpl k).length a)
def Arm64.
Overlay all blocks k < lib. of lib with some Perm. and their relocated code bytes lib. in m, leaving all addresses outside lib's blocks unchanged.
def Arm64.loadMultiCodeMem (lib : Arm64.Obj.MultiPlacedLib) (mpl : Arm64.Obj.MultiPlacement)
(m : Arm64.Memory) : Arm64.Memory :=
⟨fun a =>
match h : lib.findCodeBlock mpl a with
| some k =>
have hf : (List.range lib.blocks.length).find?
(fun j => decide (Arm64.InRegion (mpl.base j) (lib.blockPatched mpl j).length a)) =
some k := h
have hd := List.find?_some hf
have hin : Arm64.InRegion (mpl.base k) (lib.blockPatched mpl k).length a :=
of_decide_eq_true hd
some (some { Arm64.Perm.rx with anon := m.isAnon a },
(lib.blockPatched mpl k)[(a - mpl.base k).toNat]'hin)
| none => m.cells a⟩
def Arm64.
Restore m0. across all code blocks of lib under mpl, keeping mf. outside lib's code blocks.
def Arm64.restoreMultiCodeMem (lib : Arm64.Obj.MultiPlacedLib) (mpl : Arm64.Obj.MultiPlacement)
(m0 mf : Arm64.Memory) : Arm64.Memory :=
⟨fun a =>
match lib.findCodeBlock mpl a with
| some _ => m0.cells a
| none => mf.cells a⟩
def Arm64.
Entry state for running block i of lib at entry_pc under mpl: sets lr := mpl., pc := entry_pc, and overlays all blocks of lib via loadMultiCodeMem.
def Arm64.multiCodeROHookEntry (lib : Arm64.Obj.MultiPlacedLib) (mpl : Arm64.Obj.MultiPlacement)
(i : Nat) (entry_pc : BitVec 64) (s0 : Arm64.State) : Arm64.State :=
((s0.writeReg64 .lr (mpl.base i + 1#64)).setPC entry_pc).setMem
(Arm64.loadMultiCodeMem lib mpl s0.mem)
def Arm64.
Exit state restoring caller lr, return pc (when sf' stopped at the sentinel mpl.), and code-block memory cells via restoreMultiCodeMem.
def Arm64.multiCodeROHookExit (lib : Arm64.Obj.MultiPlacedLib) (mpl : Arm64.Obj.MultiPlacement)
(i : Nat) (s0 sf' : Arm64.State) : Arm64.State :=
let lr0 := s0.readReg64 .lr
let sf1 := if sf'.pc = mpl.base i + 1#64 ∧ sf'.status = .Running then sf'.setPC lr0 else sf'
(sf1.writeReg64 .lr lr0).setMem (Arm64.restoreMultiCodeMem lib mpl s0.mem sf'.mem)
def Arm64.
State-transformer hook (State → State) induced by exported subroutine fnName of lib under placement mpl, overlaying all blocks via loadMultiCodeMem on entry and restoring caller code-block cells via restoreMultiCodeMem on exit so lib. (↦ᵣ) suffices in spec. without PermsRX or CodeLoaded s0..
open Classical in
noncomputable def Arm64.Obj.MultiPlacedLib.codeROSubroutineHook (lib : Arm64.Obj.MultiPlacedLib)
(mpl : Arm64.Obj.MultiPlacement) (fnName : String)
(externs : String → Option (Arm64.State → Arm64.State) := fun _ => none)
(overrides : String → Option (Arm64.State → Arm64.State) := fun _ => none)
(svc : Arm64.State → Arm64.State := Arm64.Syscall.standard) :
Arm64.State → Arm64.State :=
match Arm64.Obj.lookupBlockSym fnName lib.blocks with
| some (i, _) => fun s0 =>
let prog := lib.blockProgram mpl i externs overrides svc
let s0' := Arm64.multiCodeROHookEntry lib mpl i (lib.fnAddr mpl fnName) s0
if h : ∃ sf', Arm64.StepsUntil prog (Arm64.SubroutineStop s0') s0' sf' ∧
Arm64.SubroutineStop s0' sf' then
Arm64.multiCodeROHookExit lib mpl i s0 (Classical.choose h)
else
s0
| none => id69 declarations not shown (lines 106–1151): theorems, which Lean checks, or definitions that no headline statement uses
Arm64., Arm64., Arm64., ProofLib., ProofLib., ProofLib., ProofLib., ProofLib., ProofLib., ProofLib., ProofLib., ProofLib., ProofLib., ProofLib., ProofLib., ProofLib., ProofLib., ProofLib., ProofLib., ProofLib., ProofLib., ProofLib., ProofLib., ProofLib., ProofLib., ProofLib., ProofLib., ProofLib., ProofLib., ProofLib., ProofLib., ProofLib., ProofLib., ProofLib., ProofLib., ProofLib., ProofLib., ProofLib., ProofLib., ProofLib., _private., ProofLib., ProofLib., ProofLib., ProofLib., ProofLib., ProofLib., ProofLib., ProofLib., ProofLib., _private., _private., _private., _private., ProofLib., ProofLib., _private., _private., _private., ProofLib., …