Skip to content

FORCODEX.md

Latest commit

 

History

History
322 lines (276 loc) · 18.4 KB

FORCODEX.md

File metadata and controls

322 lines (276 loc) · 18.4 KB
Raw

FORCODEX — minidregg handoff, 2026-08-11

Overnight convergence — latest authoritative status

The recovered swarm is integrated through cd0c336; the tree-wide theorem-footprint gate is restored in e6abd03. The exact committed-source hbox build E-20260812T013903-51208-hbox-cd0c336de51b-lake completed 3,354/3,354 jobs with command and source-integrity exits zero. The subsequent exact census run E-20260812T014653-64736-hbox-cd0c336de51b-bash rebuilt the same tree, passed its self-test, and reported 1,440 declared carriers, 644 outside-home producers, five audited non-targets, and 591 nominal actionable carriers. That last number remains a reachability signal, not a backlog: its leaders include nested values already constructed by surrounding witnesses, configuration indices, explicit security premises, and legacy carriers.

Material changes since the previous 537b273 snapshot:

  • The bounded forward-link path now also has a Lean-owned SQLite transaction model and a dependency-free Rust adapter tested across separate processes. Exact hbox evidence passes six lifecycle tests: rollback before commit, lost-response reopen/retry, concurrent conflicting transaction/no-overwrite, corruption/torn bytes, oversize rejection, and the exact 14-byte Lean fixture. This exercises a real SQLite rollback-journal path; it does not prove SQLite, FFI, POSIX/fsync, stable media, or power-loss refinement.
  • Authenticated settlement finality binds canonical candidate bytes and derived slots to current authority roots, versioned key directories, key/policy epochs, and revocation state. A concrete three-signer witness includes rotation, handoff, stale-key, revoked-key, wrong-slot, and wrong-payload teeth. Credential envelopes now reach the semantic lifecycle through an opaque/fallible signature boundary. EUF-CMA, key custody, signature implementation, authenticated transport, quorum availability, and liveness remain explicit premises.
  • Reactive terminal outboxes now have a stable message/attempt/receiver/ack state machine joined to the concrete leased Hyperdocument scheduler. Duplicate delivery is exact replay and acknowledgements bind the installed outbox bytes; scheduler fairness, transport, authenticated ACK delivery, and eventual progress are deliberately outside the safety theorem.
  • Declared create/write/move execution has a concrete four-entry, sixteen-shard V1 page representation with exact cSHAKE roots and a registry, plus a statement- specific AIR descriptor. Its reflection theorem returns to the existing ordered executor and binds declaration bytes, policy id/epoch, pre-root, sparse observed values, guards, and modulus bounds. It is not a second interpreter or a policy verifier.
  • Bounded forall/exists policy views compile into the existing first-order Pred.all/Pred.any AST and reuse committed-policy reflection. Cross-slot affine predicates, coordination/merge classification, and disclosure-mode proof evidence remain real design gaps.
  • Raw history now exposes the exact executed cSHAKE-collision endpoints and names the smallest honest full-query same-coin realization sufficient for the birthday theorem. A negative theorem prevents relabeling deterministic cSHAKE output as a fresh uniform slot. No Merkle/ROM price is claimed until a genuine sponge/ROM coupling records the complete fresh-query table.
  • Ext6 has nonzero versioned suite/controller/codec pins and a positive controlled receipt, but semantic proof admission is still equivalent to supplying the exact eight-event same-coin security carrier. BFV and NoteSpend remain correctly non-deployable at their currently authorized zero suite pins.
  • The finite finalized-domain crawler now proves returned backlinks iff declared backlinks inside its exact manifest and handles ordered ingest, replay, successor deletion/rebinding, forks, stale cursors, and missing pages. It does not generalize finite declared coverage into global web/history completeness.
  • Loom's exact one-third-UD proximity error is sharpened to (floor(delta*n)+1)/|F| and attained by the landed F5 example. The original oracle-log obligations are exhibited only at the universal slack price one; their intended low-price forms remain machine-refuted rather than papered over.

