Why
The prover pipeline now pins infc to d2a2ec4353042959912f2c64e566929ab112a7a2 because the latest published release, v0.0.5 (2d274505c47e10d4a98d23b4761a5a3d5483bc68), emits the retired Rocq contract:
From Wasm Require Import ... verifier
list N spec payloads
- two-argument
ValidModule
That output fails against the deployed wasm-verifier library before obligations can be processed. The pinned source build emits the current WasmVerifier imports, hassert payloads with type guards, ValidModule/1, and ValidSpec/2.
Both the release and current source builds still print infc 0.0.1, so infc --version cannot identify which contract a binary emits. --commit-hash is the only usable discriminator today.
Tracking prover-side integration: Inferara/inference-ai-prover#57.
Request
Please cut a release from compiler main at or after d2a2ec4353042959912f2c64e566929ab112a7a2 before 2026-10-11, and make the release binary report a distinguishable version.
Acceptance
- A tagged release newer than
v0.0.5 contains the current wasm-verifier emitter.
infc --version reports that release version rather than 0.0.1.
- The released binary reports the release commit through
infc --commit-hash.
- Proof-mode output for
tests/test_data/inf/with_spec.inf matches the current contract and its all-Admitted. form compiles against wasm-verifier@0bbf9b723da5478c9df1b3a4f0d787e35e37f6b9.
Why
The prover pipeline now pins
infctod2a2ec4353042959912f2c64e566929ab112a7a2because the latest published release,v0.0.5(2d274505c47e10d4a98d23b4761a5a3d5483bc68), emits the retired Rocq contract:From Wasm Require Import ... verifierlist Nspec payloadsValidModuleThat output fails against the deployed wasm-verifier library before obligations can be processed. The pinned source build emits the current
WasmVerifierimports, hassert payloads with type guards,ValidModule/1, andValidSpec/2.Both the release and current source builds still print
infc 0.0.1, soinfc --versioncannot identify which contract a binary emits.--commit-hashis the only usable discriminator today.Tracking prover-side integration: Inferara/inference-ai-prover#57.
Request
Please cut a release from compiler main at or after
d2a2ec4353042959912f2c64e566929ab112a7a2before 2026-10-11, and make the release binary report a distinguishable version.Acceptance
v0.0.5contains the current wasm-verifier emitter.infc --versionreports that release version rather than0.0.1.infc --commit-hash.tests/test_data/inf/with_spec.infmatches the current contract and its all-Admitted.form compiles againstwasm-verifier@0bbf9b723da5478c9df1b3a4f0d787e35e37f6b9.