Iprop module-linking - #143
Closed
Isabelle9999 wants to merge 18 commits into
Closed
Conversation
Isabelle9999
force-pushed
the
module-linking-clean
branch
2 times, most recently
from
July 13, 2026 17:21
ad18dff to
c83a93e
Compare
Isabelle9999
marked this pull request as ready for review
July 13, 2026 17:34
Collaborator
|
Merge this on top of latest branch of #133 to keep them in sync |
Contributor
Author
|
…truction rules, and adequacy
…2/store32 (zero sorry)
…ith ownership tokens
…stores, wasm_heap_adequacy_with_mem
mfornet
approved these changes
Jul 18, 2026
|
|
||
| open Wasm | ||
|
|
||
| axiom dlmalloc_alloc_spec |
Collaborator
There was a problem hiding this comment.
@El3ssar this might be enough for you for the moment for the encode/decode experiment
@Isabelle9999 please open an issue tracking this axiom: the goal is to convert it to a theorem
…t, Frame dedup, 64-bit WasmRules
…rship, soundness bridge - WasmHeap: GenHeap instantiation (UInt32 → Option UInt8), pointsTo notation, pointsTo_u64/u32 (8/4-byte ownership), arrayAt with element lemmas - WasmRules: load_sound/store_sound bridging physical and ghost memory - WasmWP: Prop-level wp_wasm_prop definition (exists fuel, exec matches Q) - iris-lean added as dependency (BSD, Lean 4.31-matched)
…ock, wpure, per-instruction rules, arrayAt
…equacy sorrys remain)
…(1 adequacy sorry remains)
…th iProp framed specs
…in all module linking files
Isabelle9999
force-pushed
the
module-linking-clean
branch
from
July 26, 2026 15:27
c83a93e to
0145c08
Compare
Contributor
Author
|
rebased onto #156 and got rid of conflicts |
Contributor
Author
|
closing to adapt to small-step |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Overview
module linking :: function specs carry iProp ownership (pointsTo_u64, separating conjunction ∗), so the frame rule guarantees that callers' private memory is untouched across function calls automatically without manual disjointness proofs.
This is the standard Iris-Wasm pattern (PLDI'23, §2.2) adapted for Talos's big-step fuel semantics.
Why we needed
wp_wasm_iPropTalos's existing
wp_wasmtakesQ : Store Unit → List Value → Prop, which is a Prop-level postcondition. This works for intra-module proofs (swap, merge_sort) where Prop composition suffices. But for modulelinking, function specs need iProp postconditions (pointsTo_u64, ∗) so the frame rule operates at the iProp level where ∗ is native.
The solution: a parallel
wp_wasm_iPropthat takesΦ : Store Unit → List Value → IProp WasmHeapGFas postcondition. Both WPs coexist, existing proofs usewp_wasmunchanged, module linking useswp_wasm_iProp. A bridge theorem connects them:This is Talos-specific: Iris-Wasm (small-step) has wp_bind built into Iris generically. Our big-step fuel semantics requires explicit fuel composition (
wp_wasm_iProp_call), which is the standard adaptation every Iris instantiation makes for its language (HeapLang haswp_rec, Iris-Wasm haswp_invoke_native, we havewp_wasm_iProp_call).This parallel architecture means each per-construct rule (block, call, loop) needs both Prop and iProp versions, which cost more maintenance cost.
Generated with Claude Code