Skip to content

EXPLAINME.adoc

Latest commit

 

History

History
95 lines (84 loc) · 5.42 KB

EXPLAINME.adoc

File metadata and controls

95 lines (84 loc) · 5.42 KB
Raw

Implementation evidence

Observation horizon: local canonical checkouts inspected for the four families on 2026-09-07, with the focused commands below. This ledger does not establish remote CI status, deployed behaviour, whole-repository correctness or the state of every historical copy. See repository ownership.

Executable boundaries

Boundary Evidence Limit

Lithoglyph proof registry

Pinned Zig 0.15.2: core-zig’s `zig build test passes 27 test executions. Three new regression cases first failed, then passed after the verifier fix.

No builtin mathematical verifier is implemented. Registration remains available; its positive control checks callback plumbing, not theorem validity.

GNPL narration and private typed substrate

Lean 4.15.0: lake build succeeds; lake test passes five suites, including 35 narration checks and 26 private-substrate checks. Real CLI runs construct accounts and check focalization and hypothetical withdrawal. Lean checks withdrawal exclusion and preservation of requested claims/order; a default build audits their transitive axiom footprint and that of narrate as propext.

Narration uses imported snapshots and direct-evidence warrants. The live Lithoglyph/Glyphbase path, general derivation chains and confidence composition remain unimplemented. The private substrate still refuses persistent execution, complete IR wire interchange and attached-proof checking; its separate proof assumptions remain.

KRL / QuandleDB fragment

Julia 1.12.6: the specification’s fragment corpus passes 11 checks against the local QuandleDB parser; QuandleDB’s integration suite passes 112 checks and its new resolution-boundary suite passes 8.

Provider-based integration tests use fixtures. Stronger resolution assurance is refused; heuristic bucket candidates are not checked isotopy witnesses.

VCL-UT parsing/admissibility/wire boundary

The standalone Rust parser workspace passes 36 tests with RUST_MIN_STACK=16777216 (16 MiB) in that recorded local run, including conformance, rejection and wire tests.

Default test-thread stack overflowed in the property-test harness. The reproduction command below follows the existing Parse Gate workflow setting of 32 MiB; it is distinct from the recorded local run. These tests do not demonstrate that every VeriSimDB operation invokes the external gate.

Hermeneia invoke slice

39 default Rust tests and 7 end-to-end slice tests passed, the latter against the real tropecheck-rs binary. The Slice workflow runs this boundary.

Uses Hermeneia’s own JSONL store. This is not a demonstrated connection to Vocarium’s store; declared grades are inputs to sufficiency checking.

Vocarium invoke slice

Six Zig tests passed. Invoking the same stored trope under casual-note and critical-paraphrase produced checker exits 0 and 1 respectively; the latter named witness e_paraphrase. An unwarranted edge was refused with exit 2.

Demonstrates the invoke/checker boundary, not all planned language operations or a completed warrant-withdrawal lifecycle. Vocarium CI’s invoke-slice gate already checks both verdicts and the warrant refusal.

Reproduce at the owning repository

Use each repository’s pinned toolchain and its own build instructions.

  • Lithoglyph: from core-zig/, zig build test --summary all with Zig 0.15.2. See docs/proof-verification-boundary.adoc.

  • GNPL: lake build, then lake test. See docs/narration-slice.adoc, docs/executable-boundary.adoc, test/NarrationTest.lean and test/SubstrateTest.lean.

  • KRL: julia --startup-file=no tests/conformance/retrieval_fragment.jl /path/to/quandledb. See spec/SURFACES.adoc; this is fragment conformance.

  • QuandleDB: julia --startup-file=no server/krl/test/seam_test.jl and julia --startup-file=no server/krl/test/resolution_boundary_test.jl.

  • VCL-UT: RUST_MIN_STACK=33554432 cargo test --manifest-path src/interface/parse/Cargo.toml --locked.

  • Hermeneia: cargo test --workspace, then provide the real checker through HERMENEIA_TROPECHECK and run cargo test -p hermeneia-cli --features e2e --test slice.

  • Vocarium: tests/e2e/invoke_slice.sh; it pins Zig and a checker revision, and accepts an explicitly supplied TROPECHECK_BIN for an existing checker build.

The KRL fragment conformance workflow and the added QuandleDB/GNPL checks are local changes in this pass. Their tests were run locally; no remote run is claimed.

Design implications

VeriSimDB has real storage, drift and selected regeneration paths; its documented regeneration coverage must stay explicit. A configured optional gate is not a mandatory checked boundary. Glyphbase’s inspected routes still include demo responses; they do not establish a durable GNPL account workflow.

QuandleDB’s Julia semantic tests could not be run in the selected server project during this review because its KnotTheory dependency was unresolved. The passing base-Julia fragment tests do not substitute for those mathematical tests.

Each family needs evidence appropriate to its own semantic contract. A passing lookup does not prove consonance, a local refinement does not warrant an account, an invariant match does not resolve isotopy, and a declared grade does not prove that a linguistic transformation deserves that grade.