Feat/wasm verifier e2e#235
Draft
0xGeorgii wants to merge 5 commits into
Draft
Conversation
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_<mod> : ValidModule <mod>.` always (even for zero-spec modules). - Emit per-spec obligations with the 2-arg `ValidSpec`: `Theorem valid_<mod>__<Spec> : ValidSpec <mod> <mod>__<Spec>_specs.` (was the pre-#21 2-arg `ValidModule <mod> <mod>__<Spec>_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) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0162V1zxr9wVSwNFXuZiF46U
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) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0162V1zxr9wVSwNFXuZiF46U
…sue #6) 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 <mod>__<S>_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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Ev6Ch1XeDGdSCJbuzjDxuP
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.