vcl-ut #25 P5a: trusted Rust/SPARK-grade String->Statement parser#26
Merged
Conversation
First slice of the boundary-reinforcement workstream (#25). Adds a new workspace crate `src/interface/parse` (`vcltotal-parse`): a TOTAL, panic-free parser for the VCL-total relational core, the trust anchor that will feed the Idris2 certifier across the C-ABI (P5b/P5c). SPARK-grade posture (enforced statically, gated in CI): - #![forbid(unsafe_code)] - #![deny(clippy::{unwrap_used, expect_used, panic, indexing_slicing, arithmetic_side_effects, unreachable, todo, unimplemented, exit})] => no UB, no panics, no unchecked arithmetic; the only arithmetic is cursor saturating_add; every failure is a typed ParseError. - proptest panic-free invariant (4096 cases x 3 strategies incl. arbitrary bytes) = runtime witness of totality. Faithful AST mirror of src/core/Grammar.idr (ast.rs is 1:1 with the Idris constructors so the P5b marshaller is a structural map). Expr VqlType slots deliberately omitted — the parser establishes syntax only; type resolution + the L0-L10 decision stay the certifier's job. Coverage (first slice): SELECT/FROM/WHERE/GROUP BY/HAVING/ORDER BY/ LIMIT/OFFSET, full expression grammar (literals, params, *, fields, aggregates, comparisons, AND/OR/NOT, parens, scalar subqueries). The VCL-total extension clauses (PROOF/EFFECTS/AT VERSION/CONSUME| USAGE/EPISTEMIC) and modal expressions are FAIL-CLOSED: a typed "not yet supported" error, never a silently-wrong AST. Full grammar coverage iterates per the #25 roadmap. requested_level: a documented, conservative P5a policy (max feature-implied level), explicitly NOT a proven fact; authoritative reconciliation with the ReScript bridge is a later #25 iteration. Also: - .github/workflows/parse-gate.yml: hard CI gate (clippy -D warnings over the SPARK lint set + tests/proptest). - root Cargo.toml: add the workspace member. - PROOF-NEEDS.md: correct the ReScript-bridge nit (it is a standalone frontend, NOT on the verified path; the trusted parser is this crate). Reconciles with VERIFICATION-STANCE.adoc. Verified locally: cargo clippy -p vcltotal-parse --all-targets -D warnings (exit 0), cargo test -p vcltotal-parse (11/11), cargo fmt --check (clean). Refs #25, hyperpolymath/standards#124. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
🔍 Hypatia Security ScanFindings: 21 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 idris-community/setup-idris@v1 needs attention",
"type": "unpinned_action",
"file": "proof-corpus.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"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 (1 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 (2 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"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
…ion) CI revealed the parent virtual workspace cannot load in a standalone checkout: the pre-existing src/interface member path-deps on an out-of-repo sibling (echidna-core = ../../../echidna/...), which only resolves on the estate layout. Any whole-workspace cargo op (incl. the prior parse-gate, and the repos other Rust jobs) fails fast in CI. Decouple the trusted boundary parser: it is now its own [workspace] root with its own Cargo.lock; parse-gate runs via --manifest-path --locked, never traversing the broken parent. Remove it from the root members. P5a code unchanged; verified standalone: clippy --locked -D warnings clean, 11/11 tests, fmt clean. Root Cargo.lock reverted to main (the earlier change is moot now parse is not a member). The parent-workspace external-path-dep breakage is pre-existing and out of #25 scope; reported separately. Refs #25. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
🔍 Hypatia Security ScanFindings: 21 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 idris-community/setup-idris@v1 needs attention",
"type": "unpinned_action",
"file": "proof-corpus.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"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 (1 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 (2 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"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
This was referenced May 19, 2026
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
1 participant
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.
P5a — trusted Rust/SPARK-grade
String -> StatementparserFirst slice of the boundary-reinforcement workstream (#25). The
verified corpus certifies an already-built
Statement; nothingturned a query string into the certified AST. This adds the trust
anchor that will: parse text → (P5b) marshal across the C-ABI → (P5c)
hand to the proof-gated Idris2 certifier → (P5d) return a signed
attestation.
What this PR adds
src/interface/parse(vcltotal-parse) — atotal, panic-free recursive-descent parser for the VCL-total
relational core.
#![forbid(unsafe_code)],#![deny(clippy::{unwrap_used, expect_used, panic, indexing_slicing, arithmetic_side_effects, unreachable, todo, unimplemented, exit})].The only arithmetic is cursor
saturating_add; every failure is atyped
ParseError.(arbitrary UTF-8, arbitrary bytes, token-salad). A green run is
machine evidence of totality.
src/core/Grammar.idr—ast.rsis 1:1with the Idris constructors so the P5b marshaller is a structural
map. Expr
VqlTypeslots deliberately omitted: the parserestablishes syntax only; type resolution + the L0–L10 decision
remain the certifier's job (kept honest about what parsing proves).
.github/workflows/parse-gate.yml— hard gate (cargo clippy --all-targets -D warningsover the SPARK lint set + tests/proptest).PROOF-NEEDS.md— corrects the ReScript-bridge nit: it is astandalone frontend, not on the verified path; the trusted
parser is this crate. Reconciles with
VERIFICATION-STANCE.adoc'sprecise "no string→
Statementparser exists" (= none whose outputis the certified Idris2
Statement).Scope / honesty
Covered:
SELECT/FROM/WHERE/GROUP BY/HAVING/ORDER BY/LIMIT/OFFSET+full expression grammar (literals, params,
*, fields, aggregates,comparisons, AND/OR/NOT, parens, scalar sub-queries). The VCL-total
extension clauses (PROOF / EFFECTS / AT VERSION / CONSUME|USAGE /
EPISTEMIC) and modal expressions are fail-closed: a typed
"not yet supported" error, never a silently-wrong AST. Full grammar
coverage iterates per the #25 roadmap.
requested_levelis a documented, conservative P5a policy (maxfeature-implied level), explicitly not a proven fact; authoritative
reconciliation with the ReScript bridge / certifier is a later #25
iteration.
OCTAD≡HEXADaccepted pending that reconciliation.Verification (local, CI-faithful)
cargo clippy -p vcltotal-parse --all-targets -- -D warnings→ exit 0cargo test -p vcltotal-parse→ 11/11 (6 lib + 5 integration incl.proptest)
cargo fmt -p vcltotal-parse -- --check→ cleanDoes not touch the Idris corpus or PR #24. Refs
#25, hyperpolymath/standards#124.
🤖 Generated with Claude Code