LibcHooks.lean🔗

Libc and Allocator HookOk Witnesses

Provides HookOk witnesses for leaf and field-query external hooks (retHook, hookNoop, hookReturnZero, fieldHook, fieldHook64), stack-frame splitting combinators, standard memory operations (memset, memcpy, memmove), and single-slot or bump-pointer pool allocators (witnessAlloc, bumpAllocator, bumpAllocReg).

@[expose] public section

namespace ProofLib

open Arm64

Leaf and field-query hooks

def retHookL36–38 ↗#

Wrap a state transformer f as a leaf subroutine hook that returns to LR (X30).

def retHook (f : State → State) (s : State) : State :=
  (f s).setPC (s.readReg64 .lr)

13 declarations not shown (lines 40–125): theorems, which Lean checks, or definitions that no headline statement uses

ProofLib.hookNoop, ProofLib.hookReturnZero, ProofLib.hookAllocNull, ProofLib.retHook_ok, ProofLib.hookNoop_ok, ProofLib.hookReturnZero_ok, ProofLib.retHook_writeReg64_x0, ProofLib.retHook_writeReg32_x0, ProofLib.regHook_ok, ProofLib.fieldHook, ProofLib.fieldHook64, ProofLib.fieldHook_readReg32_x0, ProofLib.fieldHook64_readReg64_x0

elabL127–147 ↗#

Auto-parameter helper that unfolds concrete Spec.pre / Spec.post projections so simp [ctype_simp] reduces lowered c_spec / c_type_spec handle query contracts.

elab "close_field_hook_entails" : tactic => do
  Lean.Elab.Tactic.evalTactic (← `(tactic| intros))
  let goal ← Lean.Elab.Tactic.getMainGoal
  let ty ← Lean.instantiateMVars (← goal.getType)
  let ty' ← Lean.Core.transform ty (pre := fun e => do
    if e.isAppOfArity ``Spec.pre 4 || e.isAppOfArity ``Spec.post 5 then
      let specExpr := (e.getAppArgs)[1]!
      if let some specUnf ← Lean.Meta.unfoldDefinition? specExpr then
        let args := e.getAppArgs.set! 1 specUnf
        return .visit (← Lean.Meta.whnf (Lean.mkAppN e.getAppFn args))
    return .continue)
  let goal' ← goal.replaceTargetDefEq ty'
  Lean.Elab.Tactic.replaceMainGoal [goal']
  Lean.Elab.Tactic.evalTactic (← `(tactic|
    (try dsimp only;
     try simp only [ctype_simp, true_and, and_true, pure_true_sepConj, sepConj_pure_true,
       sepConj_emp, emp_sepConj];
     try rw [show _ = _ by ac_rfl];
     exact Entails.refl _)))

7 declarations not shown (lines 149–248): theorems, which Lean checks, or definitions that no headline statement uses

ProofLib.fieldHook_ok, ProofLib.fieldHook64_ok, ProofLib.stackAt_split_bottom_of_eq, ProofLib.stackAt_split_hook, ProofLib.stackAt_refold_bottom, ProofLib.len_lt_of_memRegion_hookFrame, ProofLib.hookMemset

def hookMemcpyL250–258 ↗#

Functional hook for void *memcpy(void *dst, const void *src, size_t n) / void *memmove(void *dst, const void *src, size_t n): reads n bytes from X1, writes them to X0, and returns X0 at LR.

def hookMemcpy : State → State :=
  retHook fun s =>
    let dst := s.readReg64 .x0
    let src := s.readReg64 .x1
    let n := (s.readReg64 .x2).toNat
    s.setMem (s.mem.writeBytes dst (s.mem.readBytes src n))

abbrev hookMemmoveL260 ↗#

abbrev hookMemmove : State → State := hookMemcpy

27 declarations not shown (lines 262–675): theorems, which Lean checks, or definitions that no headline statement uses

ProofLib.libcMemsetSpec, ProofLib.hookMemset_ok, ProofLib.memsetRegionSpec, ProofLib.hookMemset_region_ok, ProofLib.libcMemcpySpec, ProofLib.hookMemcpy_ok, ProofLib.memcpyRegionSpec, ProofLib.hookMemcpy_region_ok, ProofLib.libcMemmoveSpec, ProofLib.hookMemmove_ok, ProofLib.witnessAlloc, ProofLib.mallocPoolHook, ProofLib.freePoolHook, ProofLib.witnessAlloc_ok, ProofLib.bumpAllocator, ProofLib.satisfies_bumpAllocator_init, ProofLib.bumpAllocReg, ProofLib.bumpAllocReg_step, ProofLib.bumpAllocReg_noWrap, ProofLib.libcMemcpyROSpec, ProofLib.Allocator.optRegion_zero, ProofLib.Allocator.optRegion_of_ne_zero, ProofLib.Allocator.optZeroBytes_zero, ProofLib.Allocator.allocSeq_nil, ProofLib.Allocator.allocSeq_cons, ProofLib.Allocator.allocSeq_pair_ne, ProofLib.hookFree_ok

end ProofLib