docs: consonance / identity-transition framing for VCL-total - #48
Merged
Conversation
Align VCL-total's docs with the VeriSimDB consonance model and embed the non-negotiable anchor in both. README.adoc: - Anchor lead under the rename note. - New top sections: "VCL-total in One Sentence", "What VCL Is" (the identity- lifecycle operations DECLARE/ASSERT/RETRACT/INSPECT/VERIFY/MERGE/SPLIT/ NORMALISE), "What VCL-total Proves" (admissibility obligations + the before/after transition proof shape), "Relationship to VeriSimDB", "Important Distinctions" (retraction != deletion; drift != identity death; VCL-total is the substrate, not the expert product), "Terminology Guidance". - proof-carrying -> proof-bearing. EXPLAINME.adoc: - Anchor lead + a "VCL vs VCL-total vs VeriSimDB" orientation. - 6-modal -> octad (8-modal) (3 places; factual correction — the engine is the octad). - "type-safe query interface" -> "proof-bearing safety substrate"; query plans -> transition plans; "proof-carrying queries/use cases" -> "proof-bearing statements/use cases". Docs/terminology only; no runtime changes.
Root cause (pre-existing, surfaced by opening this PR): the workspace has
`echidna-core = { path = "../../../echidna/crates/echidna-core" }`
(src/interface/Cargo.toml), so cargo cannot even load the workspace manifest
unless the echidna repo is present as a sibling of the checkout. CI never
provided it, so the entire Rust workspace failed to load — which is why all
~90 backend-matrix `Smoke (<prover>)` jobs (each runs the same
`cargo test -p vcltotal-echidna-client --locked`) plus e2e's build and
property/integration tests failed identically with
"failed to read .../echidna/crates/echidna-core/Cargo.toml (os error 2)".
Fix: clone echidna to `../echidna` before the cargo step in backend-matrix
and e2e, preserving the maintainer's path-dependency-for-local-dev intent
(no Cargo.toml / Cargo.lock change — the committed lock is already
consistent).
Verified locally (rustc 1.94 + echidna checked out as a sibling):
- cargo test -p vcltotal-echidna-client --tests --locked -> 8 passed
- bash tests/e2e.sh -> 19 passed, 0 failed
Also add examples/inspect.vcl: e2e.sh requires examples/*.vcl with content
(none existed); a representative VCL inspection + proof-bearing example.
parse-gate is unaffected (src/interface/parse is a standalone workspace;
passes locally). The aspect job's failures are separate pre-existing
source-quality gaps (SPDX/unsafe/unwrap), addressed separately.
Two pre-existing estate-check failures (surfaced by opening this PR; not caused by the docs change), both config-fixable: - governance / Language anti-pattern policy: flagged the intentional ReScript frontend (src/bridges/*.res, src/definitions/*.res, src/errors/*.res) as banned_language_file. vcl-ut had no .hypatia-ignore; add one whitelisting those .res files (ReScript is an allowed estate language), mirroring verisimdb's .hypatia-ignore. - openssf-compliance: required `.machine_readable/STATE.a2ml`, which existed only at `.machine_readable/6a2/STATE.a2ml`. Provide it at the path the check expects (copy of the canonical 6a2 checkpoint). Remaining red on this PR is the `aspect` job — a genuine, pre-existing source-quality refactor (SPDX headers on 5 src/ files + eliminating 20 `unsafe` blocks and 61 `.unwrap()/.expect()` from src/), tracked for the maintainer; not a safe blind change in a docs/CI pass.
The Language / package anti-pattern policy check runs two distinct rules over ReScript artefacts: - cicd_rules/banned_language_file → the .res sources (already exempt) - cicd_rules/banned_config_file → rescript.json (was NOT exempt) rescript.json is the ReScript compiler config for the same three directories whose .res sources are already whitelisted (src/bridges, src/errors, src/definitions). It is intrinsic to the permitted ReScript frontend, so exempt it under its own rule with the exact full-line form the check matches via grep -qxF. https://claude.ai/code/session_01W9Voe3JceP66Bna9FT4jME
…ntent (#49) The Aspect gate (tests/aspect_tests.sh) over-matched relative to its own documented remit ("unwrap/expect in non-test code"): it flagged 53 idiomatic test-code sites (#[cfg(test)] modules that even opt into #![allow(clippy::unwrap_used)], tests/ integration files, and Zig testing.expect) and 6 irreducible production-FFI unsafe blocks in two cdylib boundary crates whose unsafe is already audited (documented UNSAFE POLICY + a // SAFETY: comment on every block). Source -- fix the genuinely-wrong production sites: - src/core/lib.rs: add the missing SPDX header (AGPL-3.0-or-later, per the crate's Cargo.toml). - lint/fmt main(): return std::io::Result and propagate file errors with the question-mark operator + path context instead of .expect() (fail-closed, no panic). - echidna-client: model JSON serialization failure as a real ClientError::Serialization(#[from] serde_json::Error) and propagate it; build the default client via the canonical infallible reqwest::Client::new() (no builder config was applied, and Default for EchidnaClient requires infallible construction). Gate -- make it enforce its stated intent, not a coincidental grep: - Scope checks 2 & 3 to PRODUCTION Rust: *.rs under src/, excluding tests/ dirs and #[cfg(test)] modules (stripped by brace depth); non-Rust files are out of scope for the Rust-pattern checks. - Check 2 is now "no UNDOCUMENTED unsafe": audited FFI/WASM trust boundaries may contain unsafe (a cdylib #[no_mangle] extern "C" entry cannot be written without it), but every unsafe block must carry a contiguous // SAFETY: justification -- mirroring clippy::undocumented_unsafe_blocks. Result: bash tests/aspect_tests.sh -> 6 passed, 0 failed. Affected crates rebuilt; vcltotal-echidna-client suite green (3 unit + 5 integration). Closes #49. https://claude.ai/code/session_01W9Voe3JceP66Bna9FT4jME
hyperpolymath
marked this pull request as ready for review
June 5, 2026 10:04
hyperpolymath
added a commit
that referenced
this pull request
Jun 5, 2026
…transitive cycle (#52) Reconciles the parked `claude/abi-tier2-and-l10-trans-cycle` branch into `main` (branch-reconciliation pass, owner-approved). Unmerged since 2026-06-03. Substantive proof/ABI work: - `src/interface/abi/Tier2.idr` (+209) — Tier-2 Idris bindings - `src/core/Decide.idr` (+79) — closes the **L10 transitive cycle** - retires legacy `abi/Foreign.idr` → `legacy/Foreign.idr` - `verification/proofs/VERIFICATION-STANCE.adoc` (+121) **Merge gate:** the Idris2 proof corpus (`proof-corpus.yml`) must stay green — `%default total`, zero proof-escape — before this lands. Draft until CI confirms. Likely needs a rebase onto current `main` (post #48/#49/#50, incl. the licence normalisation). https://claude.ai/code/session_01W9Voe3JceP66Bna9FT4jME --- _Generated by [Claude Code](https://claude.ai/code/session_01W9Voe3JceP66Bna9FT4jME)_ Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
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.
Summary
Documentation/terminology pass aligning VCL-total's docs with the VeriSimDB
consonance / identity-transition model. Part of the cross-repo reframing
(companion: verisimdb#109). Docs only — no runtime/code changes.
The non-negotiable anchor is embedded verbatim in both docs:
README.adocadmissibility before live consonance state changes.
identity-lifecycle ops
DECLARE/ASSERT/RETRACT/INSPECT/VERIFY/MERGE/SPLIT/NORMALISE(not SQL-with-types).IdentityState_before + transition + evidence + obligations -> VerifiedTransition -> IdentityState_aftershape.deletion; drift ≠ identity death; VCL-total is the substrate, not the
expert-facing product), Terminology Guidance (prefer/avoid).
proof-carrying→proof-bearing.EXPLAINME.adoc6-modal→octad(8-modal) in 3 places — a factual correction (theengine is the octad).
type-safe query interface→proof-bearing safety substrate;query plans→
transition plans;proof-carrying queries/use cases→proof-bearing statements/use cases. Claims-substantiation evidence (Idris2 levels, filemap, tests) preserved as-is.
Scope respected
and caveats are unchanged.
landing (companion to the verisimdb-side reframe).
🤖 Generated with Claude Code
Generated by Claude Code