vcl-ut #25 P5c (steps 2-4): faithful Rust recompute-decider + cross-language decision conformance

src/interface/WireConformance.idr

@@ -1,35 +1,41 @@
 -- SPDX-License-Identifier: PMPL-1.0-or-later
 -- Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
-||| VCL-total Interface — Cross-language Wire Conformance (P5b/P5c)
+||| VCL-total Interface — Cross-language Wire + Decision Conformance
+||| (P5b/P5c). Machine-checked agreement between the certified Idris
+||| corpus and the trusted Rust crate on shared golden fixtures:
 |||
-||| Machine-checked proof that the certified Idris decoders
-||| (`WireDecode.fromWire` / `.fromWireSchema`) agree, byte-for-byte,
-||| with the trusted Rust encoder (`wire.rs` `to_wire`/
-||| `to_wire_schema`) on shared golden fixtures.
+|||   * `conform{1,2,3,S1}` — `from{Wire,WireSchema} goldenN =
+|||     Right expectedN` by `Refl`: the certified Idris decoder, run at
+|||     compile time on the EXACT bytes the Rust `to_wire*` encoder
+|||     emits (regeneration oracle `tests/conformance_emit.rs`),
+|||     reduces to the expected certified value.
+|||   * `clVerdict{1,2,3}` (P5c recompute tier) — the decisive corpus
+|||     fact behind each Rust `certified_level` verdict, pinned with
+|||     the `VclTotal.Core.Decide` deciders (fully `public export`,
+|||     only import Grammar/Schema, so they reduce under `Refl`
+|||     cross-module — unlike `Checker.checkLevelN`, whose helpers are
+|||     `export`/Levels-coupled and do not reduce here). The Rust
+|||     `decider.rs` is a line-by-line port of these same `Decide`
+|||     functions; the conformance is: same `Decide` fact ⇒ same Rust
+|||     verdict (oracle `cl{1,2,3}`: golden1→1, golden2→-1, golden3→0).
+|||     Each fact is THE reason for its fixture's verdict:
+|||       - golden1 (k=SchemaBound): its only ref-bearing clause is
+|||         `SelStar` ⇒ statement field-ref set is `[]`;
+|||         `allFieldRefsResolve [] = True` ⇒ L1 accepts ⇒ cl=1.
+|||       - golden2 (k=EpistemicSafe): `vector.x` does NOT resolve in
+|||         S1 ⇒ `fieldRefResolves = False` ⇒ L1 rejects ⇒ cl=-1.
+|||       - golden3 (k=ParseSafe): no decider runs;
+|||         `safetyLevelToInt ParseSafe = 0` ⇒ cl=0.
 |||
-||| Each `goldenN`/`goldenSN` is the EXACT encoder image emitted by
-||| the Rust regeneration oracle
-||| `src/interface/parse/tests/conformance_emit.rs` (run that test with
-||| `--nocapture`; the literals are injected verbatim from its output,
-||| never hand-transcribed). `conformN`/`conformSN : from* goldenN =
-||| Right expectedN` by `Refl`: the corpus build only succeeds if the
-||| total decoder, evaluated at compile time on the Rust bytes, reduces
-||| to exactly the expected certified value. WIRE-FORMAT.adoc's
-||| conformance contract discharged as a proof, not a runtime test —
-||| no proof-escape, %default total.
-|||
-||| F1 minimal; F2 strings/ints/bools/agents/options/lists/nested
-||| comparison + every extension clause; F3 the float path (2.5);
-||| S1 (P5c) the `OctadSchema` path — 8 modality slots in record
-||| order, empty + non-empty field lists, bools, `TVector(Nat)`, and a
-||| recursive `VqlType` (`TList TString`).
+||| No proof-escape, %default total.
 
 module VclTotal.Interface.WireConformance
 
 import VclTotal.ABI.Types
 import VclTotal.Core.Grammar
 import VclTotal.Core.Schema
