Reject a specification function whose obligation says nothing (#356)

[0xGeorgii]

Closes #356.

The problem

A spec function whose body computes instead of asserting contributed a vacuous obligation with no diagnostic:

spec Caller {
  fn caller() -> i32 {
    return helper();
  }
}

emitted Definition ..._hspec1 : hassert := HA_true. The semantic content ("caller equals helper") was dropped, the theorem was trivially provable, and the user got a green Qed with zero verification content and no warning.

The fix

New fatal proof-mode diagnostic P010.

The issue named three paths (Stmt::Return, the empty contribution list, plain spec methods). There are at least twelve. Because HAssert::and/imp/or/ex all absorb the identity (core/hassert/src/ir.rs:143-179), every one of them collapses to exactly HAssert::True, so the predicate is a single equality on the value translate_fn returns — no shape enumeration to keep in sync.

That distinction is load-bearing. Two shapes look like they contribute and do not:

• a trailing assume block, where the fold is Imp(p, ⊤) = ⊤
• an if whose branches are all vacuous

A body-shape check would pass both. Checking the translated result catches the whole family.

P010 is raised after the existing P001–P008 early-continue, so it never stacks on a function that already reported. Its wording is keyed on what the body claimed, via a new claim.rs scan that picks the message only — it never decides whether an obligation is emitted, so a mistake there can mis-word a diagnostic but cannot drop a claim.

P009 widened

A plain (Regular) spec method that states a real property was dropped with neither an entry nor a diagnostic — worse than the HA_true this fixes, and the escape hatch that made a function-only rule falsifiable. It now raises P009. A method that only computes stays a silent helper, since a method produces no obligation either way.

Consequences

A computing helper can no longer live inside a spec block; it belongs at file scope, where a spec function still applies it as a T_app. Compile mode is unaffected (it has no obligations), and any spec function that already stated a property emits byte-identical output.

Known asymmetry, stated in the CHANGELOG rather than quietly widened: spec S { fn h() -> i32 { return 1; } } is rejected, but the same helper wrapped in a spec-inner struct still compiles, because a spec method keeps its helper exemption.

Evidence in committed artifacts

Artifact	Before	After
tests/test_data/rocq/spec_literal_ctx.v	hspec1 := HA_true.	a real T_app 2 obligation against Vi64 4294967296
proof_specs.wasm hspecs section	106 B, two 0x00 (⊤) trees	165 B, two real trees

A fixture that was not testing what it claimed

spec_narrow_uzumaki.inf exists to cover narrow-width HA_has_type slot guards. All three of its functions bound slots and never asserted, so the translator dropped every guard and all 3/3 obligations were HA_true — that coverage had never reached the printer or coqc. It now asserts through file-scope identity helpers, and the guards emit for real: T_i32 for u8/i8/u16/i16/bool/enum, T_i64 for i64/u64.

HA_true also becomes unreachable from any source program, so every_stub_declaration_has_a_producer grows a hand-built producer for it rather than an exemption — an exemption claims a producer is impossible, and here one is possible.

Verification

• cargo test --workspace --no-fail-fast: 5821 passed, 0 failed, 68 binaries
• coqc (Rocq 9.2) genuinely ran; no gate reported a skip
• The issue's exact example exits 1 with the P010 diagnostic and writes no artifacts; the same source still exits 0 in compile mode
• Every tests/test_data/inf/*.inf verified P010-clean end to end
• cargo clippy -p inference-wasm-codegen --all-targets -- -D warnings clean

New coverage

core/wasm-codegen/src/hassert/tests.rs gains a section with 13 tests: every verified vacuity path, message-wording pins per claim variant, and negative controls — a real obligation is kept, a bare call statement is a genuine HA_app_ok and not vacuous, P010 does not stack on P002/P004, and a vacuous sibling does not take a real obligation down with it.

Note for reviewers

T_app on a spec-local helper still cannot round-trip the full infc -v pipeline (#390 — spec bodies are omitted from the .v module record). That is pre-existing and unrelated, but it is why the sibling-call test drives the translation pass directly rather than compiling.

Confidence Score: 4/5

The PR is not yet safe to merge because an existential-mode conditional with vacuous branches still bypasses P010 and emits a verification-free tautology.

The structural equality check catches literal HA_true, but existential conditional translation can produce the logically true, non-canonical form Or(nz(cond), eqz(cond)), so the previously reported vacuous-obligation path remains reachable.

Files Needing Attention: core/wasm-codegen/src/hassert/mod.rs and core/wasm-codegen/src/hassert/translate.rs

Important Files Changed

Filename	Overview
core/wasm-codegen/src/hassert/mod.rs	Adds P010 rejection and revised P009 dispatch while retaining the structural HAssert::True predicate.
core/wasm-codegen/src/hassert/claim.rs	Separates diagnostic wording from recursive assertion detection, fixing false P009 reports for property-less nondeterministic blocks.
core/wasm-codegen/src/hassert/tests.rs	Adds broad vacuity and method-classification regression coverage.
core/wasm-codegen/src/hassert/diag.rs	Registers P010 and updates the documented P009 scope.
core/wasm-to-v/ROCQ_CONTRACT.md	Documents the revised proof-obligation and diagnostic contract.

Flowchart

%%{init: {'theme': 'neutral'}}%%
flowchart TD
  A[Translate spec function] --> B{Earlier P001-P008 diagnostics?}
  B -- Yes --> C[Record diagnostics; emit no obligation]
  B -- No --> D{Translated result equals HA_true?}
  D -- Yes --> E[Record P010; emit no obligation]
  D -- No --> F[Emit hassert obligation]
  G[Inspect spec method] --> H{Quantified or contains assert?}
  H -- Yes --> I[Record P009]
  H -- No --> J[Keep silent helper exemption]

Loading

_{Reviews (2): Last reviewed commit: "Report a spec method only when an assert..." | Re-trigger Greptile}

Context used (3)

• Knowledge Base — WASM Codegen and Linker
• Knowledge Base — WASM-to-V: Translating Compiled WASM into Rocq Proof Obligations
• Knowledge Base — Test Suite: Integration Fixtures and Fuzzing

[codecov]

Codecov Report

❌ Patch coverage is 94.93671% with 4 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
core/wasm-codegen/src/hassert/claim.rs	92.50%	3 Missing ⚠️
core/wasm-codegen/src/hassert/mod.rs	97.36%	1 Missing ⚠️

📢 Thoughts on this report? Let us know!