Reporting this as a consumer who hit it while trying to discharge a downstream zero-coverage-gap object-code-verification obligation (gale T2 / REQ-OS-OBJVERIFY-001). It is disclosed in your source rather than hidden — the issue is that it turns out to be load-bearing for someone downstream.
The two halves don't meet on i32.const
synth verify (per-rule SMT, ASIL-D path) explicitly declines Const/Local operations:
No verifiable computational rules for this function.
(LocalGet/Set/Const are register operations, not verified by SMT)
That is a reasonable split — it defers those to the per-rule Rocq obligations. And three of the four deferred-to theorems are closed:
| theorem |
status |
local_get_correct |
Qed |
local_set_correct |
Qed |
local_tee_correct |
Qed |
i64_const_correct |
Qed |
i32_const_correct |
Admitted |
So for i32.const, SMT skips it and the rule proof is open. Neither half covers it.
It is false as stated, and the content is already proven
Proof.
(* See the T3 rationale above: false in the large branch for un-normalized
[n]; the reconstruction arithmetic itself is proven in
[i32_const_large_reconstruct]. *)
Admitted.Both supporting lemmas are closed:
i32_const_large_reconstruct — Qedmovw_movt_reconstruct_Z — Qed
So this isn't missing mathematics. The theorem statement quantifies over un-normalized n where it doesn't hold.
The fix pattern is in the same file
CorrectnessI64.v records that i64_add_correct/i64_sub_correct were Admitted in v0.9.0 and got discharged, and i64_const_correct is now closed by restating it dual-register with result-equation axioms (i64_const_lo_spec / i64_const_hi_spec). The i32 twin looks like it just never got the same treatment.
Ask: restate i32_const_correct with the normalization precondition (or split small/large branches the way the i64 version splits registers) so it can be discharged from the two lemmas that are already Qed.
Why it matters downstream
On our dissolved OS object (the whole gust:os composite lowered through meld → loom → synth):
- 473
i32.const occurrences
- 34 of 67 functions contain at least one
- BIN-VERIFY: 23/23 functions run, 24 rules verified, 0 failed, 0 unknown, plus 20 LRAT-certified I64 expansions — genuinely clean everywhere else
Our obligation's kill-criterion is literally "any applied codegen rule on this object lacks a RULE-VERIFY obligation". Everything else on that object passes; this one instruction is what stands between us and the claim. Closing it would make an ASIL-D-path zero-gap statement possible on a real object.
Related: #242 (VCR epic) covers this area broadly, but nothing tracks this specific admit.
Happy to test a candidate — we have a reproducible object and the verify-enabled build wired up.
Reporting this as a consumer who hit it while trying to discharge a downstream zero-coverage-gap object-code-verification obligation (gale T2 /
REQ-OS-OBJVERIFY-001). It is disclosed in your source rather than hidden — the issue is that it turns out to be load-bearing for someone downstream.The two halves don't meet on
i32.constsynth verify(per-rule SMT, ASIL-D path) explicitly declines Const/Local operations:That is a reasonable split — it defers those to the per-rule Rocq obligations. And three of the four deferred-to theorems are closed:
local_get_correctlocal_set_correctlocal_tee_correcti64_const_correcti32_const_correctSo for
i32.const, SMT skips it and the rule proof is open. Neither half covers it.It is false as stated, and the content is already proven
Both supporting lemmas are closed:
i32_const_large_reconstruct— Qedmovw_movt_reconstruct_Z— QedSo this isn't missing mathematics. The theorem statement quantifies over un-normalized
nwhere it doesn't hold.The fix pattern is in the same file
CorrectnessI64.vrecords thati64_add_correct/i64_sub_correctwere Admitted in v0.9.0 and got discharged, andi64_const_correctis now closed by restating it dual-register with result-equation axioms (i64_const_lo_spec/i64_const_hi_spec). The i32 twin looks like it just never got the same treatment.Ask: restate
i32_const_correctwith the normalization precondition (or split small/large branches the way the i64 version splits registers) so it can be discharged from the two lemmas that are already Qed.Why it matters downstream
On our dissolved OS object (the whole
gust:oscomposite lowered through meld → loom → synth):i32.constoccurrencesOur obligation's kill-criterion is literally "any applied codegen rule on this object lacks a RULE-VERIFY obligation". Everything else on that object passes; this one instruction is what stands between us and the claim. Closing it would make an ASIL-D-path zero-gap statement possible on a real object.
Related: #242 (VCR epic) covers this area broadly, but nothing tracks this specific admit.
Happy to test a candidate — we have a reproducible object and the verify-enabled build wired up.