Skip to content

docs(vclt-gate): freeze the VCL-total ↔ VeriSimDB admissibility gate contract - #58

Merged
hyperpolymath merged 1 commit into
mainfrom
claude/peaceful-clarke-h3i92h
Jun 13, 2026
Merged

hyperpolymath merged 1 commit into
mainfrom
claude/peaceful-clarke-h3i92h

Conversation

@hyperpolymath

Copy link
Copy Markdown
Owner

Freezes the vclt-gate contract — the single shared artifact that lets the vcl-ut and verisimdb workstreams proceed in separate threads against a fixed seam, with no further coordination.

docs/vclt-gate-contract.adoc specifies the VCL-total ↔ VeriSimDB admissibility gate: a pure CLI subprocess (JSON request → JSON verdict) wrapping vcltotal-parse's lexer/parser + decider::certified_level.

Grounded in the real primitives I read in this repo, not invented:

  • SafetyLevel tags 0–10 (ast.rs) and certified_level(stmt, schema) -> i64 (decider.rs) — the authoritative level vocabulary and verdict function.
  • Key finding baked into the contract: all ten level predicates are statically decidable today (presence of LIMIT/effect-decl/version-const, no WHERE string-literal, epistemic acyclicity, …). The echidna proof tier is only for proof discharge of PROOF clauses — a separate downstream check, not a blocker on this gate. So the gate is far stronger than "L1–L4 static tier."

The spec covers: transport rationale (subprocess decouples the two toolchains with no shared build), request/response schemas (schema_version: 1), the authoritative level table, exit-code verdict (0 admit / 1 reject / 2 gate-error), a purity guarantee (safe to call on the write path), the consumer-side integration (VERISIM_VCLT_GATE env gate, pre-mutation invocation point, fail-closed default with an advisory override), versioning, two worked fixtures (an admit and an injection-reject), and a per-side build checklist.

With this frozen, Week-3's vclt-gate splits cleanly: the producer half (the binary) builds here, the consumer half (execute-path invocation) builds in verisimdb, and they meet only at this wire shape.

https://claude.ai/code/session_01E8BpV19yxhf67UrCrvkfTr


Generated by Claude Code

…e contract

The single shared artifact that lets the vcl-ut and verisimdb workstreams
proceed in separate threads against a fixed seam. Specifies the vclt-gate
boundary: a pure CLI subprocess (JSON request -> JSON verdict) wrapping
vcltotal-parse's lexer/parser + decider::certified_level.

- Transport rationale (subprocess over FFI/lib/network: decouples the two
  toolchains with no shared build).
- Request/response schemas (schema_version 1), grounded in the real
  primitives: SafetyLevel tags 0-10 (ast.rs) and certified_level (decider.rs).
- Authoritative level table (all 10 predicates are statically decidable
  today; the echidna proof tier is a SEPARATE downstream check, not a
  blocker on this gate).
- Exit-code verdict (0 admit / 1 reject / 2 gate-error) + purity guarantee.
- Consumer integration: VERISIM_VCLT_GATE env gate, pre-mutation invocation
  point, fail-closed default with an advisory override.
- Per-side build checklists + two worked fixtures (admit, injection-reject).

Enables Week-3 item 'vclt-gate' to be split cleanly: producer half here,
consumer half in verisimdb, meeting only at this wire shape.

https://claude.ai/code/session_01E8BpV19yxhf67UrCrvkfTr
@hyperpolymath
hyperpolymath marked this pull request as ready for review June 13, 2026 16:37
@hyperpolymath
hyperpolymath merged commit d302956 into main Jun 13, 2026
128 checks passed
@hyperpolymath
hyperpolymath deleted the claude/peaceful-clarke-h3i92h branch June 13, 2026 16:37
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants