veridical-simulation-core

Shared core for the veridical-simulation program: lexical Agda parser, generic octad importer, octad veridicality prober, and a cross-repo bridge probe. Originally extracted from `email-octad-experiment’s phase-1 plumbing; first ingested formal artefacts in Phase 2 (echo-types) and Phase 3 (absolute-zero CNOs).

What it does

The framework treats raw artefacts as the territory and any structured representation as a map. Each artefact becomes one octad-entity in verisimdb across eight shapes (Graph / Vector / Tensor / Semantic / Document / Temporal / Provenance / Spatial). A prober scores each shape in [0, 1]; the geometric mean is the map fidelity. An empty shape is a finding, not a failure — the framework refuses to fake content the territory does not have.

Components

Crate	What
agda-lexparse	Lexical Agda parser. Extracts top-level definitions (data / record / function / postulate / nested module) plus their leading doc comments and lexical references. Conservative — unclassified lines are surfaced honestly rather than silently dropped.
agda-octad-importer	Two-pass importer: pass 1 creates one octad per definition with Document / Semantic / Vector / Tensor / Provenance / Temporal shapes; pass 2 wires references Graph edges to in-corpus targets resolved through the importer’s qname-to-octad map.
agda-octad-prober	Veridicality probes per shape, plus parser-coverage and reference- integrity meta-probes. Emits A2ML report + Nickel schema. Tensor is intentionally capped at 0.75 (per-definition statistics ≠ corpus-level proof-tree-shape Tensor — a standing finding); Spatial scores 1.0 iff empty (faithful to a non-spatial territory).
cross-repo-bridge-probe	Given a bridge .agda file plus two single-repo import reports, classifies references into resolved-A-only / B-only / both / unresolved. A bridge whose references resolve in only one corpus is a name-bridge, not a content-bridge — a candidate informal-formal disagreement signal.

Idris2 proof bundles

Each phase ships a small per-target theorem bundle alongside the empirical probe report. All proofs typecheck under %default total with no banned patterns (believe_me, assert_total, Admitted, sorry, unsafeCoerce).

Bundle	Theorems	Buys
src/abi/AgdaImporter.idr	3	Importer-side invariants the Graph and pass-2 logic depend on: qualified-name determinism, suffix-match agreement, lexer reference-set monotonicity.
src/abi/Phase1Verisim.idr	3	Phase 1 fixes are identity functions on their respective fields: temporal RFC 3339 round-trip, ?include=types preservation, ?include=embedding byte-exactness.
src/abi/Phase2EchoTypes.idr	3	Conservation of definitions (created + failed = seen) pass-2 wiring is a sublist of pass-1 candidates.
src/abi/Phase3AbsoluteZero.idr	3	bridge_fidelity ∈ [0, 1] and a decidable isNameBridge predicate that captures the EchoCNOBridge finding.
src/abi/Phase4aJanuskey.idr	6	OperationType.inverse is involutive on the four self-inverse kinds; Delete↔Create are mutual inverses; Copy is not involutive (recorded as a typed fact).
src/abi/Phase4bChimichanga.idr	6	Per-capability expand_one shapes are pinned by Refl (drift in any single case re-breaks the corresponding equation); Jaccard similarity is bounded in [0, 1].
src/abi/Phase4cWharf.idr	3	Per-snapshot read ∘ write = id and base-case retention idempotence on the empty ledger.

Verify any one with:

cd src/abi && idris2 --check <Bundle>.idr

Outstanding follow-up theorems (LIFO undo cascade for januskey, the includes? ↔ ∈ expand biconditional for chimichanga, retention idempotence for arbitrary lists, etc.) are queued for echidnabot under echidnabot-priorities/<phase>-proofs.a2ml with claim statement, strategy, and what each buys.

Phase 2 — echo-types (2026-04-27)

agda-octad-importer --source /var/mnt/eclipse/repos/echo-types/proofs/agda \
                    --territory echo-types \
                    --report docs/import-report-echo-types.json
agda-octad-prober   --source /var/mnt/eclipse/repos/echo-types/proofs/agda \
                    --import-report docs/import-report-echo-types.json \
                    --out docs/octad-veridicality-echo-types.a2ml \
                    --schema nickel/veridicality-echo-types.ncl

Result: 391 definitions parsed across 55 files, 388 octads created. Per-shape scores all 1.0 except Tensor (0.75 cap, by design) and Spatial (1.0, scored as faithful-empty for a formal corpus). Overall geometric mean = 0.9647.

Phase 3 — absolute-zero CNOs (2026-04-27)

agda-octad-importer --source /var/mnt/eclipse/repos/verification-ecosystem/absolute-zero/proofs/agda \
                    --territory absolute-zero \
                    --report docs/import-report-absolute-zero.json
agda-octad-prober   --source /var/mnt/eclipse/repos/verification-ecosystem/absolute-zero/proofs/agda \
                    --import-report docs/import-report-absolute-zero.json \
                    --out docs/octad-veridicality-absolute-zero.a2ml \
                    --schema nickel/veridicality-absolute-zero.ncl

Result: 42 definitions parsed from CNO.agda, 42 octads created. Overall geometric mean = 0.9647.

Cross-repo bridge probe — EchoCNOBridge (2026-04-27)

cross-repo-bridge-probe \
  --bridge /var/mnt/eclipse/repos/echo-types/proofs/agda/EchoCNOBridge.agda \
  --report-a docs/import-report-echo-types.json \
  --report-b docs/import-report-absolute-zero.json \
  --out docs/cross-repo-echo-cno.a2ml

Finding: EchoCNOBridge.agda resolves 20 references into the echo-types corpus, 0 into the absolute-zero corpus, 12 unresolved (stdlib). Bridge fidelity 0.00. The file is a name-bridge — uses CNO terminology in name — but defines its own local CNOOp data type rather than importing absolute-zero’s IsCNO predicate. This is a candidate informal-formal disagreement signal, not a failure.

Licence

MPL-2.0 (preferred); MPL-2.0 is the automatic legal fallback until PMPL is formally recognised. Crate metadata declares MPL-2.0 explicitly because crates.io requires an OSI-approved licence string.

License

This project is licensed under the Mozilla Public License, v. 2.0. See the LICENSE file for details.

SPDX-License-Identifier: MPL-2.0