Skip to content

Work up VCL-UT: repair CI, reconcile the level ladder, and set direction#75

Merged
hyperpolymath merged 5 commits into
mainfrom
worktree-vcl-ut-workup
Jul 21, 2026
Merged

Work up VCL-UT: repair CI, reconcile the level ladder, and set direction#75
hyperpolymath merged 5 commits into
mainfrom
worktree-vcl-ut-workup

Conversation

@hyperpolymath

Copy link
Copy Markdown
Owner

Two parts, as asked: deal with the immediate issues first, then work up where this goes — theory and VeriSimDB application kept separate.

Part A — immediate issues (all measured, all verified)

Two CI faults, independent:

  • dogfood-gate.yml was malformed YAML. The embedded Python started at column 1 while the run: | block scalar was indented 10, so YAML closed the scalar early. The workflow had failed every run in 0s since at least 2026-07-06 — it never once validated anything — and it broke Dependabot's github_actions updater with dependency_file_not_parseable. Verified by executing the extracted step against valid and invalid manifests, not just by parsing it. (~80 of 266 estate copies carry the identical fault.)
  • dependabot.yml declared mix/npm/pip/nix with no manifests present — four of the five weekly failures. Also: this repo has five cargo workspace roots and the single / entry covered one, so the parser and vclt-gate were invisible to Dependabot.

Two crates had silently stopped compiling. ast::Statement gained the consonance field verb; attest and recompute-wasm were never updated (E0063). Only their test modules were stale, so the libraries still built and nothing complained — 12 tests had just stopped running, in the crates carrying the attestation and recompute boundaries. They were covered by no CI job at all, which is exactly how they rotted. Now fixed and gated.

Coverage gaps closed: e2e.yml ran 69 of the root workspace's 102 tests — every e2e and fuzz test was skipped. Also removed two git clone echidna steps that cloned a whole repo per run for nothing (proven: 102 tests and e2e.sh 19/19 pass with no sibling present).

Correction to an earlier finding of mine: I had recorded "0 unit tests, root cargo test is a fake gate". That was wrong — an artefact of truncating the log. The root crate is a re-export facade whose whole surface lives in tests/; the tests-102 pass badge was exact. Noted in the workflow header so the misreading isn't repeated.

Documentation truth pass — the level ladder disagreed with the code three ways:

