Skip to main content

Module falsifiers

Module falsifiers 

Source
Expand description

GREEN contract falsifiers for the apr-format extraction (issue #2231).

One #[test] per proof obligation in contracts/apr-format-extraction-v1.yaml + the companion apr-format-leaf-sovereignty-v1.yaml, named exactly as those contracts’ falsification_tests[].test fields cite them so pv lint Gate-4 / strict-test-binding resolves the refs with no dangling-ref errors.

Stage 1 shipped these as RED unimplemented! stubs (the obligation existed before the implementation). Stage 2 discharges them against the real bytes: the golden byte-identity oracle, the cargo metadata dependency closure, the CRC known-answer + golden trailer, the metadata round-trip, and the Jidoka quality gate. A falsifier going RED here means its obligation regressed.

§f16 scoping note (issue #2231 / PMAT-905 class)

Byte-identity is asserted for F32 payloads only. The golden fixtures use F32 weights, so they are unaffected by the documented f16 write change (the leaf now uses IEEE round-to-nearest-even via the half crate instead of the legacy non-RNE trueno::f32_to_f16). See crate::f16.