The trust audit found 58 recovered modules using bare #print axioms. Commit e6abd03 converts all of them to exact #guard_msgs pins using the immutable hbox output; a mechanical scan now reports zero bare theorem-footprint prints. There are no new axiom declarations, sorry, or semantic/native-refinement shortcuts.

The strongest honest deployment-shaped result remains the bounded local forward-link slice. The new signature/finality, SQLite, crawler, AIR, and outbox surfaces make its boundary narrower and more explicit, but do not create external network finality, a physical durability proof, production key custody, a complete ROM coupling, a secure nonzero proof suite, or an end-to-end service SLO.

The shared worktree still contains a separately owned Uwueave/Preoscript Projection-V2 lane (Compiler.lean, Lake metadata, prover registry/generated/test files). Codex has not staged, reset, or included any of it. Hbox is the active heavy worker. Persvati is currently CPU/RAM-idle but its root filesystem is 100% full (about 487 MiB free), so do not dispatch builds there until its storage is cleared by an owner.

Historical: first Codex integration refresh — later on 2026-08-11

The handoff below was exactly the right warning at 25d2a5a, but it is now a historical diagnosis rather than current status. The follow-up swarm did not paper over the empty carriers; it changed the representations, built witnesses, and retained the impossibility results as regression teeth.

What changed:

  • CellState.LogicalState now uses one canonical dependent finite map. The four deployed schema materializers and cells are exhibited (83d889f, e5ccb49), with the old total-function cardinality obstruction retained as a theorem.
  • The Hyperdocument causal layer is no longer unexplored: a real semantic family, accepted genesis/append path, and canonical authority projection landed in 430d591 and c15d2a3.
  • Policy selection is committed by authority state. AuthState binds a policy root/address, authorization retains exact membership/address evidence, the compiler derives the committed PredCompile path, and generated artifacts were refreshed (9faa3cf, 47d9e4c, 54e331c).
  • The old SemanticHistoryTower256CheckpointGame.JointGameFamily is not an inhabitation target. 62c0997 proves it impossible at every positive Merkle height: completeness plus universal PositionBinding would inject more words into the 256-bit cSHAKE root range than that range can contain. The honest replacement is the raw path in 384b1bd, which retains equivocation and gives a same-coin four-event ledger with extracted collision and transport obligations.
  • Kernel semantics grew actual frontiers rather than more callbacks: canonical resource effects (4119cf4), durable payload/read-guard intents (d8d4e53), authority-guarded Hyperdocument commit (deebdbb), fee-first admission (c3854a6), heterogeneous cell lifecycle (604a3ca), scoped history projection (b4a4866), and an executable two-leg declared-hyperedge-to-typed bridge (8e84438).

Current verification: local lake build Minidregg is green at 3,264 jobs; import-boundary, carrier-census self-test, and git diff --check are green. Exact committed-source remote replays are recorded in the evidence ledger; production cryptography, physical storage refinement, and consumer cutover remain explicit.

The highest-value next stretches are now:

  1. instantiate the raw proof/controller path with concrete executable verifier, transcript transport, and priced cSHAKE/PCS/ROM events;
  2. join reactive finalization to durable settlement with a canonical terminal promise cell and race/exclusivity semantics;
  3. exhibit a real two-parent Hyperdocument merge/publication and then cut over one user/agent workflow end to end;
  4. refine durable payload/WAL semantics into a framed physical implementation with torn-write recovery, replication/finality, and liveness stated separately; and
  5. replace existence codecs/roots with versioned deployed codecs and cryptographic binding, without weakening the semantic constructions they currently witness.

Everything below remains useful as the original fault report and as a record of the traps that found the bugs. Read its present-tense status claims as applying to the tree named in its opening paragraph.

Written by claude at the end of a long 08-10 session. Not a status report: the things here are the ones that will change what you do, in the order they'll change it. GOAL.md has the full trail; ATLAS.md still has the sixteen laws and is unchanged.

