vcl-ut #25 P5b (step 2): certified Idris wire decoder + cross-language Refl conformance#29
Merged
Merged
Conversation
…e Refl conformance The certified half of the hypatia<->verisim marshalling seam. The trusted Rust parser (P5a, #26) and codec (P5b step 1, #28) serialise a `Statement` to the v1 wire format (src/interface/parse/WIRE-FORMAT.adoc); this adds the certified receiver and machine-checks that the two agree. New corpus modules (vclut-core.ipkg now 12, idris2 0.8.0 --build exit 0, %default total, ZERO proof-escape — CI-enforced): - VclTotal.Interface.WireDecode — a total decoder of the v1 wire format into Grammar.idr's certified `Statement`. No believe_me / postulate / assert_* / idris_crash / sorry: totality is structural. The grammar is mutually recursive (Expr <-> Statement via Subquery) so a binary parser is not structurally recursive on the input; recursion is bounded by an input-length *fuel* Nat, sound because every node costs >= 1 discriminant byte (a well-formed stream never spuriously exhausts). The recursion-bearing list element decoders are inlined into the `mutual` block so the size-change analysis sees the fuel-decreasing edges directly. Omitted `VqlType` slots are filled `TAny` (the grammar's documented pre-typecheck convention; the 10-level checker resolves them at L2+). IEEE-754 binary64 is reconstructed by exact power-of-two scaling (repeated *2.0 / /2.0, exact in IEEE incl. gradual underflow) so all finite values (incl. subnormals, f64::MIN/MAX) and both infinities are bit-exact. Strict total UTF-8 decode (rejects overlong/surrogate/out-of-range). - VclTotal.Interface.WireConformance — cross-language conformance as a build-time PROOF, not a test: `conformN : fromWire goldenN = Right expectedN` by `Refl`. The corpus only builds if the total decoder, evaluated at compile time on the Rust encoder's exact bytes, reduces to the expected certified `Statement`. Fixtures: F1 minimal; F2 strings/ints/bools/agents/options/lists/nested comparison + every extension clause; F3 the float path (2.5). - src/interface/parse/tests/conformance_emit.rs — the regeneration oracle: emits the exact to_wire image of the fixtures (and a round-trip self-check). The golden byte lists in WireConformance.idr are injected verbatim from its output, never hand-transcribed. Disclosed limitation (not a hidden gap): Idris2 0.8.0 has no pure, bit-exact Bits64 -> Double, so the certified decoder decodes any NaN bit-pattern to *a* NaN; the NaN *payload* is not preserved across the Idris Double boundary. Finite and infinite values are bit-exact. The exhaustive bit-exact float witness — NaN payload included — remains the Rust proptest wire.rs::golden_bit_exact_floats. Docs (truth-maintained, authoritative VERIFICATION-STANCE.adoc leads): - VERIFICATION-STANCE.adoc: Phase 5 roadmap entry; NAMED OWED updated (the "no string->Statement parser" headline item is closed — trusted Rust parser exists; the C-ABI Statement *decode* side is now *certified*; encode/Idris->C build/attestation remain OWED, P5c/P5d); module count corrected to 12; provenance + closing paragraph updated; NaN-payload limitation disclosed. - WIRE-FORMAT.adoc: "Certified decoder + cross-language conformance" section + NaN disclosure. - verification/proofs/README.adoc, PROOF-NEEDS.md, CHANGELOG.md: 12 modules, P5b step-2 entry, decode-side-certified status. - .github/workflows/proof-corpus.yml: proof-escape audit extended to the two new modules (docstring prose mentioning escape symbols is comment-filtered exactly as for the existing corpus; verified locally). Still OWED (precisely, tracked #25): encode direction (Idris->wire) + OctadSchema marshalling; Idris->C build linking the fail-closed Zig shim to certifiedLevel (P5c); signed-attestation contract over (sha256(query), schema_id, level) + ADR + OWED->RESOLVED stance flip (P5d). A C ABI carrying a re-checkable dependent proof is impossible by construction; trusted-certifier attestation is the stated honest target. Refs #25. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
| @@ -0,0 +1,643 @@ | |||
| -- SPDX-License-Identifier: PMPL-1.0-or-later | |||
🔍 Hypatia Security ScanFindings: 22 issues detected
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 |
…in the stance
The prior docs (inherited from the Phase-3d FFI-honesty work) framed
"a re-checkable dependent proof across a C ABI is impossible by
construction; trusted-certifier attestation is the honest target" as
*the* ceiling. That is true of a C ABI specifically, but defends a
boundary the estate decided not to cross: the estate transport/
compilation target is typed-wasm, whose module boundary is *typed, not
erased*. The framing was circular (use a C ABI -> attestation is the
ceiling -> document attestation -> keep building the C ABI).
This corrects the authoritative VERIFICATION-STANCE.adoc to a
canonical **two-tier boundary model** (referenced from every other
mention), and re-scopes the P5c roadmap accordingly:
- C-ABI tier (FALLBACK, P5d): erases to machine words -> cannot carry
a re-checkable proof; ceiling is trusted-certifier attestation
(unforgeable token bound to (sha256(query), schema_id, level)). Only
for consumers reachable solely over C. The `ffi/zig` fail-closed
shim is this tier's scaffolding, NOT the architectural endpoint.
- typed-wasm tier (ESTATE TARGET, the real P5c objective): typed,
non-erasing boundary -> the proof term crosses faithfully and a
value of the proof type cannot be forged without the linear
capability. Riding a small proof-checker kernel the consumer runs
yields proof-carrying code: the consumer RE-VALIDATES the
certificate. TCB shrinks from "trust the whole certifier" to "trust
the checker kernel + the typed-wasm verifier". (typed-wasm's own
type system is linear/structural, not dependent, so it does not
re-check the safety predicate itself — the shipped kernel does;
standard PCC, strictly stronger than attestation.)
So "impossible by construction" is true *of a C ABI*, not of any FFI.
P5c's objective is the typed-wasm PCC tier; P5d attestation is the
explicit weaker fallback, not the ceiling.
Docs updated (no corpus/.idr/.ipkg change — the certified decoder and
its Refl conformance from P5b step 2 stand unchanged; this is purely
the transport framing):
- VERIFICATION-STANCE.adoc: canonical two-tier boundary model added
under "What is NOT proven"; every "impossible by construction / the
honest target is attestation" site rewritten to reference it; P5c
roadmap re-scoped to typed-wasm PCC (Zig shim = fallback only); new
Consumer-guidance bullet ("the ceiling is PCC, not attestation").
- WIRE-FORMAT.adoc: format declared transport-agnostic (C-ABI fallback
payload AND typed-wasm proof-term payload); pointer to the two-tier
model.
- PROOF-NEEDS.md, CHANGELOG.md: P5c re-scoped to typed-wasm PCC; P5d
labelled the fallback tier.
Refs #25.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
🔍 Hypatia Security ScanFindings: 22 issues detected
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 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
P5b (step 2) — certified Idris wire decoder + cross-language
ReflconformanceThe certified half of the hypatia↔verisim marshalling seam. The trusted
Rust parser (P5a, #26) and codec (P5b step 1, #28) serialise a
Statementto the v1 wire format (src/interface/parse/WIRE-FORMAT.adoc);this adds the certified receiver and machine-checks that the two
agree byte-for-byte.
What this adds (corpus now 12 modules,
idris2 0.8.0 --buildexit 0,%default total, ZERO proof-escape — CI-enforced)VclTotal.Interface.WireDecode— a total decoder of the v1 wireformat into
Grammar.idr's certifiedStatement. Totality isstructural, not asserted (no
believe_me/postulate/assert_*/idris_crash/sorry): the grammar is mutually recursive(
Expr ↔ StatementviaSubquery), so recursion is bounded by aninput-length fuel
Nat— sound because every node costs ≥ 1discriminant byte, so a well-formed stream never spuriously exhausts.
Recursion-bearing list decoders are inlined into the
mutualblock sothe size-change analysis sees the fuel-decreasing edges directly.
Omitted
VqlTypeslots →TAny(the grammar's documentedpre-typecheck convention). IEEE-754 binary64 reconstructed by exact
power-of-two scaling: all finite values (incl. subnormals,
f64::MIN/MAX) and both infinities bit-exact. Strict total UTF-8.VclTotal.Interface.WireConformance— cross-language conformanceas a build-time proof, not a test:
conformN : fromWire goldenN = Right expectedNbyRefl. The corpus only builds if the totaldecoder, evaluated at compile time on the Rust encoder's exact bytes,
reduces to the expected certified
Statement. Fixtures: F1 minimal;F2 strings/ints/bools/agents/options/lists/nested comparison + every
extension clause; F3 the float path.
src/interface/parse/tests/conformance_emit.rs— the regenerationoracle (emits the exact
to_wireimage + a round-trip self-check).The golden byte lists are injected verbatim from its output, never
hand-transcribed.
Disclosed limitation (not a hidden gap)
Idris2 0.8.0 has no pure, bit-exact
Bits64 -> Double. The certifieddecoder decodes any NaN bit-pattern to a NaN; the NaN payload is
not preserved across the Idris
Doubleboundary. Finite and infinitevalues are bit-exact. The exhaustive bit-exact float witness — NaN
payload included — remains the Rust proptest
wire.rs::golden_bit_exact_floats. Disclosed here, inWIRE-FORMAT.adoc, and in the authoritativeVERIFICATION-STANCE.adoc.Verified
rm -rf verification/proofs/build && idris2 --build verification/proofs/vclut-core.ipkg→ exit 0, 12/12 modules incl.WireDecode(3/12) andWireConformance(4/12).OK: zero proof-escape symbols outside comments— docstring prosementioning escape symbols is comment-filtered, and the audit's file
list is extended to the two new modules.
parse-gateequivalent:cargo clippy --all-targets --locked -D warningsclean,cargo test --lockedgreen (incl. the newconformance_emitround-trip self-check),cargo fmt --checkclean.Docs (truth-maintained; authoritative
VERIFICATION-STANCE.adocleads)VERIFICATION-STANCE.adocPhase-5 entry; the previously-headline "nostring→
Statementparser" OWED item is closed (trusted Rust parserexists; the C-ABI
Statementdecode side is now certified);encode/Idris→C build/attestation remain precisely OWED (P5c/P5d). Module
count corrected to 12 across STANCE/README/PROOF-NEEDS/CHANGELOG;
WIRE-FORMAT.adocconformance + NaN-disclosure section added.Still OWED (tracked #25)
Encode direction (Idris→wire) +
OctadSchemamarshalling; Idris→C buildlinking the fail-closed Zig shim to
certifiedLevel(P5c); signedattestation contract over
(sha256(query), schema_id, level)+ ADR +the
OWED→RESOLVEDstance flip (P5d). A C ABI carrying a re-checkabledependent proof is impossible by construction — trusted-certifier
attestation is the stated honest target.
Refs #25.
🤖 Generated with Claude Code