From 3aaec1d020219fefa97fe23f356c424ea9c3e79e Mon Sep 17 00:00:00 2001 From: 0xGeorgii Date: Fri, 26 Jun 2026 19:46:56 +0900 Subject: [PATCH 1/5] feat(wasm-to-v): emit post-#21 WasmVerifier contract + e2e fixture MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The translator now emits the proof-skeleton shape the in-tree contract (ROCQ_CONTRACT.md) already documents but the code had not caught up to: - Import the downstream library: `From WasmVerifier Require Import Verifier.` (was `From Wasm Require Import datatypes verifier.`, a non-existent `Wasm.verifier`). - Emit the 1-arg structural obligation `Theorem valid_ : ValidModule .` always (even for zero-spec modules). - Emit per-spec obligations with the 2-arg `ValidSpec`: `Theorem valid___ : ValidSpec ___specs.` (was the pre-#21 2-arg `ValidModule ___specs`). Adds `tests/test_data/inf/spec_const.inf` — a minimal, non-`forall` spec (`spec Answer { fn p() -> i32 { return 42 } }`) whose generated `.v` is discharged end to end against the WasmVerifier Rocq library (`wasm-verifier/theories/examples/E2EGenerated.v`, both `ValidModule` and `ValidSpec` completed with real `Qed`s). A `forall`/uzumaki spec is NOT used on purpose: it lowers to custom `0xfc` opcodes (`BI_uzumaki_num`) that vanilla WasmCert-Coq cannot parse — that path stays blocked pending the assertion-language quantifier lowering. Updates the unit + integration test assertions to the new shape and pins the end-to-end fixture (`spec_propagation_inf::fixture_spec_const_e2e`). Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_0162V1zxr9wVSwNFXuZiF46U --- core/wasm-to-v/src/lib.rs | 26 +++++++++-- core/wasm-to-v/src/translator.rs | 19 +++++++- tests/src/spec_propagation.rs | 44 ++++++++++++------ tests/src/spec_propagation_inf.rs | 73 ++++++++++++++++++++++++++++-- tests/test_data/inf/spec_const.inf | 9 ++++ 5 files changed, 146 insertions(+), 25 deletions(-) create mode 100644 tests/test_data/inf/spec_const.inf diff --git a/core/wasm-to-v/src/lib.rs b/core/wasm-to-v/src/lib.rs index 4fcb873a..6541c814 100644 --- a/core/wasm-to-v/src/lib.rs +++ b/core/wasm-to-v/src/lib.rs @@ -293,9 +293,20 @@ mod tests { output.contains("Definition Fac__Spec1_specs : list N := (3 :: 4 :: 7 :: nil)%N."), "output should contain Fac__Spec1_specs definition; got:\n{output}", ); + // Structural well-formedness theorem (1-arg ValidModule), always emitted. assert!( - output.contains("Theorem valid_Fac__Spec1 : ValidModule Fac Fac__Spec1_specs."), - "output should contain per-spec ValidModule theorem; got:\n{output}", + output.contains("Theorem valid_Fac : ValidModule Fac."), + "output should contain the structural ValidModule theorem; got:\n{output}", + ); + // Per-spec verification theorem uses the 2-arg ValidSpec predicate (post-#21). + assert!( + output.contains("Theorem valid_Fac__Spec1 : ValidSpec Fac Fac__Spec1_specs."), + "output should contain per-spec ValidSpec theorem; got:\n{output}", + ); + // The downstream library namespace is WasmVerifier, not Wasm. + assert!( + output.contains("From WasmVerifier Require Import Verifier."), + "output should import the WasmVerifier contract; got:\n{output}", ); } @@ -312,9 +323,16 @@ mod tests { !output.contains("_specs : list N"), "output should contain no per-spec definitions when the map is empty; got:\n{output}", ); + // No per-spec ValidSpec theorems when there are no specs. + assert!( + !output.contains("ValidSpec"), + "output should contain no ValidSpec theorems when the spec map is empty; got:\n{output}", + ); + // The structural ValidModule theorem is still emitted (contract: a zero-spec module + // emits only the module record and `Theorem valid_ : ValidModule `). assert!( - !output.contains("Theorem valid_"), - "output should contain no theorems when the spec map is empty; got:\n{output}", + output.contains("Theorem valid_Fac : ValidModule Fac."), + "output should still contain the structural ValidModule theorem; got:\n{output}", ); } } diff --git a/core/wasm-to-v/src/translator.rs b/core/wasm-to-v/src/translator.rs index 3af707e9..a36fe00a 100644 --- a/core/wasm-to-v/src/translator.rs +++ b/core/wasm-to-v/src/translator.rs @@ -134,6 +134,7 @@ //! From Wasm Require Import bytes. //! From Wasm Require Import numerics. //! From Wasm Require Import datatypes. +//! From WasmVerifier Require Import Verifier. //! //! (* Helper definitions *) //! Definition Vi32 i := ... @@ -338,7 +339,8 @@ impl WasmParseData<'_> { res.push_str("Require Import ZArith.\n"); res.push_str("From Wasm Require Import bytes.\n"); res.push_str("From Wasm Require Import numerics.\n"); - res.push_str("From Wasm Require Import datatypes verifier.\n"); + res.push_str("From Wasm Require Import datatypes.\n"); + res.push_str("From WasmVerifier Require Import Verifier.\n"); res.push('\n'); res.push_str("Definition Vi32 i := VAL_int32 (Wasm_int.int_of_Z i32m i).\n"); res.push_str("Definition Vi64 i := VAL_int64 (Wasm_int.int_of_Z i64m i).\n"); @@ -571,11 +573,24 @@ impl WasmParseData<'_> { res.push_str("Section Host.\n"); res.push_str("Context `{ho: host}.\n"); res.push('\n'); + // Structural well-formedness obligation. Always emitted (even for a module with + // zero specs): `ValidModule` is the 1-argument predicate fixed by ROCQ_CONTRACT.md + // and asserts the module type-checks (WasmCert's `module_typing`), independent of + // any spec indices. + res.push('\n'); + res.push_str( + format!("Theorem valid_{module_name} : ValidModule {module_name}.\n").as_str(), + ); + res.push_str("Proof.\n"); + res.push_str(" (* TODO: fill the proof *)\n"); + res.push_str("Qed.\n"); + // Per-spec verification obligations. `ValidSpec` is the 2-argument predicate (module + // and the list of WASM function indices for this spec); it entails `ValidModule`. for (spec_name, _) in &spec_entries { res.push('\n'); res.push_str( format!( - "Theorem valid_{module_name}__{spec_name} : ValidModule {module_name} {module_name}__{spec_name}_specs.\n" + "Theorem valid_{module_name}__{spec_name} : ValidSpec {module_name} {module_name}__{spec_name}_specs.\n" ) .as_str(), ); diff --git a/tests/src/spec_propagation.rs b/tests/src/spec_propagation.rs index e3380837..e33454b1 100644 --- a/tests/src/spec_propagation.rs +++ b/tests/src/spec_propagation.rs @@ -342,8 +342,8 @@ mod scenario_4_per_spec_emission { use rustc_hash::FxHashMap; /// Two specs `A` and `B` produce per-spec definitions and theorems sorted - /// alphabetically. Each spec yields a `ValidModule ___specs` - /// theorem. + /// alphabetically. Each spec yields a `ValidSpec ___specs` + /// theorem (alongside the single structural `ValidModule `). /// /// Note: the codegen always embeds module name `"output"` into the WASM /// name section, which the translator's custom-name-section handling uses @@ -367,11 +367,15 @@ mod scenario_4_per_spec_emission { "specs should be emitted alphabetically (A before B):\n{v}" ); assert!( - v.contains("Theorem valid_output__A : ValidModule output output__A_specs."), + v.contains("Theorem valid_output : ValidModule output."), + "structural ValidModule theorem missing:\n{v}" + ); + assert!( + v.contains("Theorem valid_output__A : ValidSpec output output__A_specs."), "per-spec theorem for A missing:\n{v}" ); assert!( - v.contains("Theorem valid_output__B : ValidModule output output__B_specs."), + v.contains("Theorem valid_output__B : ValidSpec output output__B_specs."), "per-spec theorem for B missing:\n{v}" ); } @@ -574,8 +578,8 @@ mod scenario_5_empty_list { /// /// The codegen embeds module name `"output"` into the WASM name section, /// so even though we pass `"Empty"`, the module definition is named - /// `output`. With no specs, the translator emits no theorems at all - /// (each `ValidModule ___specs` theorem is per-spec). + /// `output`. With no specs, the translator emits no per-spec `ValidSpec` + /// theorems, but it still emits the structural `valid_ : ValidModule `. #[test] fn empty_map_yields_no_spec_definition() { let source = r#"pub fn main() -> i32 { return 0; }"#; @@ -587,8 +591,12 @@ mod scenario_5_empty_list { "no per-spec definitions expected when map is empty:\n{v}" ); assert!( - !v.contains("Theorem valid_"), - "no theorems expected when the spec map is empty:\n{v}" + !v.contains("ValidSpec"), + "no per-spec ValidSpec theorems expected when the spec map is empty:\n{v}" + ); + assert!( + v.contains("Theorem valid_output : ValidModule output."), + "the structural ValidModule theorem should still be emitted:\n{v}" ); } @@ -1241,7 +1249,7 @@ mod scenario_7_empty_spec { /// A user-authored empty `spec MySpec { }` must surface a per-spec entry /// with an empty index list, so the Rocq translator still emits both a /// `Definition output__MySpec_specs : list N := (@nil N).` line and a - /// `Theorem valid_output__MySpec : ValidModule output output__MySpec_specs.` + /// `Theorem valid_output__MySpec : ValidSpec output output__MySpec_specs.` /// theorem. Without `ensure_spec_registered`, the spec vanished silently /// from the proof artifact because the bucket iteration only recorded /// entries for non-empty inner defs. @@ -1268,7 +1276,7 @@ mod scenario_7_empty_spec { "empty spec must emit the `(@nil N)` definition line:\n{v}" ); assert!( - v.contains("Theorem valid_output__MySpec : ValidModule output output__MySpec_specs."), + v.contains("Theorem valid_output__MySpec : ValidSpec output output__MySpec_specs."), "empty spec must emit the per-spec theorem:\n{v}" ); } @@ -1493,8 +1501,8 @@ mod scenario_10_wasm_to_v_compile_mode { /// Compile a spec-bearing source in compile mode and feed the bytes to /// `wasm_to_v` with an empty explicit map. Result: NO per-spec definitions - /// and NO theorems at all (the `ValidModule ___specs` - /// theorems are strictly per-spec, so a specless translation emits none). + /// and NO per-spec `ValidSpec` theorems (specs are stripped in compile mode), + /// but the structural `valid_ : ValidModule ` is still emitted. /// /// The WASM-embedded module name `"output"` overrides `mod_name`. #[test] @@ -1504,16 +1512,22 @@ mod scenario_10_wasm_to_v_compile_mode { let empty: FxHashMap> = FxHashMap::default(); let v = inference::wasm_to_v("Mod", output.wasm(), &empty).expect("translate ok"); - // No per-spec definition or theorem lines. + // No per-spec definition or ValidSpec lines. assert_eq!( v.matches("_specs : list N").count(), 0, "no per-spec definitions expected:\n{v}" ); assert_eq!( - v.matches("Theorem valid_").count(), + v.matches("ValidSpec").count(), 0, - "no theorems expected for a specless translation:\n{v}" + "no per-spec ValidSpec theorems expected for a specless translation:\n{v}" + ); + // The structural ValidModule theorem is still emitted. + assert_eq!( + v.matches("Theorem valid_output : ValidModule output.").count(), + 1, + "exactly one structural ValidModule theorem expected:\n{v}" ); } } diff --git a/tests/src/spec_propagation_inf.rs b/tests/src/spec_propagation_inf.rs index aa160159..114571c1 100644 --- a/tests/src/spec_propagation_inf.rs +++ b/tests/src/spec_propagation_inf.rs @@ -132,8 +132,8 @@ mod fixture_spec_method { "per-spec definition for Geometry must be emitted:\n{v}" ); assert!( - v.contains("Theorem valid_specmethod__Geometry : ValidModule specmethod specmethod__Geometry_specs."), - "per-spec ValidModule theorem missing:\n{v}" + v.contains("Theorem valid_specmethod__Geometry : ValidSpec specmethod specmethod__Geometry_specs."), + "per-spec ValidSpec theorem missing:\n{v}" ); } } @@ -255,10 +255,15 @@ mod fixture_three_specs { "empty spec must emit `(@nil N)`:\n{v}" ); - // Each spec also gets its `valid___` theorem. + // The structural well-formedness theorem is emitted once. + assert!( + v.contains("Theorem valid_threespecs : ValidModule threespecs."), + "missing structural ValidModule theorem in:\n{v}" + ); + // Each spec also gets its `valid___ : ValidSpec` theorem. for spec in &["Alpha", "Beta", "Gamma"] { let needle = format!( - "Theorem valid_threespecs__{spec} : ValidModule threespecs threespecs__{spec}_specs." + "Theorem valid_threespecs__{spec} : ValidSpec threespecs threespecs__{spec}_specs." ); assert!( v.contains(&needle), @@ -362,3 +367,63 @@ mod fixture_with_spec_smoke { ); } } + +// ============================================================================ +// Fixture 6: spec_const.inf — the end-to-end WasmVerifier contract artifact +// ============================================================================ +#[cfg(test)] +mod fixture_spec_const_e2e { + use super::helpers::compile_inf; + use inference_wasm_codegen::CompilationMode; + use rustc_hash::FxHashMap; + + /// `spec_const.inf` is the fixture whose generated `.v` is discharged end to + /// end against the WasmVerifier Rocq library (see + /// `wasm-verifier/theories/examples/E2EGenerated.v`, which completes the two + /// `(* TODO *)` proofs with real `Qed`s). This test pins the *generated* + /// shape the downstream proof depends on: the `WasmVerifier.Verifier` import, + /// the spec function `p` returning the constant 42, the per-spec index list, + /// and the post-#21 contract theorems (1-arg `ValidModule` + 2-arg + /// `ValidSpec`). If any of these drift, the downstream `.v` stops compiling. + #[test] + fn spec_const_inf_emits_wasmverifier_contract() { + let output = compile_inf("spec_const.inf", CompilationMode::Proof, "spec_const"); + let wasm = output.wasm(); + inf_wasmparser::validate(wasm).expect("WASM must validate"); + + let by_spec = output.spec_func_indices_by_spec(); + assert!( + by_spec.contains_key("Answer"), + "spec Answer must appear in the per-spec map; got {by_spec:?}" + ); + + let empty: FxHashMap> = FxHashMap::default(); + let v = inference::wasm_to_v("spec_const", wasm, &empty).expect("translate ok"); + + // Downstream contract namespace. + assert!( + v.contains("From WasmVerifier Require Import Verifier."), + "generated .v must import the WasmVerifier contract:\n{v}" + ); + // The spec function `p` (WASM index 1) returns the constant 42. + assert!( + v.contains("BI_const_num (Vi32 42)"), + "spec function body must push the constant 42:\n{v}" + ); + assert!( + v.contains("Definition spec_const__Answer_specs : list N := (1 :: nil)%N."), + "per-spec index list must be [1]:\n{v}" + ); + // Post-#21 contract: 1-arg ValidModule + 2-arg ValidSpec. + assert!( + v.contains("Theorem valid_spec_const : ValidModule spec_const."), + "structural ValidModule theorem missing:\n{v}" + ); + assert!( + v.contains( + "Theorem valid_spec_const__Answer : ValidSpec spec_const spec_const__Answer_specs." + ), + "per-spec ValidSpec theorem missing:\n{v}" + ); + } +} diff --git a/tests/test_data/inf/spec_const.inf b/tests/test_data/inf/spec_const.inf new file mode 100644 index 00000000..50d6da86 --- /dev/null +++ b/tests/test_data/inf/spec_const.inf @@ -0,0 +1,9 @@ +fn dummy() -> i32 { + return 0; +} + +spec Answer { + fn p() -> i32 { + return 42; + } +} From 9a7ca5b7a69d3fae9beec97f63e230f71e5a2d95 Mon Sep 17 00:00:00 2001 From: 0xGeorgii Date: Fri, 26 Jun 2026 23:04:06 +0900 Subject: [PATCH 2/5] feat(wasm-codegen): lower spec `@` (uzumaki) to a function parameter MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Inside a `spec` block a scalar `@` denotes a universally-quantified value, not runtime non-determinism. Emitting the custom 0xfc uzumaki opcode made a `forall`-spec body unparseable by the downstream vanilla WasmCert-Coq library. Instead, in proof mode (`current_spec.is_some()`) pre-scan the spec function body for scalar `@` occurrences (collect_spec_uzumaki_params), append one synthetic i32/i64 parameter per `@` (uzumaki_param_map), and lower each `@` to a `local.get` of its param. The `forall` then collapses into the universal the downstream ValidSpec/sem_triple already quantifies over, so a `forall`-spec body becomes ordinary WASM and is dischargeable. A function-level `fn f() forall { .. }` body never emitted the `forall` *wrapper* opcode (codegen lowers the body block's statements directly), so `@` was the only non-vanilla opcode — this closes the whole gap. Non-spec functions and array/struct `@` are unchanged. Fixture tests/test_data/inf/refl_spec.inf + regression spec_propagation_inf::fixture_refl_spec_e2e pin the lowered shape (`refl : (i32) -> ()`, vanilla body, no custom opcode in the generated .v). Discharged end to end in wasm-verifier's E2EReflSpec.v. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_0162V1zxr9wVSwNFXuZiF46U --- core/wasm-codegen/src/compiler.rs | 186 ++++++++++++++++++++++++++++++ tests/src/spec_propagation_inf.rs | 73 ++++++++++++ tests/test_data/inf/refl_spec.inf | 10 ++ 3 files changed, 269 insertions(+) create mode 100644 tests/test_data/inf/refl_spec.inf diff --git a/core/wasm-codegen/src/compiler.rs b/core/wasm-codegen/src/compiler.rs index 869fd30b..6dc1be66 100644 --- a/core/wasm-codegen/src/compiler.rs +++ b/core/wasm-codegen/src/compiler.rs @@ -56,6 +56,19 @@ //! //! Non-det blocks are structured blocks (like `block`/`loop`/`if`), terminated by a //! regular `end` instruction (0x0b). +//! +//! # Spec functions: `@` → parameter (proof mode) +//! +//! Inside a `spec` block, a scalar `@` (uzumaki) denotes a *universally-quantified* value, +//! not runtime non-determinism. Rather than emit the non-vanilla `0xfc` opcode (which the +//! downstream Rocq library built on vanilla WasmCert-Coq cannot parse), each scalar `@` in a +//! spec function is lowered to a synthetic **function parameter** (read back with `local.get`): +//! see [`Compiler::collect_spec_uzumaki_params`] / [`Compiler::uzumaki_param_map`] and the +//! `Expr::Uzumaki` arm of [`Compiler::lower_expression`]. The `forall` then collapses into the +//! ∀ the downstream `ValidSpec`/`sem_triple` already quantifies over, so a `forall`-spec body +//! becomes ordinary WASM (a function-level `fn f() forall { .. }` body never emits the `forall` +//! *wrapper* opcode — codegen lowers the body block's statements directly). Non-spec functions +//! and array/struct `@` keep the opcode path above unchanged. use crate::errors::CodegenError; use rustc_hash::FxHashMap; @@ -369,6 +382,14 @@ pub(crate) struct Compiler { /// zero. Set only during variable initialization (`Stmt::VarDef`), never /// during assignment where slots may hold non-zero data. init_zero_elision: bool, + /// Per-function map from a scalar `@` (uzumaki) expression to the WASM local + /// index of the synthetic function parameter it was lowered to. Populated only + /// for functions inside a `spec` block (proof mode): there each `@` denotes a + /// universally-quantified value, which we model as an extra function parameter + /// (the `forall` becomes the ∀ the downstream `ValidSpec`/`sem_triple` already + /// quantifies over) rather than the non-vanilla `0xfc` uzumaki opcode. An empty + /// map (every non-spec function) leaves `@` lowering byte-identical to before. + uzumaki_param_map: FxHashMap, /// WASM function indices for functions that originated in `spec` blocks, /// keyed by spec name. Populated during Stage 1 registration in proof mode; /// consumed (moved out) by [`Self::finish_and_take`] so the Rocq translator @@ -431,6 +452,7 @@ impl Compiler { loop_ctx: LoopContext::default(), parent_blocks_stack: Vec::new(), init_zero_elision: false, + uzumaki_param_map: FxHashMap::default(), spec_func_indices_by_spec: FxHashMap::default(), frame_sizes: FxHashMap::default(), emit_bounds_checks: false, @@ -1037,6 +1059,7 @@ impl Compiler { let mut params: Vec = vec![]; self.locals_map.clear(); + self.uzumaki_param_map.clear(); self.loop_ctx = LoopContext::default(); self.parent_blocks_stack.clear(); let mut local_idx: u32 = 0; @@ -1088,6 +1111,29 @@ impl Compiler { } } + // Spec-mode `@` (uzumaki) lowering: inside a `spec` block each scalar `@` + // denotes a universally-quantified value. Rather than emit the non-vanilla + // `0xfc` uzumaki opcode (which vanilla WasmCert-Coq cannot parse), we append + // one synthetic function parameter per `@`, so the `forall` collapses into the + // ∀ that the downstream `ValidSpec`/`sem_triple` already quantifies over and the + // whole spec body becomes plain WASM. Synthetic params follow the declared + // params/locals in index order, sorted by source position for determinism. + // Non-spec functions never enter this branch, so their `@` stays byte-identical. + if self.current_spec.is_some() { + let mut uzumaki_exprs: Vec<(ExprId, ValType)> = Vec::new(); + Self::collect_spec_uzumaki_params(arena, body_id, ctx, &mut uzumaki_exprs); + for (expr_id, vt) in uzumaki_exprs { + cov_mark::hit!(wasm_codegen_assign_uzumaki_param); + params.push(vt); + let prev = self.uzumaki_param_map.insert(expr_id, local_idx); + debug_assert!( + prev.is_none(), + "each `@` expression id is visited once by the uzumaki pre-scan", + ); + local_idx += 1; + } + } + let param_count = local_idx; let has_return_value = is_sret || !results.is_empty(); @@ -1376,6 +1422,136 @@ impl Compiler { } } + /// Pre-scans a `spec`-function body collecting every scalar `@` (uzumaki) + /// expression together with the WASM value type it lowers to, in source order. + /// Each becomes a synthetic function parameter (see the call site in + /// [`Self::visit_function_definition_body`]). Array/struct uzumaki are excluded: + /// they lower to element-wise memory stores rather than a single scalar value, + /// so they keep the existing opcode path and are out of scope for the + /// `@`→parameter spec lowering. The block descent mirrors + /// [`Self::pre_scan_locals`]. + fn collect_spec_uzumaki_params( + arena: &AstArena, + block_id: BlockId, + ctx: &TypedContext, + out: &mut Vec<(ExprId, ValType)>, + ) { + for &stmt_id in &arena[block_id].stmts { + match &arena[stmt_id].kind { + Stmt::Expr(e) | Stmt::Return { expr: e } | Stmt::Assert { expr: e } => { + Self::collect_uzumaki_in_expr(arena, *e, ctx, out); + } + Stmt::Assign { left, right } => { + Self::collect_uzumaki_in_expr(arena, *left, ctx, out); + Self::collect_uzumaki_in_expr(arena, *right, ctx, out); + } + Stmt::VarDef { value, .. } => { + if let Some(v) = value { + Self::collect_uzumaki_in_expr(arena, *v, ctx, out); + } + } + Stmt::Block(inner) => { + Self::collect_spec_uzumaki_params(arena, *inner, ctx, out); + } + Stmt::If { + condition, + then_block, + else_block, + } => { + Self::collect_uzumaki_in_expr(arena, *condition, ctx, out); + Self::collect_spec_uzumaki_params(arena, *then_block, ctx, out); + if let Some(else_id) = else_block { + Self::collect_spec_uzumaki_params(arena, *else_id, ctx, out); + } + } + Stmt::Loop { condition, body } => { + if let Some(c) = condition { + Self::collect_uzumaki_in_expr(arena, *c, ctx, out); + } + Self::collect_spec_uzumaki_params(arena, *body, ctx, out); + } + Stmt::Break | Stmt::TypeDef { .. } | Stmt::ConstDef(_) => {} + } + } + } + + /// Recursively collects scalar `@` (uzumaki) expressions in `expr_id` and its + /// sub-expressions. Supporting helper for [`Self::collect_spec_uzumaki_params`]; + /// the expression descent mirrors [`Self::expr_has_dynamic_array_index`]. + fn collect_uzumaki_in_expr( + arena: &AstArena, + expr_id: ExprId, + ctx: &TypedContext, + out: &mut Vec<(ExprId, ValType)>, + ) { + match &arena[expr_id].kind { + Expr::Uzumaki => { + if let Some(vt) = ctx + .get_node_typeinfo(NodeId::Expr(expr_id)) + .and_then(|ti| Self::scalar_uzumaki_valtype(&ti.kind)) + { + out.push((expr_id, vt)); + } + } + Expr::ArrayIndexAccess { array, index } => { + Self::collect_uzumaki_in_expr(arena, *array, ctx, out); + Self::collect_uzumaki_in_expr(arena, *index, ctx, out); + } + Expr::Binary { left, right, .. } => { + Self::collect_uzumaki_in_expr(arena, *left, ctx, out); + Self::collect_uzumaki_in_expr(arena, *right, ctx, out); + } + Expr::PrefixUnary { expr, .. } + | Expr::Parenthesized { expr } + | Expr::MemberAccess { expr, .. } + | Expr::TypeMemberAccess { expr, .. } => { + Self::collect_uzumaki_in_expr(arena, *expr, ctx, out); + } + Expr::FunctionCall { function, args, .. } => { + Self::collect_uzumaki_in_expr(arena, *function, ctx, out); + for (_, arg) in args { + Self::collect_uzumaki_in_expr(arena, *arg, ctx, out); + } + } + Expr::StructLiteral { fields, .. } => { + for (_, value) in fields { + Self::collect_uzumaki_in_expr(arena, *value, ctx, out); + } + } + Expr::ArrayLiteral { elements } => { + for &e in elements { + Self::collect_uzumaki_in_expr(arena, e, ctx, out); + } + } + Expr::Identifier(_) + | Expr::NumberLiteral { .. } + | Expr::BoolLiteral { .. } + | Expr::StringLiteral { .. } + | Expr::UnitLiteral + | Expr::Type(_) => {} + } + } + + /// Returns the WASM value type for a scalar uzumaki of the given type kind, or + /// `None` for non-scalar (array/struct) uzumaki. Mirrors the scalar arms of the + /// `Expr::Uzumaki` case in [`Self::lower_expression`]. + fn scalar_uzumaki_valtype(kind: &TypeInfoKind) -> Option { + match kind { + TypeInfoKind::Bool + | TypeInfoKind::Number( + NumberType::I8 + | NumberType::U8 + | NumberType::I16 + | NumberType::U16 + | NumberType::I32 + | NumberType::U32, + ) + | TypeInfoKind::Enum(_, _) => Some(ValType::I32), + TypeInfoKind::Number(NumberType::I64 | NumberType::U64) => Some(ValType::I64), + _ => None, + } + } + /// Returns `true` if the function body contains at least one *dynamic* array /// index — an `Expr::ArrayIndexAccess` whose index is not a numeric literal. /// @@ -2351,6 +2527,16 @@ impl Compiler { } Expr::Type(_) => todo!(), Expr::Uzumaki => { + // Spec-mode lowering: a scalar `@` inside a `spec` block was assigned + // a synthetic function parameter (see `visit_function_definition_body`). + // Read it back as a plain `local.get` instead of emitting the non-vanilla + // `0xfc` uzumaki opcode, so the spec body is ordinary WASM. The map is + // empty for every non-spec function, so this branch is never taken there. + if let Some(¶m_idx) = self.uzumaki_param_map.get(&expr_id) { + cov_mark::hit!(wasm_codegen_emit_uzumaki_param); + self.func().instruction(&Instruction::LocalGet(param_idx)); + return; + } let node_id = NodeId::Expr(expr_id); let type_info = ctx .get_node_typeinfo(node_id) diff --git a/tests/src/spec_propagation_inf.rs b/tests/src/spec_propagation_inf.rs index 114571c1..717ba0c9 100644 --- a/tests/src/spec_propagation_inf.rs +++ b/tests/src/spec_propagation_inf.rs @@ -427,3 +427,76 @@ mod fixture_spec_const_e2e { ); } } + +// ============================================================================ +// Fixture 7: refl_spec.inf — the SPEC ESSENCE e2e (forall + @ + assert) +// ============================================================================ +#[cfg(test)] +mod fixture_refl_spec_e2e { + use super::helpers::compile_inf; + use inference_wasm_codegen::CompilationMode; + use rustc_hash::FxHashMap; + + /// `refl_spec.inf` exercises the spec constructs the earlier `spec_const` + /// fixture dodged — a `forall`-block introducing a `@` (uzumaki) value and an + /// `assert`. The codegen `@`→parameter lowering turns the whole spec body into + /// *vanilla* WASM (no `0xfc` opcode), so it both validates and is dischargeable + /// downstream (`wasm-verifier/theories/examples/E2EReflSpec.v` completes the two + /// generated proofs with real `Qed`s). This test pins the lowered shape: + /// the `@` became function parameter 0 (`refl : (i32) -> ()`), the body is + /// `local.get; local.set; local.get; local.get; i32.eq; i32.eqz; if`, and no + /// custom uzumaki/nondet opcode survives. + #[test] + fn refl_spec_inf_lowers_uzumaki_to_param() { + let output = compile_inf("refl_spec.inf", CompilationMode::Proof, "refl_spec"); + let wasm = output.wasm(); + // A `0xfc`-prefixed uzumaki opcode would make this fail to validate under + // vanilla rules; that it validates is the proof the body is plain WASM. + inf_wasmparser::validate(wasm).expect("WASM must validate (no custom opcodes)"); + + let by_spec = output.spec_func_indices_by_spec(); + assert_eq!( + by_spec.get("ReflSpec").map(Vec::as_slice), + Some([1u32].as_slice()), + "spec ReflSpec's function must be WASM index 1; got {by_spec:?}" + ); + + let empty: FxHashMap> = FxHashMap::default(); + let v = inference::wasm_to_v("refl_spec", wasm, &empty).expect("translate ok"); + + // The `@` was lowered to a parameter: the spec function's type is (i32) -> (). + assert!( + v.contains("Tf (T_num T_i32 :: nil) (nil)"), + "refl's type must take the @-introduced value as an i32 param:\n{v}" + ); + // The lowered assert body is vanilla WASM. + for needle in [ + "BI_local_get 0%N", + "BI_local_set 1%N", + "BI_relop T_i32 (Relop_i ROI_eq)", + "BI_testop T_i32 TO_eqz", + "BI_if (BT_valtype None)", + ] { + assert!(v.contains(needle), "generated body missing `{needle}`:\n{v}"); + } + // No custom uzumaki/nondet opcode leaks into the generated Rocq. + for forbidden in ["uzumaki", "BI_uzumaki", "forall", "nondet"] { + assert!( + !v.contains(forbidden), + "generated .v must not mention `{forbidden}`:\n{v}" + ); + } + // Post-#21 contract theorems present. + assert!( + v.contains("Theorem valid_refl_spec : ValidModule refl_spec."), + "structural ValidModule theorem missing:\n{v}" + ); + assert!( + v.contains( + "Theorem valid_refl_spec__ReflSpec : \ + ValidSpec refl_spec refl_spec__ReflSpec_specs." + ), + "per-spec ValidSpec theorem missing:\n{v}" + ); + } +} diff --git a/tests/test_data/inf/refl_spec.inf b/tests/test_data/inf/refl_spec.inf new file mode 100644 index 00000000..0a99913a --- /dev/null +++ b/tests/test_data/inf/refl_spec.inf @@ -0,0 +1,10 @@ +fn dummy() -> i32 { + return 0; +} + +spec ReflSpec { + fn refl() forall { + let i: i32 = @; + assert(i == i); + } +} From fa97aae8489f8b696f9b251ec3bd5d0a61c990be Mon Sep 17 00:00:00 2001 From: 0xGeorgii Date: Sun, 28 Jun 2026 06:44:15 +0400 Subject: [PATCH 3/5] add quantifier blocks --- core/wasm-codegen/src/compiler.rs | 265 ++++++++++++++++++++------- tests/src/spec_propagation_inf.rs | 98 ++++++++++ tests/test_data/inf/agg_quant.inf | 15 ++ tests/test_data/inf/nested_quant.inf | 15 ++ 4 files changed, 323 insertions(+), 70 deletions(-) create mode 100644 tests/test_data/inf/agg_quant.inf create mode 100644 tests/test_data/inf/nested_quant.inf diff --git a/core/wasm-codegen/src/compiler.rs b/core/wasm-codegen/src/compiler.rs index 6dc1be66..8578e2eb 100644 --- a/core/wasm-codegen/src/compiler.rs +++ b/core/wasm-codegen/src/compiler.rs @@ -57,18 +57,30 @@ //! Non-det blocks are structured blocks (like `block`/`loop`/`if`), terminated by a //! regular `end` instruction (0x0b). //! -//! # Spec functions: `@` → parameter (proof mode) +//! # Spec functions: `@` → parameter, vanilla quantifier blocks (proof mode) //! -//! Inside a `spec` block, a scalar `@` (uzumaki) denotes a *universally-quantified* value, -//! not runtime non-determinism. Rather than emit the non-vanilla `0xfc` opcode (which the -//! downstream Rocq library built on vanilla WasmCert-Coq cannot parse), each scalar `@` in a -//! spec function is lowered to a synthetic **function parameter** (read back with `local.get`): -//! see [`Compiler::collect_spec_uzumaki_params`] / [`Compiler::uzumaki_param_map`] and the -//! `Expr::Uzumaki` arm of [`Compiler::lower_expression`]. The `forall` then collapses into the -//! ∀ the downstream `ValidSpec`/`sem_triple` already quantifies over, so a `forall`-spec body -//! becomes ordinary WASM (a function-level `fn f() forall { .. }` body never emits the `forall` -//! *wrapper* opcode — codegen lowers the body block's statements directly). Non-spec functions -//! and array/struct `@` keep the opcode path above unchanged. +//! Inside a `spec` block, `@` (uzumaki) and the `forall`/`exists`/`unique`/`assume` blocks +//! denote *logical* quantification/assumption, not runtime non-determinism. Rather than emit +//! the non-vanilla `0xfc` opcodes (which the downstream Rocq library built on vanilla +//! WasmCert-Coq cannot parse), a spec function is lowered to **ordinary WASM** and the meaning +//! is carried by the downstream Rocq *contract predicate* +//! (`ValidSpec`/`ValidExistsSpec`/`ValidUniqueSpec`): +//! +//! - **`@`→parameter.** A *scalar* `@` becomes one synthetic **function parameter** (read back +//! with `local.get`); an *aggregate* (`array`/`struct`) `@` becomes one parameter per scalar +//! *leaf*, written into the aggregate's frame memory by `local.get; i32.store`. See +//! [`Compiler::collect_spec_uzumaki_params`] / [`Compiler::uzumaki_leaf_valtypes`] / +//! [`Compiler::uzumaki_param_map`] (which records each `@`'s *base* parameter index) and the +//! `Expr::Uzumaki` arm of [`Compiler::lower_expression`], with the leaf cursor +//! [`Compiler::uzumaki_leaf_cursor`] / [`Compiler::emit_uzumaki_or_param`]. +//! - **Vanilla quantifier blocks.** [`Compiler::lower_block`] suppresses the custom `0xfc` +//! nondet *wrapper* for any non-`Regular` block inside a spec function, emitting only the +//! block's statements. (A function-level quantifier body is iterated directly anyway, so this +//! matters for *nested* `assume`/`exists`/`unique` blocks.) +//! +//! The `forall` then collapses into the ∀ the downstream `ValidSpec`/`sem_triple` already +//! quantifies over; `exists`/`unique` map to existential-reachability predicates. Non-spec +//! functions keep the `0xfc` opcode path above unchanged. use crate::errors::CodegenError; use rustc_hash::FxHashMap; @@ -390,6 +402,13 @@ pub(crate) struct Compiler { /// quantifies over) rather than the non-vanilla `0xfc` uzumaki opcode. An empty /// map (every non-spec function) leaves `@` lowering byte-identical to before. uzumaki_param_map: FxHashMap, + /// While lowering an *aggregate* (`array`/`struct`) spec-mode `@` to parameters, holds + /// the next synthetic-parameter index to consume for the next scalar *leaf*. `None` + /// outside such lowering (and always `None` for non-spec functions, which keep the + /// custom `0xfc` uzumaki opcode). Set from [`Self::uzumaki_param_map`] (the aggregate's + /// base index) around `lower_array_uzumaki`/`lower_struct_uzumaki`; each leaf consumes + /// one index in the same order [`Self::uzumaki_leaf_valtypes`] reserved them. + uzumaki_leaf_cursor: Option, /// WASM function indices for functions that originated in `spec` blocks, /// keyed by spec name. Populated during Stage 1 registration in proof mode; /// consumed (moved out) by [`Self::finish_and_take`] so the Rocq translator @@ -453,6 +472,7 @@ impl Compiler { parent_blocks_stack: Vec::new(), init_zero_elision: false, uzumaki_param_map: FxHashMap::default(), + uzumaki_leaf_cursor: None, spec_func_indices_by_spec: FxHashMap::default(), frame_sizes: FxHashMap::default(), emit_bounds_checks: false, @@ -1120,17 +1140,28 @@ impl Compiler { // params/locals in index order, sorted by source position for determinism. // Non-spec functions never enter this branch, so their `@` stays byte-identical. if self.current_spec.is_some() { - let mut uzumaki_exprs: Vec<(ExprId, ValType)> = Vec::new(); - Self::collect_spec_uzumaki_params(arena, body_id, ctx, &mut uzumaki_exprs); - for (expr_id, vt) in uzumaki_exprs { + // Each `@` reserves one synthetic parameter per scalar *leaf* (one for a scalar, + // `total_leaf_count` for an aggregate), recorded by its *base* index; the leaves + // consume base, base+1, ... in the same order the body lowers them. + let mut uzumaki_exprs: Vec<(ExprId, Vec)> = Vec::new(); + Self::collect_spec_uzumaki_params( + arena, + body_id, + ctx, + &self.current_module_path, + &mut uzumaki_exprs, + ); + for (expr_id, vts) in uzumaki_exprs { cov_mark::hit!(wasm_codegen_assign_uzumaki_param); - params.push(vt); let prev = self.uzumaki_param_map.insert(expr_id, local_idx); debug_assert!( prev.is_none(), "each `@` expression id is visited once by the uzumaki pre-scan", ); - local_idx += 1; + for vt in vts { + params.push(vt); + local_idx += 1; + } } } @@ -1434,41 +1465,42 @@ impl Compiler { arena: &AstArena, block_id: BlockId, ctx: &TypedContext, - out: &mut Vec<(ExprId, ValType)>, + module_path: &[String], + out: &mut Vec<(ExprId, Vec)>, ) { for &stmt_id in &arena[block_id].stmts { match &arena[stmt_id].kind { Stmt::Expr(e) | Stmt::Return { expr: e } | Stmt::Assert { expr: e } => { - Self::collect_uzumaki_in_expr(arena, *e, ctx, out); + Self::collect_uzumaki_in_expr(arena, *e, ctx, module_path, out); } Stmt::Assign { left, right } => { - Self::collect_uzumaki_in_expr(arena, *left, ctx, out); - Self::collect_uzumaki_in_expr(arena, *right, ctx, out); + Self::collect_uzumaki_in_expr(arena, *left, ctx, module_path, out); + Self::collect_uzumaki_in_expr(arena, *right, ctx, module_path, out); } Stmt::VarDef { value, .. } => { if let Some(v) = value { - Self::collect_uzumaki_in_expr(arena, *v, ctx, out); + Self::collect_uzumaki_in_expr(arena, *v, ctx, module_path, out); } } Stmt::Block(inner) => { - Self::collect_spec_uzumaki_params(arena, *inner, ctx, out); + Self::collect_spec_uzumaki_params(arena, *inner, ctx, module_path, out); } Stmt::If { condition, then_block, else_block, } => { - Self::collect_uzumaki_in_expr(arena, *condition, ctx, out); - Self::collect_spec_uzumaki_params(arena, *then_block, ctx, out); + Self::collect_uzumaki_in_expr(arena, *condition, ctx, module_path, out); + Self::collect_spec_uzumaki_params(arena, *then_block, ctx, module_path, out); if let Some(else_id) = else_block { - Self::collect_spec_uzumaki_params(arena, *else_id, ctx, out); + Self::collect_spec_uzumaki_params(arena, *else_id, ctx, module_path, out); } } Stmt::Loop { condition, body } => { if let Some(c) = condition { - Self::collect_uzumaki_in_expr(arena, *c, ctx, out); + Self::collect_uzumaki_in_expr(arena, *c, ctx, module_path, out); } - Self::collect_spec_uzumaki_params(arena, *body, ctx, out); + Self::collect_spec_uzumaki_params(arena, *body, ctx, module_path, out); } Stmt::Break | Stmt::TypeDef { .. } | Stmt::ConstDef(_) => {} } @@ -1482,45 +1514,45 @@ impl Compiler { arena: &AstArena, expr_id: ExprId, ctx: &TypedContext, - out: &mut Vec<(ExprId, ValType)>, + module_path: &[String], + out: &mut Vec<(ExprId, Vec)>, ) { match &arena[expr_id].kind { Expr::Uzumaki => { - if let Some(vt) = ctx - .get_node_typeinfo(NodeId::Expr(expr_id)) - .and_then(|ti| Self::scalar_uzumaki_valtype(&ti.kind)) + if let Some(ti) = ctx.get_node_typeinfo(NodeId::Expr(expr_id)) + && let Some(vts) = Self::uzumaki_leaf_valtypes(&ti.kind, ctx, module_path) { - out.push((expr_id, vt)); + out.push((expr_id, vts)); } } Expr::ArrayIndexAccess { array, index } => { - Self::collect_uzumaki_in_expr(arena, *array, ctx, out); - Self::collect_uzumaki_in_expr(arena, *index, ctx, out); + Self::collect_uzumaki_in_expr(arena, *array, ctx, module_path, out); + Self::collect_uzumaki_in_expr(arena, *index, ctx, module_path, out); } Expr::Binary { left, right, .. } => { - Self::collect_uzumaki_in_expr(arena, *left, ctx, out); - Self::collect_uzumaki_in_expr(arena, *right, ctx, out); + Self::collect_uzumaki_in_expr(arena, *left, ctx, module_path, out); + Self::collect_uzumaki_in_expr(arena, *right, ctx, module_path, out); } Expr::PrefixUnary { expr, .. } | Expr::Parenthesized { expr } | Expr::MemberAccess { expr, .. } | Expr::TypeMemberAccess { expr, .. } => { - Self::collect_uzumaki_in_expr(arena, *expr, ctx, out); + Self::collect_uzumaki_in_expr(arena, *expr, ctx, module_path, out); } Expr::FunctionCall { function, args, .. } => { - Self::collect_uzumaki_in_expr(arena, *function, ctx, out); + Self::collect_uzumaki_in_expr(arena, *function, ctx, module_path, out); for (_, arg) in args { - Self::collect_uzumaki_in_expr(arena, *arg, ctx, out); + Self::collect_uzumaki_in_expr(arena, *arg, ctx, module_path, out); } } Expr::StructLiteral { fields, .. } => { for (_, value) in fields { - Self::collect_uzumaki_in_expr(arena, *value, ctx, out); + Self::collect_uzumaki_in_expr(arena, *value, ctx, module_path, out); } } Expr::ArrayLiteral { elements } => { for &e in elements { - Self::collect_uzumaki_in_expr(arena, e, ctx, out); + Self::collect_uzumaki_in_expr(arena, e, ctx, module_path, out); } } Expr::Identifier(_) @@ -1532,6 +1564,40 @@ impl Compiler { } } + /// The ordered scalar-leaf WASM value types a spec-mode `@` of type `kind` reserves as + /// synthetic parameters: `[vt]` for a scalar, and, for an *aggregate*, one entry per + /// scalar leaf **in the exact order the body lowers them** ([`Self::lower_array_uzumaki`] + /// / [`Self::lower_struct_uzumaki`]) — arrays row-major, structs in field-layout order + /// (recursing into array fields). `None` for kinds with no scalar leaves. + fn uzumaki_leaf_valtypes( + kind: &TypeInfoKind, + ctx: &TypedContext, + module_path: &[String], + ) -> Option> { + match kind { + TypeInfoKind::Array(elem, length) => { + let elem_vts = Self::uzumaki_leaf_valtypes(&elem.kind, ctx, module_path)?; + let mut out = Vec::with_capacity(elem_vts.len() * (*length as usize)); + for _ in 0..*length { + out.extend_from_slice(&elem_vts); + } + Some(out) + } + TypeInfoKind::Struct(name, _) | TypeInfoKind::Custom(name) => { + let struct_info = ctx.lookup_struct_in(name, module_path)?; + let (_, fields) = + compute_struct_field_layout(&struct_info, ctx, module_path).ok()?; + let mut out = Vec::new(); + for field in &fields { + let fvts = Self::uzumaki_leaf_valtypes(&field.type_kind, ctx, module_path)?; + out.extend(fvts); + } + Some(out) + } + other => Self::scalar_uzumaki_valtype(other).map(|vt| vec![vt]), + } + } + /// Returns the WASM value type for a scalar uzumaki of the given type kind, or /// `None` for non-scalar (array/struct) uzumaki. Mirrors the scalar arms of the /// `Expr::Uzumaki` case in [`Self::lower_expression`]. @@ -2332,14 +2398,32 @@ impl Compiler { } /// Lowers a block (regular or non-det) to WASM instructions. + /// + /// In **proof mode**, a *spec function*'s quantifier/assumption blocks + /// (`forall`/`exists`/`unique`/`assume`) lower to **vanilla** WASM — the custom `0xfc` + /// nondet wrapper is *not* emitted, only the block's statements are. The quantifier / + /// assumption semantics live downstream in the Rocq **contract predicate** + /// (`ValidSpec` for `forall`, `ValidExistsSpec`/`ValidUniqueSpec` for `exists`/`unique`, + /// and an `assume` is a precondition conjunct) — not in the bytecode. Combined with the + /// `@`→parameter lowering and the vanilla `assert`, an entire spec body becomes ordinary + /// WASM that the downstream `wasm-verifier` library can type-check and discharge. + /// + /// (A function-level quantifier body is already iterated directly by + /// `visit_function_definition_body`, so this only affects *nested* such blocks; non-spec + /// code keeps the opcode path unchanged.) fn lower_block(&mut self, arena: &AstArena, block_id: BlockId, ctx: &TypedContext) { let block = &arena[block_id]; - let opcode = match block.block_kind { - BlockKind::Forall => Some(FORALL_OPCODE), - BlockKind::Exists => Some(EXISTS_OPCODE), - BlockKind::Assume => Some(ASSUME_OPCODE), - BlockKind::Unique => Some(UNIQUE_OPCODE), - BlockKind::Regular => None, + let in_spec = self.current_spec.is_some(); + let opcode = if in_spec { + None + } else { + match block.block_kind { + BlockKind::Forall => Some(FORALL_OPCODE), + BlockKind::Exists => Some(EXISTS_OPCODE), + BlockKind::Assume => Some(ASSUME_OPCODE), + BlockKind::Unique => Some(UNIQUE_OPCODE), + BlockKind::Regular => None, + } }; if let Some(op) = opcode { @@ -2352,6 +2436,8 @@ impl Compiler { } self.emit_nondet_block_start(op); self.loop_ctx.wasm_block_depth += 1; + } else if in_spec && block.block_kind != BlockKind::Regular { + cov_mark::hit!(wasm_codegen_spec_block_vanilla); } let stmts = block.stmts.clone(); @@ -2527,16 +2613,13 @@ impl Compiler { } Expr::Type(_) => todo!(), Expr::Uzumaki => { - // Spec-mode lowering: a scalar `@` inside a `spec` block was assigned - // a synthetic function parameter (see `visit_function_definition_body`). - // Read it back as a plain `local.get` instead of emitting the non-vanilla - // `0xfc` uzumaki opcode, so the spec body is ordinary WASM. The map is - // empty for every non-spec function, so this branch is never taken there. - if let Some(¶m_idx) = self.uzumaki_param_map.get(&expr_id) { - cov_mark::hit!(wasm_codegen_emit_uzumaki_param); - self.func().instruction(&Instruction::LocalGet(param_idx)); - return; - } + // Spec-mode lowering: inside a `spec` block each `@` was assigned synthetic + // function parameter(s) (see `visit_function_definition_body`) — one for a + // scalar, one per scalar *leaf* for an aggregate. We read them back as plain + // `local.get`s instead of emitting the non-vanilla `0xfc` uzumaki opcode, so + // the whole spec body is ordinary WASM. The map is empty for every non-spec + // function, so `param_base` is `None` there and the opcode path is unchanged. + let param_base = self.uzumaki_param_map.get(&expr_id).copied(); let node_id = NodeId::Expr(expr_id); let type_info = ctx .get_node_typeinfo(node_id) @@ -2552,15 +2635,29 @@ impl Compiler { | NumberType::U32, ) | TypeInfoKind::Enum(_, _) => { - cov_mark::hit!(wasm_codegen_emit_uzumaki_i32); - self.emit_uzumaki(UZUMAKI_I32_OPCODE); + if let Some(idx) = param_base { + cov_mark::hit!(wasm_codegen_emit_uzumaki_param); + self.func().instruction(&Instruction::LocalGet(idx)); + } else { + cov_mark::hit!(wasm_codegen_emit_uzumaki_i32); + self.emit_uzumaki(UZUMAKI_I32_OPCODE); + } } TypeInfoKind::Number(NumberType::I64 | NumberType::U64) => { - cov_mark::hit!(wasm_codegen_emit_uzumaki_i64); - self.emit_uzumaki(UZUMAKI_I64_OPCODE); + if let Some(idx) = param_base { + cov_mark::hit!(wasm_codegen_emit_uzumaki_param); + self.func().instruction(&Instruction::LocalGet(idx)); + } else { + cov_mark::hit!(wasm_codegen_emit_uzumaki_i64); + self.emit_uzumaki(UZUMAKI_I64_OPCODE); + } } TypeInfoKind::Array(elem_type, length) => { - cov_mark::hit!(wasm_codegen_emit_array_uzumaki); + if param_base.is_some() { + cov_mark::hit!(wasm_codegen_array_uzumaki_param); + } else { + cov_mark::hit!(wasm_codegen_emit_array_uzumaki); + } let length = *length; let elem_type = elem_type.clone(); let var_name = enclosing_var_name.unwrap_or_else(|| { @@ -2568,21 +2665,32 @@ impl Compiler { "Array uzumaki (expr_id={expr_id:?}) has no enclosing variable name" ) }); - if let Err(e) = - self.lower_array_uzumaki(arena, &elem_type, length, var_name) - { + // In spec mode the leaves consume synthetic params [base..); else 0xfc. + let saved = self.uzumaki_leaf_cursor; + self.uzumaki_leaf_cursor = param_base; + let r = self.lower_array_uzumaki(arena, &elem_type, length, var_name); + self.uzumaki_leaf_cursor = saved; + if let Err(e) = r { panic!("array uzumaki lowering failed: {e}"); } } TypeInfoKind::Struct(name, _) | TypeInfoKind::Custom(name) => { - cov_mark::hit!(wasm_codegen_emit_struct_uzumaki); + if param_base.is_some() { + cov_mark::hit!(wasm_codegen_struct_uzumaki_param); + } else { + cov_mark::hit!(wasm_codegen_emit_struct_uzumaki); + } let name = name.clone(); let var_name = enclosing_var_name.unwrap_or_else(|| { panic!( "Struct uzumaki (expr_id={expr_id:?}) has no enclosing variable name" ) }); - if let Err(e) = self.lower_struct_uzumaki(ctx, &name, var_name) { + let saved = self.uzumaki_leaf_cursor; + self.uzumaki_leaf_cursor = param_base; + let r = self.lower_struct_uzumaki(ctx, &name, var_name); + self.uzumaki_leaf_cursor = saved; + if let Err(e) = r { panic!("struct uzumaki lowering failed: {e}"); } } @@ -3807,7 +3915,7 @@ impl Compiler { .instruction(&Instruction::LocalGet(frame_ptr_local)); self.func().instruction(&Instruction::I32Const(byte_offset)); self.func().instruction(&Instruction::I32Add); - self.emit_uzumaki(uzumaki_opcode); + self.emit_uzumaki_or_param(uzumaki_opcode); self.func().instruction(store_instr); } } @@ -3911,7 +4019,7 @@ impl Compiler { .instruction(&Instruction::LocalGet(frame_ptr_local)); self.func().instruction(&Instruction::I32Const(byte_offset)); self.func().instruction(&Instruction::I32Add); - self.emit_uzumaki(uzumaki_opcode); + self.emit_uzumaki_or_param(uzumaki_opcode); self.func().instruction(&store_instr); } CompoundFieldLayout::NestedArray { @@ -3937,7 +4045,7 @@ impl Compiler { .instruction(&Instruction::LocalGet(frame_ptr_local)); self.func().instruction(&Instruction::I32Const(byte_offset)); self.func().instruction(&Instruction::I32Add); - self.emit_uzumaki(uzumaki_opcode); + self.emit_uzumaki_or_param(uzumaki_opcode); self.func().instruction(&store_instr); } } @@ -4985,6 +5093,23 @@ impl Compiler { self.func().raw([OPCODE_PREFIX, opcode]); } + /// Emits a single non-deterministic scalar *leaf* value onto the operand stack. + /// + /// In spec mode for an aggregate `@` ([`Self::uzumaki_leaf_cursor`] is `Some`), the leaf + /// reads back a synthetic function parameter (`local.get`) and advances the cursor — the + /// `array`/`struct` `@` becomes plain WASM whose leaves are universally/existentially + /// quantified parameters. Otherwise it emits the custom `0xfc` uzumaki opcode (the + /// unchanged non-spec path). + fn emit_uzumaki_or_param(&mut self, opcode: u8) { + if let Some(idx) = self.uzumaki_leaf_cursor { + cov_mark::hit!(wasm_codegen_emit_uzumaki_leaf_param); + self.func().instruction(&Instruction::LocalGet(idx)); + self.uzumaki_leaf_cursor = Some(idx + 1); + } else { + self.emit_uzumaki(opcode); + } + } + fn emit_memory_copy(&mut self, byte_size: u32) { #[allow(clippy::cast_possible_wrap)] self.func() diff --git a/tests/src/spec_propagation_inf.rs b/tests/src/spec_propagation_inf.rs index 717ba0c9..e2c78ada 100644 --- a/tests/src/spec_propagation_inf.rs +++ b/tests/src/spec_propagation_inf.rs @@ -500,3 +500,101 @@ mod fixture_refl_spec_e2e { ); } } + +// ============================================================================ +// Fixture: nested_quant.inf — NESTED assume/exists blocks in a spec function +// ============================================================================ +#[cfg(test)] +mod fixture_nested_quant_e2e { + use super::helpers::{compile_inf, wasm_contains}; + use inference_wasm_codegen::CompilationMode; + use rustc_hash::FxHashMap; + + /// `nested_quant.inf`'s spec function `demo` has a `forall` body containing a *nested* + /// `assume { precond(x); }` block and a *nested* `exists { let y = @; assert(y == y); }` + /// block. In proof mode these nested quantifier/assumption blocks lower to **vanilla** + /// WASM — no custom `0xfc` nondet wrapper — because the quantifier/assumption meaning + /// lives downstream in the Rocq contract predicate (`ValidSpec`/`ValidExistsSpec`/ + /// `ValidUniqueSpec`), not in the bytecode. The `@` inside the nested `exists` still + /// becomes a function parameter, and the `assert` is its plain lowered shape. + /// + /// That the module validates under vanilla rules is the proof that no custom opcode + /// (which would be a `0xfc 0x3a..0x3d`/`0x31..0x32` byte pair) survives. + #[test] + fn nested_quant_inf_lowers_blocks_to_vanilla() { + let output = compile_inf("nested_quant.inf", CompilationMode::Proof, "nested_quant"); + let wasm = output.wasm(); + inf_wasmparser::validate(wasm) + .expect("WASM must validate (nested assume/exists lowered to vanilla)"); + + // No custom nondet/uzumaki opcode byte-pair survives in the module. + for op in [0x3au8, 0x3b, 0x3c, 0x3d, 0x31, 0x32] { + assert!( + !wasm_contains(wasm, &[0xfc, op]), + "custom 0xfc {op:#x} nondet/uzumaki opcode leaked into vanilla WASM" + ); + } + + let by_spec = output.spec_func_indices_by_spec(); + assert!( + by_spec.contains_key("NestedQuant"), + "spec NestedQuant must be present; got {by_spec:?}" + ); + + let empty: FxHashMap> = FxHashMap::default(); + let v = inference::wasm_to_v("nested_quant", wasm, &empty).expect("translate ok"); + // The body lowered to vanilla WASM (the @-introduced value is a param; the assert is + // the `i32.eqz; if` shape). + for needle in ["BI_local_get", "BI_if (BT_valtype None)"] { + assert!(v.contains(needle), "generated body missing `{needle}`:\n{v}"); + } + // No custom uzumaki/nondet opcode leaks into the generated Rocq. + for forbidden in ["uzumaki", "BI_uzumaki", "nondet"] { + assert!( + !v.contains(forbidden), + "generated .v must not mention `{forbidden}`:\n{v}" + ); + } + } +} + +// ============================================================================ +// Fixture: agg_quant.inf — ARRAY/STRUCT `@` lowered to (multiple) parameters +// ============================================================================ +#[cfg(test)] +mod fixture_agg_quant_e2e { + use super::helpers::{compile_inf, wasm_contains}; + use inference_wasm_codegen::CompilationMode; + + /// `agg_quant.inf` has two spec functions whose `forall` bodies bind an *aggregate* `@`: + /// `let a: [i32; 3] = @` (an array) and `let p: Point = @` (a 2-field struct). In proof + /// mode each aggregate `@` is lowered to **one synthetic parameter per scalar leaf** (3 + /// params for the array, 2 for the struct), written into the aggregate's frame memory by + /// plain `local.get; i32.store` — no custom `0xfc` uzumaki opcode. The downstream + /// quantification is over those leaf parameters (which the `wasm-verifier` library reads + /// back with its memory rules), exactly as the scalar `@`→parameter rule does for one + /// value. + /// + /// That the module validates under vanilla rules is the proof no custom opcode survives. + #[test] + fn agg_quant_inf_lowers_aggregate_uzumaki_to_params() { + let output = compile_inf("agg_quant.inf", CompilationMode::Proof, "agg_quant"); + let wasm = output.wasm(); + inf_wasmparser::validate(wasm) + .expect("WASM must validate (aggregate @ lowered to leaf parameters)"); + + // No custom uzumaki opcode byte-pair survives. + for op in [0x31u8, 0x32, 0x3a, 0x3b, 0x3c, 0x3d] { + assert!( + !wasm_contains(wasm, &[0xfc, op]), + "custom 0xfc {op:#x} uzumaki/nondet opcode leaked into vanilla WASM" + ); + } + + let by_spec = output.spec_func_indices_by_spec(); + assert!( + by_spec.contains_key("AggQuant"), + "spec AggQuant must be present; got {by_spec:?}" + ); + } +} diff --git a/tests/test_data/inf/agg_quant.inf b/tests/test_data/inf/agg_quant.inf new file mode 100644 index 00000000..5186b9fa --- /dev/null +++ b/tests/test_data/inf/agg_quant.inf @@ -0,0 +1,15 @@ +struct Point { + x: i32; + y: i32; +} + +spec AggQuant { + fn arr() forall { + let a: [i32; 3] = @; + assert(a[0] == a[0]); + } + fn strct() forall { + let p: Point = @; + assert(p.x == p.x); + } +} diff --git a/tests/test_data/inf/nested_quant.inf b/tests/test_data/inf/nested_quant.inf new file mode 100644 index 00000000..c3019cc9 --- /dev/null +++ b/tests/test_data/inf/nested_quant.inf @@ -0,0 +1,15 @@ +fn precond(x: i32) -> i32 { + return x; +} + +spec NestedQuant { + fn demo(x: i32) -> () forall { + assume { + precond(x); + } + exists { + let y: i32 = @; + assert(y == y); + } + } +} From f94595150e7e97f8b3e016e47be424a535bd26a7 Mon Sep 17 00:00:00 2001 From: 0xGeorgii Date: Mon, 29 Jun 2026 08:35:32 +0400 Subject: [PATCH 4/5] more tests --- core/wasm-codegen/src/compiler.rs | 75 +++++- core/wasm-codegen/src/lib.rs | 47 +++- core/wasm-codegen/src/spec_section.rs | 213 ++++++++++++++-- core/wasm-linker/src/merge.rs | 11 +- core/wasm-linker/src/parse.rs | 14 +- core/wasm-linker/src/spec_funcs.rs | 155 +++++++++--- core/wasm-linker/tests/link.rs | 69 +++++ core/wasm-to-v/ROCQ_CONTRACT.md | 90 ++++++- core/wasm-to-v/src/lib.rs | 10 + core/wasm-to-v/src/translator.rs | 266 ++++++++++++++++---- core/wasm-to-v/src/wasm_parser.rs | 85 ++++++- tests/src/spec_propagation_inf.rs | 158 ++++++++++++ tests/test_data/inf/e2e_call.inf | 14 ++ tests/test_data/inf/e2e_loop.inf | 12 + tests/test_data/inf/e2e_quant_kinds.inf | 29 +++ tests/test_data/inf/quant_kinds.inf | 35 +++ tests/test_data/inf/spec_name_collision.inf | 13 + 17 files changed, 1149 insertions(+), 147 deletions(-) create mode 100644 tests/test_data/inf/e2e_call.inf create mode 100644 tests/test_data/inf/e2e_loop.inf create mode 100644 tests/test_data/inf/e2e_quant_kinds.inf create mode 100644 tests/test_data/inf/quant_kinds.inf create mode 100644 tests/test_data/inf/spec_name_collision.inf diff --git a/core/wasm-codegen/src/compiler.rs b/core/wasm-codegen/src/compiler.rs index 8578e2eb..f83847b6 100644 --- a/core/wasm-codegen/src/compiler.rs +++ b/core/wasm-codegen/src/compiler.rs @@ -81,8 +81,17 @@ //! The `forall` then collapses into the ∀ the downstream `ValidSpec`/`sem_triple` already //! quantifies over; `exists`/`unique` map to existential-reachability predicates. Non-spec //! functions keep the `0xfc` opcode path above unchanged. +//! +//! Because the lowered body is vanilla, it no longer records *which* quantifier the function +//! carried — yet the translator must pick `ValidSpec` vs `ValidExistsSpec` vs `ValidUniqueSpec` +//! from exactly that. So the obligation kind travels as metadata: `crate::spec_obligation_kind` +//! reads the spec function's body [`inference_ast::nodes::BlockKind`] (the function-level +//! quantifier *is* the body block) into a [`SpecObligationKind`], threaded per index into the +//! `inference.spec_funcs` section (`crate::spec_section`, wire-format v2). See that module for the +//! encoding and `core/wasm-to-v` for the predicate selection. use crate::errors::CodegenError; +use crate::spec_section::{SpecObligationKind, SpecObligations}; use rustc_hash::FxHashMap; use inference_ast::arena::AstArena; @@ -415,6 +424,14 @@ pub(crate) struct Compiler { /// can emit per-spec `Definition ___specs : list N` /// definitions. spec_func_indices_by_spec: FxHashMap>, + /// Per-spec proof-obligation kinds, parallel to + /// [`Self::spec_func_indices_by_spec`] (same key, same order): the i-th kind + /// describes the i-th recorded function index. Carried into the + /// `inference.spec_funcs` section so the Rocq translator can emit + /// `ValidExistsSpec`/`ValidUniqueSpec` (not just `ValidSpec`) for + /// `exists`/`unique` spec functions. Kept separate from the index map so the + /// public [`crate::CodegenOutput`] surface (indices only) is unchanged. + spec_func_kinds_by_spec: FxHashMap>, /// Real shadow-stack frame size in bytes for each function, keyed by its /// canonical [`FnKey`] display string. Recorded in /// [`Self::visit_function_definition`] right after the frame layout is @@ -474,6 +491,7 @@ impl Compiler { uzumaki_param_map: FxHashMap::default(), uzumaki_leaf_cursor: None, spec_func_indices_by_spec: FxHashMap::default(), + spec_func_kinds_by_spec: FxHashMap::default(), frame_sizes: FxHashMap::default(), emit_bounds_checks: false, bounds_check_scratch_local: None, @@ -490,23 +508,37 @@ impl Compiler { self.emit_bounds_checks = enabled; } - /// Records a single WASM function index as belonging to `spec_name`. - pub(crate) fn record_spec_index(&mut self, spec_name: &str, idx: u32) { + /// Records a single WASM function index as belonging to `spec_name`, tagged + /// with the proof obligation (`Spec`/`Exists`/`Unique`) its quantifier + /// implies. The index and kind are appended in lockstep so the parallel + /// maps stay aligned by position. + pub(crate) fn record_spec_index( + &mut self, + spec_name: &str, + idx: u32, + kind: SpecObligationKind, + ) { self.spec_func_indices_by_spec .entry(spec_name.to_string()) .or_default() .push(idx); + self.spec_func_kinds_by_spec + .entry(spec_name.to_string()) + .or_default() + .push(kind); } - /// Ensures `spec_name` has an entry in `spec_func_indices_by_spec`, - /// inserting an empty index list if absent. Called for every visited - /// `spec` block in proof mode so user-authored `spec MySpec { }` (with - /// zero inner emittable defs) still produces a per-spec `.v` definition - /// and theorem downstream. + /// Ensures `spec_name` has an entry in the spec maps, inserting empty lists + /// if absent. Called for every visited `spec` block in proof mode so + /// user-authored `spec MySpec { }` (with zero inner emittable defs) still + /// produces a per-spec `.v` definition and theorem downstream. pub(crate) fn ensure_spec_registered(&mut self, spec_name: &str) { self.spec_func_indices_by_spec .entry(spec_name.to_string()) .or_default(); + self.spec_func_kinds_by_spec + .entry(spec_name.to_string()) + .or_default(); } /// Borrows the recorded `(spec_name -> [func_idx])` map so a caller can @@ -516,6 +548,33 @@ impl Compiler { &self.spec_func_indices_by_spec } + /// Zips the parallel index and kind maps into the `(func_idx, kind)` shape + /// the `inference.spec_funcs` encoder consumes. A spec missing a kinds entry + /// (or with fewer kinds than indices — neither happens via + /// [`Self::record_spec_index`]/[`Self::ensure_spec_registered`], which write + /// both in lockstep) defaults its surplus indices to + /// [`SpecObligationKind::Spec`], so the section is always well-formed. + fn spec_obligations(&self) -> SpecObligations { + self.spec_func_indices_by_spec + .iter() + .map(|(name, indices)| { + let kinds = self.spec_func_kinds_by_spec.get(name); + let items = indices + .iter() + .enumerate() + .map(|(i, &idx)| { + let kind = kinds + .and_then(|ks| ks.get(i)) + .copied() + .unwrap_or_default(); + (idx, kind) + }) + .collect(); + (name.clone(), items) + }) + .collect() + } + fn func(&mut self) -> &mut Function { self.func .as_mut() @@ -5244,7 +5303,7 @@ impl Compiler { if !self.spec_func_indices_by_spec.is_empty() { let spec_section = - crate::spec_section::SpecFuncSection::new(&self.spec_func_indices_by_spec); + crate::spec_section::SpecFuncSection::new(&self.spec_obligations()); module.section(&spec_section); } diff --git a/core/wasm-codegen/src/lib.rs b/core/wasm-codegen/src/lib.rs index 09b06b3c..0bb0b7a5 100644 --- a/core/wasm-codegen/src/lib.rs +++ b/core/wasm-codegen/src/lib.rs @@ -48,7 +48,7 @@ use inference_ast::arena::AstArena; use inference_ast::ids::DefId; -use inference_ast::nodes::Def; +use inference_ast::nodes::{BlockKind, Def}; use inference_type_checker::typed_context::TypedContext; use rustc_hash::FxHashMap; @@ -71,11 +71,21 @@ pub use target::{CompilationMode, OptLevel, Target}; /// place. pub use crate::spec_section::SECTION_NAME as SPEC_FUNCS_SECTION_NAME; -/// Wire-format version of the `inference.spec_funcs` custom section payload. -/// Decoders must reject payloads whose leading varuint32 does not equal this -/// constant; bumping the value is a breaking change to the section format. +/// Legacy wire-format version of the `inference.spec_funcs` payload (function +/// indices only). Decoders accept this alongside +/// [`SPEC_FUNCS_SECTION_VERSION_WITH_KINDS`]; the encoder emits it whenever +/// every obligation is the default [`SpecObligationKind::Spec`]. pub use crate::spec_section::SECTION_VERSION as SPEC_FUNCS_SECTION_VERSION; +/// Wire-format version that additionally carries one [`SpecObligationKind`] +/// byte per index. Emitted only when an `exists`/`unique` obligation is present. +pub use crate::spec_section::SECTION_VERSION_WITH_KINDS as SPEC_FUNCS_SECTION_VERSION_WITH_KINDS; + +/// The downstream proof obligation a spec function carries (`Spec` / `Exists` / +/// `Unique`), threaded through the `inference.spec_funcs` section so the Rocq +/// translator can pick `ValidSpec` / `ValidExistsSpec` / `ValidUniqueSpec`. +pub use crate::spec_section::SpecObligationKind; + /// Generates WebAssembly binary from a typed AST for the specified target and compilation mode. /// /// `module_name` is written into the WASM module-name subsection and flows @@ -533,6 +543,7 @@ fn register_function_indices( compiler.record_spec_index( &qualified_spec_name(&entry.module_path, &entry.spec_name), *assigned_idx, + spec_obligation_kind(arena, entry.def_id), ); } @@ -556,6 +567,7 @@ fn register_function_indices( compiler.record_spec_index( &qualified_spec_name(&entry.module_path, &entry.spec_name), *assigned_idx, + spec_obligation_kind(arena, entry.def_id), ); } @@ -578,6 +590,33 @@ fn register_function_indices( Ok(()) } +/// Recovers the downstream proof obligation a spec function carries from the +/// quantifier on its body. +/// +/// Inference's function-level quantifier convention (`fn f() forall { … }`, +/// `fn f() exists { … }`, `fn f() unique { … }`) lowers the quantifier block +/// *as* the function body, so the obligation kind is exactly the body block's +/// [`BlockKind`]: `Exists` → [`SpecObligationKind::Exists`], `Unique` → +/// [`SpecObligationKind::Unique`]. A `forall`, regular, or `assume` body — and +/// any non-function def — is a universal safety obligation +/// ([`SpecObligationKind::Spec`], the default), which the downstream contract +/// discharges as `ValidSpec`. A quantifier written as a *nested* statement +/// inside a regular body (`fn f() { exists { … } }`) leaves the body `Regular` +/// and is treated as `Spec`; the established spec convention uses the +/// function-level form. +fn spec_obligation_kind(arena: &AstArena, def_id: DefId) -> SpecObligationKind { + match &arena[def_id].kind { + Def::Function { body, .. } => match arena[*body].block_kind { + BlockKind::Exists => SpecObligationKind::Exists, + BlockKind::Unique => SpecObligationKind::Unique, + BlockKind::Forall | BlockKind::Assume | BlockKind::Regular => { + SpecObligationKind::Spec + } + }, + _ => SpecObligationKind::Spec, + } +} + /// A top-level free function to emit, tagged with its defining file's module /// path (empty for the entry file). The module path file-qualifies the /// function's flat WASM name so two files can each define a same-named function. diff --git a/core/wasm-codegen/src/spec_section.rs b/core/wasm-codegen/src/spec_section.rs index 78da4e79..3e8c2905 100644 --- a/core/wasm-codegen/src/spec_section.rs +++ b/core/wasm-codegen/src/spec_section.rs @@ -12,7 +12,7 @@ //! ## Payload format //! //! ```text -//! version : LEB128 u32 -- format version (currently 1) +//! version : LEB128 u32 -- format version (1 = legacy, 2 = with kinds) //! count : LEB128 u32 -- number of (spec_name, indices) pairs //! repeated `count` times: //! spec_name_len : LEB128 u32 @@ -20,6 +20,9 @@ //! indices_count : LEB128 u32 //! repeated `indices_count` times: //! func_idx : LEB128 u32 +//! -- version 2 only: one obligation-kind byte per index, same order: +//! repeated `indices_count` times (v2 only): +//! kind_byte : u8 -- 0 = Spec, 1 = Exists, 2 = Unique //! ``` //! //! Entries are emitted sorted by spec name for deterministic, byte-stable @@ -30,6 +33,24 @@ //! not recognise must refuse to translate, rather than treating the next //! varuint32 as a spec count and silently misparsing the rest of the //! payload. +//! +//! ## Obligation kinds (version 2) +//! +//! Version 1 carried only the function index, implying a single universal +//! ("for-all") proof obligation per spec function (`ValidSpec` downstream). +//! Inference also has `exists`- and `unique`-quantified spec functions, whose +//! downstream obligation is `ValidExistsSpec` / `ValidUniqueSpec` — predicates +//! that assert existential reachability, *strictly more* than the trap-freedom +//! a universal `ValidSpec` asserts. The vanilla WASM body no longer carries the +//! quantifier (the `0xfc` wrapper opcode is suppressed for spec functions), so +//! the obligation kind must travel as metadata here for the translator to pick +//! the right predicate. +//! +//! The encoder emits **version 1** whenever every obligation is the default +//! [`SpecObligationKind::Spec`], so all pre-existing `forall`/regular modules +//! stay byte-identical; it emits **version 2** (with the trailing kind bytes) +//! only when at least one `exists`/`unique` obligation must be carried. Both +//! decoders (the linker and the Rocq translator) accept either version. use rustc_hash::FxHashMap; use wasm_encoder::{CustomSection, Encode, Section, SectionId}; @@ -38,12 +59,65 @@ use wasm_encoder::{CustomSection, Encode, Section, SectionId}; /// map. Re-exported from the crate root as `SPEC_FUNCS_SECTION_NAME`. pub const SECTION_NAME: &str = "inference.spec_funcs"; -/// Wire-format version emitted into the head of the `inference.spec_funcs` -/// payload. Consumers must reject unrecognised values. Re-exported from the -/// crate root as `SPEC_FUNCS_SECTION_VERSION` and consumed verbatim by the -/// `wasm-to-v` decoder so encoder and decoder share a single source of truth. +/// Legacy wire-format version of the `inference.spec_funcs` payload: function +/// indices only, no obligation-kind bytes. Re-exported from the crate root as +/// `SPEC_FUNCS_SECTION_VERSION`. The encoder still emits this version whenever +/// every obligation is the default [`SpecObligationKind::Spec`], so modules +/// without `exists`/`unique` specs stay byte-identical to pre-kinds output. pub const SECTION_VERSION: u32 = 1; +/// Wire-format version that additionally carries one [`SpecObligationKind`] +/// byte per function index (see the module docs). Emitted only when at least +/// one obligation is not the default `Spec` kind. Both decoders accept it +/// alongside [`SECTION_VERSION`]. +pub const SECTION_VERSION_WITH_KINDS: u32 = 2; + +/// The downstream proof obligation a spec function carries, recovered from the +/// quantifier on its (now-vanilla) body. +/// +/// Selects which Rocq predicate the translator emits: `Spec` → `ValidSpec` +/// (universal trap-freedom), `Exists` → `ValidExistsSpec` (existential +/// reachability), `Unique` → `ValidUniqueSpec` (a unique witness). A `forall`, +/// regular, or `assume` body maps to `Spec`; only `exists`/`unique` bodies need +/// a distinct kind. +#[derive(Clone, Copy, PartialEq, Eq, Debug, Default)] +pub enum SpecObligationKind { + /// Universal safety obligation — `forall`, regular, or `assume` bodies. + #[default] + Spec, + /// Existential-reachability obligation — an `exists`-quantified body. + Exists, + /// Unique-witness obligation — a `unique`-quantified body. + Unique, +} + +impl SpecObligationKind { + /// Wire encoding of this kind (a single payload byte in version 2). + #[must_use] + pub fn to_byte(self) -> u8 { + match self { + SpecObligationKind::Spec => 0, + SpecObligationKind::Exists => 1, + SpecObligationKind::Unique => 2, + } + } + + /// Decodes a wire byte, or `None` for an unrecognised value. + #[must_use] + pub fn from_byte(b: u8) -> Option { + match b { + 0 => Some(SpecObligationKind::Spec), + 1 => Some(SpecObligationKind::Exists), + 2 => Some(SpecObligationKind::Unique), + _ => None, + } + } +} + +/// Per-spec function obligations: each spec name maps to its `(func_idx, kind)` +/// pairs, in registration order. The payload codec's in-memory shape. +pub(crate) type SpecObligations = FxHashMap>; + /// Upper bound, in bytes, on a single spec name embedded in the /// `inference.spec_funcs` payload. /// @@ -128,46 +202,67 @@ pub(crate) fn spec_name_rocq_invalidity_reason(qualified: &str) -> Option>) -> Vec { - let mut entries: Vec<(&str, &[u32])> = map +/// Encodes the spec obligations into the canonical payload bytes. +/// +/// Emits the legacy [`SECTION_VERSION`] layout (indices only) when every +/// obligation is the default [`SpecObligationKind::Spec`], so modules without +/// `exists`/`unique` specs stay byte-identical to pre-kinds output; emits +/// [`SECTION_VERSION_WITH_KINDS`] (a trailing kind byte per index) otherwise. +pub(crate) fn encode_payload(map: &SpecObligations) -> Vec { + let mut entries: Vec<(&str, &[(u32, SpecObligationKind)])> = map .iter() - .map(|(name, indices)| (name.as_str(), indices.as_slice())) + .map(|(name, items)| (name.as_str(), items.as_slice())) .collect(); entries.sort_unstable_by(|a, b| a.0.cmp(b.0)); + let has_kinds = entries + .iter() + .any(|(_, items)| items.iter().any(|(_, k)| *k != SpecObligationKind::Spec)); + let version = if has_kinds { + SECTION_VERSION_WITH_KINDS + } else { + SECTION_VERSION + }; + let count = u32::try_from(entries.len()) .expect("more than u32::MAX specs cannot fit in a WASM custom section"); let mut payload = Vec::new(); - SECTION_VERSION.encode(&mut payload); + version.encode(&mut payload); count.encode(&mut payload); - for (spec_name, indices) in entries { + for (spec_name, items) in entries { let name_bytes = spec_name.as_bytes(); let name_len = u32::try_from(name_bytes.len()) .expect("spec name longer than u32::MAX bytes"); - let idx_count = u32::try_from(indices.len()) + let idx_count = u32::try_from(items.len()) .expect("more than u32::MAX function indices per spec"); name_len.encode(&mut payload); payload.extend_from_slice(name_bytes); idx_count.encode(&mut payload); - for idx in indices { + for (idx, _) in items { idx.encode(&mut payload); } + // Version 2 appends the kind bytes after all indices for this spec, in + // the same order; version 1 omits them entirely. + if has_kinds { + for (_, kind) in items { + payload.push(kind.to_byte()); + } + } } payload } -/// A `wasm_encoder::Section` carrying the encoded spec-name → indices map. +/// A `wasm_encoder::Section` carrying the encoded spec-name → obligations map. pub(crate) struct SpecFuncSection { payload: Vec, } impl SpecFuncSection { - pub(crate) fn new(map: &FxHashMap>) -> Self { + pub(crate) fn new(map: &SpecObligations) -> Self { Self { payload: encode_payload(map), } @@ -194,33 +289,100 @@ impl Section for SpecFuncSection { mod tests { use super::*; + /// Builds a [`SpecObligations`] map from `(name, [(idx, kind)])` literals. + fn obligations( + entries: &[(&str, &[(u32, SpecObligationKind)])], + ) -> SpecObligations { + entries + .iter() + .map(|(name, items)| ((*name).to_string(), items.to_vec())) + .collect() + } + + /// All-`Spec` sugar: `(name, [idx])` pairs with the default obligation kind. + fn spec_only(entries: &[(&str, &[u32])]) -> SpecObligations { + entries + .iter() + .map(|(name, indices)| { + let items = indices + .iter() + .map(|&idx| (idx, SpecObligationKind::Spec)) + .collect(); + ((*name).to_string(), items) + }) + .collect() + } + #[test] fn empty_map_encodes_zero_count() { - let map: FxHashMap> = FxHashMap::default(); - let payload = encode_payload(&map); + let payload = encode_payload(&SpecObligations::default()); // version=1, count=0 assert_eq!(payload, vec![1, 0]); } #[test] fn single_spec_round_trip_bytes() { - let mut map: FxHashMap> = FxHashMap::default(); - map.insert("S".into(), vec![3, 4]); - let payload = encode_payload(&map); + let payload = encode_payload(&spec_only(&[("S", &[3, 4])])); // version=1, count=1, name_len=1, 'S', idx_count=2, 3, 4 assert_eq!(payload, vec![1, 1, 1, b'S', 2, 3, 4]); } #[test] fn sorted_by_spec_name() { - let mut map: FxHashMap> = FxHashMap::default(); - map.insert("B".into(), vec![5]); - map.insert("A".into(), vec![2]); - let payload = encode_payload(&map); + let payload = encode_payload(&spec_only(&[("B", &[5]), ("A", &[2])])); // version=1, count=2, name_len=1, 'A', idx_count=1, 2, name_len=1, 'B', idx_count=1, 5 assert_eq!(payload, vec![1, 2, 1, b'A', 1, 2, 1, b'B', 1, 5]); } + #[test] + fn all_spec_kinds_stay_version_one_byte_identical() { + // An all-`Spec` obligations map must encode identically to the legacy + // index-only payload, so existing modules are byte-stable. + let with_kinds = encode_payload(&obligations(&[( + "S", + &[(3, SpecObligationKind::Spec), (4, SpecObligationKind::Spec)], + )])); + let legacy = encode_payload(&spec_only(&[("S", &[3, 4])])); + assert_eq!(with_kinds, legacy); + assert_eq!(with_kinds, vec![1, 1, 1, b'S', 2, 3, 4]); + } + + #[test] + fn exists_kind_promotes_to_version_two_with_kind_bytes() { + let payload = encode_payload(&obligations(&[( + "S", + &[(3, SpecObligationKind::Exists)], + )])); + // version=2, count=1, name_len=1, 'S', idx_count=1, idx=3, kind=1 (Exists) + assert_eq!(payload, vec![2, 1, 1, b'S', 1, 3, 1]); + } + + #[test] + fn mixed_kinds_emit_kinds_for_every_spec_in_version_two() { + // One non-`Spec` kind anywhere promotes the whole payload to v2, so even + // the all-`Spec` spec must carry its (zero) kind bytes. + let payload = encode_payload(&obligations(&[ + ("A", &[(0, SpecObligationKind::Spec)]), + ("B", &[(1, SpecObligationKind::Unique)]), + ])); + // v2, count=2, + // 'A': name_len=1 'A', idx_count=1, idx=0, kind=0 (Spec) + // 'B': name_len=1 'B', idx_count=1, idx=1, kind=2 (Unique) + assert_eq!(payload, vec![2, 2, 1, b'A', 1, 0, 0, 1, b'B', 1, 1, 2]); + } + + #[test] + fn obligation_kind_byte_round_trip() { + for kind in [ + SpecObligationKind::Spec, + SpecObligationKind::Exists, + SpecObligationKind::Unique, + ] { + assert_eq!(SpecObligationKind::from_byte(kind.to_byte()), Some(kind)); + } + assert_eq!(SpecObligationKind::from_byte(3), None); + } + #[test] fn name_within_cap_passes_check() { let mut map: FxHashMap> = FxHashMap::default(); @@ -263,8 +425,7 @@ mod tests { #[test] fn payload_starts_with_version_byte() { - let map: FxHashMap> = FxHashMap::default(); - let payload = encode_payload(&map); + let payload = encode_payload(&SpecObligations::default()); let expected = u8::try_from(SECTION_VERSION).expect("version fits in a byte"); assert_eq!( payload.first().copied(), diff --git a/core/wasm-linker/src/merge.rs b/core/wasm-linker/src/merge.rs index 5114a70c..c2350ab5 100644 --- a/core/wasm-linker/src/merge.rs +++ b/core/wasm-linker/src/merge.rs @@ -677,15 +677,18 @@ impl Plan { fn remap_spec_funcs( &self, main: &ParsedModule, - spec_funcs: &[(String, Vec)], - ) -> Result)>, LinkError> { + spec_funcs: &[crate::spec_funcs::SpecEntry], + ) -> Result, LinkError> { spec_funcs .iter() .map(|(name, indices)| { + // Remap the function index into the post-link space; carry the + // obligation-kind byte through unchanged (it is metadata about + // the spec, not a position in the function space). let mapped = indices .iter() - .map(|&idx| self.map_main_func(main, idx)) - .collect::, _>>()?; + .map(|&(idx, kind)| Ok((self.map_main_func(main, idx)?, kind))) + .collect::, LinkError>>()?; Ok((name.clone(), mapped)) }) .collect() diff --git a/core/wasm-linker/src/parse.rs b/core/wasm-linker/src/parse.rs index f128edbf..c179bb3b 100644 --- a/core/wasm-linker/src/parse.rs +++ b/core/wasm-linker/src/parse.rs @@ -144,11 +144,12 @@ pub(crate) struct ParsedModule { /// function do not. Retained so the proof artifact keeps local debug names. pub local_names: BTreeMap>, /// The decoded `inference.spec_funcs` custom section: `spec_name -> - /// [func_idx]` in the *pre-link* index space. The merge rewrites each index - /// into the output space and re-emits the section, so a bare linked `.wasm` - /// still names the correct spec functions (the input to formal verification). - /// Only the main module carries one; externals never do. - pub spec_funcs: Option)>>, + /// [(func_idx, kind_byte)]` in the *pre-link* index space. The merge + /// rewrites each index into the output space (carrying the obligation-kind + /// byte through verbatim) and re-emits the section, so a bare linked `.wasm` + /// still names the correct spec functions with their kinds (the input to + /// formal verification). Only the main module carries one; externals never do. + pub spec_funcs: Option>, /// The logical, `::`-joined module reference this module was bound under /// (e.g. `"crypto::sha256"`), for an external; empty for the main module. /// The merge matches each main-module import's recorded `(module, field)` @@ -674,7 +675,8 @@ mod tests { let main = ParsedModule::parse(&bytes).expect("main parse"); assert_eq!( main.spec_funcs, - Some(vec![("S".to_string(), vec![0])]), + // A v1 payload decodes with a default kind byte of 0 per index. + Some(vec![("S".to_string(), vec![(0u32, 0u8)])]), "the main module must decode its spec section" ); diff --git a/core/wasm-linker/src/spec_funcs.rs b/core/wasm-linker/src/spec_funcs.rs index c9309351..592068c6 100644 --- a/core/wasm-linker/src/spec_funcs.rs +++ b/core/wasm-linker/src/spec_funcs.rs @@ -11,17 +11,22 @@ //! ## Payload format (LEB128 u32 throughout) //! //! ```text -//! version -- format version (must equal `VERSION`) +//! version -- 1 = legacy (indices only), 2 = with kind bytes //! count -- number of (spec_name, indices) pairs //! repeat `count` times: //! name_len name_bytes(utf-8) //! idx_count repeat `idx_count` times: func_idx +//! -- version 2 only: one obligation-kind byte per index, same order: +//! repeat `idx_count` times (v2 only): kind_byte (u8) //! ``` //! //! The format mirrors `inference_wasm_codegen::spec_section`; the linker keeps a -//! self-contained copy rather than depend on the codegen crate. The decoder is -//! fully bounds-checked: a malformed external `.wasm` (or a corrupt main module) -//! must surface a clean [`LinkError`], never a panic or an unbounded allocation. +//! self-contained copy rather than depend on the codegen crate. The obligation +//! kind selects the downstream Rocq predicate (`ValidSpec`/`ValidExistsSpec`/ +//! `ValidUniqueSpec`); the linker does not interpret it — it carries each byte +//! through verbatim alongside the index it remaps. The decoder is fully +//! bounds-checked: a malformed external `.wasm` (or a corrupt main module) must +//! surface a clean [`LinkError`], never a panic or an unbounded allocation. use inf_wasmparser::BinaryReader; @@ -33,33 +38,52 @@ use crate::LinkError; /// crate. pub(crate) const SECTION_NAME: &str = "inference.spec_funcs"; -/// Wire-format version. Kept in lock-step with the codegen emitter. +/// Legacy wire-format version: function indices only. Kept in lock-step with +/// the codegen emitter. const VERSION: u32 = 1; +/// Wire-format version that additionally carries one obligation-kind byte per +/// index. Kept in lock-step with the codegen emitter. The decoder accepts both +/// versions; [`encode`] re-emits whichever the kinds require. +const VERSION_WITH_KINDS: u32 = 2; + +/// A decoded spec entry: the spec name and its `(func_idx, kind_byte)` pairs. +/// The kind byte is carried verbatim (0 for legacy v1 inputs); the linker +/// remaps the index but never the kind. +pub(crate) type SpecEntry = (String, Vec<(u32, u8)>); + /// Defensive upper bound on a single spec name's length, matching the decoder /// in `wasm-to-v`. A hand-crafted payload could advertise a far longer name; /// cap it so the per-name allocation stays bounded. const MAX_SPEC_NAME_LEN: usize = 255; -/// Decodes the `inference.spec_funcs` payload into `(spec_name, [func_idx])` -/// pairs, preserving the encoded order so a round-trip is byte-stable. +/// Decodes the `inference.spec_funcs` payload into [`SpecEntry`] pairs, +/// preserving the encoded order so a round-trip is byte-stable. +/// +/// Accepts both [`VERSION`] (legacy, indices only — every kind byte defaults to +/// `0`) and [`VERSION_WITH_KINDS`] (a trailing kind byte per index). /// /// # Errors /// /// Returns [`LinkError::Parse`] on any malformed input: an unrecognised /// version, a truncated LEB128, invalid UTF-8 in a spec name, an /// over-advertised pair/index count, or a name exceeding [`MAX_SPEC_NAME_LEN`]. -pub(crate) fn decode(data: &[u8]) -> Result)>, LinkError> { +pub(crate) fn decode(data: &[u8]) -> Result, LinkError> { let mut reader = BinaryReader::new(data, 0); let version = reader .read_var_u32() .map_err(|e| LinkError::Parse(format!("spec_funcs section: truncated version: {e}")))?; - if version != VERSION { - return Err(LinkError::Parse(format!( - "spec_funcs section: unsupported version {version} (expected {VERSION})" - ))); - } + let has_kinds = match version { + VERSION => false, + VERSION_WITH_KINDS => true, + other => { + return Err(LinkError::Parse(format!( + "spec_funcs section: unsupported version {other} \ + (expected {VERSION} or {VERSION_WITH_KINDS})" + ))); + } + }; let count = reader .read_var_u32() @@ -73,7 +97,7 @@ pub(crate) fn decode(data: &[u8]) -> Result)>, LinkError> )); } - let mut out: Vec<(String, Vec)> = Vec::with_capacity(count as usize); + let mut out: Vec = Vec::with_capacity(count as usize); for _ in 0..count { // `read_string` returns a borrowed `&str` into the payload (no // allocation). Enforce the length cap on that borrow *before* copying it @@ -94,20 +118,31 @@ pub(crate) fn decode(data: &[u8]) -> Result)>, LinkError> let idx_count = reader.read_var_u32().map_err(|e| { LinkError::Parse(format!("spec_funcs section: truncated indices count: {e}")) })?; - // Each index consumes at least one payload byte, so `idx_count` cannot - // legitimately exceed the remaining payload. + // Each index consumes at least one payload byte; in v2 each also needs a + // trailing kind byte, so the entry needs `idx_count` (v1) or + // `2 * idx_count` (v2) bytes. Bound by the smaller v1 figure before + // allocating — the per-index reads below still fail closed if the kind + // bytes are truncated. if idx_count as usize > reader.bytes_remaining() { return Err(LinkError::Parse( "spec_funcs section: declared index count exceeds remaining payload".into(), )); } - let mut indices = Vec::with_capacity(idx_count as usize); + let mut indices: Vec<(u32, u8)> = Vec::with_capacity(idx_count as usize); for _ in 0..idx_count { let idx = reader.read_var_u32().map_err(|e| { LinkError::Parse(format!("spec_funcs section: truncated index: {e}")) })?; - indices.push(idx); + indices.push((idx, 0)); + } + if has_kinds { + for slot in &mut indices { + let kind = reader.read_u8().map_err(|e| { + LinkError::Parse(format!("spec_funcs section: truncated kind byte: {e}")) + })?; + slot.1 = kind; + } } out.push((name, indices)); } @@ -126,16 +161,26 @@ pub(crate) fn decode(data: &[u8]) -> Result)>, LinkError> Ok(out) } -/// Encodes `(spec_name, [func_idx])` pairs into the canonical payload bytes. +/// Encodes [`SpecEntry`] pairs into the canonical payload bytes. /// -/// The encoded order matches the input order; the merge preserves the decoded -/// order, which is the encoder's sorted-by-name order, so a decode/remap/encode -/// round-trip stays byte-stable. -pub(crate) fn encode(pairs: &[(String, Vec)]) -> Vec { +/// Emits [`VERSION`] (indices only) when every kind byte is `0`, so a v1 input +/// round-trips byte-identically; emits [`VERSION_WITH_KINDS`] (a trailing kind +/// byte per index) when any kind is non-zero. The encoded order matches the +/// input order; the merge preserves the decoded order, which is the encoder's +/// sorted-by-name order, so a decode/remap/encode round-trip stays byte-stable. +pub(crate) fn encode(pairs: &[SpecEntry]) -> Vec { use wasm_encoder::Encode; + let has_kinds = pairs + .iter() + .any(|(_, indices)| indices.iter().any(|&(_, kind)| kind != 0)); + let mut payload = Vec::new(); - VERSION.encode(&mut payload); + if has_kinds { + VERSION_WITH_KINDS.encode(&mut payload); + } else { + VERSION.encode(&mut payload); + } let count = u32::try_from(pairs.len()).expect("more than u32::MAX specs"); count.encode(&mut payload); @@ -147,9 +192,14 @@ pub(crate) fn encode(pairs: &[(String, Vec)]) -> Vec { name_len.encode(&mut payload); payload.extend_from_slice(name_bytes); idx_count.encode(&mut payload); - for idx in indices { + for &(idx, _) in indices { idx.encode(&mut payload); } + if has_kinds { + for &(_, kind) in indices { + payload.push(kind); + } + } } payload @@ -161,9 +211,11 @@ mod tests { #[test] fn round_trips_a_two_spec_payload() { - let pairs = vec![ - ("A".to_string(), vec![2, 3]), - ("B".to_string(), vec![5]), + // All-zero kinds → legacy v1 layout, byte-identical to the pre-kinds + // encoder so a v1 input survives a decode/encode round-trip unchanged. + let pairs: Vec = vec![ + ("A".to_string(), vec![(2, 0), (3, 0)]), + ("B".to_string(), vec![(5, 0)]), ]; let bytes = encode(&pairs); // version=1, count=2, len=1 'A', idxc=2, 2,3, len=1 'B', idxc=1, 5 @@ -171,9 +223,38 @@ mod tests { assert_eq!(decode(&bytes).unwrap(), pairs); } + #[test] + fn round_trips_a_v2_payload_with_kinds() { + // A non-zero kind byte promotes the payload to v2; the kinds survive a + // decode/encode round-trip alongside their (unremapped here) indices. + let pairs: Vec = vec![ + ("A".to_string(), vec![(2, 0)]), + ("B".to_string(), vec![(5, 1), (6, 2)]), + ]; + let bytes = encode(&pairs); + // v2, count=2, + // 'A': len=1 'A', idxc=1, idx=2, kind=0 + // 'B': len=1 'B', idxc=2, idx=5, idx=6, kind=1, kind=2 + assert_eq!( + bytes, + vec![2, 2, 1, b'A', 1, 2, 0, 1, b'B', 2, 5, 6, 1, 2] + ); + assert_eq!(decode(&bytes).unwrap(), pairs); + } + + #[test] + fn decodes_a_legacy_v1_payload_with_zero_kinds() { + // A hand-crafted v1 payload (no kind bytes) decodes with every kind 0. + let bytes = vec![1, 1, 1, b'S', 2, 3, 4]; + assert_eq!( + decode(&bytes).unwrap(), + vec![("S".to_string(), vec![(3, 0), (4, 0)])] + ); + } + #[test] fn empty_payload_round_trips() { - let pairs: Vec<(String, Vec)> = Vec::new(); + let pairs: Vec = Vec::new(); let bytes = encode(&pairs); assert_eq!(bytes, vec![1, 0]); assert_eq!(decode(&bytes).unwrap(), pairs); @@ -181,11 +262,21 @@ mod tests { #[test] fn rejects_an_unsupported_version() { - // version=2, count=0 - let err = decode(&[2, 0]).unwrap_err(); + // version=3 is neither v1 nor v2. + let err = decode(&[3, 0]).unwrap_err(); assert!(matches!(err, LinkError::Parse(_)), "got {err:?}"); } + #[test] + fn rejects_a_truncated_v2_kind_byte() { + // v2, count=1, name_len=1 'S', idx_count=1, idx=0, + let err = decode(&[2, 1, 1, b'S', 1, 0]).unwrap_err(); + assert!( + matches!(&err, LinkError::Parse(msg) if msg.contains("kind")), + "expected a Parse error naming the missing kind byte, got {err:?}" + ); + } + #[test] fn rejects_an_over_advertised_pair_count() { // version=1, count=255 in a 3-byte payload. @@ -206,7 +297,7 @@ mod tests { // Silently dropping the trailing bytes (the prior behavior) would mask a // corrupt or version-skewed section; the decoder must fail closed, matching // the other truncation checks in this codec. - let mut bytes = encode(&[("S".to_string(), vec![0])]); + let mut bytes = encode(&[("S".to_string(), vec![(0, 0)])]); bytes.extend_from_slice(&[0xff, 0xff]); let err = decode(&bytes).unwrap_err(); assert!( diff --git a/core/wasm-linker/tests/link.rs b/core/wasm-linker/tests/link.rs index deff5593..f59a36fc 100644 --- a/core/wasm-linker/tests/link.rs +++ b/core/wasm-linker/tests/link.rs @@ -155,6 +155,31 @@ fn decode_spec_funcs(data: &[u8]) -> Vec<(String, Vec)> { out } +/// Decodes the v2 (`with kinds`) `inference.spec_funcs` payload into +/// `(spec_name, [(idx, kind_byte)])` pairs, for asserting that the obligation +/// kind survives the decode/remap/re-encode link path alongside the remapped +/// index. +fn decode_spec_funcs_v2(data: &[u8]) -> Vec<(String, Vec<(u32, u8)>)> { + let mut reader = inf_wasmparser::BinaryReader::new(data, 0); + let version = reader.read_var_u32().unwrap(); + assert_eq!(version, 2, "spec_funcs version (with kinds)"); + let count = reader.read_var_u32().unwrap(); + let mut out = Vec::new(); + for _ in 0..count { + let name = reader.read_string().unwrap().to_string(); + let idx_count = reader.read_var_u32().unwrap(); + let mut indices: Vec<(u32, u8)> = Vec::new(); + for _ in 0..idx_count { + indices.push((reader.read_var_u32().unwrap(), 0)); + } + for slot in &mut indices { + slot.1 = reader.read_u8().unwrap(); + } + out.push((name, indices)); + } + out +} + /// Whether the body of the function at `func_idx` contains an `i32.add`. fn body_has_i32_add(bytes: &[u8], func_idx: usize) -> bool { let mut idx = 0; @@ -1993,6 +2018,50 @@ fn spec_funcs_section_survives_and_is_reindexed() { ); } +/// Same H25 + C1 reindexing as above, but for a **version-2** spec section that +/// carries an obligation-kind byte per index (here `Exists` = 1). The link must +/// remap the index from the pre-link space (1) to the post-link space (0) while +/// preserving the kind byte verbatim, and re-emit a v2 section (the kind is +/// non-zero, so it cannot normalize back to v1). This pins the kind-preserving +/// remap path that drives downstream `ValidExistsSpec`/`ValidUniqueSpec` +/// selection. +#[test] +fn spec_funcs_v2_section_survives_reindexed_and_keeps_kind() { + // version=2, count=1, name_len=1 'S', idx_count=1, index=1, kind=1 (Exists) + let spec_payload = [2u8, 1, 1, b'S', 1, 1, 1]; + let main_wat = r#" + (module + (type (;0;) (func (param i32 i32) (result i32))) + (import "mathlib" "sum" (func (;0;) (type 0))) + (func (;1;) (type 0) (param i32 i32) (result i32) + local.get 0 + local.get 1 + call 0) + (export "compute" (func 1))) + "#; + let mut main = wasm(main_wat); + use wasm_encoder::Section as _; + wasm_encoder::CustomSection { + name: "inference.spec_funcs".into(), + data: (&spec_payload[..]).into(), + } + .append_to(&mut main); + + let lib = mathlib_pure(); + let linked = link(&main, &[&lib]).expect("link must preserve the v2 spec section"); + assert_valid(&linked); + + let data = custom_section_data(&linked, "inference.spec_funcs") + .expect("the linked module must still carry the spec_funcs section (H25)"); + let decoded = decode_spec_funcs_v2(&data); + assert_eq!( + decoded, + vec![("S".to_string(), vec![(0u32, 1u8)])], + "pre-link index 1 must rewrite to post-link index 0 (C1) while the \ + Exists kind byte (1) is preserved verbatim" + ); +} + #[test] fn out_of_range_spec_funcs_index_is_a_clean_parse_error() { // S2: a spec index past the main module's function count must reject as a diff --git a/core/wasm-to-v/ROCQ_CONTRACT.md b/core/wasm-to-v/ROCQ_CONTRACT.md index 28956c46..43e4b956 100644 --- a/core/wasm-to-v/ROCQ_CONTRACT.md +++ b/core/wasm-to-v/ROCQ_CONTRACT.md @@ -31,7 +31,30 @@ The translator assumes a Rocq context that supplies the following: this document fixes the arity (`module → list N → Prop`) and the call shape (`Theorem valid___ : ValidSpec ___specs`); the downstream library defines what the per-spec invariant actually - says about each indexed function. + says about each indexed function. `ValidSpec` is the obligation for + `forall`-quantified and regular spec functions: a **universal** safety + property (the function is trap-free for every input). +- A predicate `ValidExistsSpec : module -> list N -> Prop`, the obligation + for `exists`-quantified spec functions. Same arity and call shape as + `ValidSpec` (`Theorem valid____exists : ValidExistsSpec + ___exists_specs`), but a strictly stronger + property: **existential reachability** — there is an input from which + the function runs to completion without trapping. This is *more than + trap-freedom*; a universal `ValidSpec` does not imply it. +- A predicate `ValidUniqueSpec : module -> list N -> Prop`, the obligation + for `unique`-quantified spec functions (`Theorem + valid____unique : ValidUniqueSpec + ___unique_specs`): existential reachability **plus** that + the witness input is the only non-trapping one. + +`ValidSpec`/`ValidExistsSpec`/`ValidUniqueSpec` all share the +`module → list N → Prop` arity. `ValidModule` and `ValidSpec` are defined +in the downstream library's `Verifier` module; `ValidExistsSpec` and +`ValidUniqueSpec` in its `Exists` module. The generated file always +`Require Import Verifier`, and additionally `Require Import Exists` when +(and only when) it emits an `exists`/`unique` obligation — so an +all-`forall`/regular program's output is byte-identical to before these +predicates existed. The pre-#21 form `ValidModule : module -> list N -> Prop` is no longer emitted. Downstream proofs that consumed the old 2-argument shape must @@ -73,11 +96,41 @@ Qed. End Host. ``` +### Quantified specs: `exists` / `unique` + +When a spec function is `exists`- or `unique`-quantified, its obligation +is `ValidExistsSpec` / `ValidUniqueSpec` instead of `ValidSpec`, over a +kind-suffixed list. A spec's functions are partitioned by kind and each +non-empty group emits its own `_specs` list and theorem: + +```coq +(* spec Q with a forall fn at index 3 and an exists fn at index 4 *) +Definition Foo__Q_specs : list N := [3]%N. +Definition Foo__Q__exists_specs : list N := [4]%N. + +Theorem valid_Foo__Q : ValidSpec Foo Foo__Q_specs. +Theorem valid_Foo__Q__exists : ValidExistsSpec Foo Foo__Q__exists_specs. +``` + +The kind-suffixed list/theorem names join the kind with the reserved +`__` separator: `____exists_specs` / `valid_____exists` +and `____unique_specs` / `valid_____unique`. The `__` +(not a plain `_`) is deliberate: since `validate_rocq_identifier` forbids +`__` inside any module or spec name, a kind-suffixed name can never alias +another spec's `_specs` list (a plain-`_` form would let a spec literally +named `_exists` collide with spec ``'s exists list). A spec +with only `forall`/regular functions emits exactly its prior single +`_specs`/`ValidSpec` pair (byte-identical to pre-quantifier output); a +spec with no functions at all keeps the legacy `_specs := (@nil N)` + +`ValidSpec` shape. The obligation kind is recovered from the +`inference.spec_funcs` section (see below) — the vanilla WASM body no +longer carries the quantifier. + Notes: -- Per-spec lists and per-spec `ValidSpec` theorems are emitted **only - when** there is at least one spec block. A module with zero specs - emits only `Foo` and `Theorem valid_Foo`. +- Per-spec lists and per-spec theorems are emitted **only when** there is + at least one spec block. A module with zero specs emits only `Foo` and + `Theorem valid_Foo`. - The separator between the module name and the spec name is `__` (two underscores). Single `_` would be ambiguous when the user's spec names contain underscores: a module `foo_foo` with a spec `bar` and a @@ -120,10 +173,11 @@ the same map in the WASM binary as a custom section named ### Wire format of the `inference.spec_funcs` payload -The payload uses LEB128 unsigned varints throughout: +The payload uses LEB128 unsigned varints throughout (except the v2 kind +bytes, which are raw `u8`): ```text -version : varuint32 -- currently 1; bump on breaking change +version : varuint32 -- 1 = legacy (indices only), 2 = with kinds count : varuint32 -- number of (spec_name, indices) pairs repeated `count` times: spec_name_len : varuint32 @@ -131,6 +185,9 @@ repeated `count` times: indices_count : varuint32 repeated `indices_count` times: func_idx : varuint32 + -- version 2 only: one obligation-kind byte per index, same order: + repeated `indices_count` times (v2 only): + kind_byte : u8 -- 0 = Spec, 1 = Exists, 2 = Unique ``` Entries are emitted sorted by spec name for deterministic, byte-stable @@ -138,11 +195,22 @@ output. The decoder validates each spec name against the Rocq identifier rules at the decode boundary, rejecting `WasmToVError::InvalidRocqIdentifier` before any Rocq emission runs. -The leading `version` varuint32 is the contract's escape hatch. The current -decoder rejects unsupported versions with `WasmToVError::WasmParse` carrying -the literal string "version" — see -`inference_wasm_codegen::SPEC_FUNCS_SECTION_VERSION` for the constant. A -future revision that bumps the version will trip this branch on today's +The obligation kind selects the downstream predicate (`Spec` → +`ValidSpec`, `Exists` → `ValidExistsSpec`, `Unique` → `ValidUniqueSpec`). +A `forall`/regular/`assume` spec function maps to `Spec`, so the encoder +emits **version 1** (no kind bytes) whenever every obligation is `Spec` — +keeping all pre-quantifier modules byte-identical — and **version 2** (the +trailing kind bytes) only when an `exists`/`unique` obligation is present. +Both decoders (the Rocq translator and the linker, which remaps each index +on link while carrying the kind byte through verbatim) accept either +version; a v1 payload decodes with every kind defaulting to `Spec`. + +The leading `version` varuint32 is the contract's escape hatch. The +decoder rejects *unrecognised* versions (neither 1 nor 2) with +`WasmToVError::WasmParse` carrying the literal string "version" — see +`inference_wasm_codegen::SPEC_FUNCS_SECTION_VERSION` and +`…SPEC_FUNCS_SECTION_VERSION_WITH_KINDS` for the constants. A future +revision that bumps the version further will trip this branch on today's parsers instead of silently misparsing the rest of the payload. `wasm_to_v` / `translate_bytes` accept the map as an explicit argument and diff --git a/core/wasm-to-v/src/lib.rs b/core/wasm-to-v/src/lib.rs index 6541c814..fd28cf5b 100644 --- a/core/wasm-to-v/src/lib.rs +++ b/core/wasm-to-v/src/lib.rs @@ -178,6 +178,16 @@ pub use inference_wasm_codegen::SPEC_FUNCS_SECTION_NAME; /// expected leading varuint32. pub use inference_wasm_codegen::SPEC_FUNCS_SECTION_VERSION; +/// Wire-format version that additionally carries one [`SpecObligationKind`] +/// byte per index (see `inference_wasm_codegen::spec_section`). The decoder +/// accepts this alongside [`SPEC_FUNCS_SECTION_VERSION`]. +pub use inference_wasm_codegen::SPEC_FUNCS_SECTION_VERSION_WITH_KINDS; + +/// The downstream proof obligation a spec function carries (`Spec` / `Exists` / +/// `Unique`). Recovered from the `inference.spec_funcs` section to choose the +/// emitted predicate (`ValidSpec` / `ValidExistsSpec` / `ValidUniqueSpec`). +pub use inference_wasm_codegen::SpecObligationKind; + #[cfg(test)] mod tests { use super::wasm_parser::translate_bytes; diff --git a/core/wasm-to-v/src/translator.rs b/core/wasm-to-v/src/translator.rs index a36fe00a..7ce2b6e4 100644 --- a/core/wasm-to-v/src/translator.rs +++ b/core/wasm-to-v/src/translator.rs @@ -169,6 +169,7 @@ use inf_wasmparser::{ }; use rustc_hash::{FxHashMap, FxHashSet}; +use crate::SpecObligationKind; use crate::errors::WasmToVError; const LCB: &str = "{|\n"; @@ -234,10 +235,82 @@ pub(crate) struct WasmParseData<'a> { /// Rocq definition consumed by the corresponding `ValidModule` theorem. pub(crate) spec_funcs_by_spec: FxHashMap>, + /// Per-index proof obligations, parallel to [`Self::spec_funcs_by_spec`] + /// (same key, same order). Recovered from the `inference.spec_funcs` + /// section's version-2 kind bytes; empty (or short) entries default to + /// [`SpecObligationKind::Spec`]. Drives the choice of emitted predicate: + /// `Spec` → `ValidSpec`, `Exists` → `ValidExistsSpec`, `Unique` → + /// `ValidUniqueSpec`. + pub(crate) spec_func_kinds_by_spec: FxHashMap>, + translated_function_names: Vec, translated_functions_string: String, } +/// One spec's WASM function indices, partitioned by the downstream proof +/// obligation their quantifier implies. Each group is emitted as its own +/// `_specs` list + `Valid*Spec` theorem; empty groups are skipped (except the +/// legacy zero-function shape — see [`WasmParseData::spec_obligation_groups`]). +struct SpecKindGroups { + /// File-qualified spec name (the `` in `__`). + name: String, + /// Universal trap-freedom obligations (`forall`/regular/`assume`) → + /// `ValidSpec`. + spec: Vec, + /// Existential-reachability obligations (`exists`) → `ValidExistsSpec`. + exists: Vec, + /// Unique-witness obligations (`unique`) → `ValidUniqueSpec`. + unique: Vec, +} + +impl SpecKindGroups { + /// True when the spec contributed no function indices at all — the legacy + /// empty-`spec {}` case, which still emits a single `ValidSpec` over `@nil`. + fn is_empty(&self) -> bool { + self.spec.is_empty() && self.exists.is_empty() && self.unique.is_empty() + } +} + +/// Emits a `Definition : list N := …` for a group's indices. +/// +/// Empty lists use `(@nil N)` (not `[]%N`) so the definition type-checks +/// regardless of whether `Open Scope N_scope` is in effect at the consumer's +/// `Require` site; non-empty lists use the `(… :: nil)%N` cons form. +fn push_specs_definition(res: &mut String, def_name: &str, indices: &[u32]) { + res.push('\n'); + if indices.is_empty() { + res.push_str(format!("Definition {def_name} : list N := (@nil N).\n").as_str()); + } else { + let indices_str = indices + .iter() + .map(u32::to_string) + .collect::>() + .join(" :: "); + res.push_str( + format!("Definition {def_name} : list N := ({indices_str} :: nil)%N.\n").as_str(), + ); + } +} + +/// Emits a `Theorem : .` with the +/// standard `(* TODO: fill the proof *)` skeleton the downstream Rocq library +/// completes. +fn push_valid_theorem( + res: &mut String, + thm_name: &str, + predicate: &str, + module_name: &str, + specs_name: &str, +) { + res.push('\n'); + res.push_str( + format!("Theorem {thm_name} : {predicate} {module_name} {specs_name}.\n").as_str(), + ); + res.push_str("Proof.\n"); + res.push_str(" (* TODO: fill the proof *)\n"); + res.push_str("Qed.\n"); +} + impl WasmParseData<'_> { /// Creates a new empty [`WasmParseData`] with the given module name and spec indices. /// @@ -268,12 +341,53 @@ impl WasmParseData<'_> { function_type_indexes: Vec::new(), function_bodies: Vec::new(), spec_funcs_by_spec, + spec_func_kinds_by_spec: FxHashMap::default(), translated_function_names: Vec::new(), translated_functions_string: String::new(), } } + /// Partitions every spec's recorded indices by obligation kind, returning + /// one [`SpecKindGroups`] per spec, sorted by spec name for deterministic + /// output. + /// + /// Each index's kind comes from the parallel + /// [`Self::spec_func_kinds_by_spec`] map (populated from the + /// `inference.spec_funcs` section); a missing or short entry — e.g. a legacy + /// v1 section, or an explicit caller map with no embedded kinds — defaults + /// every such index to [`SpecObligationKind::Spec`], so the output reduces + /// to the historical all-`ValidSpec` shape. + fn spec_obligation_groups(&self) -> Vec { + let mut out: Vec = self + .spec_funcs_by_spec + .iter() + .map(|(name, indices)| { + let kinds = self.spec_func_kinds_by_spec.get(name); + let mut groups = SpecKindGroups { + name: name.clone(), + spec: Vec::new(), + exists: Vec::new(), + unique: Vec::new(), + }; + for (i, &idx) in indices.iter().enumerate() { + let kind = kinds + .and_then(|ks| ks.get(i)) + .copied() + .unwrap_or(SpecObligationKind::Spec); + match kind { + SpecObligationKind::Spec => groups.spec.push(idx), + SpecObligationKind::Exists => groups.exists.push(idx), + SpecObligationKind::Unique => groups.unique.push(idx), + } + } + groups + }) + .collect(); + out.sort_by(|a, b| a.name.cmp(&b.name)); + out + } + /// Translates the parsed WASM data into complete Rocq code. /// /// This is the main translation entry point. It generates a complete Rocq file @@ -332,6 +446,16 @@ impl WasmParseData<'_> { for spec_name in self.spec_funcs_by_spec.keys() { crate::rocq_names::validate_spec_join_boundary(&self.mod_name, spec_name)?; } + // Partition every spec's indices by obligation kind up front: it both + // drives the per-group definitions/theorems below and decides whether + // the header must pull in the `Exists` module (which defines + // `ValidExistsSpec`/`ValidUniqueSpec`). `Verifier` alone suffices for an + // all-`forall`/regular program, keeping its output byte-identical. + let spec_groups = self.spec_obligation_groups(); + let needs_exists_import = spec_groups + .iter() + .any(|g| !g.exists.is_empty() || !g.unique.is_empty()); + let mut res = String::new(); res.push_str("Require Import List.\n"); res.push_str("Require Import String.\n"); @@ -341,6 +465,13 @@ impl WasmParseData<'_> { res.push_str("From Wasm Require Import numerics.\n"); res.push_str("From Wasm Require Import datatypes.\n"); res.push_str("From WasmVerifier Require Import Verifier.\n"); + if needs_exists_import { + // `ValidExistsSpec` / `ValidUniqueSpec` live in `Exists` (which + // itself re-requires `Verifier`); emit it only when an + // `exists`/`unique` spec is present so existing artifacts are + // unchanged. + res.push_str("From WasmVerifier Require Import Exists.\n"); + } res.push('\n'); res.push_str("Definition Vi32 i := VAL_int32 (Wasm_int.int_of_Z i32m i).\n"); res.push_str("Definition Vi64 i := VAL_int64 (Wasm_int.int_of_Z i64m i).\n"); @@ -533,37 +664,57 @@ impl WasmParseData<'_> { res.push_str(format!(" mod_exports :=\n{created_exports};\n").as_str()); res.push_str(RCB_DOT); - // Emit per-spec lists of WASM function indices, sorted by spec name - // for deterministic output. Spec names were validated against the - // Rocq identifier rules at the top of `translate()` so that - // `___specs` is always a syntactically legal Rocq - // identifier. - let mut spec_entries: Vec<(&String, &Vec)> = - self.spec_funcs_by_spec.iter().collect(); - spec_entries.sort_by(|a, b| a.0.cmp(b.0)); - - for (spec_name, indices) in &spec_entries { - res.push('\n'); - if indices.is_empty() { - // (@nil N): no literals to disambiguate, and works regardless - // of scope state at the Require site. - res.push_str( - format!( - "Definition {module_name}__{spec_name}_specs : list N := (@nil N).\n" - ) - .as_str(), + // Emit per-spec lists of WASM function indices, sorted by spec name for + // deterministic output and split by obligation kind. Spec names were + // validated against the Rocq identifier rules at the top of `translate()` + // so that `___specs` (and the `__exists_specs` / + // `__unique_specs` siblings) are always syntactically legal Rocq + // identifiers. + // + // A spec function's quantifier picks its predicate: `forall`/regular → + // `ValidSpec`, `exists` → `ValidExistsSpec`, `unique` → `ValidUniqueSpec` + // (the existential predicates assert *reachability*, strictly more than + // the universal trap-freedom `ValidSpec` asserts). A spec with no + // functions keeps the legacy single `_specs := (@nil N)` / `ValidSpec` + // shape, and an all-`forall`/regular spec keeps exactly its prior + // `_specs` / `ValidSpec` output — only `exists`/`unique` functions add + // the new sibling definitions and theorems. + // + // The kind is joined with the reserved `__` separator + // (`____exists_specs`), not a plain `_`. Because + // `validate_rocq_identifier` forbids `__` inside any module or spec name, + // a kind-suffixed name can never alias another spec's `_specs` list: the + // single-`_` form (`___exists_specs`) would collide with a spec + // literally named `_exists`, but `____exists_specs` cannot, + // since no spec name contains the `__` run. + for g in &spec_groups { + if g.is_empty() { + push_specs_definition( + &mut res, + &format!("{module_name}__{}_specs", g.name), + &[], ); - } else { - let indices_str = indices - .iter() - .map(u32::to_string) - .collect::>() - .join(" :: "); - res.push_str( - format!( - "Definition {module_name}__{spec_name}_specs : list N := ({indices_str} :: nil)%N.\n" - ) - .as_str(), + continue; + } + if !g.spec.is_empty() { + push_specs_definition( + &mut res, + &format!("{module_name}__{}_specs", g.name), + &g.spec, + ); + } + if !g.exists.is_empty() { + push_specs_definition( + &mut res, + &format!("{module_name}__{}__exists_specs", g.name), + &g.exists, + ); + } + if !g.unique.is_empty() { + push_specs_definition( + &mut res, + &format!("{module_name}__{}__unique_specs", g.name), + &g.unique, ); } } @@ -584,19 +735,48 @@ impl WasmParseData<'_> { res.push_str("Proof.\n"); res.push_str(" (* TODO: fill the proof *)\n"); res.push_str("Qed.\n"); - // Per-spec verification obligations. `ValidSpec` is the 2-argument predicate (module - // and the list of WASM function indices for this spec); it entails `ValidModule`. - for (spec_name, _) in &spec_entries { - res.push('\n'); - res.push_str( - format!( - "Theorem valid_{module_name}__{spec_name} : ValidSpec {module_name} {module_name}__{spec_name}_specs.\n" - ) - .as_str(), - ); - res.push_str("Proof.\n"); - res.push_str(" (* TODO: fill the proof *)\n"); - res.push_str("Qed.\n"); + // Per-spec verification obligations, one theorem per non-empty kind group. + // `ValidSpec`/`ValidExistsSpec`/`ValidUniqueSpec` are all 2-argument + // predicates (module, list of WASM function indices) and each entails + // `ValidModule`. + for g in &spec_groups { + if g.is_empty() { + push_valid_theorem( + &mut res, + &format!("valid_{module_name}__{}", g.name), + "ValidSpec", + module_name, + &format!("{module_name}__{}_specs", g.name), + ); + continue; + } + if !g.spec.is_empty() { + push_valid_theorem( + &mut res, + &format!("valid_{module_name}__{}", g.name), + "ValidSpec", + module_name, + &format!("{module_name}__{}_specs", g.name), + ); + } + if !g.exists.is_empty() { + push_valid_theorem( + &mut res, + &format!("valid_{module_name}__{}__exists", g.name), + "ValidExistsSpec", + module_name, + &format!("{module_name}__{}__exists_specs", g.name), + ); + } + if !g.unique.is_empty() { + push_valid_theorem( + &mut res, + &format!("valid_{module_name}__{}__unique", g.name), + "ValidUniqueSpec", + module_name, + &format!("{module_name}__{}__unique_specs", g.name), + ); + } } res.push('\n'); res.push_str("End Host.\n"); diff --git a/core/wasm-to-v/src/wasm_parser.rs b/core/wasm-to-v/src/wasm_parser.rs index 48991128..692811e3 100644 --- a/core/wasm-to-v/src/wasm_parser.rs +++ b/core/wasm-to-v/src/wasm_parser.rs @@ -95,6 +95,7 @@ use inf_wasmparser::{ use rustc_hash::FxHashMap; use std::collections::HashMap; +use crate::SpecObligationKind; use crate::errors::WasmToVError; use crate::rocq_names::{sanitize_rocq_identifier, validate_rocq_identifier}; use crate::translator::WasmParseData; @@ -232,6 +233,7 @@ fn parse( let explicit_non_empty = !spec_funcs_by_spec.is_empty(); let mut wasm_parse_data = WasmParseData::new(mod_name, spec_funcs_by_spec); let mut embedded_spec_funcs: Option>> = None; + let mut embedded_spec_kinds: Option>> = None; let mut seen_name_section = false; for payload in parser.parse_all(data) { @@ -323,7 +325,10 @@ fn parse( crate::SPEC_FUNCS_SECTION_NAME )))); } - embedded_spec_funcs = Some(decode_spec_funcs_section(custom_section.data())?); + let (idx_map, kind_map) = + decode_spec_funcs_section(custom_section.data())?; + embedded_spec_funcs = Some(idx_map); + embedded_spec_kinds = Some(kind_map); } else if let inf_wasmparser::KnownCustom::Name(name_section) = custom_section.as_known() { @@ -419,26 +424,50 @@ fn parse( } } + // Obligation kinds are carried *only* by the embedded section (the explicit + // caller map is indices-only). When present they align with whichever index + // map won above — on agreement the two are equal, so the embedded kinds are + // correctly keyed. When absent (no embedded section, or a v1 payload), every + // spec function defaults to a universal `Spec` obligation, recovered lazily + // per-index by the translator. + if let Some(kinds) = embedded_spec_kinds { + wasm_parse_data.spec_func_kinds_by_spec = kinds; + } + Ok(wasm_parse_data) } -/// Decodes the `inference.spec_funcs` custom section payload. +/// Decodes the `inference.spec_funcs` custom section payload into its per-spec +/// function indices and the parallel per-index obligation kinds. /// -/// Schema (LEB128 u32 throughout): +/// Schema (LEB128 u32 throughout, except the kind bytes): /// ```text /// version /// count /// repeat count times: /// spec_name_len spec_name_bytes (utf-8) /// indices_count repeat indices_count times: func_idx +/// -- version 2 only: one kind byte per index, in the same order: +/// repeat indices_count times (v2 only): kind_byte (u8) /// ``` /// +/// Accepts both [`crate::SPEC_FUNCS_SECTION_VERSION`] (legacy, indices only — +/// every kind defaults to [`SpecObligationKind::Spec`]) and +/// [`crate::SPEC_FUNCS_SECTION_VERSION_WITH_KINDS`] (with the trailing kind +/// bytes). The returned kinds map is keyed identically to the indices map, with +/// each kind vector positionally aligned to its indices. +/// /// LEB128 reads and the length-prefixed UTF-8 spec-name read are delegated to /// `inf_wasmparser::BinaryReader`, which already enforces canonical LEB128 /// encoding (overlong rejection, integer-too-large rejection) and UTF-8 /// validation. Errors are mapped to `WasmToVError::WasmParse` so the existing /// downcast points in the CLI keep working. -fn decode_spec_funcs_section(data: &[u8]) -> anyhow::Result>> { +type DecodedSpecFuncs = ( + FxHashMap>, + FxHashMap>, +); + +fn decode_spec_funcs_section(data: &[u8]) -> anyhow::Result { use inf_wasmparser::BinaryReader; let mut reader = BinaryReader::new(data, 0); @@ -448,12 +477,17 @@ fn decode_spec_funcs_section(data: &[u8]) -> anyhow::Result anyhow::Result> = FxHashMap::default(); + let mut kinds_out: FxHashMap> = FxHashMap::default(); for _ in 0..count { let name = reader .read_string() @@ -510,6 +545,8 @@ fn decode_spec_funcs_section(data: &[u8]) -> anyhow::Result reader.bytes_remaining() { return Err(anyhow::anyhow!(WasmToVError::WasmParse( "spec_funcs section: declared index count exceeds remaining payload".into(), @@ -525,19 +562,41 @@ fn decode_spec_funcs_section(data: &[u8]) -> anyhow::Result> = FxHashMap::default(); + let v = inference::wasm_to_v("quant_kinds", wasm, &empty).expect("translate ok"); + + // The header pulls in `Exists` (home of ValidExistsSpec/ValidUniqueSpec) + // because the module has exists/unique specs; `Verifier` is always present. + assert!( + v.contains("From WasmVerifier Require Import Verifier."), + "Verifier import missing:\n{v}" + ); + assert!( + v.contains("From WasmVerifier Require Import Exists."), + "Exists import must be emitted when exists/unique specs are present:\n{v}" + ); + + // A pure-`forall` spec keeps exactly the legacy `ValidSpec` shape. + assert!( + v.contains( + "Theorem valid_quant_kinds__ForallSpec : \ + ValidSpec quant_kinds quant_kinds__ForallSpec_specs." + ), + "forall spec must stay ValidSpec:\n{v}" + ); + + // The `exists` spec selects `ValidExistsSpec` over its `__exists_specs` + // list (kind joined with the reserved `__` separator), and does NOT emit + // a bare `ValidSpec` (it has no universal funcs). + assert!( + v.contains( + "Theorem valid_quant_kinds__ExistsSpec__exists : \ + ValidExistsSpec quant_kinds quant_kinds__ExistsSpec__exists_specs." + ), + "exists spec must select ValidExistsSpec:\n{v}" + ); + assert!( + v.contains("Definition quant_kinds__ExistsSpec__exists_specs : list N :="), + "exists spec must emit its __exists_specs list:\n{v}" + ); + assert!( + !v.contains("Theorem valid_quant_kinds__ExistsSpec :"), + "a pure-exists spec must not emit a bare ValidSpec theorem:\n{v}" + ); + + // The `unique` spec selects `ValidUniqueSpec`. + assert!( + v.contains( + "Theorem valid_quant_kinds__UniqueSpec__unique : \ + ValidUniqueSpec quant_kinds quant_kinds__UniqueSpec__unique_specs." + ), + "unique spec must select ValidUniqueSpec:\n{v}" + ); + + // A mixed spec partitions: a `ValidSpec` for its forall function AND a + // `ValidExistsSpec` for its exists function, over distinct lists. + assert!( + v.contains( + "Theorem valid_quant_kinds__MixedSpec : \ + ValidSpec quant_kinds quant_kinds__MixedSpec_specs." + ), + "mixed spec must keep a ValidSpec for its forall function:\n{v}" + ); + assert!( + v.contains( + "Theorem valid_quant_kinds__MixedSpec__exists : \ + ValidExistsSpec quant_kinds quant_kinds__MixedSpec__exists_specs." + ), + "mixed spec must add a ValidExistsSpec for its exists function:\n{v}" + ); + } +} + +// ============================================================================ +// Fixture: spec_name_collision.inf — kind suffix must not alias a spec name +// ============================================================================ +#[cfg(test)] +mod fixture_spec_name_collision_e2e { + use super::helpers::compile_inf; + use inference_wasm_codegen::CompilationMode; + use rustc_hash::FxHashMap; + + /// Adversarial naming: spec `Foo` has an `exists` function (so it emits a + /// kind-suffixed `Foo__exists_specs` / `valid_Foo__exists`), and a *separate* + /// spec is literally named `Foo_exists` (so it emits `Foo_exists_specs` / + /// `valid_Foo_exists`). Were the kind joined with a single `_` + /// (`Foo_exists_specs`), the two would produce the *same* `Definition` and + /// `Theorem` names — a Rocq duplicate-definition error that breaks the whole + /// artifact. Joining the kind with the reserved `__` separator keeps them + /// distinct (`Foo__exists_specs` ≠ `Foo_exists_specs`), because no spec name + /// may contain `__`. This pins that the generated names never collide. + #[test] + fn kind_suffix_does_not_alias_a_spec_named_like_the_suffix() { + let output = compile_inf( + "spec_name_collision.inf", + CompilationMode::Proof, + "collide", + ); + let wasm = output.wasm(); + inf_wasmparser::validate(wasm).expect("WASM must validate"); + + let empty: FxHashMap> = FxHashMap::default(); + let v = inference::wasm_to_v("collide", wasm, &empty).expect("translate ok"); + + // Both the kind-suffixed name (spec Foo's exists group) and the + // similarly-named spec's plain name are present and DISTINCT. + assert!( + v.contains("Definition collide__Foo__exists_specs : list N :="), + "spec Foo's exists group uses the __ separator:\n{v}" + ); + assert!( + v.contains("Definition collide__Foo_exists_specs : list N :="), + "spec Foo_exists's plain spec list is unaffected:\n{v}" + ); + + // No emitted Definition or Theorem name appears twice (the bug this + // guards: a single-`_` join would make these two collide). + for dup in [ + "Definition collide__Foo__exists_specs", + "Definition collide__Foo_exists_specs", + "Theorem valid_collide__Foo__exists ", + "Theorem valid_collide__Foo_exists ", + ] { + assert_eq!( + v.matches(dup).count(), + 1, + "`{dup}` must be emitted exactly once (no duplicate definition):\n{v}" + ); + } + } +} diff --git a/tests/test_data/inf/e2e_call.inf b/tests/test_data/inf/e2e_call.inf new file mode 100644 index 00000000..2d420e39 --- /dev/null +++ b/tests/test_data/inf/e2e_call.inf @@ -0,0 +1,14 @@ +// A spec function that calls another (non-spec) function. Recursion is forbidden +// by analysis (A035), so this is a non-recursive inter-function call: `caller` +// invokes `idfn`. The forall obligation is trap-freedom for every input. +// Exercises the BI_call lowering downstream. +fn idfn(x: i32) -> i32 { + return x; +} + +spec CallSpec { + fn caller(i: i32) forall { + let r: i32 = idfn(i); + assert(r == r); + } +} diff --git a/tests/test_data/inf/e2e_loop.inf b/tests/test_data/inf/e2e_loop.inf new file mode 100644 index 00000000..f8baf244 --- /dev/null +++ b/tests/test_data/inf/e2e_loop.inf @@ -0,0 +1,12 @@ +// A spec function whose body iterates. The forall obligation is trap-freedom for +// every input: from k = 0, `loop k < n { k = k + 1; }` either runs zero times +// (n <= 0) or counts up to n; it never traps. Exercises the loop lowering +// (block { loop { cond; eqz; br_if 1; body; br 0 } }) downstream. +spec LoopSpec { + fn lp(n: i32) forall { + let mut k: i32 = 0; + loop k < n { + k = k + 1; + } + } +} diff --git a/tests/test_data/inf/e2e_quant_kinds.inf b/tests/test_data/inf/e2e_quant_kinds.inf new file mode 100644 index 00000000..ea457a58 --- /dev/null +++ b/tests/test_data/inf/e2e_quant_kinds.inf @@ -0,0 +1,29 @@ +// End-to-end fixture for the wasm-verifier downstream proof: one module +// exercising all three spec-obligation kinds, each with a *satisfiable* body so +// the generated obligation is dischargeable to Qed downstream. +// +// forall : assert(i == i) — trap-free for every i32 -> ValidSpec +// exists : assert(i == 5) — there IS an input (5) -> ValidExistsSpec +// unique : assert(i == 5) — 5 is the ONLY such input -> ValidUniqueSpec +// +// The quantified value is the function's first parameter (local 0); the bodies +// lower to the direct compiler shape with no scratch local, matching the proven +// rules sem_refl_assert / sem_assert_const / sem_assert_const_traps over pin0. + +spec QForall { + fn fa(i: i32) forall { + assert(i == i); + } +} + +spec QExists { + fn ex(i: i32) exists { + assert(i == 5); + } +} + +spec QUnique { + fn uq(i: i32) unique { + assert(i == 5); + } +} diff --git a/tests/test_data/inf/quant_kinds.inf b/tests/test_data/inf/quant_kinds.inf new file mode 100644 index 00000000..8d1cfa1f --- /dev/null +++ b/tests/test_data/inf/quant_kinds.inf @@ -0,0 +1,35 @@ +fn helper(x: i32) -> i32 { + return x; +} + +spec ForallSpec { + fn fa() forall { + let i: i32 = @; + assert(i == i); + } +} + +spec ExistsSpec { + fn ex() exists { + let i: i32 = @; + assert(i == i); + } +} + +spec UniqueSpec { + fn uq() unique { + let i: i32 = @; + assert(i == i); + } +} + +spec MixedSpec { + fn m_fa() forall { + let i: i32 = @; + assert(i == i); + } + fn m_ex() exists { + let i: i32 = @; + assert(i == i); + } +} diff --git a/tests/test_data/inf/spec_name_collision.inf b/tests/test_data/inf/spec_name_collision.inf new file mode 100644 index 00000000..b8abd06f --- /dev/null +++ b/tests/test_data/inf/spec_name_collision.inf @@ -0,0 +1,13 @@ +spec Foo { + fn f() exists { + let i: i32 = @; + assert(i == i); + } +} + +spec Foo_exists { + fn g() forall { + let i: i32 = @; + assert(i == i); + } +} From 1c5eeb764b21988175e7d01eb1b78e81e27bd473 Mon Sep 17 00:00:00 2001 From: 0xGeorgii Date: Mon, 13 Jul 2026 18:43:07 +0900 Subject: [PATCH 5/5] feat(wasm-to-v): emit assertion-valued _specs lists (wasm-verifier issue #6) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The downstream wasm-verifier contract is assertion-valued for all three obligation kinds (ValidSpec since its PR #2, ValidExistsSpec/ ValidUniqueSpec since its issue #6): the predicates take `module -> list assertion -> Prop`, so the `list N` index lists this translator emitted no longer type-check downstream. Emit `Definition ___specs : list assertion := (@nil assertion).` for every kind group instead. The translator cannot synthesize assertion payloads from spec bodies yet, so every list is empty — the group's WASM function indices are preserved in a preceding `(* function indices: ... (assertion payloads pending) *)` comment for the downstream prover, who carries the semantic content in standalone per-function lemmas (wasm-verifier's E2EQuantKinds.v is the reference shape). Emitting real assertion payloads remains the next milestone. Header changes: `From WasmVerifier Require Import Assertions.` is emitted whenever at least one spec is present (`assertion` lives there; zero-spec artifacts gain nothing), and `From Wasm Require Import host.` is now always emitted — the always-present `Section Host. Context `{ho: host}.` wrapper referenced a class the header never imported, so the raw artifact could not type-check on its own. Verified end to end: the regenerated quant_kinds.inf artifact type-checks against wasm-verifier main (dune build in its devcontainer, with the TODO-skeleton Qeds replaced by Abort), and the full test surface passes (wasm-to-v 29, inference-tests 2286, wasm-codegen, inference). ROCQ_CONTRACT.md updated (predicate arities, emission shape, empty-list rationale now (@nil assertion), new Migration section) plus CHANGELOG. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01Ev6Ch1XeDGdSCJbuzjDxuP --- CHANGELOG.md | 12 +++ core/inference/src/lib.rs | 5 +- core/wasm-codegen/src/compiler.rs | 4 +- core/wasm-codegen/src/output.rs | 5 +- core/wasm-to-v/ROCQ_CONTRACT.md | 126 ++++++++++++++++---------- core/wasm-to-v/src/lib.rs | 21 ++++- core/wasm-to-v/src/translator.rs | 69 ++++++++++---- tests/src/codegen/wasm/extern_link.rs | 11 ++- tests/src/spec_propagation.rs | 68 +++++++++----- tests/src/spec_propagation_inf.rs | 36 +++++--- 10 files changed, 242 insertions(+), 115 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 34b1591b..17f37e5f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -9,6 +9,18 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ### Breaking +- Rocq output: the per-spec `_specs` lists are now **assertion-valued** — + `Definition ___specs : list assertion := (@nil assertion).` — + matching the downstream wasm-verifier contract + (`ValidSpec`/`ValidExistsSpec`/`ValidUniqueSpec : module -> list assertion -> Prop`; + wasm-verifier PR #2 for `ValidSpec`, issue #6 for the existential pair). The + former `list N` index lists are gone; each group's WASM function indices are + preserved in a preceding `(* function indices: … *)` comment, and the + generated file now imports `From WasmVerifier Require Import Assertions.` + whenever at least one spec is present (zero-spec output is unchanged). + Assertion payloads are not synthesized yet — every list is emitted empty; + downstream provers carry the semantic content in standalone lemmas (see + `core/wasm-to-v/ROCQ_CONTRACT.md` → Migration). - `inference_wasm_codegen::CodegenOutput::spec_func_indices: Vec` → `spec_func_indices_by_spec: FxHashMap>`. The accessor renames to `spec_func_indices_by_spec()`. Library embedders of `core/inference` must diff --git a/core/inference/src/lib.rs b/core/inference/src/lib.rs index 6aff4895..ef7fa688 100644 --- a/core/inference/src/lib.rs +++ b/core/inference/src/lib.rs @@ -761,8 +761,9 @@ fn module_is_import_free(wasm: &[u8]) -> bool { /// - `spec_funcs_by_spec`: WASM function indices that originated from `spec` /// blocks, grouped by spec name (typically obtained from /// [`CodegenOutput::spec_func_indices_by_spec`]). Emitted as per-spec -/// `Definition ___specs : list N` definitions consumed -/// by the corresponding `ValidModule` theorems. Pass an empty `FxHashMap` +/// `Definition ___specs : list assertion` definitions +/// (currently empty, indices carried in a comment) consumed by the +/// corresponding `Valid*Spec` theorems. Pass an empty `FxHashMap` /// when no spec marker is needed. /// /// # Errors diff --git a/core/wasm-codegen/src/compiler.rs b/core/wasm-codegen/src/compiler.rs index f83847b6..8245ccf8 100644 --- a/core/wasm-codegen/src/compiler.rs +++ b/core/wasm-codegen/src/compiler.rs @@ -421,8 +421,8 @@ pub(crate) struct Compiler { /// WASM function indices for functions that originated in `spec` blocks, /// keyed by spec name. Populated during Stage 1 registration in proof mode; /// consumed (moved out) by [`Self::finish_and_take`] so the Rocq translator - /// can emit per-spec `Definition ___specs : list N` - /// definitions. + /// can emit per-spec `Definition ___specs : list assertion` + /// definitions (currently empty, indices carried in a comment). spec_func_indices_by_spec: FxHashMap>, /// Per-spec proof-obligation kinds, parallel to /// [`Self::spec_func_indices_by_spec`] (same key, same order): the i-th kind diff --git a/core/wasm-codegen/src/output.rs b/core/wasm-codegen/src/output.rs index 9aed3a3e..8796d626 100644 --- a/core/wasm-codegen/src/output.rs +++ b/core/wasm-codegen/src/output.rs @@ -83,8 +83,9 @@ pub struct CodegenOutput { /// /// Empty in `compile` mode. In `proof` mode, contains per-spec function /// indices in registration order. The Rocq translator uses this to emit - /// per-spec `Definition ___specs : list N` lists consumed - /// by the corresponding `ValidModule` theorems. + /// per-spec `Definition ___specs : list assertion` lists + /// (currently empty, indices carried in a comment) consumed by the + /// corresponding `Valid*Spec` theorems. spec_func_indices_by_spec: FxHashMap>, /// Per-function shadow-stack frame sizes in bytes, keyed by the structured diff --git a/core/wasm-to-v/ROCQ_CONTRACT.md b/core/wasm-to-v/ROCQ_CONTRACT.md index 43e4b956..d3d99372 100644 --- a/core/wasm-to-v/ROCQ_CONTRACT.md +++ b/core/wasm-to-v/ROCQ_CONTRACT.md @@ -21,40 +21,58 @@ The translator assumes a Rocq context that supplies the following: the proof obligation for the structural well-formedness of the module (typing, locality, validation of the WASM sections themselves). It does **not** mention spec indices. -- A predicate `ValidSpec : module -> list N -> Prop`. **Two arguments**: - the module and a list of WASM function indices, each of which must - hold a property captured by the spec. This is the per-spec verification - obligation. Each `n ∈ idxs` is a WASM function index in module `m`; - holding `ValidSpec m idxs` asserts that, for every such index, the - function at that index satisfies the per-spec invariant supplied by - the consumer's Rocq library. The contract is intentionally generic: - this document fixes the arity (`module → list N → Prop`) and the call +- A type `assertion` (the downstream library's spec-assertion syntax, + defined in its `Assertions` module) — the element type of every emitted + `_specs` list. +- A predicate `ValidSpec : module -> list assertion -> Prop`. **Two + arguments**: the module and a list of spec assertions, each of which + must be witnessed by some function of the module. This is the per-spec + verification obligation. The contract is intentionally generic: this + document fixes the arity (`module → list assertion → Prop`) and the call shape (`Theorem valid___ : ValidSpec ___specs`); - the downstream library defines what the per-spec invariant actually - says about each indexed function. `ValidSpec` is the obligation for - `forall`-quantified and regular spec functions: a **universal** safety - property (the function is trap-free for every input). -- A predicate `ValidExistsSpec : module -> list N -> Prop`, the obligation - for `exists`-quantified spec functions. Same arity and call shape as - `ValidSpec` (`Theorem valid____exists : ValidExistsSpec - ___exists_specs`), but a strictly stronger + the downstream library defines what holding a spec assertion means. + `ValidSpec` is the obligation for `forall`-quantified and regular spec + functions: a **universal** safety property (the witnessing function is + trap-free for every input, reaching the assertion). +- A predicate `ValidExistsSpec : module -> list assertion -> Prop`, the + obligation for `exists`-quantified spec functions. Same arity and call + shape as `ValidSpec` (`Theorem valid_____exists : + ValidExistsSpec ____exists_specs`), but a different property: **existential reachability** — there is an input from which - the function runs to completion without trapping. This is *more than - trap-freedom*; a universal `ValidSpec` does not imply it. -- A predicate `ValidUniqueSpec : module -> list N -> Prop`, the obligation - for `unique`-quantified spec functions (`Theorem - valid____unique : ValidUniqueSpec - ___unique_specs`): existential reachability **plus** that - the witness input is the only non-trapping one. + the witnessing function runs to completion (without trapping) into the + assertion. This is *more than trap-freedom*; a universal `ValidSpec` + does not imply it. +- A predicate `ValidUniqueSpec : module -> list assertion -> Prop`, the + obligation for `unique`-quantified spec functions (`Theorem + valid_____unique : ValidUniqueSpec + ____unique_specs`): existential reachability **plus** + that the witness input is the only non-trapping one. `ValidSpec`/`ValidExistsSpec`/`ValidUniqueSpec` all share the -`module → list N → Prop` arity. `ValidModule` and `ValidSpec` are defined -in the downstream library's `Verifier` module; `ValidExistsSpec` and -`ValidUniqueSpec` in its `Exists` module. The generated file always -`Require Import Verifier`, and additionally `Require Import Exists` when -(and only when) it emits an `exists`/`unique` obligation — so an -all-`forall`/regular program's output is byte-identical to before these -predicates existed. +`module → list assertion → Prop` arity (assertion-valued: wasm-verifier +PR #2 for `ValidSpec`, issue #6 for the existential pair — the former +`module → list N → Prop` index-list forms are gone downstream). +`ValidModule` and `ValidSpec` are defined in the downstream library's +`Verifier` module; `ValidExistsSpec` and `ValidUniqueSpec` in its `Exists` +module; `assertion` in its `Assertions` module. The generated file always +`Require Import Verifier` (and `From Wasm Require Import host`, which +supplies the `host` typeclass behind the always-emitted `Section Host` +wrapper); it additionally `Require Import Assertions` when (and only +when) it emits at least one `_specs` list — so a zero-spec module's +output gains no WasmVerifier imports beyond `Verifier` — and +`Require Import Exists` when (and only when) it emits an +`exists`/`unique` obligation. With these imports the raw artifact +type-checks against the downstream library as-is (checked by replacing +the `Qed` skeletons with `Abort`). + +The translator cannot yet synthesize assertion payloads from spec bodies, +so **every emitted `_specs` list is currently empty** — +`(@nil assertion)` — with the group's WASM function indices preserved in +a preceding comment (`(* function indices: … (assertion payloads +pending) *)`) for the downstream prover, who carries the semantic content +in standalone per-function lemmas (see wasm-verifier's +`examples/E2EQuantKinds.v` for the reference shape). Emitting real +assertion payloads is the next translator milestone. The pre-#21 form `ValidModule : module -> list N -> Prop` is no longer emitted. Downstream proofs that consumed the old 2-argument shape must @@ -71,8 +89,10 @@ indices `[3, 4]` and `[7]` respectively, the generator produces: Definition Foo : module := {| ... |}. -Definition Foo__A_specs : list N := [3; 4]%N. -Definition Foo__B_specs : list N := [7]%N. +(* function indices: 3 4 (assertion payloads pending) *) +Definition Foo__A_specs : list assertion := (@nil assertion). +(* function indices: 7 (assertion payloads pending) *) +Definition Foo__B_specs : list assertion := (@nil assertion). Section Host. Context `{ho: host}. @@ -105,8 +125,10 @@ non-empty group emits its own `_specs` list and theorem: ```coq (* spec Q with a forall fn at index 3 and an exists fn at index 4 *) -Definition Foo__Q_specs : list N := [3]%N. -Definition Foo__Q__exists_specs : list N := [4]%N. +(* function indices: 3 (assertion payloads pending) *) +Definition Foo__Q_specs : list assertion := (@nil assertion). +(* function indices: 4 (assertion payloads pending) *) +Definition Foo__Q__exists_specs : list assertion := (@nil assertion). Theorem valid_Foo__Q : ValidSpec Foo Foo__Q_specs. Theorem valid_Foo__Q__exists : ValidExistsSpec Foo Foo__Q__exists_specs. @@ -119,10 +141,10 @@ and `____unique_specs` / `valid_____unique`. The `__` `__` inside any module or spec name, a kind-suffixed name can never alias another spec's `_specs` list (a plain-`_` form would let a spec literally named `_exists` collide with spec ``'s exists list). A spec -with only `forall`/regular functions emits exactly its prior single -`_specs`/`ValidSpec` pair (byte-identical to pre-quantifier output); a -spec with no functions at all keeps the legacy `_specs := (@nil N)` + -`ValidSpec` shape. The obligation kind is recovered from the +with only `forall`/regular functions emits exactly its single +`_specs`/`ValidSpec` pair; a spec with no functions at all keeps the +legacy `_specs := (@nil assertion)` + `ValidSpec` shape (with no indices +comment). The obligation kind is recovered from the `inference.spec_funcs` section (see below) — the vanilla WASM body no longer carries the quantifier. @@ -146,16 +168,13 @@ Notes: - Spec entries are sorted by spec name. The order is deterministic regardless of how the spec map was assembled (codegen ordering, embedded-section ordering, or caller-supplied ordering). -- Empty per-spec lists are emitted as `(@nil N)` (not `[]%N`) so that - the generated definition type-checks regardless of whether - `Open Scope N_scope` is in effect at the Require site. The `%N` scope - notation depends on `Open Scope N_scope` being active at the consumer's - `Require` site, which the emitter cannot guarantee. `(@nil N)` is the - explicit form and resolves regardless of consumer scope state. This +- Every per-spec list is emitted as `(@nil assertion)` (not `[]` or + `nil`): the explicit form resolves regardless of consumer scope/notation + state at the `Require` site, which the emitter cannot guarantee. This matches the convention used by Coq's own program extraction and - CompCert's AST emission — future contributors should not "modernize" - to `[]%N` because that breaks consumer modules that omit - `Open Scope N_scope`. + CompCert's AST emission (the same rationale that previously mandated + `(@nil N)` over `[]%N`) — future contributors should not "modernize" + to bracket notation. - Spec names are validated against the Rocq identifier rules (see `core/wasm-to-v/src/rocq_names.rs`). A spec named `Definition`, `forall`, or `list` is rejected with `WasmToVError::InvalidRocqIdentifier` @@ -227,6 +246,19 @@ so compile-mode `.wasm` is byte-identical to pre-`spec` output. ## Migration +### `list N` → `list assertion` (assertion-valued specs) + +The `_specs` lists were previously `list N` (WASM function indices). +They are now `list assertion` and emitted empty, with the indices in a +comment. Downstream proofs that destructured the index lists must move +that per-function content into standalone lemmas (wasm-verifier's +`examples/E2EQuantKinds.v` shows the pattern: the emptied obligation is +discharged over `[::]`, the per-function reachability/uniqueness lemmas +stand alone). This tracks wasm-verifier PR #2 (`ValidSpec`) and issue #6 +(`ValidExistsSpec`/`ValidUniqueSpec`). + +### Pre-#21 `ValidModule` (2-argument) + If you previously consumed: ```coq diff --git a/core/wasm-to-v/src/lib.rs b/core/wasm-to-v/src/lib.rs index fd28cf5b..8f404a42 100644 --- a/core/wasm-to-v/src/lib.rs +++ b/core/wasm-to-v/src/lib.rs @@ -299,10 +299,22 @@ mod tests { map.insert("Spec1".to_string(), vec![3, 4, 7]); let output = translate_bytes("Fac", &bytes, &map).expect("translate succeeds"); + // Assertion-valued contract (wasm-verifier PR #2 / issue #6): the list + // is `list assertion`, emitted empty with the indices in a comment. assert!( - output.contains("Definition Fac__Spec1_specs : list N := (3 :: 4 :: 7 :: nil)%N."), + output + .contains("Definition Fac__Spec1_specs : list assertion := (@nil assertion)."), "output should contain Fac__Spec1_specs definition; got:\n{output}", ); + assert!( + output.contains("(* function indices: 3 4 7 (assertion payloads pending) *)"), + "output should carry the spec's function indices in a comment; got:\n{output}", + ); + // `assertion` comes from the Assertions module. + assert!( + output.contains("From WasmVerifier Require Import Assertions."), + "output should import Assertions for the `assertion` type; got:\n{output}", + ); // Structural well-formedness theorem (1-arg ValidModule), always emitted. assert!( output.contains("Theorem valid_Fac : ValidModule Fac."), @@ -330,7 +342,7 @@ mod tests { let output = translate_bytes("Fac", &bytes, &empty).expect("translate succeeds"); assert!( - !output.contains("_specs : list N"), + !output.contains("_specs : list assertion"), "output should contain no per-spec definitions when the map is empty; got:\n{output}", ); // No per-spec ValidSpec theorems when there are no specs. @@ -338,6 +350,11 @@ mod tests { !output.contains("ValidSpec"), "output should contain no ValidSpec theorems when the spec map is empty; got:\n{output}", ); + // Zero-spec artifacts are unchanged: no Assertions import either. + assert!( + !output.contains("From WasmVerifier Require Import Assertions."), + "zero-spec output should not import Assertions; got:\n{output}", + ); // The structural ValidModule theorem is still emitted (contract: a zero-spec module // emits only the module record and `Theorem valid_ : ValidModule `). assert!( diff --git a/core/wasm-to-v/src/translator.rs b/core/wasm-to-v/src/translator.rs index 7ce2b6e4..e12ac946 100644 --- a/core/wasm-to-v/src/translator.rs +++ b/core/wasm-to-v/src/translator.rs @@ -134,7 +134,10 @@ //! From Wasm Require Import bytes. //! From Wasm Require Import numerics. //! From Wasm Require Import datatypes. +//! From Wasm Require Import host. +//! From WasmVerifier Require Import Assertions. (* only when specs are present *) //! From WasmVerifier Require Import Verifier. +//! From WasmVerifier Require Import Exists. (* only when exists/unique specs are present *) //! //! (* Helper definitions *) //! Definition Vi32 i := ... @@ -231,8 +234,11 @@ pub(crate) struct WasmParseData<'a> { pub(crate) function_type_indexes: Vec, pub(crate) function_bodies: Vec>, /// WASM function indices that originated from `spec` blocks, keyed by - /// spec name. Each entry materializes as a `___specs : list N` - /// Rocq definition consumed by the corresponding `ValidModule` theorem. + /// spec name. Each entry materializes as a + /// `___specs : list assertion` Rocq definition (emitted + /// empty, with the indices preserved in a comment, until the translator + /// can synthesize assertion payloads) consumed by the corresponding + /// `Valid*Spec` theorem. pub(crate) spec_funcs_by_spec: FxHashMap>, /// Per-index proof obligations, parallel to [`Self::spec_funcs_by_spec`] @@ -271,25 +277,31 @@ impl SpecKindGroups { } } -/// Emits a `Definition : list N := …` for a group's indices. +/// Emits a `Definition : list assertion := …` for a spec group. /// -/// Empty lists use `(@nil N)` (not `[]%N`) so the definition type-checks -/// regardless of whether `Open Scope N_scope` is in effect at the consumer's -/// `Require` site; non-empty lists use the `(… :: nil)%N` cons form. +/// The downstream contract is **assertion-valued** (`ValidSpec`/ +/// `ValidExistsSpec`/`ValidUniqueSpec : module -> list assertion -> Prop` — +/// wasm-verifier PR #2 for `ValidSpec`, issue #6 for the existential pair). +/// The translator cannot synthesize assertion payloads from spec bodies yet, +/// so every list is emitted **empty** — `(@nil assertion)`, the explicit form +/// that type-checks regardless of consumer scope state (same rationale as the +/// former `(@nil N)`) — and the group's WASM function indices are preserved in +/// a comment for the downstream prover, who carries the semantic content in +/// standalone per-function lemmas (see wasm-verifier's `E2EQuantKinds.v`). fn push_specs_definition(res: &mut String, def_name: &str, indices: &[u32]) { res.push('\n'); - if indices.is_empty() { - res.push_str(format!("Definition {def_name} : list N := (@nil N).\n").as_str()); - } else { + if !indices.is_empty() { let indices_str = indices .iter() .map(u32::to_string) .collect::>() - .join(" :: "); + .join(" "); res.push_str( - format!("Definition {def_name} : list N := ({indices_str} :: nil)%N.\n").as_str(), + format!("(* function indices: {indices_str} (assertion payloads pending) *)\n") + .as_str(), ); } + res.push_str(format!("Definition {def_name} : list assertion := (@nil assertion).\n").as_str()); } /// Emits a `Theorem : .` with the @@ -464,6 +476,17 @@ impl WasmParseData<'_> { res.push_str("From Wasm Require Import bytes.\n"); res.push_str("From Wasm Require Import numerics.\n"); res.push_str("From Wasm Require Import datatypes.\n"); + // The `host` typeclass backs the always-emitted `Section Host. + // Context `{ho: host}.` wrapper around the theorems; without this + // import the raw artifact does not type-check. + res.push_str("From Wasm Require Import host.\n"); + if !spec_groups.is_empty() { + // The `_specs` lists are `list assertion` (assertion-valued + // contract); `assertion` lives in `Assertions`, which `Verifier` + // Requires but does not re-export. Emit it only when a spec is + // present so zero-spec artifacts are unchanged. + res.push_str("From WasmVerifier Require Import Assertions.\n"); + } res.push_str("From WasmVerifier Require Import Verifier.\n"); if needs_exists_import { // `ValidExistsSpec` / `ValidUniqueSpec` live in `Exists` (which @@ -664,21 +687,27 @@ impl WasmParseData<'_> { res.push_str(format!(" mod_exports :=\n{created_exports};\n").as_str()); res.push_str(RCB_DOT); - // Emit per-spec lists of WASM function indices, sorted by spec name for - // deterministic output and split by obligation kind. Spec names were - // validated against the Rocq identifier rules at the top of `translate()` - // so that `___specs` (and the `__exists_specs` / + // Emit per-spec `_specs` lists, sorted by spec name for deterministic + // output and split by obligation kind. Spec names were validated + // against the Rocq identifier rules at the top of `translate()` so + // that `___specs` (and the `__exists_specs` / // `__unique_specs` siblings) are always syntactically legal Rocq // identifiers. // + // The lists are ASSERTION-VALUED (`list assertion`, matching the + // downstream `ValidSpec`/`ValidExistsSpec`/`ValidUniqueSpec : + // module -> list assertion -> Prop` — wasm-verifier PR #2 / issue #6) + // and currently emitted empty, with each group's function indices in a + // comment (see `push_specs_definition`). + // // A spec function's quantifier picks its predicate: `forall`/regular → // `ValidSpec`, `exists` → `ValidExistsSpec`, `unique` → `ValidUniqueSpec` // (the existential predicates assert *reachability*, strictly more than // the universal trap-freedom `ValidSpec` asserts). A spec with no - // functions keeps the legacy single `_specs := (@nil N)` / `ValidSpec` - // shape, and an all-`forall`/regular spec keeps exactly its prior - // `_specs` / `ValidSpec` output — only `exists`/`unique` functions add - // the new sibling definitions and theorems. + // functions keeps the legacy single `_specs` / `ValidSpec` shape, and + // an all-`forall`/regular spec emits only its single `_specs` / + // `ValidSpec` pair — only `exists`/`unique` functions add the sibling + // definitions and theorems. // // The kind is joined with the reserved `__` separator // (`____exists_specs`), not a plain `_`. Because @@ -737,7 +766,7 @@ impl WasmParseData<'_> { res.push_str("Qed.\n"); // Per-spec verification obligations, one theorem per non-empty kind group. // `ValidSpec`/`ValidExistsSpec`/`ValidUniqueSpec` are all 2-argument - // predicates (module, list of WASM function indices) and each entails + // predicates (module, list of spec assertions) and each entails // `ValidModule`. for g in &spec_groups { if g.is_empty() { diff --git a/tests/src/codegen/wasm/extern_link.rs b/tests/src/codegen/wasm/extern_link.rs index e5ce7826..cb00aff4 100644 --- a/tests/src/codegen/wasm/extern_link.rs +++ b/tests/src/codegen/wasm/extern_link.rs @@ -313,10 +313,15 @@ mod extern_link_tests { let empty: FxHashMap> = FxHashMap::default(); let rocq = wasm_to_v("c1prog", &unified, &empty).expect("wasm-to-v succeeds"); - // Post-link indices: add_three=0, check=1, merged sum=2. + // Post-link indices: add_three=0, check=1, merged sum=2. The list is + // assertion-valued (empty); the post-link index survives in the comment. assert!( - rocq.contains("Definition c1prog__MySpec_specs : list N := (1 :: nil)%N."), - "MySpec_specs must name `check` at post-link index 1, not the merged \ + rocq.contains("Definition c1prog__MySpec_specs : list assertion := (@nil assertion)."), + "MySpec_specs definition missing; .v was:\n{rocq}" + ); + assert!( + rocq.contains("(* function indices: 1 (assertion payloads pending) *)"), + "MySpec's comment must name `check` at post-link index 1, not the merged \ extern at 2; .v was:\n{rocq}" ); } diff --git a/tests/src/spec_propagation.rs b/tests/src/spec_propagation.rs index e33454b1..4fd3d32c 100644 --- a/tests/src/spec_propagation.rs +++ b/tests/src/spec_propagation.rs @@ -6,7 +6,7 @@ //! 2. Export gating //! 3. Custom WASM section round-trip //! 4. Per-spec emission ordering and theorems -//! 5. Empty list `(@nil N)` +//! 5. Empty list `(@nil assertion)` //! 6. Invalid module names //! 7. No regressions (verified out-of-band via `cargo test`) //! 8. Compile-mode emits no spec section @@ -553,17 +553,26 @@ mod scenario_4_per_spec_emission { // mod_name argument is overridden by the embedded "output" module name. let v = inference::wasm_to_v("M", output.wasm(), &map).expect("translate ok"); assert!( - v.contains("Definition output__A_specs : list N := (0 :: nil)%N."), + v.contains("Definition output__A_specs : list assertion := (@nil assertion)."), "A def:\n{v}" ); assert!( - v.contains("Definition output__B_specs : list N := (1 :: nil)%N."), + v.contains("Definition output__B_specs : list assertion := (@nil assertion)."), "B def:\n{v}" ); + // The indices survive as comments (one per spec, sorted A then B). + assert!( + v.contains("(* function indices: 0 (assertion payloads pending) *)"), + "A indices comment:\n{v}" + ); + assert!( + v.contains("(* function indices: 1 (assertion payloads pending) *)"), + "B indices comment:\n{v}" + ); } } -// Scenario 5: Empty list `(@nil N)` +// Scenario 5: Empty list `(@nil assertion)` #[cfg(test)] mod scenario_5_empty_list { use super::helpers::compile; @@ -571,7 +580,7 @@ mod scenario_5_empty_list { use rustc_hash::FxHashMap; /// When the spec map is empty, the translator must emit no `_specs` line - /// at all (no per-spec definition). The `(@nil N)` literal is only relevant + /// at all (no per-spec definition). The `(@nil assertion)` literal is only relevant /// once a spec exists but has no surviving inner functions; the current /// emission strategy is to skip `Definition` lines entirely when the map /// is empty. @@ -587,7 +596,7 @@ mod scenario_5_empty_list { let empty: FxHashMap> = FxHashMap::default(); let v = inference::wasm_to_v("Empty", output.wasm(), &empty).expect("translate ok"); assert!( - !v.contains("_specs : list N"), + !v.contains("_specs : list assertion"), "no per-spec definitions expected when map is empty:\n{v}" ); assert!( @@ -600,8 +609,8 @@ mod scenario_5_empty_list { ); } - /// `(@nil N)` is emitted when an explicit spec is present but its indices - /// list is empty. Asserts that NO `[]%N` substring leaks through. + /// `(@nil assertion)` is emitted when an explicit spec is present but its + /// indices list is empty. Asserts that NO `[]%N` substring leaks through. #[test] fn explicit_spec_with_empty_indices_emits_at_nil_n_not_bracket_pct_n() { let source = r#"pub fn main() -> i32 { return 0; }"#; @@ -612,8 +621,8 @@ mod scenario_5_empty_list { map.insert("MySpec".to_string(), Vec::new()); let v = inference::wasm_to_v("Mod", output.wasm(), &map).expect("translate ok"); assert!( - v.contains("(@nil N)"), - "expected `(@nil N)` for empty spec indices list:\n{v}" + v.contains("(@nil assertion)"), + "expected `(@nil assertion)` for empty spec indices list:\n{v}" ); assert_eq!( v.matches("[]%N").count(), @@ -1248,7 +1257,8 @@ mod scenario_7_empty_spec { /// A user-authored empty `spec MySpec { }` must surface a per-spec entry /// with an empty index list, so the Rocq translator still emits both a - /// `Definition output__MySpec_specs : list N := (@nil N).` line and a + /// `Definition output__MySpec_specs : list assertion := (@nil assertion).` + /// line and a /// `Theorem valid_output__MySpec : ValidSpec output output__MySpec_specs.` /// theorem. Without `ensure_spec_registered`, the spec vanished silently /// from the proof artifact because the bucket iteration only recorded @@ -1272,8 +1282,12 @@ mod scenario_7_empty_spec { let empty: FxHashMap> = FxHashMap::default(); let v = inference::wasm_to_v("Mod", output.wasm(), &empty).expect("translate ok"); assert!( - v.contains("Definition output__MySpec_specs : list N := (@nil N)."), - "empty spec must emit the `(@nil N)` definition line:\n{v}" + v.contains("Definition output__MySpec_specs : list assertion := (@nil assertion)."), + "empty spec must emit the `(@nil assertion)` definition line:\n{v}" + ); + assert!( + !v.contains("(* function indices:"), + "an empty spec has no indices to carry in a comment:\n{v}" ); assert!( v.contains("Theorem valid_output__MySpec : ValidSpec output output__MySpec_specs."), @@ -1281,10 +1295,11 @@ mod scenario_7_empty_spec { ); } - /// T1: mixing an empty spec with a non-empty one must produce both kinds - /// of `Definition` line in the generated Rocq output, in alphabetical - /// order. The empty list renders as `(@nil N)`, the non-empty as - /// `(idx :: nil)%N`. This guards a regression where empty-spec handling could + /// T1: mixing an empty spec with a non-empty one must produce both + /// `Definition` lines in the generated Rocq output, in alphabetical + /// order. Both lists render as `(@nil assertion)` (assertion payloads + /// pending); the non-empty one additionally carries its indices in a + /// comment. This guards a regression where empty-spec handling could /// short-circuit the per-spec emission loop and drop the non-empty entry /// (or vice versa). #[test] @@ -1306,13 +1321,18 @@ mod scenario_7_empty_spec { let empty: FxHashMap> = FxHashMap::default(); let v = inference::wasm_to_v("Mod", output.wasm(), &empty).expect("translate ok"); assert!( - v.contains("Definition output__A_specs : list N := (@nil N)."), - "empty spec A must render `(@nil N)`:\n{v}" + v.contains("Definition output__A_specs : list assertion := (@nil assertion)."), + "empty spec A must render `(@nil assertion)`:\n{v}" + ); + assert!( + v.contains("Definition output__B_specs : list assertion := (@nil assertion)."), + "non-empty spec B must render `(@nil assertion)` too:\n{v}" ); - let expected_b = format!("Definition output__B_specs : list N := ({b_idx} :: nil)%N."); + let expected_b_comment = + format!("(* function indices: {b_idx} (assertion payloads pending) *)"); assert!( - v.contains(&expected_b), - "non-empty spec B must render `({b_idx} :: nil)%N`:\n{v}" + v.contains(&expected_b_comment), + "non-empty spec B must carry its index in a comment:\n{v}" ); let pos_a = v.find("Definition output__A_specs").unwrap(); let pos_b = v.find("Definition output__B_specs").unwrap(); @@ -1430,7 +1450,7 @@ mod scenario_8_compile_mode_no_section { let empty: FxHashMap> = FxHashMap::default(); let v = inference::wasm_to_v("Mod", output.wasm(), &empty).expect("translate ok"); assert_eq!( - v.matches("_specs : list N").count(), + v.matches("_specs : list assertion").count(), 0, "compile-mode .v output must contain zero per-spec definitions:\n{v}", ); @@ -1514,7 +1534,7 @@ mod scenario_10_wasm_to_v_compile_mode { // No per-spec definition or ValidSpec lines. assert_eq!( - v.matches("_specs : list N").count(), + v.matches("_specs : list assertion").count(), 0, "no per-spec definitions expected:\n{v}" ); diff --git a/tests/src/spec_propagation_inf.rs b/tests/src/spec_propagation_inf.rs index 03fa7340..e1d3b5ab 100644 --- a/tests/src/spec_propagation_inf.rs +++ b/tests/src/spec_propagation_inf.rs @@ -188,12 +188,17 @@ mod fixture_spec_calls_top { "top-level main must also call helper at 0; observed: {main_call_target}" ); - // Round-trip must emit Caller's per-spec list with exactly one index. + // Round-trip must emit Caller's per-spec list (assertion-valued, empty) + // with exactly index 2 carried in the comment. let empty: FxHashMap> = FxHashMap::default(); let v = inference::wasm_to_v("Ignored", wasm, &empty).expect("translate ok"); assert!( - v.contains("Definition calltop__Caller_specs : list N := (2 :: nil)%N."), - "Caller_specs should list exactly index 2:\n{v}" + v.contains("Definition calltop__Caller_specs : list assertion := (@nil assertion)."), + "Caller_specs definition missing:\n{v}" + ); + assert!( + v.contains("(* function indices: 2 (assertion payloads pending) *)"), + "Caller_specs should carry exactly index 2 in its comment:\n{v}" ); } } @@ -248,11 +253,12 @@ mod fixture_three_specs { "definitions must be emitted alphabetically (Alpha < Beta < Gamma):\n{v}" ); - // The empty spec is emitted with `(@nil N)` (NOT `[]%N`); this is - // load-bearing for consumer modules without `Open Scope N_scope`. + // The empty spec is emitted with `(@nil assertion)` (NOT `[]`); the + // explicit form is load-bearing for consumer modules regardless of + // scope state (same rationale as the former `(@nil N)`). assert!( - v.contains("Definition threespecs__Gamma_specs : list N := (@nil N)."), - "empty spec must emit `(@nil N)`:\n{v}" + v.contains("Definition threespecs__Gamma_specs : list assertion := (@nil assertion)."), + "empty spec must emit `(@nil assertion)`:\n{v}" ); // The structural well-formedness theorem is emitted once. @@ -411,8 +417,12 @@ mod fixture_spec_const_e2e { "spec function body must push the constant 42:\n{v}" ); assert!( - v.contains("Definition spec_const__Answer_specs : list N := (1 :: nil)%N."), - "per-spec index list must be [1]:\n{v}" + v.contains("Definition spec_const__Answer_specs : list assertion := (@nil assertion)."), + "per-spec assertion list (empty, payloads pending) must be emitted:\n{v}" + ); + assert!( + v.contains("(* function indices: 1 (assertion payloads pending) *)"), + "per-spec index comment must carry index 1:\n{v}" ); // Post-#21 contract: 1-arg ValidModule + 2-arg ValidSpec. assert!( @@ -662,8 +672,8 @@ mod fixture_quant_kinds_e2e { "exists spec must select ValidExistsSpec:\n{v}" ); assert!( - v.contains("Definition quant_kinds__ExistsSpec__exists_specs : list N :="), - "exists spec must emit its __exists_specs list:\n{v}" + v.contains("Definition quant_kinds__ExistsSpec__exists_specs : list assertion :="), + "exists spec must emit its (assertion-valued) __exists_specs list:\n{v}" ); assert!( !v.contains("Theorem valid_quant_kinds__ExistsSpec :"), @@ -732,11 +742,11 @@ mod fixture_spec_name_collision_e2e { // Both the kind-suffixed name (spec Foo's exists group) and the // similarly-named spec's plain name are present and DISTINCT. assert!( - v.contains("Definition collide__Foo__exists_specs : list N :="), + v.contains("Definition collide__Foo__exists_specs : list assertion :="), "spec Foo's exists group uses the __ separator:\n{v}" ); assert!( - v.contains("Definition collide__Foo_exists_specs : list N :="), + v.contains("Definition collide__Foo_exists_specs : list assertion :="), "spec Foo_exists's plain spec list is unaffected:\n{v}" );