Skip to content

Commit 642bdc9

Browse files
Isabelle9999Isabelle9999
committed
sep-logic: wp_wasm_iProp_call + linked_terminates PROVEN, zero sorry in all module linking files
1 parent fc558ed commit 642bdc9

2 files changed

Lines changed: 176 additions & 0 deletions

File tree

‎codelib/CodeLib/SepLogic/Adequacy.lean‎

Lines changed: 106 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1375,4 +1375,110 @@ theorem wasm_heap_adequacy_with_mem
13751375
(wasm_adequacy m st locals prog env Q σ hagree)
13761376
exact hbupd.trans bupd_elim
13771377

1378+
-- ── iProp trivialize / bridge ──────────────────────────────────────────────────
1379+
1380+
/-- Trivialize the iProp postcondition: any wp_wasm_iProp entails the Prop WP with
1381+
True postcondition. Proved by lfp induction: Ψ' s = wp_wasm_iProp s.{Φ:=⌜True⌝}.
1382+
Base cases close by `BI.pure_intro trivial`; step case closes by definitional
1383+
equality (Ψ' ignores the Φ field, so Ψ' {Φ=post} = Ψ' {Φ=⌜True⌝} = lfp {⌜True⌝}). -/
1384+
lemma wp_wasm_iProp_trivialize
1385+
{m : Module} {st : Store Unit} {locals : Locals} {prog : Program}
1386+
{env : HostEnv Unit} {post : Store Unit → List Value → IProp WasmHeapGF} :
1387+
wp_wasm_iProp m st locals prog env post ⊢
1388+
wp_wasm m st locals prog env (fun _ _ => True) := by
1389+
rw [wp_wasm_iProp_pure]
1390+
let Ψ' : LeibnizO WasmStateIProp → IProp WasmHeapGF :=
1391+
fun s => bi_least_fixpoint wp_wasm_iProp_F
1392+
⟨{ m := s.car.m, st := s.car.st, locals := s.car.locals,
1393+
prog := s.car.prog, env := s.car.env,
1394+
Φ := fun _ _ => iprop% ⌜True⌝ }⟩
1395+
haveI hΨ' : OFE.NonExpansive Ψ' :=
1396+
⟨fun _ _ _ H => (OFE.eq_of_eqv (OFE.discrete H)) ▸ OFE.Dist.rfl⟩
1397+
have hstep : ⊢ □ (∀ y : LeibnizO WasmStateIProp, wp_wasm_iProp_F Ψ' y -∗ Ψ' y) := by
1398+
iintro !> %s
1399+
obtain ⟨ws⟩ := s
1400+
rcases hprog : ws.prog with _ | ⟨instr, rest⟩
1401+
· -- prog = [] : postcondition → ⌜True⌝ trivially in affine BI
1402+
unfold wp_wasm_iProp_F Ψ'; simp only [LeibnizO.car, hprog]
1403+
iintro _H
1404+
iapply least_fixpoint_unfold_mpr
1405+
unfold wp_wasm_iProp_F; simp only [LeibnizO.car, hprog]
1406+
exact BI.pure_intro trivial
1407+
· by_cases h_ret : instr = Instruction.ret
1408+
· -- prog = .ret :: _ : same trivial close
1409+
subst h_ret
1410+
unfold wp_wasm_iProp_F Ψ'; simp only [LeibnizO.car, hprog]
1411+
iintro _H
1412+
iapply least_fixpoint_unfold_mpr
1413+
unfold wp_wasm_iProp_F; simp only [LeibnizO.car, hprog]
1414+
exact BI.pure_intro trivial
1415+
· -- prog = instr :: rest (instr ≠ .ret): Ψ' ignores Φ, so Hwp IS the goal
1416+
unfold wp_wasm_iProp_F Ψ'; simp only [LeibnizO.car, hprog]
1417+
iintro Hwp
1418+
iapply least_fixpoint_unfold_mpr
1419+
unfold wp_wasm_iProp_F; simp only [LeibnizO.car, hprog]
1420+
iexact Hwp
1421+
have hfp :
1422+
bi_least_fixpoint wp_wasm_iProp_F ⟨{ m, st, locals, prog, env, Φ := post }⟩ ⊢
1423+
Ψ' ⟨{ m, st, locals, prog, env, Φ := post }⟩ :=
1424+
BI.sep_elim_emp_valid_left hstep
1425+
(BI.wand_elim ((BI.wand_entails (least_fixpoint_iter (F := wp_wasm_iProp_F))).trans
1426+
(BI.forall_elim (⟨{ m, st, locals, prog, env, Φ := post }⟩ : LeibnizO WasmStateIProp))))
1427+
exact hfp
1428+
1429+
/-- iProp call bridge: from a function spec instance and a valid initial combined
1430+
assertion `⊢ genHeapInterp σ ∗ pre st`, extract Prop-level termination.
1431+
1432+
Takes the funcSatisfies spec instantiated at a specific (env={}, st, args=[]):
1433+
hspec : ⊢ pre st -∗ wp_wasm_iProp m st (f.toLocals []) f.body {} post
1434+
1435+
Proof chain:
1436+
hspec + h_init → ⊢ genHeapInterp σ ∗ wp_wasm_iProp ... post
1437+
wp_wasm_iProp_trivialize → ⊢ genHeapInterp σ ∗ wp_wasm ... True
1438+
wasm_adequacy + pure_soundness → wp_wasm_prop m st (f.toLocals []) f.body {} True
1439+
wp_wasm_prop_to_TerminatesWith → TerminatesWith {} m callid st [] (fun _ _ => True)
1440+
1441+
NOTE: `⊢ genHeapInterp σ ∗ pre st` is the CORRECT combined form (AUTH ∗ FRAG
1442+
together), obtainable via `genHeap_init` at allocation time. The form
1443+
`genHeapInterp σ ⊢ pre st` (AUTH ⊢ FRAG) is false in the genHeap RA model
1444+
and cannot serve as a hypothesis here.
1445+
1446+
NOTE: This theorem lives in Adequacy (not ModuleLinking) to avoid a circular
1447+
import: ModuleLinking imports Adequacy, so Adequacy cannot reference
1448+
`funcSatisfies`. Callers unpack `funcSatisfies` via `obtain ⟨f, hf, hspec⟩`
1449+
before calling this lemma. -/
1450+
theorem wp_wasm_iProp_call
1451+
{m : Module} {st : Store Unit} {callid : Nat}
1452+
{pre : Store Unit → IProp WasmHeapGF}
1453+
{post : Store Unit → List Value → IProp WasmHeapGF}
1454+
{f : Function} {σ : WasmHeapMap (Option UInt8)}
1455+
(hf : m.funcs[callid]? = some f)
1456+
(hspec : ⊢ pre st -∗
1457+
wp_wasm_iProp m st (f.toLocals []) f.body {} (fun st' vs => post st' vs))
1458+
(h_init : ⊢ genHeapInterp σ ∗ pre st)
1459+
(himp : m.imports[callid]? = none)
1460+
(h_noimports : m.imports.length = 0)
1461+
(hresults : f.results.length = 0) :
1462+
TerminatesWith {} m callid st [] (fun _ _ => True) := by
1463+
-- Combine initial assertion with body spec
1464+
have hwp_init : ⊢ genHeapInterp σ ∗
1465+
wp_wasm_iProp m st (f.toLocals []) f.body {} (fun st' vs => post st' vs) :=
1466+
h_init.trans (BI.sep_mono_right (BI.wand_entails hspec))
1467+
-- Trivialize iProp postcondition to get Prop-level WP
1468+
have hwp_true : ⊢ genHeapInterp σ ∗ wp_wasm m st (f.toLocals []) f.body {} (fun _ _ => True) :=
1469+
hwp_init.trans (BI.sep_mono_right wp_wasm_iProp_trivialize)
1470+
-- Extract Prop-level wp_wasm_prop via adequacy
1471+
have hwp_prop : wp_wasm_prop m st (f.toLocals []) f.body {} (fun _ _ => True) :=
1472+
pure_soundness (hwp_true.trans (wasm_adequacy m st (f.toLocals []) f.body {} (fun _ _ => True) σ))
1473+
-- Convert to TerminatesWith
1474+
have h_adj : m.funcs[callid - m.imports.length]? = some f := by
1475+
rw [h_noimports, Nat.sub_zero]; exact hf
1476+
-- Convert hwp_prop: (args.take f.numParams).reverse for args=[] equals []
1477+
have hwp_prop' :
1478+
wp_wasm_prop m st
1479+
(f.toLocals (([] : List Value).take f.numParams).reverse)
1480+
f.body {} (fun _ _ => True) := by
1481+
simp only [List.take_nil, List.reverse_nil]; exact hwp_prop
1482+
exact wp_wasm_prop_to_TerminatesWith h_adj himp hresults (Nat.zero_le _) (fun _ _ h => h) hwp_prop'
1483+
13781484
end Wasm.SepLogic

‎codelib/CodeLib/SepLogic/LinkingExample.lean‎

Lines changed: 70 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -61,4 +61,74 @@ theorem linked_two_calls
6161
exact h
6262
exact ⟨h1, h2v⟩
6363

64+
/-- iProp → Prop bridge: the increment function terminates from a valid initial
65+
combined assertion `⊢ genHeapInterp σ ∗ (ptr ↦ v ∗ ptr₂ ↦ u)`.
66+
67+
Uses `wp_wasm_iProp_call` to chain:
68+
funcSatisfies (via frame_rule) + h_init
69+
→ ⊢ genHeapInterp σ ∗ wp_wasm_iProp ... (pointsTo ptr (v+1) ∗ pointsTo ptr₂ u)
70+
→ ⊢ genHeapInterp σ ∗ wp_wasm ... True (trivialize postcondition)
71+
→ wp_wasm_prop ... True (wasm_adequacy + pure_soundness)
72+
→ TerminatesWith {} m incr_idx st [] (fun _ _ => True) (conversion)
73+
74+
## Why `fun _ _ => True` and not `fun st' _ => st'.mem.read64 ptr = v + 2`
75+
76+
The `v + 2` conclusion would require:
77+
1. Sequential composition: a second `TerminatesWith` for the post-state `st₁`
78+
from the first call. But after extracting `True` from the first call we
79+
lose track of `st₁` and cannot build `⊢ genHeapInterp σ₁ ∗ pointsTo ptr (v+1)`
80+
needed to run `wp_wasm_iProp_call` again.
81+
2. Ghost-to-physical link: `genHeap_valid` gives `get? σ addr = some (some byte)`
82+
(ghost map content), not `st'.mem.bytes addr.toNat = byte` (physical memory).
83+
The connection requires `heapAgreesWithMem σ mem` as a maintained invariant,
84+
which is not currently set up as an iProp invariant.
85+
86+
Both missing pieces belong to a heap-with-invariant setup (e.g. Iris invariants
87+
for `heapAgreesWithMem`). This theorem shows the iProp→Prop adequacy path
88+
is already in place; only the sequential ghost-state tracking is missing.
89+
90+
## Hypothesis note
91+
`⊢ genHeapInterp σ ∗ (...)` is the CORRECT combined form (AUTH ∗ FRAG).
92+
The form `genHeapInterp σ ⊢ ...` (AUTH ⊢ FRAG alone) is false in the genHeap
93+
RA model and cannot be used here. -/
94+
theorem linked_terminates
95+
(m : Wasm.Module) (ptr ptr₂ : UInt32) (v u : UInt64)
96+
(incr_idx : Nat)
97+
(h_incr : ∀ w, incrementSpec m incr_idx ptr w)
98+
(st : Store Unit) (σ : WasmHeapMap (Option UInt8))
99+
(h_init : ⊢ genHeapInterp σ ∗ (pointsTo_u64 ptr v ∗ pointsTo_u64 ptr₂ u))
100+
(himp : m.imports[incr_idx]? = none)
101+
(h_noimports : m.imports.length = 0)
102+
(hresults : ∀ f, m.funcs[incr_idx]? = some f → f.results.length = 0) :
103+
TerminatesWith {} m incr_idx st [] (fun _ _ => True) := by
104+
obtain ⟨f, hf, hspec⟩ := frame_rule (pointsTo_u64 ptr₂ u) (h_incr v)
105+
-- Coerce hspec {} st [] to explicit iProp types to avoid HOU when chaining below:
106+
-- the framed pre beta-reduces to (pointsTo_u64 ptr v ∗ pointsTo_u64 ptr₂ u) by
107+
-- (fun _ => pointsTo_u64 ptr v) st = pointsTo_u64 ptr v, handled by isDefEq.
108+
have hspec_inst : ⊢ (iprop% pointsTo_u64 ptr v ∗ pointsTo_u64 ptr₂ u) -∗
109+
wp_wasm_iProp m st (f.toLocals []) f.body {}
110+
(fun st' vs => iprop% pointsTo_u64 ptr (v + 1) ∗ pointsTo_u64 ptr₂ u) :=
111+
hspec {} st []
112+
-- Chain h_init through hspec_inst: ⊢ genHeapInterp σ ∗ wp_wasm_iProp ...
113+
have hwp_init : ⊢ genHeapInterp σ ∗
114+
wp_wasm_iProp m st (f.toLocals []) f.body {}
115+
(fun st' vs => iprop% pointsTo_u64 ptr (v + 1) ∗ pointsTo_u64 ptr₂ u) :=
116+
h_init.trans (BI.sep_mono_right (BI.wand_entails hspec_inst))
117+
-- Trivialize iProp postcondition → Prop WP with True
118+
have hwp_true : ⊢ genHeapInterp σ ∗ wp_wasm m st (f.toLocals []) f.body {} (fun _ _ => True) :=
119+
hwp_init.trans (BI.sep_mono_right wp_wasm_iProp_trivialize)
120+
-- Adequacy: extract Prop-level wp_wasm_prop
121+
have hwp_prop : wp_wasm_prop m st (f.toLocals []) f.body {} (fun _ _ => True) :=
122+
pure_soundness (hwp_true.trans
123+
(wasm_adequacy m st (f.toLocals []) f.body {} (fun _ _ => True) σ))
124+
-- Normalize args form for TerminatesWith ([] take/reverse = [])
125+
have hwp_prop' :
126+
wp_wasm_prop m st
127+
(f.toLocals (([] : List Value).take f.numParams).reverse)
128+
f.body {} (fun _ _ => True) := by
129+
simp only [List.take_nil, List.reverse_nil]; exact hwp_prop
130+
exact wp_wasm_prop_to_TerminatesWith
131+
(by rw [h_noimports, Nat.sub_zero]; exact hf)
132+
himp (hresults f hf) (Nat.zero_le _) (fun _ _ h => h) hwp_prop'
133+
64134
end Wasm.SepLogic.LinkingExample

0 commit comments

Comments
 (0)