Problem
Draft PR #235 (feat/wasm-verifier-e2e, 5 commits, based 62 commits behind main) carries the pre-hassert proof-pipeline design: scalar+aggregate @->synthetic-parameter lowering, quantifier-wrapper suppression, inference.spec_funcs wire-v2 kind bytes, assertion-valued _specs emission. The #299 hassert pipeline on main supersedes its emission approach (spec functions omitted from the module; obligations as hassert payloads; spec bodies never verified operationally downstream), and wasm-verifier's CLAUDE.md still documents the branch design as current (being fixed downstream).
Undecided pieces worth an explicit disposition rather than silent rot:
- @->parameter lowering: obsolete under the hassert regime (spec bodies aren't run downstream)? Or still wanted so proof-mode spec bodies are standard wasm (today they carry custom 0xfc opcodes — the proof-mode
.wasm fails stock wasm-tools validate; the compile-mode artifact is clean because specs are stripped, wasm-codegen/src/lib.rs:779-819)?
- kind bytes: the exists/unique kind channel will be re-needed (P001-lift issue) — harvest the v2 codec design or redesign on hspecs?
- aggregate-@ leaf enumeration (
uzumaki_leaf_valtypes etc.): prior art for the hassert aggregate-@ extension.
Work
Decide per piece: harvest into a fresh PR, re-scope, or close #235 + delete the branch; record the decision in ROCQ_CONTRACT.md. (Recommendation from the audit: close the PR, keep the branch tip tagged for reference, harvest the leaf-enumeration + kind-codec designs into the new issues.)
References: PR #235; P001-lift issue; aggregate-hassert issue. Provenance: cross-repo audit 2026-08-08; branch state verified via git merge-base.
Related: the exists/unique kind channel is re-designed in the P001-lift issue; aggregate leaf enumeration feeds the hassert-expressiveness issue. Verifier-side doc fix: Inference-Global-Software/wasm-verifier#27.
Problem
Draft PR #235 (
feat/wasm-verifier-e2e, 5 commits, based 62 commits behind main) carries the pre-hassert proof-pipeline design: scalar+aggregate@->synthetic-parameter lowering, quantifier-wrapper suppression,inference.spec_funcswire-v2 kind bytes, assertion-valued_specsemission. The #299 hassert pipeline on main supersedes its emission approach (spec functions omitted from the module; obligations as hassert payloads; spec bodies never verified operationally downstream), and wasm-verifier's CLAUDE.md still documents the branch design as current (being fixed downstream).Undecided pieces worth an explicit disposition rather than silent rot:
.wasmfails stockwasm-tools validate; the compile-mode artifact is clean because specs are stripped,wasm-codegen/src/lib.rs:779-819)?uzumaki_leaf_valtypesetc.): prior art for the hassert aggregate-@ extension.Work
Decide per piece: harvest into a fresh PR, re-scope, or close #235 + delete the branch; record the decision in ROCQ_CONTRACT.md. (Recommendation from the audit: close the PR, keep the branch tip tagged for reference, harvest the leaf-enumeration + kind-codec designs into the new issues.)
References: PR #235; P001-lift issue; aggregate-hassert issue. Provenance: cross-repo audit 2026-08-08; branch state verified via git merge-base.
Related: the exists/unique kind channel is re-designed in the P001-lift issue; aggregate leaf enumeration feeds the hassert-expressiveness issue. Verifier-side doc fix: Inference-Global-Software/wasm-verifier#27.