Checkpoint 2026-06-05: reconciliation + Coq proof-debt (machine-checked) + REUSE licence cleanup

[hyperpolymath]

Durable session checkpoint (survives context compaction). State + owed work as of 2026-06-05.

Branch reconciliation (owner-approved plan)

• Supersede PR docs: high-standards baseline (EXPLAINME + 6a2 refresh + dust/Dustfile) #107 with a rebased test/ci-full-verisimdb PR carrying: EXPLAINME.adoc, 6a2 refresh, k9→self-validating rename, bot_directives/*.a2ml, contractiles/dust/Dustfile, CI timeout-minutes — with docs: high-standards baseline (EXPLAINME + 6a2 refresh + dust/Dustfile) #107's STATE proof claim corrected (below) and the throwaway TEST_CI_VERIFY.md dropped.
• Drop redundant branches: docs/explainme-6a2-baseline-2026-06-02 (== docs: high-standards baseline (EXPLAINME + 6a2 refresh + dust/Dustfile) #107 head, fully contained) and test/ci-timeout-fix-… (subset).
• docs: high-standards baseline (EXPLAINME + 6a2 refresh + dust/Dustfile) #107 held from auto-merge until its STATE is corrected.

Coq proof-debt — machine-checked 2026-06-05 (coqc 8.18.0; all 9 modules compile; Print Assumptions)

Corrects #107's blanket "8/8 closed / foundation-pack DONE". Honest per-module status:

• 0-axiom (fully closed): Transaction (C2), VCL (V2).
• Carrier-polymorphic / closed-mod-standard-primitives: Octad O-series+R1–R3 (ident,mval only), Provenance P2/P3 (abstract hash — does not even use collision-resistance), WAL C7 (decidable-eq).
• Structural over uninterpreted operations (not implementation-linked): Drift D1/D2 (abstract score algebra + uninterpreted f_*_drift), Normalizer N2 (uninterpreted winner/drifted).
• Crux currently an axiom: Planner/PlannerSemantic Q1 (optimize_is_permutation).
• OWED (real proof-debt): (1) discharge the Q1 optimize_is_permutation axiom; (2) add a Coq-model ↔ Rust-impl refinement link (instantiate the Parameters with production code) — the missing analogue of vcl-ut's Refl wire-conformance.
  NB: coq-build.yml's per-module assumptions whitelist guard is rigorous and honest — keep it as the gate.

Licence / REUSE (REUSE 6.2.0 audit 2026-06-05; reuse lint: FAIL) — far cleaner than vcl-ut

Policy: code = MPL-2.0, docs = CC-BY-SA-4.0. (Tree is already ~uniform MPL-2.0; GitHub Licensee correctly shows MPL-2.0.)

• P1: add LICENSES/MPL-2.0.txt (+ CC-BY-SA-4.0.txt) — their absence is the lint failure.
• P2: 9 connectors/shared/json-schema/*.json put SPDX in a $comment field → parsed as invalid MPL-2.0"; move to REUSE.toml/.license sidecars.
• P3: playground/package.json "license":"AGPL-3.0-or-later" → MPL-2.0 (lone contradiction).
• P4: SPDX headers on ~12 docs/root files lacking them.
• P5: docs/security-lessons.lgt + CONTRIBUTING.md code-example double-stamps → REUSE-Ignore wrap.
• Install the provable gate (REUSE + k9/Nickel policy + pre-commit + required CI), replacing the toothless governance / Licence consistency.

Docs/STATE currency

• 6a2/STATE.a2ml: overall-completion 0 (bug) + stale coverage 42.6 (cf vcl-ut/verisimdb Elixir suite remediation: integration opt-in, 10 consensus/Raft failures, unit coverage #110); refresh on the supersede branch.
• .claude/CLAUDE.md says machine-readable are .scm — they're .a2ml (in 6a2/). Fix.
• machine_readable gap vs vcl-ut: missing anchors/ANCHOR.a2ml, ai/, agent_instructions/, compliance/, configs/, policies/, scripts/, and the full contractile set — gap-fill to estate-canonical.

Ref: https://claude.ai/code/session_01W9Voe3JceP66Bna9FT4jME

[hyperpolymath]

Verified 2026-07-21 — licence section fully closed; Coq proof-debt confirmed still open

Re-measured every claim in this checkpoint with the actual tools rather than by inspection.

Licence / REUSE — P1 through P5 are all DONE

$ reuse lint
* Bad licenses: 0        * Deprecated licenses: 0
* Missing licenses: 0    * Unused licenses: 0
* Used licenses: MPL-2.0, CC-BY-SA-4.0
* Files with copyright information: 773 / 773
* Files with license information: 773 / 773
Congratulations! Your project is compliant with version 3.3 of the REUSE Specification :-)

reuse 5.0.2, exit 0. LICENSES/ contains exactly MPL-2.0.txt and CC-BY-SA-4.0.txt — matching the stated policy (code MPL-2.0, docs CC-BY-SA-4.0), with no stray third licence. REUSE Compliance is green in CI. P1 (missing licence texts), P2 ($comment SPDX in the 9 JSON schemas), P3 (the playground/package.json AGPL contradiction), P4 and P5 are all resolved.

⚠️ One caution: the local checkout carries an unpushed sweep commit adding LICENSES/AGPL-3.0-or-later.txt. Nothing uses it, so it would turn this green reuse lint into an Unused licenses failure. Do not push those sweep commits.

Coq proof-debt — machine-checked again, under a newer compiler

All 9 modules compile under coqc 8.20.1 (this checkpoint used 8.18.0):

Octad.v OK   Drift.v OK   WAL.v OK        Transaction.v OK   VCL.v OK
Provenance.v OK   Normalizer.v OK   Planner.v OK   PlannerSemantic.v OK

just -f formal/Justfile check-assumptions — the per-module Print Assumptions whitelist gate — passes, exit 0. Your assessment that this gate is "rigorous and honest" holds up: it does compare each module's actual assumption set against a named whitelist, and it does fail on anything outside it.

The Q1 crux is still an axiom. optimize_is_permutation remains Axiom in both formal/Planner.v:63 and formal/PlannerSemantic.v:94, and is applied at five call sites. Planner.v:102 even records the intent — "Anything else fails the CI guard." So OWED item (1) is untouched, and OWED item (2), the Coq-model ↔ Rust-impl refinement link, has no artefact in the tree.

Both remain genuine, correctly-described proof-debt. Neither is addressed by #185, which is scoped to CI and the #47 residual.

Still to verify

I have not re-checked the branch-reconciliation plan (PR #107 supersede) or the 6a2/STATE.a2ml overall-completion 0 / stale-coverage bug. Those are the live remainder of this checkpoint.