vcl-ut #25 P5c (step 6): stance flip OWED->RESOLVED (Tier-1 recompute-PCC) + ADR-0002

[hyperpolymath]

P5c (step 6) — stance flip OWED→RESOLVED (Tier-1 recompute-PCC) + ADR-0002

The final P5c step: the authoritative-doc flip. Tier-1
(recompute-PCC over plain wasm32) is now RESOLVED; Tier-2 (the
C-ABI signed-attestation fallback, P5d) is the only remaining OWED
boundary item. Docs-only — no corpus/.idr/.ipkg change (12
modules, idris2 --build exit 0, escape-scan OK, unchanged).

VERIFICATION-STANCE.adoc (authoritative)

• Canonical two-tier boundary model rewritten:
  • Tier-1 (RESOLVED, achieved): consumer is shipped the wasm32
    module (src/interface/recompute-wasm, vcl_recompute) +
    (Statement, OctadSchema) wire bytes + claimed level, re-runs
    the certified decision, compares. PCC by recomputation, not
    proof transport (proof-term+kernel was rejected — Idris2 ships no
    embeddable kernel). TCB = once-proved corpus soundness
    (offline-re-checkable) + the WireConformance pin + the wasm
    runtime — not the whole certifier, not a trusted tag. Plain
    wasm32 is sufficient and not a compromise (type system not
    load-bearing under recompute). affinescriptiser disclosed N/A
    (resource-required + wasm-backend Phase-2-pending), not faked.
  • Tier-2 (OWED, P5d): the explicit weaker C-ABI attestation
    fallback for consumers that cannot run the wasm.
• Headline status, NAMED OWED, consumer guidance, roadmap Phase 5,
  closing paragraph, provenance all updated to Tier-1 RESOLVED /
  Tier-2 OWED; disclosed limits restated precisely (NaN-payload;
  cross-module Refl non-reduction of find/elemBy ⇒
  schema-resolution verdicts pinned Rust-side + input-value
  conformance; L9/L10 predicate depth; additive↔ceil alignUp).

docs/decisions/0002-ffi-attestation-trust-boundary.adoc (new ADR)

Mirrors the 0001 format. Records why the two-tier boundary: the
C-ABI type-erasure constraint, the rejected proof-term-PCC design, why
affinescriptiser does not apply, why plain-wasm32 recompute is the
correct achieved tier, and that P5d (Tier-2) remains OWED. Status:
Accepted (Tier-1 RESOLVED; Tier-2/P5d OWED).

Subordinate docs

PROOF-NEEDS.md, CHANGELOG.md: currency edits to Tier-1 RESOLVED /
Tier-2 OWED, deferring to STANCE as authoritative.

Closes P5c

The vcl-ut#25 boundary-reinforcement workstream is complete bar
the precisely-scoped, disclosed P5d C-ABI attestation fallback for
non-wasm consumers (Tier-2). Recap of what landed:
P5a (#26) trusted parser · P5b-1 (#28) wire codec · P5b-2 (#29)
certified Statement decoder + Refl conformance · P5c-1 (#30)
certified OctadSchema codec · P5c-2/3/4 (#31) faithful Rust decision
port machine-pinned to the corpus · P5c-5 (#32) fail-closed recompute
wasm32 artefact · P5c-6 (this PR) stance flip + ADR.

Refs #25.

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 25 issues detected

Severity	Count
🔴 Critical	6
🟠 High	9
🟡 Medium	10

⚠️ 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