Multi.lean
Multi-Block Placed Libraries
Proof infrastructure for Obj.: per-block symbol-resolution coherence (MultiPlacedLib.), ELF loading and Program. transfer (codeLoaded_of_inElf, subroutineOk_toPureMem), cross-block stepping and call tactics (sepWP_call_block, subroutine_ok_of_block, wp_cut_codeLoaded, wp_call_block), kernel-checked Placeable, InElf, and DataDisjoint checkers (checkInElf_spec, Interned., Interned.), sub-library embedding (embedsAt, embed_subroutine_ok), and logarithmic tree-indexed symbol and data lookup (SymIndex, gen_multi_sym_index).
@[expose] public sectionnamespace Arm64.Objopen Arm64.Process ProofLib ProofLib.ObjectLoad ProofLib.ProgramReflection21 declarations not shown (lines 43–319): theorems, which Lean checks, or definitions that no headline statement uses
Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64.
def MultiPlacedLib.
Writable data objects of lib under mpl share no byte with any other data object.
def MultiPlacedLib.DataDisjoint (lib : MultiPlacedLib) (mpl : MultiPlacement) : Prop :=
lib.data.Pairwise fun d₁ d₂ =>
(d₁.readOnly = true ∧ d₂.readOnly = true) ∨
∀ a, InRegion (mpl.ρ d₁.sym) (lib.patchedData mpl d₁).length a →
¬ InRegion (mpl.ρ d₂.sym) (lib.patchedData mpl d₂).length a21 declarations not shown (lines 328–715): theorems, which Lean checks, or definitions that no headline statement uses
Arm64., Arm64., Arm64., Arm64., Arm64., ProofLib., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64.
end Arm64.Objsyntax
Re-establish lib. at an intermediate cut point mid across preceding instructions (including STR/STP memory stores). Pair with wp_steps; wp_call_block ....
syntax "wp_cut_codeLoaded" (ppSpace colGt term:max)? : tacticmacro_rules
macro_rules
| `(tactic| wp_cut_codeLoaded) =>
`(tactic| apply Arm64.Obj.MultiPlacedLib.seq_codeLoaded ‹_›)
| `(tactic| wp_cut_codeLoaded $hcl:term) =>
`(tactic| apply Arm64.Obj.MultiPlacedLib.seq_codeLoaded $hcl)2 declarations not shown (lines 732–774): theorems, which Lean checks, or definitions that no headline statement uses
ProofLib., ProofLib.
syntax
Step a cross-block subroutine call in a MultiPlacedLib: closes any active wp_cut_codeLoaded (MultiPlacedLib.) segment via SepWP. to refresh lib., infers the target block index j from hcall, proves s., and invokes wp_call (MultiPlacedLib. (j := j) (by decide) hcall). Supports wp_call_block hcall, wp_call_block hcall arg, wp_call_block hcall (x := arg), and wp_call_block hcall ... (on_panic := term).
syntax "wp_call_block" ppSpace colGt term:max (ppSpace colGt wppCallOpt)* : tacticelab_rules
elab_rules : tactic
| `(tactic| wp_call_block $hcall:term $[$opts:wppCallOpt]*) => do
let _ ← tryTactic do
let g ← getMainGoal
let isSeqCodeLoaded ← g.withContext do
let ty := (← instantiateMVars (← g.getType)).consumeMData
unless ty.isAppOfArity ``SepWP 6 do return false
let postExpr := (ty.getArg! 4).consumeMData
unless postExpr.isLambda && postExpr.bindingBody!.consumeMData.isLambda do return false
let body2 := postExpr.bindingBody!.consumeMData.bindingBody!.consumeMData
match body2 with
| .forallE _ dom _ _ => return dom.consumeMData.isAppOfArity ``MultiPlacedLib.CodeLoaded 3
| _ => return false
if isSeqCodeLoaded then
let hclId ← freshIdent `hcl_m
evalTactic (← `(tactic| (
apply SepWP.done
· first | wp_norm_lhs | wp_norm_goal | rfl
· wp_norm_lhs
intro $hclId:ident
)))
else
throwError "not seq_codeLoaded"
let g ← getMainGoal
let (jIdx, entryStx?, plIdents, rhoEqs) ← g.withContext do
let hcallExpr ← elabTerm hcall none
let hcallTy ← inferType hcallExpr
let (_, _, concl) ← forallMetaTelescopeReducing hcallTy
let concl ← whnfR (← instantiateMVars concl)
unless concl.isAppOfArity ``Arm64.subroutine_ok 4 do
throwError "wp_call_block: expected `subroutine_ok` contract, got `{concl}`"
let qProg := concl.getArg! 1
let entryE := concl.getArg! 2
let specE := concl.getArg! 3
unless specE.isAppOfArity ``MultiPlacedLib.withCodeLoaded 4 do
throwError "wp_call_block: expected callee spec wrapped with `MultiPlacedLib.withCodeLoaded`, got `{specE}`"
let libE := specE.getArg! 1
let mplE := specE.getArg! 2
let mut foundJ : Option Nat := none
for j in [:64] do
let jStx := Syntax.mkNumLit (toString j)
let libStx ← Term.exprToSyntax libE
let mplStx ← Term.exprToSyntax mplE
let cand ← elabTerm (← `(Arm64.Obj.MultiPlacedLib.blockProgram $libStx $mplStx $jStx)) none
if ← withTransparency .all (isDefEq qProg cand) then
foundJ := some j
break
let some j := foundJ
| throwError "wp_call_block: could not match callee program `{qProg}` to `lib.blockProgram mpl j` for any `j < 64`"
let goalTy ← instantiateMVars (← g.getType)
let scanExpr := mkApp3 (mkConst ``And) goalTy entryE libE
let plIds ← collectPlacementIdents scanExpr
let rhoPairs ← collectRhoEqs goalTy mplE
let mut rhoEqs : Array (TSyntax `term × TSyntax `term) := #[]
for (lhsE, rhsE) in rhoPairs do
rhoEqs := rhoEqs.push (← Term.exprToSyntax lhsE, ← Term.exprToSyntax rhsE)
let eStx ← Term.exprToSyntax entryE
return (j, some eStx, plIds, rhoEqs)
for (lhsStx, rhsStx) in rhoEqs do
let _ ← tryTactic do
let hRhoId ← freshIdent `h_rho
evalTactic (← `(tactic| have $hRhoId:ident : $lhsStx = $rhsStx := rfl))
let jLit := Syntax.mkNumLit (toString jIdx)
let gCur ← getMainGoal
let (progStx, sStx, progIdents) ← gCur.withContext do
let ty := (← instantiateMVars (← gCur.getType)).consumeMData
let pE := ty.getArg! 0
let pIdsRef ← IO.mkRef (#[] : Array Ident)
pE.forEach fun sub => do
if sub.isConst then
let nm := sub.constName!
let sTy ← inferType sub
if sTy.getForallBody.isConstOf ``Arm64.Program then
let pIds ← pIdsRef.get
if !pIds.any (fun i => i.getId == nm) then
pIdsRef.set (pIds.push (mkIdent nm))
return (← Term.exprToSyntax pE, ← Term.exprToSyntax (ty.getArg! 2), ← pIdsRef.get)
let dsimpIds : Array Ident := plIdents ++ #[
mkIdent ``MultiPlacedLib.blockPlacement,
mkIdent ``MultiPlacedLib.fnAddr,
mkIdent ``MultiPlacedLib.resolve,
mkIdent ``lookupBlockSym,
mkIdent ``lookupBlockSymAux,
mkIdent ``lookup]
if let some eStx := entryStx? then
let _ ← tryTactic do
let hpcCallId ← freshIdent `hpc_call
evalTactic (← `(tactic|
have $hpcCallId:ident : ($sStx : Arm64.State).pc = $eStx := by
simp only [wp_norm, arm64_norm]
try simp [$[$dsimpIds:ident],*]
try bv_omega))
let hcallBlkId ← freshIdent `hcall_blk
evalTactic (← `(tactic|
have $hcallBlkId:ident :=
Arm64.Obj.MultiPlacedLib.subroutine_ok_of_block (P := $progStx) (j := $jLit) (by decide) $hcall
(by intro pc; simp only [$[$progIdents:ident],*,
Arm64.Obj.PlacedLib.externAt?_mk_program_none,
Arm64.Obj.MultiPlacedLib.externAt?_mk_blockProgram_none,
Arm64.Obj.PlacedLib.externAt?_program_rebase_none,
Arm64.Obj.MultiPlacedLib.externAt?_blockProgram_rebase_none,
Arm64.Obj.PlacedLib.externAt?_program_none,
Arm64.Obj.MultiPlacedLib.externAt?_blockProgram_none])
(by simp [$[$progIdents:ident],*, Arm64.Obj.MultiPlacedLib.blockProgram, Arm64.Obj.PlacedLib.program, Arm64.Program.rebase])))
evalTactic (← `(tactic| wp_call $hcallBlkId:ident $[$opts]*))
let _ ← tryTactic do evalTactic (← `(tactic| clear $hcallBlkId:ident))138 declarations not shown (lines 900–2568): theorems, which Lean checks, or definitions that no headline statement uses
Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., Arm64., …
end5 declarations not shown (lines 2580–2639): theorems, which Lean checks, or definitions that no headline statement uses
Arm64., _private., _private., _private., _private., _private.
syntax genMultiSymIndex
gen_multi_sym_index <idxName> <lib>: precompute and kernel-certify an O(log B) / O(log S) MultiPlacedLib. over <lib>.blocks and <lib>.data.
syntax (name := genMultiSymIndex) "gen_multi_sym_index " ident ppSpace ident : command1 declaration not shown (lines 2645–2797): theorems, which Lean checks, or definitions that no headline statement uses
Arm64.