Tree state at handoff: 25d2a5a (mine) under e9c7f3a (ember's Pages site). lake build Minidregg green at 3245 jobs, import boundary green, 861 pinned axiom footprints, zero bare #print axioms, zero sorry. 289 Lean files, 128,209 lines.

1. Read this before you believe any theorem about a cell

Every CellState.Materializer in this tree is provably empty, at all four schemas: CredentialAuthorityState.schema, Hyperdocument.cellSchema, HyperdocumentEventLog.cellSchema, and DeclaredTurn.effectSchema. The proofs are in Theory/MaterializerCardinality.lean and Kernel/EventLogMaterializerLimit.lean.

The argument is three lines. A materializer carries LawfulCodec (LogicalState S); decode_encode makes encode injective; so a materializer is an injection from the schema's entire state space into List UInt8, which is countable. Each schema has infinitely many two-valued fields, so its state space is not.

Consequence: every theorem quantified over a Materialized cell at a deployed schema is vacuously true. Credential issuance, attenuation, revocation, epoch rotation; the whole Hyperdocument operations layer; the atomic two-cell publication; the flat multi-incidence turn. Nothing is false. Nothing was checked either, and vacuous theorems read exactly like real ones — which is why this survived a year.

If you touch anything downstream of a cell, that is the fact to hold. The two schema modules say it in their own headers now, and README.md / PROJECT.md no longer claim maturity for those layers.

2. The instrument that would have caught it — use it

scripts/check-carrier-census.sh (wrapping scripts/CarrierCensus.lean) walks the environment and answers: which carriers are quantified over somewhere and produced nowhere outside their own defining module?

Today: 974 carriers, 338 produced outside home, 112 skipped as trivially inhabited, 521 unwitnessed and load-bearing, ranked by how many declarations quantify over each. The ranking is the product; the raw list is a dump.

246  CredentialAuthorityState.ProjectionUniverse
224  CausalVersionDag.SemanticFamily        <- nobody has looked at this layer
206  CausalVersionDag.Anchor
182  DeclaredHyperedge.Declaration
161  Tower256AdditiveFriController.MerklePcs
133  HyperdocumentOperations.Config
 92  HyperdocumentOperations.Accepted
 68  SemanticHistoryTower256CheckpointGame.JointGameFamily

Three things about it you need:

  • It is a reachability query, not a proof of emptiness. An unwitnessed carrier may be perfectly inhabitable and merely unbuilt. JointGameFamily is probably that. The four materializers needed a separate emptiness proof, and that is still the only way to know.
  • It has its own teeth. selfTest pins six carriers whose answer is known by construction and fails the run if any flips. A census that quietly stopped detecting would otherwise look exactly like a clean tree.
  • The wrapper fails on a broken instrument, never on the count. 521 is today's honest number, not a threshold. Gating it would reward hiding carriers instead of witnessing them.

Companion discipline, already enforced: every #print axioms in the tree is #guard_msgs-pinned, so an axiom regression fails the build rather than printing a different list into a log nobody reads. Use #guard_msgs (whitespace := lax) in — Lean wraps the axiom list for long declaration names and a strict pin passes for short names while failing for long ones.

3. In flight: the LogicalState migration

ember chose the design on 08-10: Option-valued sparse encoding as the primitive, with schema-side and state-side defaults derived on top as views rather than as rival cores. Her framing, and it's the right one — there is nothing to choose.

Landed:

  • Theory/SparseLogicalState.lean — SparseState with read (Option-valued) and readD (takes a default, gives either convention). readD_empty proves "no default" and "default everywhere" are one object seen two ways. nonempty_lawfulCodec_sparse_effect carries it to an actual codec for DeclaredTurn.effectSchema, the schema proved empty as a total function.
  • Theory/StoreFiniteSupport.lean — the boundary invariant. Scoping changed the step's shape: EffectDeclaration.Store has 113 references but only 20 cross into materialization, and the other 93 are semantics, which needs no codec. So the store stays a total function where it does semantics, and finite support is required exactly at the boundary. sparseOfStore_readD is the faithfulness theorem: read the sparse state back with the zero default and you get the original store at every key.

Remaining for step 1, mechanical: point DeclaredTurn's materialization at sparseOfStore, thread finitelySupported_ofZero through the 20 boundary callers, switch effectSchema's cell to SparseState.

Steps 2–4 are the other three schemas, in the order and with the reasoning written into SparseLogicalState.lean's footer. Each needs a Countable (Sigma S.FieldType) instance that does not exist yet — Countable AuthorityField alone wants a deriving instance, and the capability value types reach Countable through Finset. That plumbing is part of the step, not a precondition someone else supplies.

materializer_nonempty_iff_countable means there is exactly one criterion: whatever replaces the total function is correct iff it lands in a countable type. The refactor cannot fail for a subtle reason.

This is a staged migration with a named endpoint: deletion of the total-function field in CellState.LogicalState. It is a deliberate temporary twin. If you find yourself extending both shapes, stop — that is the state the endpoint exists to prevent.

4. Traps that cost me hours

  • Tailscale lies about the build boxes. It reported hbox offline 15d and persvati 42d while both were up (25 and 31 days) and reachable over plain ssh hbox / ssh persvati on mDNS. The QUIESCELOG blamed a missing persvati replay on NeedsLogin for weeks; nobody had tried the front door. There is now one persvati replay: E-20260810T201633-25551-persvati-9d61e61aa1f1-lake, all exits 0.
  • hbox is yours and minidregg stayed off it. At handoff it was load 22.5 on 24 cores, 96 of 123 GiB, 38 sessions. Everything remote went to persvati. If datacake is not supposed to be that hot, that is worth a look independently.
  • A stale .olean manufactures a RED, not just a green. lake env lean on an edited file writes no olean, so an importing file silently loads the previous version. I spent several cycles convinced a canonical post-root refused to move; the witness was right and the cache was old. lake build <Module> first, then re-check.
  • Grep the TYPE, not the names you expect. I built a byte-codec toolkit in Theory/ on the claim the repo had two lawful codecs. It has a complete and better one — Compiler.Tower256ConcreteBackend.StreamCodec, a prefix codec with the append law, xmap/product/sum/list/nat in base-255. I had grepped for five spellings I expected and confirmed my own expectation. Reverted in 6efe4f3; the request/Action/Declaration codecs were rebuilt on StreamCodec in Compiler/, where byte transport belongs.
  • Section variables silently swallow declarations. In one module a variable (transcript : ...) followed by structure/defs produced "unused variable" warnings and the declarations never entered the environment, with no error. Explicit binders per declaration fixed it. If a #check says a name you just defined is unknown, suspect this before suspecting yourself.

5. What is actually open, ranked

  1. The census's top entries. CausalVersionDag.SemanticFamily (224) and Anchor (206) are a layer nobody has examined; they were the census earning its keep on its first run. Check whether they are unbuilt-but-inhabitable or another MaterializerCardinality.
  2. Migration step 1's mechanical remainder, then steps 2–4.
  3. JointGameFamily — defined in one file, consumed in two, constructed nowhere, so the four-event end-to-end price is conditional on a carrier nobody has built. Unlike the materializers this is unexhibited, not proved empty, and its fields look inhabitable.
  4. QUIESCELOG.md resume item 5 (cut over one user/agent workflow) is blocked, and the block is item 1 of this list: the workflow's cells are uninhabitable until the migration lands.

6. Conventions worth keeping

  • scripts/local-check.sh HEAD -- lake build Minidregg for isolated committed-source evidence; scripts/remote-check.sh persvati HEAD -- ... for cross-machine. The remote schema has no dependencyIntegrityExit — it pins the seed by revision manifest and a run-private tree — so don't quote it as the local runner's third exit code.
  • Witnesses carry refutations. Every witness added on 08-10 ships teeth showing its equations are constraints, because an inhabitation theorem alone is satisfied by a carrier that does nothing.
  • Commit named pathsets, never git add -A; prose messages via git commit -F (backticks in -m get command-substituted by zsh).
  • Unsigned commits are expected while working autonomously.

One editorial note, since it shaped everything above. The best result of the session did not come from proving something — it came from trying to build something and failing. Four emptiness proofs and a census fell out of one failed attempt at a witness. The corresponding smell: if a construction feels unreasonably hard, ask whether it is possible before assuming you are bad at it.