was now
Numbering 1–10 L0–L10 (they're wire tags — requesting 7 got Effect-Tracking, not the Cardinality documented)
Vocabulary FETCH/REMOVE SELECT/RETRACT — the documented verbs are rejected by the parser
Count ten eleven — L10 EpistemicSafe appeared in no document anywhere

Part B/C — the work-up

docs/2026-07-21-workup-consonance-and-verisim.adoc, two strands kept separate.

Theory. The strongest argument for the consonance reframe came from the code, not from taste: the eleventh level isn't a query-safety property at all, and it's the one level not inherited from TypeLL (a UI panel has no federation, so no warrant question). The paper is titled "A Decalogue…" — its own title can't house its own eleventh level. The gap in the world is stated honestly: type-safe query languages are a crowded, mature field and a ten-levels paper reads as synthesis. What none of them do is type warrant — every one assumes a single source of truth that cannot disagree with itself.

The whitepaper reframe is a proposal, not an executed rewrite. The 1,909-line .tex is untouched. Structure + a full draft abstract are offered for approval first — how a paper argues its claim is yours to settle, and it's the least testable change available here.

Application. Opens with the uncomfortable fact: VCL-UT delivers nothing to VeriSimDB at runtime today — the producer is finished and the consumer was never written (verisim-api/src/vcl.rs has zero vclt-gate references). Two VeriSimDB defects located precisely, including VCLTypeChecker.res:60 building the default context with six modalities though the type admits eight — Provenance and Spatial silently absent from every default type-check. Those are VeriSimDB changes and are not made here.

Closes with a falsification section, including one thing that should be measured before the wiring work rather than after: subprocess latency on the hot path.

Verification

reuse lint                       -> compliant, 460/460
23 workflows                     -> 0 malformed
cargo test --workspace --locked  -> 102 passed
cargo test (parse)               ->  36 passed
cargo test (attest)              ->   9 passed   (was: did not compile)
cargo test (recompute-wasm)      ->   3 passed   (was: did not compile)
bash tests/e2e.sh                -> 19/19, no echidna sibling
                                    150 tests total

Note

The three unpushed main commits (sweep2/3/4, Mistral Vibe) are not carried here. They break reuse lint — a genuinely fail-closed gate — by adding an AGPL licence file to a repo with zero AGPL-declared files, and they inject @metadatastician as owner/sponsor into a hyperpolymath repo while duplicating correct .github/ files. Recommend main be reset to origin/main with a sweep-quarantine branch kept for reachability. This branch is based at origin/main and is unaffected.

🤖 Generated with Claude Code

hyperpolymath and others added 5 commits July 21, 2026 13:22
Two independent, measured CI faults.

1. .github/workflows/dogfood-gate.yml was MALFORMED YAML.

   The `run: |` literal block scalar takes its indentation indicator from
   its first line (10 spaces), but the embedded Python validator started
   at column 1. YAML therefore terminated the block scalar and tried to
   read `import tomllib, sys` as a mapping key:

     while scanning a simple key ... could not find expected ':'

   Consequences, both measured:
     - the workflow has failed EVERY run in 0s (startup_failure) since at
       least 2026-07-06 — it has never once validated anything;
     - it broke Dependabot's github_actions updater with
       `dependency_file_not_parseable`, which is why trimming the
       ecosystem list alone would NOT have made Dependabot green.

   Fix: indent the Python into the block scalar. Because YAML strips the
   block indentation uniformly, the shell still receives the script at
   column 0, and relative (Python-significant) indentation is preserved.

   Verified by execution, not inspection: the step was extracted from the
   parsed YAML and run against both a valid and an invalid manifest —
   exit 0 with `Valid: ...`, and exit 1 with the `::error` annotation
   respectively. All 22 workflows now parse.

   NOTE: this file is a template copied across the estate; ~80 of 266
   copies carry the identical fault. Fixing the template is tracked
   separately.

2. .github/dependabot.yml was the unedited RSR template.

   It declared mix / npm / pip / nix, none of which have a manifest in
   this Rust-only repository (verified absent: mix.exs, package.json,
   requirements.txt, pyproject.toml, flake.nix). Those four ecosystems
   accounted for four of the five recurring weekly failures since
   2026-07-13.

   Also: this repository has FIVE cargo workspace roots, and the single
   `directory: "/"` entry covered only the root one — so the crates
   holding most of the real code, including the parser and vclt-gate,
   were invisible to Dependabot. Added explicit entries for
   src/interface/{parse,attest,recompute-wasm}, each self-contained.

   src/interface/echidna-client remains deliberately excluded: it reaches
   ../../interface, which carries an out-of-tree path dependency on the
   echidna sibling repo that Dependabot cannot resolve. Declaring it
   would reintroduce exactly the always-red job this trim removes.

Verification:
  reuse lint                    -> compliant, 458/458 (MPL-2.0, CC-BY-SA-4.0)
  22 workflows                  -> 0 malformed
  cargo test --workspace        -> 102 passed
  cargo test (parse workspace)  -> 36 passed

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…gaps

vcl-ut has FIVE cargo workspace roots. CI covered three of them, and the
two it missed had stopped compiling without anyone noticing.

WHAT ROTTED

`ast::Statement` gained the S1 consonance field `verb` (Select / Inspect /
Verify / Assert / Declare / Retract / Merge / Split / Normalise) — the
consonance turn itself. Two downstream crates were never updated:

  src/interface/attest          E0063: missing field `verb`
  src/interface/recompute-wasm  E0063: missing field `verb`

In both cases only the in-file `#[cfg(test)]` module was stale; the
libraries still built. That is why nothing downstream complained — 12
tests had simply stopped running, in the crates carrying the attestation
and recompute boundaries.

Fixed by supplying `verb: Verb::Select` at both sites. Both constructions
are the bare `SELECT * FROM STORE "s"` case and both already used the full
eight-modality `OctadSchema`, so the octad was already correct there; only
the verb was missing.

  attest          9 tests, now green
  recompute-wasm  3 tests, now green

Their Cargo.lock files had also drifted (recompute-wasm's recorded only the
two in-repo path crates and no external deps at all — it had not been
resolved since its manifest grew dependencies). Regenerated and committed.

WHY IT ROTTED — coverage map, measured 2026-07-21

  /                              e2e.yml             PARTIAL (see below)
  /src/interface/parse           parse-gate.yml      full
  /src/interface/echidna-client  backend-matrix.yml  needs echidna sibling
  /src/interface/attest          NOTHING
  /src/interface/recompute-wasm  NOTHING

New satellite-crates-gate.yml gates the last two: clippy `-D warnings`
plus tests, over a matrix. Both were verified to pass `-D warnings` cleanly
before the gate was added, so this is a real gate that is green, not an
aspirational one. It mirrors parse-gate.yml's deliberate use of preinstalled
rustup over a third-party toolchain action.

`--locked` is deliberately omitted there for now, and the reason is recorded
in the workflow: the lockfiles are freshly regenerated after a long ungated
drift. It should be restored once a Dependabot cycle has run against them.

ALSO FIXED IN e2e.yml

1. The root job ran `--test property_test` + `--test integration_test` only:
   69 of the root workspace's 102 tests. Every test in tests/e2e_test.rs (20)
   and tests/fuzz_test.rs (13) was skipped. Now `cargo test --workspace
   --all-targets --locked`, verified locally at 102 passed / 0 failed.

2. Removed both "Provide echidna sibling" steps, which cloned a whole
   repository on every run for nothing. `src/interface` — the member that
   carries the external `echidna-core` path-dep — is deliberately not a root
   workspace member, so neither the root tests nor tests/e2e.sh ever resolve
   it. Verified with no sibling present: 102 tests pass, e2e.sh reports 19/19.
   echidna-client remains gated by backend-matrix.yml, which does need it.

CORRECTION TO AN EARLIER FINDING

An earlier read of this repository recorded "0 unit tests; root cargo test is
a fake gate". That was wrong, and was an artefact of truncating the log to its
last lines. The root crate is a re-export facade over fmt + lint, so per-crate
UNIT counts are legitimately zero and the entire surface lives in tests/.
The README's `tests-102 pass` badge is exact. Recorded in the e2e.yml header
so the same misreading is not repeated.

Verification:
  reuse lint                          -> compliant, 459/459
  23 workflows                        -> 0 malformed
  cargo test --workspace --locked     -> 102 passed
  cargo test (parse)                  -> 36 passed
  cargo test (attest)                 -> 9 passed
  cargo test (recompute-wasm)         -> 3 passed
  bash tests/e2e.sh                   -> 19/19, no echidna sibling
                                         150 tests total

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The flagship explanatory document disagreed with the implementation on the
numbering, the vocabulary and the number of levels. All three are corrected
against `src/interface/parse/src/ast.rs` and `src/core/Levels.idr`, which are
canonical because the numbers are wire tags, not prose.

1. NUMBERING WAS OFF BY ONE

   Doc: Level 1 Parse ... Level 10 Linearity.
   Code: ParseSafe = 0 ... LinearSafe = 9, EpistemicSafe = 10.

   A reader who requested level 7 expecting Cardinality Safety would have got
   Effect-Tracking. Every heading, table and diagram shifted down by one; a
   mapping note added so old citations can be translated.

2. THE DOCUMENTED VOCABULARY DOES NOT PARSE

   The document taught `FETCH` and `REMOVE`. Neither appears anywhere in the
   parser. Measured against the real parser:

     FETCH users.name EFFECTS { Read }   -> REJECTED "expected keyword SELECT"
     REMOVE users WHERE ...              -> REJECTED "expected keyword SELECT"
     SELECT * FROM STORE main            -> parses, verb=Select
     ASSERT * FROM STORE main            -> parses, verb=Assert
     DECLARE * FROM STORE main           -> parses, verb=Declare

   The real keyword surface is SELECT / INSPECT / VERIFY / ASSERT / DECLARE /
   RETRACT / MERGE / SPLIT / NORMALISE. Replaced 19 FETCH and 3 REMOVE.

   The implementation is well AHEAD of the prose here: the consonance verbs
   are fully parseable and carry the right verb tag. Only the documentation
   was still speaking the pre-consonance language.

3. THERE ARE ELEVEN LEVELS, NOT TEN — AND THE ELEVENTH WAS UNDOCUMENTED

   L10 `EpistemicSafe` appeared in no document anywhere in the repository. It
   now has a full section, written from `Levels.idr` and `Decide` rather than
   invented: the four `EpistemicRequirement` forms, and the four conditions
   `epistemicConsistentStmt` actually decides (clause present; >=1 agent; every
   referenced agent declared; no direct ENTAILS cycle).

   Its two owed obligations are stated plainly rather than glossed —
   transitive ENTAILS-cycle detection and proposition well-typedness are
   disclosed residuals in VERIFICATION-STANCE.adoc. A safety level that
   overstates itself is worse than no level at all.

   L10 is also flagged as different in KIND. L0-L9 are safety properties: they
   rule out executions that go wrong. L10 is a warrant property: it rules out
   answers the engine is not entitled to give, though every step was
   well-typed. A passive store cannot need it — one witness cannot disagree
   with itself. A consonance engine over eight modal witnesses can.

   Correspondingly, the TypeLL inheritance diagram is corrected: L10 is NOT
   inherited from TypeLL. A UI panel has no federation and no warrant
   question. L10 originates in VCL-UT — the first level this domain
   contributed back to the theory rather than received from it.

4. NEW: THE UPPER LADDER HAS NO SURFACE SYNTAX (measured)

   `parse_statement` hardcodes proof_clause, effect_decl, version_const,
   linear_annot and epistemic_clause to None, while `infer_requested_level`
   awards L7-L10 on exactly those fields. So no parsed statement can reach
   them. Measured ceiling:

     L1  SELECT * FROM STORE a
     L4  SELECT * FROM STORE a WHERE GRAPH.x > 1
     L6  SELECT * FROM STORE a LIMIT 10
     --  EFFECTS / AS OF / USE ONCE / AGENTS  -> all rejected

   Highest level reachable from VCL source: L6. Ladder defines: L10.

   This is a DISCLOSED, fail-closed gap, not silent rot — the parser rejects
   EFFECTS with a message naming the P5a slice and issue #25 rather than
   accepting and ignoring it. Fail-closed is correct. But the honest claim is
   now recorded in the document: eleven levels are specified and proved; six
   are expressible.

Title changed from "The 10 Levels of Type Safety" to "The Levels of Type
Safety" — the count was the false part. The filename is left alone so no
existing link breaks; whether to rebrand around eleven levels is a naming
decision for the owner, not something to settle in a doc fix.

Verification:
  reuse lint -> compliant, 459/459
  all level headings cross-checked one-by-one against ast.rs SafetyLevel
  no residual "10 levels" / "levels 1-N" claims remain

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Naming, counts and status claims brought into line with what is measurably
true, following the owner's decision that VCL-UT = *Usage-Tracked* is canon
and that this repository is the source of truth for the level ladder.

README.adoc
  - Title and 18 body occurrences: VCL-total -> VCL-UT.
  - The "Ubiquitous Type-safe" gloss is removed and explicitly retired. Both
    superseded expansions ("Ubiquitous Type-safe", "-total") are named so they
    stop recirculating. Usage-Tracked is also the accurate one: what
    distinguishes this tier is that resource usage is tracked in the type
    system, L9 LinearSafe via QTT.
  - "-total" is noted as surviving in the crate name `vcl-total` and the Idris
    namespace `VclTotal`; renaming those is invasive and deliberately not
    bundled here.
  - Tests badge 102 -> 150. 102 was correct for the root workspace but counted
    only one of the five workspace roots. Measured: 102 root + 36 parse
    + 9 attest + 3 recompute-wasm.
  - "all 10 levels of type safety" -> eleven, L0-L10, with L10 EpistemicSafe
    identified as a warrant property rather than a safety property.
  - Added the honest qualification up front: eleven levels are specified and
    proved, six are expressible (surface-syntax ceiling is L6).
  - Pipeline diagram: "(10 progressive levels)" -> "(11 levels, L0-L10)".

  Left deliberately unchanged: the four "10 levels" references that describe
  TypeLL. Under the corrected framing those are correct — TypeLL defines
  L0-L9, exactly ten, and VCL-UT contributes the eleventh.

ROADMAP.adoc — rewritten, because nearly every claim was false
  - "Parser work not yet started" was false: a Rust parser exists with 36
    green tests, gated by parse-gate.yml under a SPARK-grade clippy set.
  - "Idris2 parser with totality proof" was never what shipped. The Idris
    corpus proves; the Rust port re-establishes independently.
  - Every milestone box was unchecked despite most of v0.1-v0.3 being done.
    Boxes now reflect measured state.
  - Level numbering corrected 1-10 -> L0-L10 throughout.
  - "VeriSimDB 6-modal query planner" -> octad transition planner.
  - Added a measured status table and a "Nearest Work" section ordered by
    value: surface syntax for L7-L10; wiring vclt-gate into VeriSimDB;
    discharging the two disclosed L10 residuals; retiring the HEXAD keyword.
  - New v0.4.0 milestone for the consonance level, which the old roadmap had
    no place for at all.

Cargo manifests (8 files)
  - repository = ".../vql-ut" -> ".../vcl-ut".

  Correction to an earlier note: that URL does not 404. GitHub still redirects
  vql-ut -> vcl-ut after the rename. It is stale rather than broken, and the
  reason to fix it is that the redirect stops working if the old name is ever
  reused. Measured with `gh api repos/hyperpolymath/vql-ut`, which returns
  full_name "hyperpolymath/vcl-ut".

  CHANGELOG.md's "still hyperpolymath/vql-ut" line is left alone: it is a
  dated historical entry, not a live claim.

Verification:
  reuse lint                       -> compliant, 459/459
  cargo test --workspace --locked  -> 102 passed

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…lication

The strategic deliverable. Two strands kept deliberately separate because they
have different success conditions: Strand A succeeds if the theoretical claim
is novel and defensible; Strand B succeeds if VeriSimDB is measurably safer.
Neither implies the other.

STRAND A — the theoretical claim

Argues that consonance languages are a distinct class, not query languages
with extra types, on three grounds: statements are propositions and epistemic
requests rather than read requests; retraction is not deletion and drift is a
typed condition rather than an error; and well-typedness stops being
sufficient once several modal witnesses can disagree.

The gap in the world is stated honestly. Type-safe query languages are a
crowded, mature field — LINQ, Quill, Diesel, jOOQ, TypeQL, EdgeQL for L0-L5,
and substantial literature for effects, temporal, linear and cardinality. A
"ten levels of query safety" paper enters that field as a thorough synthesis
and will be read as one. What none of them do is type WARRANT: every one
assumes a single source of truth that cannot disagree with itself. Epistemic
logic, provenance and truth-maintenance all exist, but beside the query path —
never as a type that can refuse a statement.

The decisive evidence came from the code rather than from taste. The ladder
has eleven levels; the eleventh is not a query-safety property; and it is the
one level NOT inherited from TypeLL, because a UI panel has no federation and
so no warrant question. A framework whose eleventh member does not fit its own
name is telling you the name is wrong.

WHITEPAPER REFRAME IS A PROPOSAL, NOT AN EXECUTED REWRITE

Deliberate. The direction is settled, but how a paper argues its claim is the
author's call and is the least testable, highest-blast-radius change available
here. The 1,909-line .tex is untouched. What is offered is a section-by-section
structure and a complete draft abstract, for approval first.

STRAND B — the VeriSimDB application

Opens with the uncomfortable fact: VCL-UT delivers nothing to VeriSimDB at
runtime today. The proof corpus is real, the parser is real and gated, the
gate binary exists and Contract v1 is frozen — but the seam is built on one
side only. The producer is finished and the consumer was never written.

Defends the subprocess/JSON-line seam against the obvious objection that it
looks unfashionable, using evidence from this repository: src/interface's
external path-dep on an echidna sibling is exactly the build coupling the
CLI seam avoids, and it is why echidna-client cannot even be covered by
Dependabot.

Sets out what VeriSimDB actually gets — a fail-closed admissibility check
before statements touch consonance state; one level ladder instead of two
divergent ones; independently-verifiable attestation; and vocabulary
discipline — and gives a migration path that keeps VeriSimDB's genuinely good
ReScript surface parser and diagnostics while replacing only the verdict.

Two concrete defects, both located precisely:
  - VCLTypeChecker.res:60 builds the default context with six modalities
    though the type admits eight. Provenance and Spatial are silently absent
    from every default type-check. The hexad-to-octad migration reached the
    variants and stopped before the defaults and the names — HexadType is
    still the type name in four places.
  - The seam is unwired (zero vclt-gate references in verisim-api/src/vcl.rs).

Sequenced plan, ordered by value per unit of risk, with the repository each
item belongs to marked — items 3-5 are VeriSimDB changes and cannot be
committed from this repository.

Closes with a falsification section, so the plan can be argued with rather
than assumed: if VeriSimDB's ReScript checker is materially more capable than
the corpus, "vcl-ut is source of truth" costs capability; if subprocess
latency is material on the hot path, the CLI seam is wrong and should be
measured BEFORE the wiring work rather than after; and if the consonance claim
has prior art under another name, Strand A weakens to a synthesis claim. The
prior-art search behind the gap argument was not exhaustive and says so.

Verification:
  reuse lint -> compliant, 460/460
  every factual claim in the Ground Truth table measured against the working
  tree on 2026-07-21, including the two VeriSimDB defects

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@hyperpolymath
hyperpolymath marked this pull request as ready for review July 21, 2026 13:04
@hyperpolymath
hyperpolymath merged commit a307b0e into main Jul 21, 2026
18 of 20 checks passed
@hyperpolymath
hyperpolymath deleted the worktree-vcl-ut-workup branch July 21, 2026 13:05
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.

1 participant