Skip to content

Commit c83a93e

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

3 files changed

Lines changed: 206 additions & 20 deletions

File tree

‎codelib/CodeLib/SepLogic/Adequacy.lean‎

Lines changed: 106 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -889,4 +889,110 @@ theorem wp_wasm_prop_to_TerminatesWith
889889
| ReturnCall fid st' vs => rw [hexec] at hwp_fuel; exact hwp_fuel.elim
890890
| Throwing tag targs st' s' => rw [hexec] at hwp_fuel; exact hwp_fuel.elim
891891

892+
-- ── iProp trivialize / bridge ──────────────────────────────────────────────────
893+
894+
/-- Trivialize the iProp postcondition: any wp_wasm_iProp entails the Prop WP with
895+
True postcondition. Proved by lfp induction: Ψ' s = wp_wasm_iProp s.{Φ:=⌜True⌝}.
896+
Base cases close by `BI.pure_intro trivial`; step case closes by definitional
897+
equality (Ψ' ignores the Φ field, so Ψ' {Φ=post} = Ψ' {Φ=⌜True⌝} = lfp {⌜True⌝}). -/
898+
lemma wp_wasm_iProp_trivialize
899+
{m : Module} {st : Store Unit} {locals : Locals} {prog : Program}
900+
{env : HostEnv Unit} {post : Store Unit → List Value → IProp WasmHeapGF} :
901+
wp_wasm_iProp m st locals prog env post ⊢
902+
wp_wasm m st locals prog env (fun _ _ => True) := by
903+
rw [wp_wasm_iProp_pure]
904+
let Ψ' : LeibnizO WasmStateIProp → IProp WasmHeapGF :=
905+
fun s => bi_least_fixpoint wp_wasm_iProp_F
906+
⟨{ m := s.car.m, st := s.car.st, locals := s.car.locals,
907+
prog := s.car.prog, env := s.car.env,
908+
Φ := fun _ _ => iprop% ⌜True⌝ }⟩
909+
haveI hΨ' : OFE.NonExpansive Ψ' :=
910+
⟨fun _ _ _ H => (OFE.eq_of_eqv (OFE.discrete H)) ▸ OFE.Dist.rfl⟩
911+
have hstep : ⊢ □ (∀ y : LeibnizO WasmStateIProp, wp_wasm_iProp_F Ψ' y -∗ Ψ' y) := by
912+
iintro !> %s
913+
obtain ⟨ws⟩ := s
914+
rcases hprog : ws.prog with _ | ⟨instr, rest⟩
915+
· -- prog = [] : postcondition → ⌜True⌝ trivially in affine BI
916+
unfold wp_wasm_iProp_F Ψ'; simp only [LeibnizO.car, hprog]
917+
iintro _H
918+
iapply least_fixpoint_unfold_mpr
919+
unfold wp_wasm_iProp_F; simp only [LeibnizO.car, hprog]
920+
exact BI.pure_intro trivial
921+
· by_cases h_ret : instr = Instruction.ret
922+
· -- prog = .ret :: _ : same trivial close
923+
subst h_ret
924+
unfold wp_wasm_iProp_F Ψ'; simp only [LeibnizO.car, hprog]
925+
iintro _H
926+
iapply least_fixpoint_unfold_mpr
927+
unfold wp_wasm_iProp_F; simp only [LeibnizO.car, hprog]
928+
exact BI.pure_intro trivial
929+
· -- prog = instr :: rest (instr ≠ .ret): Ψ' ignores Φ, so Hwp IS the goal
930+
unfold wp_wasm_iProp_F Ψ'; simp only [LeibnizO.car, hprog]
931+
iintro Hwp
932+
iapply least_fixpoint_unfold_mpr
933+
unfold wp_wasm_iProp_F; simp only [LeibnizO.car, hprog]
934+
iexact Hwp
935+
have hfp :
936+
bi_least_fixpoint wp_wasm_iProp_F ⟨{ m, st, locals, prog, env, Φ := post }⟩ ⊢
937+
Ψ' ⟨{ m, st, locals, prog, env, Φ := post }⟩ :=
938+
BI.sep_elim_emp_valid_left hstep
939+
(BI.wand_elim ((BI.wand_entails (least_fixpoint_iter (F := wp_wasm_iProp_F))).trans
940+
(BI.forall_elim (⟨{ m, st, locals, prog, env, Φ := post }⟩ : LeibnizO WasmStateIProp))))
941+
exact hfp
942+
943+
/-- iProp call bridge: from a function spec instance and a valid initial combined
944+
assertion `⊢ genHeapInterp σ ∗ pre st`, extract Prop-level termination.
945+
946+
Takes the funcSatisfies spec instantiated at a specific (env={}, st, args=[]):
947+
hspec : ⊢ pre st -∗ wp_wasm_iProp m st (f.toLocals []) f.body {} post
948+
949+
Proof chain:
950+
hspec + h_init → ⊢ genHeapInterp σ ∗ wp_wasm_iProp ... post
951+
wp_wasm_iProp_trivialize → ⊢ genHeapInterp σ ∗ wp_wasm ... True
952+
wasm_adequacy + pure_soundness → wp_wasm_prop m st (f.toLocals []) f.body {} True
953+
wp_wasm_prop_to_TerminatesWith → TerminatesWith {} m callid st [] (fun _ _ => True)
954+
955+
NOTE: `⊢ genHeapInterp σ ∗ pre st` is the CORRECT combined form (AUTH ∗ FRAG
956+
together), obtainable via `genHeap_init` at allocation time. The form
957+
`genHeapInterp σ ⊢ pre st` (AUTH ⊢ FRAG) is false in the genHeap RA model
958+
and cannot serve as a hypothesis here.
959+
960+
NOTE: This theorem lives in Adequacy (not ModuleLinking) to avoid a circular
961+
import: ModuleLinking imports Adequacy, so Adequacy cannot reference
962+
`funcSatisfies`. Callers unpack `funcSatisfies` via `obtain ⟨f, hf, hspec⟩`
963+
before calling this lemma. -/
964+
theorem wp_wasm_iProp_call
965+
{m : Module} {st : Store Unit} {callid : Nat}
966+
{pre : Store Unit → IProp WasmHeapGF}
967+
{post : Store Unit → List Value → IProp WasmHeapGF}
968+
{f : Function} {σ : WasmHeapMap (Option UInt8)}
969+
(hf : m.funcs[callid]? = some f)
970+
(hspec : ⊢ pre st -∗
971+
wp_wasm_iProp m st (f.toLocals []) f.body {} (fun st' vs => post st' vs))
972+
(h_init : ⊢ genHeapInterp σ ∗ pre st)
973+
(himp : m.imports[callid]? = none)
974+
(h_noimports : m.imports.length = 0)
975+
(hresults : f.results.length = 0) :
976+
TerminatesWith {} m callid st [] (fun _ _ => True) := by
977+
-- Combine initial assertion with body spec
978+
have hwp_init : ⊢ genHeapInterp σ ∗
979+
wp_wasm_iProp m st (f.toLocals []) f.body {} (fun st' vs => post st' vs) :=
980+
h_init.trans (BI.sep_mono_right (BI.wand_entails hspec))
981+
-- Trivialize iProp postcondition to get Prop-level WP
982+
have hwp_true : ⊢ genHeapInterp σ ∗ wp_wasm m st (f.toLocals []) f.body {} (fun _ _ => True) :=
983+
hwp_init.trans (BI.sep_mono_right wp_wasm_iProp_trivialize)
984+
-- Extract Prop-level wp_wasm_prop via adequacy
985+
have hwp_prop : wp_wasm_prop m st (f.toLocals []) f.body {} (fun _ _ => True) :=
986+
pure_soundness (hwp_true.trans (wasm_adequacy m st (f.toLocals []) f.body {} (fun _ _ => True) σ))
987+
-- Convert to TerminatesWith
988+
have h_adj : m.funcs[callid - m.imports.length]? = some f := by
989+
rw [h_noimports, Nat.sub_zero]; exact hf
990+
-- Convert hwp_prop: (args.take f.numParams).reverse for args=[] equals []
991+
have hwp_prop' :
992+
wp_wasm_prop m st
993+
(f.toLocals (([] : List Value).take f.numParams).reverse)
994+
f.body {} (fun _ _ => True) := by
995+
simp only [List.take_nil, List.reverse_nil]; exact hwp_prop
996+
exact wp_wasm_prop_to_TerminatesWith h_adj himp hresults (Nat.zero_le _) (fun _ _ h => h) hwp_prop'
997+
892998
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

‎programs/lean/lake-manifest.json‎

Lines changed: 30 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -8,13 +8,43 @@
88
"inherited": false,
99
"dir": "../../codelib",
1010
"configFile": "lakefile.toml"},
11+
{"url": "https://github.com/leanprover-community/iris-lean.git",
12+
"type": "git",
13+
"subDir": "Iris",
14+
"scope": "",
15+
"rev": "3877dbeccd1b0545c5be7ef73318e8c86acf79ab",
16+
"name": "iris",
17+
"manifestFile": "lake-manifest.json",
18+
"inputRev": null,
19+
"inherited": true,
20+
"configFile": "lakefile.toml"},
1121
{"type": "path",
1222
"scope": "",
1323
"name": "WasmInterpreterLean",
1424
"manifestFile": "lake-manifest.json",
1525
"inherited": true,
1626
"dir": "../../codelib/../interpreter",
1727
"configFile": "lakefile.toml"},
28+
{"url": "https://github.com/leanprover-community/batteries",
29+
"type": "git",
30+
"subDir": null,
31+
"scope": "leanprover-community",
32+
"rev": "fa08db58b30eb033edcdab331bba000827f9f785",
33+
"name": "batteries",
34+
"manifestFile": "lake-manifest.json",
35+
"inputRev": "v4.31.0",
36+
"inherited": true,
37+
"configFile": "lakefile.toml"},
38+
{"url": "https://github.com/leanprover-community/quote4",
39+
"type": "git",
40+
"subDir": null,
41+
"scope": "leanprover-community",
42+
"rev": "f46324995fca5f0483b742e4eb4daec7f4ee50d2",
43+
"name": "Qq",
44+
"manifestFile": "lake-manifest.json",
45+
"inputRev": "v4.31.0",
46+
"inherited": true,
47+
"configFile": "lakefile.toml"},
1848
{"url": "https://github.com/leanprover-community/mathlib4",
1949
"type": "git",
2050
"subDir": null,
@@ -75,26 +105,6 @@
75105
"inputRev": "master",
76106
"inherited": true,
77107
"configFile": "lakefile.toml"},
78-
{"url": "https://github.com/leanprover-community/quote4",
79-
"type": "git",
80-
"subDir": null,
81-
"scope": "leanprover-community",
82-
"rev": "f46324995fca5f0483b742e4eb4daec7f4ee50d2",
83-
"name": "Qq",
84-
"manifestFile": "lake-manifest.json",
85-
"inputRev": "master",
86-
"inherited": true,
87-
"configFile": "lakefile.toml"},
88-
{"url": "https://github.com/leanprover-community/batteries",
89-
"type": "git",
90-
"subDir": null,
91-
"scope": "leanprover-community",
92-
"rev": "fa08db58b30eb033edcdab331bba000827f9f785",
93-
"name": "batteries",
94-
"manifestFile": "lake-manifest.json",
95-
"inputRev": "main",
96-
"inherited": true,
97-
"configFile": "lakefile.toml"},
98108
{"url": "https://github.com/leanprover/lean4-cli",
99109
"type": "git",
100110
"subDir": null,

0 commit comments

Comments
 (0)