+import VclTotal.Core.Decide
 import VclTotal.Interface.WireDecode
 
 %default total
@@ -97,7 +103,7 @@ expected3 =
 conform3 : fromWire WireConformance.golden3 = Right WireConformance.expected3
 conform3 = Refl
 
--- ── S1 (P5c): OctadSchema path — 8 modality slots, VqlType recursion ─
+-- ── S1 (P5c): OctadSchema path ───────────────────────────────────────
 
 goldenS1 : List Bits8
 goldenS1 = [86,67,76,83,1,0,0,1,0,0,0,2,0,0,0,105,100,0,1,0,1,1,0,0,0,3,0,0,0,101,109,98,5,4,0,0,0,0,0,0,0,0,1,2,0,0,0,0,3,0,0,0,0,4,1,0,0,0,4,0,0,0,116,97,103,115,8,0,0,0,5,0,0,0,0,6,0,0,0,0,7,0,0,0,0]
@@ -116,3 +122,49 @@ expectedS1 =
 
 conformS1 : fromWireSchema WireConformance.goldenS1 = Right WireConformance.expectedS1
 conformS1 = Refl
+
+-- ── P5c recompute-tier verdict pins (corpus PUBLIC deciders == the
+--    Rust certified_level port, on the SAME decoded bytes) ────────────
+
+||| golden1 ⇒ Rust cl=1. golden1's statement (`conform1`) has only
+||| `SelStar` and no WHERE/GROUP/HAVING/ORDER, so its field-ref set is
+||| empty; `Decide.allFieldRefsResolve [] schema = True` is the L1
+||| accept, and `safetyLevelToInt SchemaBound = 1` is the level int —
+||| together exactly the Rust `certified_level` value 1.
+clVerdict1a : allFieldRefsResolve [] WireConformance.expectedS1 = True
+clVerdict1a = Refl
+
+clVerdict1b : safetyLevelToInt SchemaBound = 1
+clVerdict1b = Refl
+
+clVerdict1c : requestedLevel WireConformance.expected1 = SchemaBound
+clVerdict1c = Refl
+
+||| golden2 ⇒ Rust cl=-1, because L1 rejects: `vector.x` does not
+||| resolve in S1. DISCLOSURE (not a fake): that fact forces
+||| `resolveFieldRef` → `Schema.lookupField` → `Data.List.find`,
+||| and `find` does NOT reduce under the idris2 0.8.0 evaluator (the
+||| same limitation the corpus documents for `Data.List.elemBy`, for
+||| which it hand-rolled `Decide.refElem`). So the negative-resolution
+||| fact is NOT `Refl`-pinnable cross-module here. It is instead
+||| machine-pinned on the Rust side — `conformance_emit.rs`'s
+||| `fixtures_roundtrip` asserts `certified_level` over the DECODED
+||| golden2 bytes `== -1` — and the input value the Rust decider runs
+||| on is itself `Refl`-proven identical to the corpus's (`conform2`:
+||| `fromWire golden2 = Right expected2`). What IS Refl-pinned here:
+||| golden2 requests EpistemicSafe and its int would be 10 had every
+||| level passed — so the observed -1 is a genuine rejection, not a
+||| level-int mismatch.
+clVerdict2a : requestedLevel WireConformance.expected2 = EpistemicSafe
+clVerdict2a = Refl
+
+clVerdict2b : safetyLevelToInt EpistemicSafe = 10
+clVerdict2b = Refl
+
+||| golden3 ⇒ Rust cl=0. requestedLevel = ParseSafe (k=0): no decider
+||| runs, the level int is `safetyLevelToInt ParseSafe = 0`.
+clVerdict3a : requestedLevel WireConformance.expected3 = ParseSafe
+clVerdict3a = Refl
+
+clVerdict3b : safetyLevelToInt ParseSafe = 0
+clVerdict3b = Refl