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

[hyperpolymath]

P5c (steps 2–4) — faithful Rust recompute-decider + cross-language decision conformance

The recompute-PCC tier's verdict engine. Per the locked design
(VERIFICATION-STANCE.adoc two-tier boundary model): the corpus proves
soundness once (checkLevelNSound, offline-re-checkable); the
consumer re-runs that exact decision over a wire-decoded
(Statement, OctadSchema) and compares to the producer's claimed
level. This adds the re-runner in Rust (→ affinescriptiser-wrapped to
typed-wasm in P5c-5) and machine-pins its faithfulness to the
corpus.

src/interface/parse/src/decider.rs (new)

SPARK lint set, total, no panic, pure. Line-by-line port of
Schema/Decide (the single source of truth) + the Checker
checkLevel0..10 / certifiedLevel spine. certified_level = (all checkLevel1..k accept, k = safetyLevelToInt(requestedLevel)) ? k : -1 (L4 polarity preserved: passes iff WHERE has no raw string
literal).

Why the no-ty Rust AST is exact here (documented in-module): the
wire format omits Expr's VqlType and every decoder fills TAny, so
on a wire-decoded statement the corpus resolveExprType is TAny
except EField (→schema) / ESubquery (→TOctad). The recompute tier
only runs on decoded statements, so the port is faithful by
construction — not a shortcut.

Conformance (tests/conformance_emit.rs ⇄ WireConformance)

• conform1/2/3/S1: Rust to_wire* ⇄ Idris certified fromWire*,
  byte-for-byte by Refl (unchanged, still green).
• Recompute pins. Rust oracle emits cl1=1, cl2=-1, cl3=0
  (certified_level over the decoded golden bytes; self-checked in
  fixtures_roundtrip). Idris Refl-pins the decisive corpus facts
  via VclTotal.Core.Decide (fully public export, Grammar/Schema-only
  ⇒ reduces cross-module; Checker.checkLevelN does not —
  export/Levels-coupled).

Disclosed, not faked (estate verification-honesty doctrine)

golden2 → -1 hinges on vector.x not resolving, which forces
Schema.lookupField → Data.List.find; find does not reduce under the
idris2 0.8.0 evaluator (same limitation the corpus documents for
elemBy → its hand-rolled refElem). So the negative-resolution fact
is not Refl-pinnable cross-module. It is machine-pinned instead
on the Rust side (fixtures_roundtrip: certified_level over decoded
golden2 == -1) with the input value Refl-proven identical to the
corpus's (conform2). The find-free decision structure (level ints,
requested levels, empty-ref accept) is Refl-pinned. Scoping is
documented verbatim in WireConformance.

Verified locally

• Corpus idris2 0.8.0 --build exit 0 — 12 modules, %default total, zero proof-escape (CI escape-audit OK, comment-filtered).
• parse-gate equivalent: clippy -D warnings / cargo test / cargo fmt --check clean; conformance self-check green (incl. decoded-bytes
  certified_level == {1,-1,0}).

P5c remaining

P5c-5: affinescriptiser-wrap certified_level → typed-wasm + C/Zig
fail-closed attestation fallback. P5c-6: stance flip OWED→RESOLVED +
ADR docs/decisions/0002-ffi-attestation-trust-boundary.adoc.

Refs #25.

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 22 issues detected

Severity	Count
🔴 Critical	6
🟠 High	7
🟡 Medium	9

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Issue in quality.yml",
    "type": "missing_workflow",
    "file": "quality.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in security-policy.yml",
    "type": "missing_workflow",
    "file": "security-policy.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Action actions/upload-artifact@v4 needs attention",
    "type": "unpinned_action",
    "file": "release.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action actions/download-artifact@v4 needs attention",
    "type": "unpinned_action",
    "file": "release.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "codeql.yml lists `language: javascript-typescript` but the repo has no source files in any CodeQL-scannable language. The analyze job will exit 'no source files' on every run. Switch the matrix to `actions` (which scans workflow files — every repo has those).",
    "type": "codeql_language_matrix_mismatch",
    "file": "codeql.yml",
    "action": "switch_codeql_matrix_to_actions",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "assert_smaller bypasses termination checker (1 occurrences, CWE-704)",
    "type": "assert_smaller",
    "file": "/home/runner/work/vcl-ut/vcl-ut/src/core/Checker.idr",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "believe_me undermines formal verification (2 occurrences, CWE-704)",
    "type": "believe_me",
    "file": "/home/runner/work/vcl-ut/vcl-ut/src/core/Decide.idr",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "believe_me undermines formal verification (3 occurrences, CWE-704)",
    "type": "believe_me",
    "file": "/home/runner/work/vcl-ut/vcl-ut/src/core/Composition.idr",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "assert_total bypasses totality checker (1 occurrences, CWE-704)",
    "type": "assert_total",
    "file": "/home/runner/work/vcl-ut/vcl-ut/src/core/Composition.idr",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence