From ec2ce3de8bd15b3dbd78db7f7b213e6858ae1027 Mon Sep 17 00:00:00 2001 From: James Ross Date: Tue, 20 Oct 2026 16:15:44 -0700 Subject: [PATCH 1/2] docs(design): revise DL-0159 after review Review ruling: enhance. Approve schema 2's direction; correct before freezing it; withdraw the previous save and recovery guarantees. - Identity follows Echo's ContentAddressV1; a head's id commits to the fact it stores and its actual edges, including the empty-root case. - New accepted host basis (Buffer -> HostBasis) with explicit transitions; lastExport only records what Jim last exported. - Filesystem claims separated: observation, attribution, exclusion. v1 export is best effort and says so; an exclusive profile obstructs when unavailable. Recovery classifies observations and never invents an Export. One unresolved, fenced export per file binding. - Explicit v1 resource envelope; ResourceLimitExceeded, ClosureInsufficient and MalformedRope stay distinct. - Reachability starts at the worldline root; retained material is named and acquired before the operation that needs it. - Path classification by observable mechanics; the divergence barrier follows the disputed dependency. - Two acceptance gates: representation and file crossing. Drafts: ContentAddressV1 helper, HostBasis fact and edges, head identity from stored fact and edges, author-side effect normalization, envelope check, closure failures classified. Draft README drift repaired. Owner issues: echo#926 echo#927 echo#928 edict#260 edict#261 edict#262 edict#263 #377 #378; ideas #379-#382. --- CHANGELOG.md | 10 + docs/design/0159-edict-rope-representation.md | 923 ++++++++++-------- edict/replace-range/draft/README.md | 80 +- edict/replace-range/draft/Reference.edict | 7 +- edict/replace-range/draft/ReplaceRange.edict | 22 +- edict/replace-range/draft/Rope.edict | 18 +- edict/replace-range/draft/Text.edict | 47 +- 7 files changed, 659 insertions(+), 448 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index bb241f22..6039641c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2,6 +2,16 @@ ## Unreleased +- Revised DL-0159 (Edict-authored rope) after review. Schema 2's direction + stands; identity now follows Echo's `ContentAddressV1`; a new accepted host + basis keeps "what Jim works against" apart from import provenance and + `lastExport`; filesystem claims are limited to what their evidence supports + (a best-effort export profile, recovery that classifies instead of inferring + writes, one fenced export per file binding); the v1 resource envelope and its + three failure classes are explicit; and acceptance splits into a + representation gate and a file-crossing gate. The draft Edict sources and + README follow, and every capability the rope needs has an owner issue. + - Jim now runs on current Echo and Edict. The native host had been pinned to Echo `90f63ae` (2026-07-17), 1054 commits behind main, so Jim never exercised the Echo being built. It now builds against Echo main `0faaf58`, with contract diff --git a/docs/design/0159-edict-rope-representation.md b/docs/design/0159-edict-rope-representation.md index 312bc578..0b48b863 100644 --- a/docs/design/0159-edict-rope-representation.md +++ b/docs/design/0159-edict-rope-representation.md @@ -7,7 +7,7 @@ status: "draft" owners: - "@flyingrobots" created: "2026-10-15" -updated: "2026-10-15" +updated: "2026-10-20" --- # DL-0159 - Edict-Authored Rope Representation @@ -15,49 +15,64 @@ updated: "2026-10-15" ## Linked Issue - [#296 Author and prove Jim's first Edict operation: `ReplaceRange`](https://github.com/flyingrobots/jedit/issues/296) -- [#302 Author ReplaceRange as Jedit-owned Edict source](https://github.com/flyingrobots/jedit/pull/302) -- [#350 Reopening a file silently reuses a stale rope](https://github.com/flyingrobots/jedit/issues/350) -- Echo decision: [Application operation semantics authored in Edict source](https://github.com/flyingrobots/echo/blob/docs/edict-authored-operation-effects/docs/topics/GeneratedRules.md#application-operation-semantics-authored-in-edict-source) - (proposed for review) -- Echo design: [Authored Operation Effects](https://github.com/flyingrobots/echo/blob/docs/edict-authored-operation-effects/docs/architecture/authored-operation-effects.md) - (proposed for review) +- [#350 Reopening a file silently reuses a stale rope](https://github.com/flyingrobots/jedit/issues/350) (closed by #356) +- Echo design: [Authored Operation Effects](https://github.com/flyingrobots/echo/blob/main/docs/architecture/authored-operation-effects.md) + (on main; its own status line says not implemented) +- Echo implementation: [echo#921 exact-parent authored graph effects](https://github.com/flyingrobots/echo/pull/921) (draft) ## Decision Summary -The rope that Jim's Edict source reads and writes uses a new text schema, -`jedit.text.schema@2`. Every structural relation is an Echo edge; atoms carry -only scalar facts. Atom payloads use Echo's canonical CBOR v1. Immutable nodes -are content-addressed over their facts and their ordered children, so unchanged -subtrees keep their identity across edits. Every head is anchored to the file -coordinate and the host digest of the bytes its lineage was imported from. - -The graph holds the **current** rope only. Echo's ticks and receipts are the -causal history of how it got there; Jim does not duplicate that history as a -chain of reachable heads. Whether superseded nodes stay retained, and how far -back a past state can be reconstructed, is Echo's retention and replay -contract, not a property of rope topology. +Review ruling (2026-10-20): **enhance**. The architectural direction is +approved; schema 2 is not frozen until the corrections below hold and the +representation gate passes. The filesystem save and recovery guarantees of the +previous revision are withdrawn and replaced by the file-crossing contract +below. + +Jim's Edict-authored rope uses a new text schema, `jedit.text.schema@2`: + +- Every structural relation is a typed Echo edge; atoms carry only scalar + facts, encoded with Echo's exact canonical codec profile. +- Immutable nodes are content-addressed under Echo's generic bridge identity + law `ContentAddressV1`, so unchanged subtrees keep their identity across + edits and both Edict and Echo compute the same ids from the stored facts. +- The graph holds the **current** representation and its current obligations + only. Echo's ticks and receipts are the causal history; Jim keeps no chain of + predecessor heads. +- Four file facts stay apart: import provenance, the current logical content, + the **accepted host basis** Jim works against, and the evidence of each + export. + +The design has two acceptance gates. The **representation gate** covers the +schema, identity, structural invariants, authored effects, resource behavior, +atomic publication, and recovery of edits. The **file-crossing gate** covers +observation evidence, the accepted host basis, the export lifecycle, +retention, interference guarantees, and reconciliation. Passing the first does +not imply anything about the second. This replaces nothing in production yet. `jedit.text.schema@1` (DL-0158), the -native planner, and its oracle remain the current truth. Schema 2 is the -representation the authored source in `edict/replace-range/draft/` targets. +native planner, and its oracle remain the current truth until the authored rope +passes the representation gate and cuts over; then the native law is deleted. ## Sponsored Human A developer editing in Jim wants every edit to be explainable and recoverable from Echo's own history, without trusting a native planner whose structure Echo -cannot see. +cannot see, and wants Jim never to claim more about their file than it knows. ## Sponsored Agent -An agent needs the current rope, and the file bytes it descends from, to be -reachable through typed graph structure, and needs past edits to be explained -by Echo's causal history, so it never decodes application JSON. +An agent needs the current rope, and the identity of the file bytes it +descends from, to be reachable through typed graph structure from the worldline +root, and needs past edits explained by Echo's causal history, so it never +decodes application JSON. When it needs earlier bytes, it needs a named +retention contract that says whether they are still available. ## Hill A reviewer can check, from this document and the draft source alone, which -node, edge, and atom an Edict-authored `ReplaceRange` reads and writes, and -which guarantees about past versions come from Echo rather than from the rope. +node, edge, and atom an Edict-authored `ReplaceRange` reads and writes, how +every id is computed, which resource envelope it supports, and which claims +about the file are backed by which evidence. ## Current Truth @@ -70,338 +85,458 @@ Schema 1 (DL-0158, `native/jedit-echo-host/src/records.rs`): - Per-node metrics include UTF-16 length, which only the native rope reads. - `BufferFact` is the only mutable node; it names the canonical head by id. -Echo facts that constrain the choice (Echo main `9b3b9396`): +Echo facts that constrain the choice: - The state root walks outgoing edges from the worldline root. Nodes reachable only through ids inside atom bytes are excluded from it (`crates/warp-core/src/snapshot.rs`, `worldline_state.rs`). - Echo's attachment law forbids hiding structural dependencies in payload bytes (`crates/warp-core/src/attachment.rs`; `docs/invariants/warp-two-plane-law.md`). -- Edge ids are caller-chosen 32 bytes; a node may have many incoming edges. -- Nothing is garbage-collected; reachability decides only what the state root - commits. - -So schema 1's current rope is itself invisible to the state root, and Edict -would have to parse JSON to follow a child. +- The bridge design fixes `ContentAddressV1`: content node ids, content edge + ids, and mutable slot edge ids, each BLAKE3 over its own domain + (Authored Operation Effects, *Identity laws*). Echo recomputes every id a + proposal creates and refuses a mismatch. +- The bridge refuses duplicate effect targets, including identical `ensure`s + (*EffectProposal*), and caps one Action batch at 128 patch operations + (*Current implementation*). Oversized proposals are refused, not split + across Ticks (*Basis, budget, retries*). +- The bridge preserves keyed readability of unreachable records until a + witnessed or versioned semantic mechanism changes it. Unreachable is not + permission to reclaim. +- Continuum import dispatch is not wired and returns `NOT_SUPPORTED` + (`continuum-transport.md`, *Import law*). Participant-history braids are an + accepted design whose implementation does not yet provide separated + Hold/Judge/Apply or conflict barriers. + +So schema 1's current rope is invisible to the state root, and Edict would have +to parse JSON to follow a child. ## Problem Jim's rope must be authored in Edict and realized by generic Echo machinery. That needs a representation whose structure Echo can see, hash, and retain; -whose bytes have one canonical spelling; and whose identity is honestly related -to the file it came from. +whose bytes have one canonical spelling; whose ids both implementations compute +identically; and whose relationship to the file is stated at exactly the +strength its evidence supports. ## Scope -- Fact types, codec, identity law, edge types, and metrics for schema 2. -- The head-to-file anchor. -- Which generic Echo and Edict capabilities this representation requires. +- Representation gate: fact types, codec, identity law, edge types, metrics, + reachability, text invariants, the resource envelope, and the authored + `ReplaceRange`. +- File-crossing gate: observation evidence, the accepted host basis, the export + lifecycle and its declared guarantees, recovery, retained material, path + classification, and divergence handling. +- The generic Echo and Edict capabilities both gates require, each with an + owner issue. ## Non-Goals -- Migrating schema 1 buffers. A witnessed migration operation is follow-on work. -- Save/export. The export crossing is designed separately; #350 covers reopen. -- Checkpoints, rewrites, diffs, and anchors beyond the import anchor. -- Any change to Echo or Edict. This document names their gaps only. +- Migrating schema 1 buffers. A witnessed migration is a later slice. +- Any change to Echo or Edict in this document; it names their gaps and owners. +- Reintroducing predecessor-head chains to compensate for an unspecified + retention contract. +- Splitting one atomic `ReplaceRange` into several visible edits to fit a + batch limit. +- Making the first authored rope wait for every part of distributed braiding. + The first executable witness stays small and complete. ## Data / State Model -Facts (alpha atoms, canonical CBOR v1 via `echo-edict-canonical`): +### Facts -| Node | Atom fields | Mutable | +Atoms use Echo's canonical codec profile exactly as `echo-edict-canonical` +defines it, with published vectors. "Canonical CBOR" alone is not a precise +interoperability label: RFC 8949 allows more than one deterministic profile. + +| Node | Atom fields | Identity class | | --- | --- | --- | -| `Buffer` | `bufferKey`, `version: U64` | yes: `version` and its `canonicalHead` edge | -| `Head` | `byteLength: U64`, `lineCount: U64`, `sequence: U64` | no | -| `Branch` | `byteLength: U64`, `lineBreaks: U64`, `height: U8` | no | -| `Leaf` | `bytes: Bytes`, `lineBreaks: U64` | no | -| `Import` | `fileCoordinate`, `hostDigest: Bytes` | no | -| `Export` | `fileCoordinate`, `logicalDigest: Bytes`, `hostDigest: Bytes`, `exportEvent: Bytes` | no | +| `Buffer` | `bufferKey`, `version: U64` | mutable | +| `Head` | `byteLength: U64`, `lineCount: U64`, `sequence: U64` | content | +| `Branch` | `byteLength: U64`, `lineBreaks: U64`, `height: U8` | content | +| `Leaf` | `bytes: Bytes`, `lineBreaks: U64` | content | +| `Import` | `fileCoordinate`, `hostDigest: Bytes`, `observation: Bytes` | content | +| `HostBasis` | `fileCoordinate`, `hostDigest: Bytes`, `evidence: Bytes`, `generation: U64` | content | +| `Export` | `exportIntent: Bytes`, `fileCoordinate`, `logicalDigest: Bytes`, `hostDigest: Bytes`, `observation: Bytes` | content | + +`observation`, `evidence`, and `exportIntent` name causal evidence that +already exists when the node is written: an admitted observation's occurrence +identity, or an admitted export intent's identity. None names the commit that +contains the node itself, so no identity is circular. -Edges (no payload; one edge per source node and type): +### Edges | Edge type | From → to | Meaning | | --- | --- | --- | +| `jedit.text.buffer` (per buffer, see Reachability) | worldline root → Buffer | attaches the buffer to the committed state | | `jedit.text.canonicalHead` | Buffer → Head | current head; retargeted by each edit | +| `jedit.text.acceptedHostBasis` | Buffer → HostBasis | the host version Jim currently works against; retargeted by the transitions below | +| `jedit.text.lastExport` | Buffer → Export | what Jim last exported; never the synchronization basis | | `jedit.text.root` | Head → Branch or Leaf | the head's tree; absent for empty text | -| `jedit.text.anchor` | Head → Import | the imported bytes this head's lineage descends from (provenance only) | -| `jedit.text.lastExport` | Buffer → Export | the last witnessed write of this buffer to its file; retargeted by each save | +| `jedit.text.anchor` | Head → Import | the import this head's lineage descends from (provenance only) | | `jedit.text.left`, `jedit.text.right` | Branch → Branch or Leaf | ordered children | -Identity law: +"One edge per source and type" is enforced where Echo enforces it, not only by +Jim's constructor: a mutable source's slot edge id is fixed by its source and +type, and Echo scans a mutable source's outgoing bucket and refuses any alias +of the same type (`IdentityLawViolation`). -- Immutable node id: `H("jedit.text.node.v2", typeId, atomBytes, childIds...)` - with children in edge-type order. Equal subtrees have equal ids. -- Edge id: `H("jedit.text.edge.v2", fromNodeId, edgeTypeId)`. This makes - "one edge per source and type" hold by construction, and retargeting the - canonical head an edge replacement rather than a new edge. -- Buffer id: `H("jedit.text.buffer.v2", bufferKey)`, as in schema 1. -- `H` is the domain-separated hash Echo exposes to Edict; which hash that is - remains an open question below. +### Identity law -Rope law (unchanged from schema 1 except where noted): +Every id is computed under `ContentAddressV1`, the bridge's generic law, never +an application-specific recipe: -- Leaves hold at most 4096 bytes and end on a UTF-8 boundary. -- Branches are binary and AVL-balanced by `height`. -- Edits path-copy: only nodes on the affected paths and the new head are new. - Nothing is deleted. -- Leaves hold their bytes inline. Schema 1's Blob indirection is dropped; - content addressing already deduplicates equal leaves. +- A content node's id commits to its type, the attachment digest of the atom it + actually stores, and its complete outgoing edge set (each edge's type and + target), exactly the edges its creating proposal gives it. +- A content node is created with every outgoing edge it will ever have, in one + proposal, and is immutable afterwards. +- `Buffer` is mutable with a program-chosen id: `BufferId` is derived from + `bufferKey` under a Jim domain, as in schema 1, and is not a content address. +- An edge from a content node has a content edge id; an edge from a mutable + node has a slot edge id that stays the same when `ReplaceEdge` retargets it. + +A `Head`'s id is therefore computed from its actual `HeadFact` and its actual +outgoing edges: `anchor`, plus `root` when the text is non-empty. The empty +head has no `root` edge and its id says so; nothing extra is hashed and nothing +stored is omitted. + +Scope of "equal subtrees have equal ids": equal under `ContentAddressV1` +within one warp instance. Ids from different identity profiles or different +warps are not comparable. + +Edict source computes ids from the inputs the bridge uses (edict#260). Both +implementations must match published, independent identity vectors, including +empty and non-empty heads. -Coordinate contract: +### Effect normalization -- Byte offsets into the UTF-8 text are the only authoritative coordinates. - Every operation takes and returns byte offsets. -- UTF-16 code-unit offsets matter for interoperability (language servers, - browser selection, external editing protocols), even though no Jim code reads - them today. Whether they are derived on demand, cached in readings, or - retained as a per-node witnessed metric is an open decision (see Follow-On - Debt). Until it is made, schema 2 does not store them, and nothing may treat - their absence as a decision that they are unneeded. +Repeated text produces repeated content ids. The authored program normalizes +its proposal before emitting it, because the bridge rejects duplicate targets: -History, current state, and retained material are three different things: +- identical target and identical intended content: emit one effect; +- identical target and different intended content: an integrity failure, + never a silent choice; +- effects in canonical order. + +The bridge's generic rejection stays; silent deduplication there would hide +mistakes in the proposal Echo is meant to witness. + +### Rope law and text invariants + +- Leaves hold at most 4096 bytes, are valid UTF-8, and end on a character + boundary. +- Branches are binary and AVL-balanced by `height`. +- Line breaks count `\n` only; `lineCount = lineBreaks + 1`. +- All length, line, and height arithmetic is checked; overflow is + `ArithmeticOverflow`, never wraparound. +- `Head.sequence` is the predecessor head's `sequence + 1`. + `Buffer.version` increases by one with every admitted change to the Buffer's + atom or its outgoing edges. +- A replacement whose bytes equal the bytes it replaces is `NoOp` and writes + nothing. +- Edits path-copy: only nodes on the affected paths, fresh leaves, and the new + head are new. + +### Coordinates + +Byte offsets into the UTF-8 text are the only authoritative coordinates. +UTF-16 offsets matter for interoperability, so schema 2 stores none and treats +them as a derived reading, cached by immutable subtree identity and conversion +version. Cold conversion cost is measured before any decision to store a +witnessed per-node metric. + +### Reachability + +A worldline holds many buffers, so the Buffer is not the worldline root. Each +Buffer is reached from the worldline root by its own typed edge, created in the +same proposal as the Buffer (echo#927). The committed current state is then: +the Buffer, its canonical Head and rope, the Head's Import, the +`acceptedHostBasis` and `lastExport` targets, and declared current metadata, +with no edge from any head to the head it replaced. + +The reachability fixture starts at the **actual worldline root**, never at a +conveniently chosen Buffer. + +### History, current state, and retained material | | Owner | What it guarantees | | --- | --- | --- | | Causal history | Echo ticks and receipts | what happened, in which causal context, with which outcome | -| Current state | this graph | the Buffer, its canonical Head, and the nodes reachable from that Head | -| Retained material | Echo retention and replay | which past states can be reconstructed, from checkpoints or replay inputs | - -The graph keeps no edge from a head to the head it replaced. After an edit, -the state root covers the current rope only. Superseded nodes leave the -reachable graph. Whether their bytes remain available is Echo's retention -policy; a tick witnessing a transition does not by itself promise that the -bytes needed to reconstruct the earlier state are still retained. - -Undo and redo are forward operations: Jim proposes a new edit whose target -state derives from a past witnessed state, subject to the evidence Echo still -retains and to admission. Nothing moves history backward. - -Head-to-file identity (anchored refinement). Three facts are kept apart: - -| Fact | Where | Claims | Never claims | -| --- | --- | --- | --- | -| Import provenance | `Import` node, `anchor` edge | these contents descend from the bytes imported from this file, with this host digest | that the rope still matches the file | -| Current logical content | computed from the current rope | the bytes Jim represents now | anything about the file | -| Host synchronization | `Export` node, Buffer `lastExport` edge | these exact bytes were written to this file, with this resulting host digest | that the file is unchanged since | - -- Importing a file creates an `Import` node and anchors the import head to it. - Every edit copies the `anchor` edge to the new head. The anchor is - provenance only; after an unsaved edit it says nothing about the file. -- The current logical digest is computed over the rope's bytes when a crossing - needs it (save, reopen, reconciliation), not on every edit, so edits stay - path-copies. The root node id is not that digest: it depends on tree shape. -- An `Export` is evidence of one crossing: the file, the logical digest of the - bytes written, the resulting host digest, and `exportEvent`, the identity of - the causal event that witnessed it. It names the exported head only through - that event and the logical digest; there is no edge to the head, so a save - does not keep a historical rope reachable. A pinned saved snapshot, if one is - ever wanted, is an explicit retention lease with its own lifetime. -- The `Export` reachable through `lastExport` witnesses the last successful - export. It is never file authority: the filesystem's current bytes are, and - every crossing re-observes them. -- Save is a crossing to a foreign system, so its steps stay separate - (`docs/jim-component-ownership.md`, `ExportIntent` and `ExportObserved`): - 1. **Export intent.** An admitted Jim operation records the head to write, - its logical digest, the expected prior host digest (the last export's, - or the import's if never exported), and an occurrence key. - 2. **Host write.** A host effector writes the bytes. Its own concurrency - protocol decides how close it gets to compare-and-write; see below. - 3. **Observation.** The effector reads back the resulting host digest. That - reading enters Echo as witnessed ingress. - 4. **Export outcome.** An admitted Jim operation records the `Export` and - retargets `lastExport` only when the observed digest equals the intended - bytes' digest. Any other observation is a typed conflict that needs an - explicit reconciliation decision. - 5. **Recovery.** An intent without an outcome is resolved by re-observing - the file under the same occurrence key: the intended digest means the - write happened; the expected prior digest means it did not and may be - retried under the same key; anything else is an external change and a - conflict. -- What this does and does not guarantee: comparing digests before writing - detects most external modifications, but a writer that changes the file - between that check and the write is not prevented by it. Echo's atomic - commit does not make the host write atomic with it. Preventing that race - needs a host-side concurrency protocol (an exclusive lock, or an atomic - compare-and-replace the filesystem actually provides). Until one is chosen, - the claim is detection after the fact, and step 3's observation is what - makes it detectable. -- Reopening compares the file's current host digest with the last exported - digest, or the import digest if the buffer was never exported. A mismatch - means the file changed outside Jim: a typed obstruction or an explicit, - witnessed external-edit transition, never silent reuse (#350). -- The `Export` node and `lastExport` edge are part of schema 2; the save - operation itself is designed separately. - -### External file reconciliation - -The filesystem is another authority, not an extension of Jim's memory. Another -process (an editor, `git checkout`, a formatter, a sync client) can write the -file while Jim holds a buffer for it. That is an ordinary case of two -authorities evolving independently, so it is part of the file model, not an -edge case of save. - -This is causal transport, not a new mechanism, and AIΩN Paper VII ("WARP: -Optics, Holograms, and Worldlines over Shared Causal History") already gives -its shape: "Distribution changes the slice boundary; it does not change the -downstream law." Jim observes a transported claim, takes part in constructing -a comparable braid, and authors the law under which that braid may be lowered. -The filesystem testifies; it does not edit Jim's history: - -- **Transport precedes judgment** (Paper VII §4.3). An observed file version - must be re-expressed at Jim's receiving frontier before it can be judged. B - is that comparable basis. The adapter establishes only the basis it can - actually support; it cannot manufacture ancestry the external writer never - supplied. -- **A braid is not a merge** (Definition 2.4, Remark 2.6). Observing (holding - the claim), braiding (presenting L and H over B), judging, and admitting are - separate acts. Under Jim's law a divergence may lawfully stay `Plural` - (§4.2) until a settlement is chosen. -- **The optic** (Definition 3.1, Ψ = (Ω, χ, ρ, Π, Λ)) is Jim's: the slice χ is - the smallest lawful comparison closure within the buffer's file site. A - whole-file comparison is acceptable at first, but it is not a requirement; - the optic is bounded. ρ presents B, L, and H as comparable claims, Π is - Jim's Edict-authored admissibility law, and Λ is the retention contract that - decides whether B's bytes remain available for a merge. - -In Echo's current contracts: - -- A filesystem adapter turns a validated observation into ingress, following - Echo's [Continuum Transport](https://github.com/flyingrobots/echo/blob/main/docs/architecture/continuum-transport.md) - import law: the adapter forms an import proposal, and only an admitted import - Intent affects history. -- What arrives is held, judged, and applied as - [Participant History as a Braid](https://github.com/flyingrobots/echo/blob/main/docs/architecture/participant-history-as-a-braid.md) - describes. **Hold:** the observation is retained as evidence and staged; - no reading of the buffer changes. **Judge:** Jim, as the receiving - authority, compares B, L, and H under its own Edict-authored law, with - outcome Derived, Plural, Conflict, or Obstruction. **Apply:** only a - witnessed forward commit on an explicit basis changes the buffer. -- The evidence is the observation, not the external editor's history. Unless - the other writer takes part in the protocol, Jim knows only the bytes and - metadata seen at one crossing, and never fabricates the writer's edit - sequence. - -The filesystem-specific work stays at the adapter boundary: stable reads, path -identity, rename and replacement detection, permissions, and safe export. The -judging law is Jim-owned Edict; Echo supplies observation, admission, history, -and effects, never merge semantics. - -Three logical versions, compared by digest: +| Current state | this graph | current representation and current obligations | +| Retained material | named retention contracts | which bytes remain available, acquired before the operation that needs them | + +After an edit, superseded nodes leave the reachable graph. Echo keeps them +keyed-readable until a witnessed mechanism changes that; Jim does not depend on +it without a retention contract. Undo and redo are forward operations whose +target derives from a past witnessed state, subject to retained material and +admission. + +## Resource Envelope + +The v1 operation supports an explicit envelope and refuses atomically outside +it. Each limit is a lawpack constant: + +| Limit | Constant | Bounds | +| --- | --- | --- | +| Replacement bytes | `text.maxReplacementBytes` | fresh leaves and the equal-length no-op read | +| Traversed nodes and edges | `text.maxClosureNodes`, `text.maxTreeHeight` | the closure read | +| Decoded and hashed bytes | `text.maxDecodedBytes` | atom decoding and id computation | +| Generated nodes and effects | `text.maxCreatedLeaves`, `text.maxCreatedBranches`, `text.maxEffects` | the proposal | +| Evaluation work and allocation | `text.replaceRangeBudget` | the evaluator meter | + +A proposal costs about `(h + 1)` path-copied branches plus +`ceil(replacement / 4096) + 2` fresh leaves, one head, and one Buffer update, +where `h ≤ 1.44 log2(leaves)`; each content node is one node, one atom, and up +to two edges. The equal-length no-op check reads the replaced range, so its +reads grow with the replacement, not only with boundary paths and spines; the +replacement bound bounds it. + +Under Echo's current 128 patch operations per Action batch, a 1 MiB replacement +(256 fresh leaves and 255 branches) is far outside any envelope. The v1 values +are chosen from a measurement fixture over generated trees and recorded with +their cost model before the representation gate; raising a cap without that +model is out of scope. Larger edits are a separate operation family (#382). + +Three failures stay distinct, and none accuses valid data of corruption: + +| Failure | Meaning | +| --- | --- | +| `ResourceLimitExceeded` | a valid operation exceeds the declared envelope | +| `ClosureInsufficient` | the selector asked for too little closure; a defect in the law | +| `MalformedRope` | the stored rope violates its invariants | + +## Runtime / API Contract + +The authored `ReplaceRange`, in schema 2 terms: + +1. Read the Buffer and its `canonicalHead`; require it equals the invocation + basis, else `BasisNotCanonical`. +2. Check the request against the envelope, else `ResourceLimitExceeded`. +3. Read the bounded closure the edit touches in one witnessed read (echo#926), + deduplicating material by node identity while preserving traversal meaning + by edge path and interval: a leaf shared by both children of one branch is + two positions. +4. Compute, purely, the new nodes and edges and their `ContentAddressV1` ids. +5. Normalize the proposal; `ensure` each new content node with all its edges, + including the new head's `root` and `anchor`; retarget `canonicalHead` and + bump `Buffer.version`. All or nothing. + +Generic capabilities the representation gate needs: + +| Need | Owner | +| --- | --- | +| Authored effects lowered, admitted, scheduled, and published atomically with receipts and WAL | echo#921 | +| Typed edge reads and a guided bounded closure read | echo#926 | +| Mutable nodes reachable from the worldline root | echo#927 | +| `ContentAddressV1` inputs in Edict source | edict#260 | +| Variant and `Option` types | edict#261 | +| Bounded recursion over depth-bounded variants | edict#262 | +| Checked arithmetic, `min`, `max` | edict#263 | + +## File-Crossing Contract + +This section is the file-crossing gate. None of it is part of the +representation gate. + +### What a filesystem observation proves + +A digest is a value witness, not a write receipt. Three claims stay distinct: + +| Claim | Evidence required | +| --- | --- | +| "These bytes were observed at this path." | A validated observation of those bytes. | +| "This export performed the write." | Evidence attributable to that host operation. | +| "No intervening external update was overwritten." | A concurrency protocol that excludes or conditionally rejects such updates. | + +Read-back cannot establish the third claim. If Jim reads B, another editor +writes X, and Jim writes L and reads L back, the read-back is correct and X is +gone; nothing in the final bytes shows X existed. + +Export profiles declare which claims they make: + +- **Best effort (v1).** Makes the first two claims only. It records an attempt + and the observed result, and says it cannot exclude an overwritten update. +- **Exclusive.** Also makes the third claim; needs an adapter with a real + exclusion or compare-and-replace protocol (#377). A caller that requires + lost-update prevention obstructs with `ExportGuaranteeUnavailable` on an + adapter that cannot provide it. + +Durability is declared separately: a validated read, an atomically published +file, and a crash-durable save (file and containing directory flushed) are +different guarantees, and each export records which it obtained. + +Digest comparability: host and logical digests are SHA-256 over raw bytes, and +v1 import and export apply no transformation (no newline or encoding change), +so equality between them is meaningful. A later transformation must declare +its mapping. + +### The accepted host basis + +`acceptedHostBasis` answers "which host version are we working against?"; +`lastExport` answers only "what did Jim last export?". Its transitions: + +| Operation | Accepted host basis afterward | +| --- | --- | +| Initial import | the imported host version | +| Hold a new observation | unchanged | +| Adopt external contents H | H | +| Accept observed agreement H = L | H, with no Export fabricated | +| Reconcile B, L, H into local result M | H; M stays locally dirty when M ≠ H | +| Confirm an applicable export of S | the witnessed exported host version S | + +Each `HostBasis` names the evidence that made it current and a `generation` +that increases with every transition, so a stale evidence item can never be +mistaken for the current one by digest equality alone. + +### Versions and conditions | Version | Meaning | | --- | --- | -| Base B | the file contents Jim last imported or exported successfully (the synchronization basis) | +| Base B | the accepted host basis | | Local L | the current rope, including unsaved edits | | Host H | the file contents in the latest validated observation | | Condition | Jim's behavior | | --- | --- | | H = B, L = B | nothing changed | -| H = B, L ≠ B | local edits only; ordinary save | +| H = B, L ≠ B | local edits only; ordinary export | | H ≠ B, L = B | external change only; Jim may adopt H as a forward transition | -| H = L, H ≠ B | the same bytes on both sides; mark synchronized after validating the observation | -| H ≠ B, L ≠ B, H ≠ L | divergence; preserve both and require an explicit decision | - -Requirements: - -1. **Watchers are hints.** A watcher event, focus, refresh, reopen (#350), or - save only prompts an observation. Every decision uses a validated host - observation: the file re-read with a stable result. A file read that - changes during the read is an unstable observation and decides nothing. An - unobserved file is `Unknown`, never assumed unchanged. -2. **Observing is not adopting.** `ObserveExternalFileChange` is the admitted - import Intent for one observation. It records the file coordinate, B's - digest, the newly observed digest, and the evidence of the read, and admits - the observed bytes as a new `Import`. It changes no head; it is the Hold - step. -3. **Occurrence identity is the adapter's, and honest.** Each observation gets - a stable occurrence identity (Echo's Continuum occurrence identity at - ingress) and an explicit receiving context: buffer, file coordinate, and B. - Re-delivering the same occurrence is idempotent and returns the retained - outcome. Distinct observations stay distinct evidence, never collapsed. A - digest identifies observed content, not the event that produced it: two - external writes can leave identical bytes. Where the adapter can tell writes - apart (file identity, change tokens), it records that; where it cannot, it - records only distinct observations and does not invent distinct writes. -4. **External-only change.** When L = B, Jim may adopt H by a separate - admitted operation that creates a head anchored to the new `Import`. It is a - forward transition; the old head stays in causal history. Automatic adoption - is allowed only under a declared policy, and is still witnessed. -5. **Divergence preserves both sides.** When H ≠ B and L ≠ B and H ≠ L, Jim's - judgment is Conflict at the buffer, and nothing that depends on the file is - admitted until it is settled. Jim never resolves silently. The explicit - settlements are: - - **Reload from disk:** adopt H; keep L recoverable as a branch or - checkpoint while its material is retained. - - **Keep local:** keep editing L. This does not grant permission to - overwrite H; save stays obstructed by the divergence. - - **Overwrite:** a separate, explicit save whose expected prior digest is - H's, recorded as overwriting a known third-party change. - - **Reconcile:** build a new version from B, L, and H and submit it as a - forward edit. -6. **Reconciliation is a forward intent.** It never rewrites existing ticks. - Jim witnesses H as observed bytes; it does not invent the external editor's - edit sequence or causal history. -7. **Base material is required to promise a three-way merge.** A digest of B is - not enough. Jim offers Reconcile only when B's bytes are retained: a - retention lease on the last synchronized head while the buffer is open, or - Echo's retention otherwise. Without them, Reconcile is refused with a typed - `MergeBaseUnavailable`, and Reload, Keep local, and Overwrite remain. -8. **Distinguish what happened to the path.** A validated observation - classifies the change before any decision: - - | Observed | Classification | Initial support | - | --- | --- | --- | - | same file, new bytes | modification | supported | - | file replaced through a temporary file and rename (atomic save) | modification, if the result is an ordinary file | supported | - | path absent | deletion | divergence-style decision; no implicit save recreates it | - | different file identity at the path | replacement | refused as ambiguous; explicit decision required | - | path became a symlink, directory, or special file | not an ordinary file | refused | - | permissions forbid reading or writing | permission change | obstruction naming the permission | - | bytes changed during the read | unstable read | no decision; observe again | - - The first version supports ordinary files only and refuses ambiguous - crossings rather than pretending the filesystem offers compare-and-swap. -9. **Save revalidates.** Save observes H first and is obstructed unless H = B, - or the user chose Overwrite against exactly this H. A change between that - check and the write is caught by the save protocol's read-back (step 3) and - reported as a conflict, never as a successful export. The guarantee is - detection; prevention needs the host-side concurrency protocol (open - decision), and Jim reports when it cannot establish the guarantee. - -Scope of the first version: detect divergence, preserve both sides, and require -explicit resolution. Automatic three-way reconciliation proposals come later, -once the observation evidence and base retention contracts hold. Then Jim can -materialize B, L, and H, compute a deterministic three-way proposal, present -overlaps as a `Plural` outcome, and submit the accepted result through Echo. - -## Runtime / API Contract +| H = L, H ≠ B | accept agreement: the basis becomes H, no Export is recorded | +| H ≠ B, L ≠ B, H ≠ L | divergence; preserve both and require an explicit settlement | + +### Export lifecycle + +- **One unresolved export per file binding.** The binding is the file, not the + buffer, so two buffers addressing one file share it. The effector serializes + or fences writes per binding: each intent carries a fencing generation, and + an effector holding a stale generation does not write. +- **Each export captures** its stable intent identity, the exact head + exported, the expected accepted host basis, the file binding and its + authorization, and the observations and host-attempt evidence that belong to + it. +- **Outcomes are evidence first.** An outcome advances the accepted host basis + only if its intent is the binding's current one and the basis it expected is + still accepted. Otherwise it is retained as historical evidence and changes + no current state. A delayed older outcome never regresses a newer basis. +- **Observation identity.** The intent keeps one identity across retries. Each + physical read is a new observation with a new identity; retransmitting an + existing observation reuses its identity. +- **Edits during a save.** A save captures head h₁; the user edits to h₂ while + the write runs. Completion records the export of h₁ and leaves h₂ canonical. + h₂ is not synchronized unless its content equals what was exported. + +### Recovery + +An intent without an outcome is resolved by a new observation, classified: + +| Classification | Meaning | +| --- | --- | +| `IntendedContentObserved` | the file now holds the intended bytes | +| `PriorContentObserved` | the file holds the expected prior bytes | +| `DifferentContentObserved` | the file holds something else | + +Each classification also records whether the original write's occurrence is +witnessed or **unknown**. Another process may have produced the intended +bytes; Jim may have written and another process restored the prior bytes; a +no-op save makes the two indistinguishable. A recovered postcondition may +settle the pending workflow under a declared policy; it never invents an +`Export` event. + +### Observation, holding, and adoption + +The filesystem is another authority. Following AIΩN Paper VII ("WARP: Optics, +Holograms, and Worldlines over Shared Causal History"), transport precedes +judgment and a braid is not a merge: Jim holds an observed claim, judges B, L, +and H under its own Edict-authored law, and applies only a witnessed forward +commit. The adapter authors an honest local observation of bytes; it cannot +turn a snapshot into an external editor's witnessed causal history. + +1. **Watchers are hints.** Every decision uses a validated observation: the + file read with a stable result. A read whose result changes during the read + decides nothing. An unobserved file is `Unknown`. +2. **Hold changes neither the canonical head nor the logical text.** It admits + the observation as evidence through Continuum import (echo#928); evidence + and status may change. +3. **Occurrence identity is the adapter's, and honest.** Re-delivering one + observation returns the retained outcome; distinct observations stay + distinct; identical bytes from two observations are two pieces of evidence, + not two distinct external writes, unless the adapter can tell writes apart. +4. **Adoption is a separate admitted forward transition** that creates a head + anchored to the new `Import` and sets the accepted host basis. Automatic + adoption is allowed only under a declared policy, and is still witnessed. + +### Path classification + +The adapter classifies observable mechanics first, then a declared policy +decides: + +| Observed mechanics | v1 policy | +| --- | --- | +| same object, changed contents | modification | +| path names another ordinary file | modification of the path under the replacement policy; never claimed to continue the prior writer's history | +| path absent | deletion; a divergence-style decision, no implicit save recreates it | +| non-ordinary object (symlink, directory, special file) | refused | +| permissions forbid reading or writing | obstruction naming the permission | +| identity or observation stability unresolved | no decision; observe again | -The authored `ReplaceRange` operation, in schema 2 terms: +Atomic-save replacement can give the path a different object identity, and a +final observation cannot tell an editor's atomic save from `git checkout`. The +policy supports ordinary-file replacement without claiming more. -1. Read Buffer and its `canonicalHead`; require it equals the invocation basis. -2. Read the bounded closure of nodes the edit touches: both boundary paths and - the spines a join may descend. -3. Compute, purely, the new nodes and edges. -4. `ensure` each new immutable node and edge, including the new head's `root` - and copied `anchor` edges; replace the `canonicalHead` edge and bump - `Buffer.version`. All or nothing. No edge points from the new head to the - old one. +### Divergence -Generic capabilities this needs, none of which exists today: +The barrier follows the disputed dependency, not the buffer's origin: -| Need | Owner | Status on main | +| Operation during divergence | Treatment | +| --- | --- | +| Read or navigate current text | allowed | +| Edit current text on an admissible basis | allowed | +| Hold another host observation | allowed | +| Preserve material or perform an explicit settlement | allowed under its own preconditions | +| Ordinary export assuming host agreement | obstructed | +| Other work requiring an established host basis | obstructed while that dependency is unsatisfied | + +Settlements, each an admitted forward operation: + +- **Reload:** adopt H. L stays recoverable only if its material was retained + before the Reload; that retention is acquired first, or Reload refuses. +- **Keep local:** keep editing L; export stays obstructed by the divergence. +- **Overwrite:** an explicit export whose expected basis is H, recorded as + overwriting a known third-party change. +- **Reconcile:** build M from B, L, and H and submit it as a forward edit; the + accepted host basis becomes H. The base may be an observed host version that + was never a Jim head. + +### Retained material + +A recorded digest is not retained bytes. Each promise names its material and +acquires it before the operation that needs it (#378, echo#896): + +| Material | Needed by | Acquired | | --- | --- | --- | -| Read outgoing edges by type (`edict_read`) | Echo | absent; reads alpha atoms only | -| Bounded closure read guided by a pure selector | Echo + Edict | absent | -| `ensure` (create, or require equal existing) | Echo + Edict | absent; create obstructs on existing | -| Multi-node, multi-edge atomic effects from evaluation | Echo | absent; see Echo bridge design | -| Edge create and replace effects | Echo + Edict | absent | -| Domain-separated hash in Edict source | Edict + Echo | absent | +| held host version H | Adopt, Reconcile, Overwrite comparison | at Hold | +| accepted base B | Reconcile | when it becomes the accepted host basis | +| displaced local version L | Reload's recoverability promise | before Reload applies | +| frozen bytes of a pending export | write, retry, recovery | at export intent | + +Missing material is a precise `MaterialUnavailable` obstruction, never a +corrupt-rope classification. Without B's bytes, Reconcile refuses with +`MergeBaseUnavailable` and the other settlements still work. + +Generic capabilities the file-crossing gate needs: + +| Need | Owner | +| --- | --- | +| Continuum import dispatch for observations | echo#928 | +| Separate braid construction, judgement, and admission | echo#898 | +| Retention guarantees | echo#896, #378 | +| Exclusive export profile | #377 | ## Lower Modes -Not applicable: this is a storage representation, not a user surface. +Not applicable: this is a storage and crossing representation, not a user +surface. ## Accessibility Posture @@ -414,134 +549,138 @@ only, as in schema 1. ## Agent Inspectability / Explainability Posture -Every relation in the current rope is a typed edge, so an agent can traverse it -without decoding application payloads. Past edits are explained from Echo's -causal history and receipts, not from rope topology. +Every relation in the current rope is a typed edge reachable from the +worldline root, so an agent traverses it without decoding application payloads. +Every claim about the file names its evidence class: observation, attempt, +exclusion, or durability. ## Linked Invariants - Echo two-plane law: structure in the skeleton, not in payload bytes. +- Echo `ContentAddressV1`: one identity law for every authored content node. - History Over State ch. 21 and 42: a rope head is the workspace coordinate, an anchored refinement of it, or the source of a witnessed crossing. - DL-0158: codec or edge migration is a separately admitted operation. -- AIΩN Paper VII ("WARP: Optics, Holograms, and Worldlines over Shared Causal - History"), as an architectural foundation, not as evidence that anything - below is implemented: - - §3.3, commitment, folding, and revelation are separate: the graph commits - the current rope; what stays retained is the contract Λ, not rope topology. - - §4.2 and §4.3, braid plurality and transport before import: the external - file reconciliation contract above. - - §6.2, the authored hot-text optic: its `replaceRangeAsTick` surface declares - a `ropeRangeClosure` slice closure and updates only `canonicalHead`. The - draft's guided closure read and the single head retarget follow that shape. - - §8 lists app-authored optic compilation and export semantics at the - causal-medium boundary as open engineering seams. This document's - Edict-authored rope and save crossing are attempts at exactly those seams. +- AIΩN Paper VII, as an architectural foundation, not as evidence that + anything here is implemented: §3.3 (commitment, folding, and revelation are + separate), §4.2 and §4.3 (braid plurality, transport before import), §6.2 + (the authored hot-text optic's `ropeRangeClosure` slice and single head + retarget), §8 (app-authored optics and export semantics as open seams). ## Design Alternatives Considered - **Child ids inside atoms (schema 1 shape).** Rejected: children fall outside the state root, and the shape breaks Echo's two-plane law. -- **Edges plus duplicated child ids in atoms.** It would let today's - `edict_read` follow children without an edge read. Rejected: two sources of - truth for one relation, with nothing enforcing agreement. -- **Keep JSON atoms.** Rejected: forces Edict source to parse JSON - byte-by-byte (the #302 Buffer-decoder probe) and admits several spellings. -- **Keep Blob slices.** Rejected for schema 2: adds an indirection and a slice - read per leaf; content-addressed leaves already deduplicate. -- **Link each head to its basis head.** Rejected: it would make every version - of every buffer permanently reachable, so the state root and retention would - grow with editing history, and it duplicates the causal history Echo's ticks - and receipts already own. History is not state. -- **Drop UTF-16 coordinates.** Rejected as a decision: no current consumer is - not a reason to discard an interoperability coordinate. Left open instead. +- **Edges plus duplicated child ids in atoms.** Rejected: two sources of truth + for one relation. +- **Keep JSON atoms.** Rejected: forces Edict source to parse JSON and admits + several spellings. +- **Keep Blob slices.** Rejected: an indirection and a slice read per leaf; + content-addressed leaves already deduplicate. +- **An application-specific id recipe.** Rejected: Echo recomputes ids under + `ContentAddressV1` and refuses any other; two recipes would disagree. +- **Link each head to its basis head.** Rejected: every version would stay + reachable, and it duplicates the history Echo's ticks already own. +- **Use `lastExport` as the synchronization basis.** Rejected: adoption and + observed agreement change the basis without any export, so a later save would + rediscover an already-accepted change as divergence. +- **Infer a write from the current digest.** Rejected: equal final bytes cannot + establish which operation happened. +- **Store UTF-16 metrics now.** Deferred: derived readings first, measured. ## Decision -Adopt schema 2 as above for the Edict-authored rope, on review of this document -and the Echo evaluation-to-effect design. +Approve schema 2's direction with the corrections above. Freeze the schema +only when the representation gate passes; accept the file crossing only when +its own gate passes. ## Implementation Slices -1. Publish `jedit.text.schema@2` (machine-readable, like schema 1). -2. Write a simple, deliberately inefficient Edict reference `ReplaceRange` - (semantic target), then the persistent rope (persistence target). -3. Build a schema 2 oracle by differential comparison: the reference and the - persistent rope must agree on logical text and outcomes, not physical roots. -4. Witnessed schema 1 → 2 migration. +Representation gate: + +1. Publish `jedit.text.schema@2` (machine-readable) with codec vectors and + `ContentAddressV1` identity vectors, including empty and non-empty heads. +2. A deliberately simple Edict reference `ReplaceRange` (semantic target). +3. The persistent rope (persistence target), with effect normalization and + the three failure classes. +4. The resource-envelope measurement fixture and its recorded v1 values. +5. The schema 2 oracle: reference and persistent rope agree on text semantics; + representation invariants and admission/effect behavior are validated + separately. +6. Cutover, then deletion of the native schema 1 law. + +File-crossing gate: + +7. Observation evidence and the accepted host basis. +8. The best-effort export lifecycle with fencing, recovery classification, and + retained material. +9. Divergence settlements. ## Tests To Write First -- Canonical codec vectors for every fact type, including rejection of - non-canonical encodings. -- Identity: equal subtrees produce equal ids; any atom or child change changes - the id. -- Reachability: after an edit, the state root covers exactly the current Buffer, - Head, Import, and rope; nodes only the superseded head used are unreachable. -- Reconstruction: a past state is rebuilt from Echo's checkpoints and replay, - and the test states which retention guarantee it relies on. -- Anchor: reopen with a changed host digest obstructs (#350). -- Each row of the B/L/H decision table, including H = L with H ≠ B. -- Observation without adoption: `ObserveExternalFileChange` changes no head. -- Occurrence idempotence: re-delivering one observation returns the retained - outcome; two observations of identical bytes stay two pieces of evidence and - are not reported as two distinct external writes. -- Barrier: while the buffer's divergence is an unsettled Conflict, an - operation that depends on the file is not admitted; unrelated work is. -- Divergence: save is obstructed under Keep local; Reload keeps L recoverable; - Overwrite records the overwritten H; Reconcile is a forward edit. -- Base gone: with B's bytes unretained, Reconcile refuses with - `MergeBaseUnavailable` and the other choices still work. -- Each path classification: atomic-save rename, deletion, replacement, - symlink, permission change, and an unstable read that decides nothing. -- Race: a file changed between the save's check and its write is reported as a - conflict at observation, never recorded as a successful export. -- Recovery: a crash between export intent and outcome resolves to written, - not written, or external change by re-observation. +Representation gate: + +| Fixture | Required result | +| --- | --- | +| Codec vectors for every fact type | canonical bytes; non-canonical encodings rejected | +| Empty and non-empty Head identity vectors | authored source and bridge compute identical ids from the actual stored fact and edges | +| Identity | equal subtrees have equal ids within one warp; any atom or child change changes the id | +| Two equal-content leaves | the proposal has no duplicate targets; both text positions still exist | +| `aa` as one shared leaf, edit the second `a` | the edit addresses the second position | +| Exhaust a closure or effect budget, or fail the final effect | correctly classified outcome; no partial application | +| Traverse from the actual worldline root | all current representation is committed; no historical-head chain | +| Restart after edits | recovered state equals the pre-restart state | + +File-crossing gate: + +| Fixture | Required result | +| --- | --- | +| Read B → external write X → Jim writes L → read L | no claim that interference was detected or prevented | +| Crash with final bytes equal to the intended or the prior bytes | recovery preserves uncertainty about the original write | +| Adopt an external version after an earlier export | the next save uses the newly accepted basis | +| H = L ≠ B | agreement accepted; no Export fabricated | +| Reconcile to M, then save | the accepted basis is H; the same divergence is not rediscovered | +| An older export outcome arrives after a newer one | evidence retained; current basis not regressed | +| An earlier effector resumes late | fencing prevents stale publication | +| Edit while an earlier head is being saved | the newer canonical head is preserved | +| Release or fail to acquire required material | a precise availability obstruction | +| Each path classification | the declared policy, never an invented history | ## Acceptance Criteria -- Schema 2 declaration published with codec vectors. -- The draft authored source reads and writes only schema 2 propositions. -- Every needed generic capability has an owner issue. +- Representation gate: slices 1–6 green, with identity vectors matched by both + implementations and the envelope recorded with its cost model. +- File-crossing gate: slices 7–9 green, with every claim recorded at the + strength its evidence supports. +- Every needed generic capability has an owner issue (listed above). ## Validation Plan -Codec and identity vectors in this repository; reachability and atomicity -through the Echo bridge once it exists. +Codec and identity vectors in this repository; reachability, atomicity, +receipts, WAL, and restart through the Echo bridge (echo#921) once it exists. +The file-crossing gate validates against a deterministic hostile-schedule +adapter (#380). ## Playback / Witness -None yet. This is a representation decision. +None yet. ## Risks -- **State-root cost.** Echo recomputes the root by walking the whole reachable - graph on every commit, so an edit costs in proportion to the current rope, - not to its history. That is still more than the edit itself; an incremental - root is Echo's open state-root decision. Recorded; deferred. -- **Unreclaimed nodes.** Echo has no garbage collection today, so superseded - nodes stay in the store after they leave the reachable graph. Reclaiming them - is Echo's retention policy, not Jim's. -- **Patch size.** About `(depth + 1) × (node + atom + up to 2 edges)` operations - per edit, against Echo's 128 operations per tick. Depth stays near - `1.44 × log2(leaves)`; to be measured. -- **Hash choice.** The id hash must be one Edict and Echo both expose. +- **State-root cost.** Echo recomputes the root by walking the reachable graph + on every commit, so an edit costs in proportion to the current rope. An + incremental root is Echo's open decision (echo#845). +- **Unreclaimed nodes.** Superseded nodes stay keyed-readable; reclaiming them + is Echo's retention policy. +- **Envelope.** Under the current batch cap the supported replacement size may + be small; the measurement decides it, and #382 covers larger edits. ## Follow-On Debt -- Open: Jim's UTF-16 coordinate contract: derive on demand, cache in readings, - or retain as a witnessed per-node metric. Decide from the interoperability - surfaces Jim commits to (language server, external protocols), not from - today's consumers. -- Open: which hash Edict source exposes for identities. -- Open: the retention lease on the last synchronized head that Reconcile - requires (External file reconciliation, requirement 7): its owner, - lifetime, and release. -- Open: the host-side concurrency protocol for the export write. -- Settled by the anchor split: a reopen check compares host digests only, so - it never materializes the rope; the logical digest is computed at save. - Open: Rewrite and Diff facts in schema 2. +- Open: the UTF-16 derived reading and its cache. +- Ideas: settlement offers that carry their prerequisites (#379), inspectable + edit costs (#381). ## Retrospective diff --git a/edict/replace-range/draft/README.md b/edict/replace-range/draft/README.md index 6099ec05..f4062de2 100644 --- a/edict/replace-range/draft/README.md +++ b/edict/replace-range/draft/README.md @@ -8,16 +8,19 @@ the program drive the language and runtime work instead of isolated probes. | File | Target | Content | | --- | --- | --- | -| `Text.edict` | shared | schema 2 facts, edge types, identity law, text metrics | +| `Text.edict` | shared | schema 2 facts, edge types, `ContentAddressV1` identity, text metrics | | `Reference.edict` | 1: semantic correctness | flat-text `ReplaceRange`; deliberately inefficient | -| `Rope.edict` | 2: persistent rope | pure AVL split, join, balance, build, collect | +| `Rope.edict` | 2: persistent rope | pure AVL split, join, balance, build, collect, normalize | | `ReplaceRange.edict` | 2: persistent rope | closure read, pure replace, `ensure` effects, head retarget | The two targets are separate on purpose. Target 1 needs almost no new language and isolates the Echo effect bridge. Target 2 adds the language features a persistent structure needs. Target 1 then serves as a differential oracle for target 2: they must agree on logical text and outcomes, not physical roots. -Target 1 does not complete the rope. +That agreement is necessary, not sufficient: representation invariants and +admission and effect behavior are validated separately, because two programs +can agree on text while both emitting an invalid graph. Target 1 does not +complete the rope. ## Compiler result @@ -30,6 +33,10 @@ Built against Edict main `e60411fc` with this application's lawpack closure: | `Rope.edict` | parse: `use module` is not an import kind | | `ReplaceRange.edict` | parse: `use module` is not an import kind | +Edict main has since landed bytes literals and explicit escapes (`6e6a0fa`, +edict#249) and source-module compilation (edict#254), which clear all four +first refusals above. The next refusals have not been re-measured. + The parser stops at the first error, so the classification below is per construct. **Confirmed** means a build against Edict main was run for that construct. **Read** means it was established by reading compiler or runtime @@ -42,22 +49,22 @@ source on main, not by running it. | Construct | Used by | Status on main | | --- | --- | --- | | Integer `+` on `U64` | both | refused, **confirmed** (`TypeMismatch`) | -| Variant types and `match` | target 2 | refused, **confirmed** (`only record type declarations`) | +| Variant types and `match` | target 2 | refused, **confirmed** (`only record type declarations`); [edict#261](https://github.com/flyingrobots/edict/issues/261) | | Recursive types with a depth bound | target 2 | refused, **confirmed** (`UnresolvedType`) | -| Recursive functions with a termination measure | target 2 | refused, **confirmed** (`ReferenceCycle`) | +| Recursive functions with a termination measure | target 2 | refused, **confirmed** (`ReferenceCycle`); [edict#262](https://github.com/flyingrobots/edict/issues/262) | | Expression `if … else if …` | both | accepted, **confirmed** | | Bytes slice and concatenation | both | accepted, **confirmed** (leaf-slice, range-assembly probes) | -| Source-module import (`use module`) | both | refused, **confirmed** | -| Bytes literals `b"…"` | both | refused anywhere, **confirmed**: lexed as identifier `b` then a string; [edict#249](https://github.com/flyingrobots/edict/issues/249) | -| `\r` and explicit byte escapes | decoder only | refused, **confirmed**; [edict#249](https://github.com/flyingrobots/edict/issues/249) | -| `Option`, `some`/`none`/`isSome`/`unwrap` | target 2 | refused, read | +| Source-module import (`use module`) | both | landed after the measured run (edict#254); not re-measured | +| Bytes literals `b"…"` | both | landed after the measured run (`6e6a0fa`, edict#249); not re-measured | +| `\r` and explicit byte escapes | decoder only | landed after the measured run (`6e6a0fa`); not re-measured | +| `Option`, `some`/`none`/`isSome`/`unwrap` | target 2 | refused, read; [edict#261](https://github.com/flyingrobots/edict/issues/261) | | `List` construction, `++`, `len(list)` | target 2 | refused, read | | `enum` declarations | target 2 | refused, read | | Record spread `{ ...x, f: v }` | both | refused, read | | Function preconditions and flow-sensitive proofs for `-` and `slice` | both | refused inside functions, read | | Typed failure in pure functions (`fails`, `expect`) | target 2 | not in the spec; proposed | -| `U64` division, `min`/`max` | target 2 | refused, read | -| Source `hash` with a domain label | both | in the spec; not implemented, read | +| `U64` division, `min`/`max`, checked `+` | target 2 | refused, read; [edict#263](https://github.com/flyingrobots/edict/issues/263) | +| `ContentAddressV1` inputs (type id, attachment digest, ordered edges) | both | absent; [edict#260](https://github.com/flyingrobots/edict/issues/260) | ### Generic data-structure primitives @@ -66,22 +73,24 @@ source on main, not by running it. | `core.bytes.at(bytes, i) -> U8` | both | UTF-8 boundary check | | `core.bytes.count(bytes, byte) -> U64` | both | line-break metric | | `core.bytes.isUtf8(bytes) -> Bool` | both | replacement validity | -| `core.cbor.encode(value)` | both | identity input in the canonical codec | +| `echo.attachmentDigest(value)`, `echo.contentAddress(type, digest, edges)` | both | `ContentAddressV1` inputs, Echo's exact codec profile (edict#260) | None of these knows about text editing. They are byte and codec utilities. ### Runtime realization (Echo) -All are covered by the proposed Echo design -[Authored Operation Effects](https://github.com/flyingrobots/echo/blob/docs/edict-authored-operation-effects/docs/architecture/authored-operation-effects.md): +All are covered by the Echo design +[Authored Operation Effects](https://github.com/flyingrobots/echo/blob/main/docs/architecture/authored-operation-effects.md), +whose implementation is [echo#921](https://github.com/flyingrobots/echo/pull/921) (draft): | Need | Used by | Status on main | | --- | --- | --- | | Evaluated operation → proposed effects → atomic commit | both | absent (read) | | `ensure` node: create, or require identical | both | absent; create obstructs on existing (read) | -| Edge read by type, edge `ensure`, edge compare-and-retarget | both | absent (read) | +| Edge read by type, edge `ensure`, edge compare-and-retarget | both | absent (read); edge reads [echo#926](https://github.com/flyingrobots/echo/issues/926) | | Atom compare-and-replace from evaluation | both | only with caller-supplied bytes (read) | -| Guided closure read with a pure Edict selector | target 2 | absent (read) | +| Guided closure read with a pure Edict selector | target 2 | absent (read); [echo#926](https://github.com/flyingrobots/echo/issues/926) | +| Buffers reachable from the worldline root | both | absent (read); [echo#927](https://github.com/flyingrobots/echo/issues/927) | | `for` with effects lowered to Target IR | target 2 | Target refuses `For` (read) | ### Performance and resources @@ -89,18 +98,18 @@ All are covered by the proposed Echo design - Closure size: two boundary paths plus their inner spines, `O(h²)` nodes, with `h ≤ 1.44 log2(leaves)`. Bounded by `text.maxClosureNodes`. - Patch size: about `(h + 1)` new branches, up to 2 new leaves plus - `replacement / 4096` leaves, two edges per branch, one head with its `root` - and `anchor` edges, and one retargeted `canonicalHead` edge. Echo caps a Tick at 128 operations, which a 1 MiB replacement exceeds; - the cap or the replacement bound must move, and that is a measured decision. -- Echo's state root walks all reachable history on every commit (DL-0159 risk). + `ceil(replacement / 4096)` fresh leaves, two edges per branch, one head with + its `root` and `anchor` edges, and one retargeted `canonicalHead` edge. Echo + caps one Action batch at 128 patch operations; a 1 MiB replacement (256 fresh + leaves and 255 branches) is far outside it. The v1 operation supports an + explicit envelope and refuses atomically outside it (DL-0159, Resource + Envelope). +- The equal-length no-op check reads the replaced range, so its reads grow with + the replacement; `text.maxReplacementBytes` bounds it. +- Echo's state root walks the reachable graph, the current representation, on + every commit (DL-0159 risk). - Echo charges a full copy for every local read; `Tree` values are large. -### Ordinary defects - -- [jedit#350](https://github.com/flyingrobots/jedit/issues/350): reopen reuses - a stale rope. Prerequisite for durable file integration. -- [edict#249](https://github.com/flyingrobots/edict/issues/249): lexer escapes. - ## Evidence plan The 40-case oracle (6 committing, 34 obstructed) is a baseline generated from @@ -109,25 +118,28 @@ the native planner. The rope is not complete until these also hold: | Property | Evidence | | --- | --- | | Edit correctness | Generated edit sequences give the same logical text through target 1 and target 2, and through the native planner where its schema 1 cases apply. | -| Persistence | After N edits, every earlier head is still readable and unchanged. | +| Persistence | After N edits, each earlier state is reconstructable exactly to the extent its retention contract promises, and the test names that contract. No predecessor-head chain is kept. | | Structural sharing | Nodes outside the boundary closure keep their ids across an edit. | | Canonicalization | Logically equal facts encode to identical bytes; non-canonical encodings are refused. | | Replay | The same admitted history reproduces identical roots and receipts on a fresh host. | | Atomicity | A failure injected at any effect of a multi-node edit leaves no partial effect. | | Conflict | A stale basis, or an `ensure` that meets different existing content, obstructs safely. | | Unicode | UTF-8 boundaries, multi-byte scalars, combining marks, and surrogate-pair characters (four-byte UTF-8) at every split position. | -| Resource bounds | Exhausting steps, bytes, closure nodes, or the Tick operation cap gives a typed result with no commit. | -| Reopen and save | An external file change can never silently reuse stale rope state (#350). | +| Resource bounds | Exhausting steps, bytes, closure nodes, effects, or the Action-batch patch cap gives `ResourceLimitExceeded` with no commit. | +| Reopen and save | DL-0159's file-crossing gate. | | Commutation | Two edits against one fixed basis: state exactly when their order can commute, and test that condition rather than assume it. | -| Closure sufficiency | Over generated trees and ranges, `replace` never fails with `ClosureTooSmall` under the selector. | +| Closure sufficiency | Over generated trees and ranges, `replace` never fails with `ClosureTooSmall` (`ClosureInsufficient`) under the selector. | +| Identity | Source and bridge compute identical `ContentAddressV1` ids from published vectors, including empty and non-empty heads. | +| Normalization | Equal-content leaves yield one effect per id and both text positions survive. | ## Open design points in the drafts - The closure selector's expansion rule (boundary paths, inner spines, and the no-op range) is argued, not proven. A `ClosureTooSmall` failure maps to - `MalformedRope`; it should instead be impossible, and a property test must - show it. -- Duplicate fresh leaves with equal content produce the same id twice; the - effect bridge must make a repeated `ensure` in one proposal canonical. + `ClosureInsufficient`, a defect in the law, never `MalformedRope`; it should + be impossible, and a property test must show it. +- Duplicate fresh leaves with equal content produce the same id twice. The + source normalizes them (`rope.normalized`) before emitting the proposal; + the bridge keeps rejecting duplicate targets. - `Reference.edict`'s single text node is bounded at 1 MiB; target 1 says nothing about larger buffers. diff --git a/edict/replace-range/draft/Reference.edict b/edict/replace-range/draft/Reference.edict index 37538f03..a551b664 100644 --- a/edict/replace-range/draft/Reference.edict +++ b/edict/replace-range/draft/Reference.edict @@ -66,7 +66,7 @@ intent replaceRange(input: Input) returns Result + slice(old.bytes, input.endByte, len(old.bytes)); require len(bytes) <= 1048576u64 else text.RangeOutOfBounds; // needs a bound proof let fact = { bytes, lineBreaks: v2.lineBreaks(bytes) }; - let newTextId = v2.nodeId("text", core.cbor.encode(fact), []); // PROPOSED encode + let newTextId = v2.contentId(fact, []); echo.ref(newTextId).ensure(fact) else text.ContentIdentityMismatch; let newHead = { @@ -74,7 +74,10 @@ intent replaceRange(input: Input) returns Result lineCount: fact.lineBreaks + 1u64, // needs checked + sequence: head.sequence + 1u64, }; - let newHeadId = v2.nodeId("head", core.cbor.encode(newHead), [newTextId, importId]); + let newHeadId = v2.contentId(newHead, [ + { edgeType: typeId(), to: newTextId }, + { edgeType: typeId(), to: importId }, + ]); let newHeadRef = echo.ref(newHeadId); newHeadRef.ensure(newHead) else text.ContentIdentityMismatch; echo.edge(newHeadRef) diff --git a/edict/replace-range/draft/ReplaceRange.edict b/edict/replace-range/draft/ReplaceRange.edict index 8df2154c..5df4abfa 100644 --- a/edict/replace-range/draft/ReplaceRange.edict +++ b/edict/replace-range/draft/ReplaceRange.edict @@ -96,6 +96,8 @@ intent replaceRange(input: Input) returns Result let importId = echo.edge(headRef) .target() else text.FactMissing; require input.endByte <= head.byteLength else text.RangeOutOfBounds; + require len(input.replacement) <= text.maxReplacementBytes + else text.ResourceLimitExceeded; // the v1 envelope (DL-0159) require core.bytes.isUtf8(input.replacement) else text.Utf8BoundaryInvalid; // PROPOSED let want = { @@ -109,7 +111,10 @@ intent replaceRange(input: Input) returns Result expand(want, _, _), // PROPOSED partial application maxNodes: text.maxClosureNodes, maxDepth: text.maxTreeHeight, - ).read() else text.MalformedRope; + ).read() else { + LimitReached => text.ResourceLimitExceeded, // PROPOSED: closure-read outcomes (echo#926) + InvariantViolated => text.MalformedRope, + }; require rope.byteLength(root) == head.byteLength else text.MalformedRope; require rope.isCharBoundaryIn(root, input.startByte) else text.Utf8BoundaryInvalid; @@ -119,8 +124,11 @@ intent replaceRange(input: Input) returns Result else text.NoOp; let next = rope.replace(root, input.startByte, input.endByte, input.replacement) - else { ClosureTooSmall => text.MalformedRope }; // PROPOSED: map a pure failure - let fresh = rope.created(next); + else { ClosureTooSmall => text.ClosureInsufficient }; // a defect in the selector, not in the data + // Repeated text yields repeated content ids. Emit one effect per id, refuse + // an id with two different contents, keep canonical order (DL-0159). + let fresh = rope.normalized(rope.created(next)) + else { ConflictingContent => text.ContentIdentityMismatch }; for leaf in fresh.leaves bounded text.maxCreatedLeaves { echo.ref(leaf.id).ensure(leaf.fact) else text.ContentIdentityMismatch; @@ -141,7 +149,13 @@ intent replaceRange(input: Input) returns Result sequence: head.sequence + 1u64, }; let rootId = if m.byteLength == 0u64 then none() else some(rope.idOf(next)); - let newHeadId = v2.nodeId("head", core.cbor.encode({ newHead, rootId }), [importId]); + // The head's id commits to the fact it stores and its actual edges: anchor, + // plus root when the text is non-empty. + let anchorEdge = { edgeType: typeId(), to: importId }; + let headEdges = if isSome(rootId) + then [{ edgeType: typeId(), to: unwrap(rootId) }, anchorEdge] + else [anchorEdge]; + let newHeadId = v2.contentId(newHead, headEdges); let newHeadRef = echo.ref(newHeadId); newHeadRef.ensure(newHead) else text.ContentIdentityMismatch; if isSome(rootId) { diff --git a/edict/replace-range/draft/Rope.edict b/edict/replace-range/draft/Rope.edict index 1d8193da..9b7a9b57 100644 --- a/edict/replace-range/draft/Rope.edict +++ b/edict/replace-range/draft/Rope.edict @@ -37,6 +37,7 @@ type Created = { // A pure function may fail only with a declared, typed failure. The caller // maps it to an obstruction. // PROPOSED: `fails` / `expect` failure ClosureTooSmall; +failure ConflictingContent; // ---- Metrics and constructors ---- @@ -63,7 +64,7 @@ fn idOf(t: Tree) -> NodeId fails ClosureTooSmall { fn leaf(bytes: Bytes) -> Tree { let fact = { bytes, lineBreaks: v2.lineBreaks(bytes) }; - return Tree::Leaf({ id: v2.nodeId("leaf", core.cbor.encode(fact), []), fact, fresh: true }); + return Tree::Leaf({ id: v2.contentId(fact, []), fact, fresh: true }); } // Both sides must be non-empty. Heights must differ by at most one. @@ -75,7 +76,10 @@ fn branch(l: Tree, r: Tree) -> Tree fails ClosureTooSmall { lineBreaks: ml.lineBreaks + mr.lineBreaks, height: max(ml.height, mr.height) + 1u8, // PROPOSED max }; - let id = v2.nodeId("branch", core.cbor.encode(fact), [expect idOf(l), expect idOf(r)]); + let id = v2.contentId(fact, [ + { edgeType: typeId(), to: expect idOf(l) }, + { edgeType: typeId(), to: expect idOf(r) }, + ]); return Tree::Branch({ id, fact, left: l, right: r, fresh: true }); } @@ -255,6 +259,16 @@ fn created(t: Tree) -> Created }; } +// The proposal Echo receives may not name one target twice (DL-0159, effect +// normalization). Equal text yields equal content ids, so keep the first of +// each id, refuse an id whose two occurrences differ, and sort by id. +fn normalized(c: Created) -> Created fails ConflictingContent { + return { + leaves: expect dedupeById(c.leaves, _.id, _.fact), // PROPOSED generic list helper + branches: expect dedupeById(c.branches, _.id, _.fact), + }; +} + // The bytes in [start, end), for the no-op check. Leaves in the range must be // expanded; the closure read expands them only when the range length equals // the replacement length, because otherwise the edit cannot be a no-op. diff --git a/edict/replace-range/draft/Text.edict b/edict/replace-range/draft/Text.edict index 806444c9..7ac6921a 100644 --- a/edict/replace-range/draft/Text.edict +++ b/edict/replace-range/draft/Text.edict @@ -6,7 +6,7 @@ package jedit.text.v2@1; use lawpack jedit.text@2 as text; use target echo.dpo@1 as echo; -// ---- Stored facts (alpha atoms, canonical CBOR v1) ---- +// ---- Stored facts (alpha atoms, Echo's canonical codec profile) ---- type BufferFact = { bufferKey: String, @@ -30,41 +30,60 @@ type LeafFact = { lineBreaks: U64, }; -// Provenance only: the bytes a head's lineage was imported from. Copying the -// anchor forward never claims the rope still matches the file. +// Provenance only: the bytes a head's lineage was imported from, and the +// observation that witnessed them. Copying the anchor forward never claims the +// rope still matches the file. type ImportFact = { fileCoordinate: String, hostDigest: Bytes, + observation: Bytes, }; -// Synchronization: one witnessed write of a buffer's bytes to its file. -// Evidence of the crossing, not file authority. `exportEvent` names the causal -// event that witnessed the write; the exported head is not reachable from it. +// The host version Jim currently works against (DL-0159, accepted host basis). +// `evidence` names the observation or export that made it current; +// `generation` increases with every transition. +type HostBasisFact = { + fileCoordinate: String, + hostDigest: Bytes, + evidence: Bytes, + generation: U64, +}; + +// What Jim last exported: evidence of one crossing, never the synchronization +// basis and never file authority. Every field names evidence that existed +// before this node was written; the exported head is not reachable from it. type ExportFact = { + exportIntent: Bytes, fileCoordinate: String, logicalDigest: Bytes, hostDigest: Bytes, - exportEvent: Bytes, + observation: Bytes, }; // ---- Edge types (no payload; one edge per source node and type) ---- +type BufferSlot = Unit; // worldline root -> Buffer, one per buffer (echo#927) type CanonicalHead = Unit; // Buffer -> Head +type AcceptedHostBasis = Unit; // Buffer -> HostBasis, retargeted by basis transitions type Root = Unit; // Head -> Branch | Leaf type Anchor = Unit; // Head -> Import, copied to every new head -type LastExport = Unit; // Buffer -> Export, retargeted by each save +type LastExport = Unit; // Buffer -> Export, retargeted by each confirmed export // No head-to-predecessor edge: Echo's ticks and receipts own history (DL-0159). type Left = Unit; // Branch -> Branch | Leaf type Right = Unit; // Branch -> Branch | Leaf -// ---- Identity law ---- +// ---- Identity law: Echo ContentAddressV1 (DL-0159) ---- +// +// A content node's id commits to its type, the attachment digest of the atom +// it actually stores, and its complete outgoing edge set. Echo recomputes it +// and refuses a mismatch, so source computes it from the same inputs, never +// from an application-specific recipe. Edge ids (content and slot) are +// computed by the edge effects themselves. -fn nodeId(kind: String, atom: Bytes, children: List) -> NodeId { - return hash("jedit.text.node.v2", { kind, atom, children }); -} +type OutEdge = { edgeType: TypeId, to: NodeId }; -fn edgeId(from: NodeId, edgeType: String) -> EdgeId { - return hash("jedit.text.edge.v2", { from, edgeType }); +fn contentId(atom: T, edges: List) -> NodeId { // PROPOSED generic helper + return echo.contentAddress(typeId(), echo.attachmentDigest(atom), edges); // PROPOSED: edict#260 } // ---- Text metrics ---- From 72dbe2c3cffa1d4fd5b94941205299514e93dca1 Mon Sep 17 00:00:00 2001 From: James Ross Date: Tue, 20 Oct 2026 16:30:01 -0700 Subject: [PATCH 2/2] docs(design): settle DL-0159's remaining review points Second review ruling: approve the architecture; correct four points. - Overwrite carries two preconditions: expectedAcceptedBasis (B's identity and generation, deciding outcome applicability) and expectedHostContents (the observed H it replaces), with overwriteAuthority bound to H's observation. H is never accepted to pass the check; a confirmed Overwrite of S advances the basis from B to S. - Observation ordering and applicability: observations name their file binding and receiving basis, record order where the adapter can, and an older or unordered observation cannot replace the current host view, head, or conflict judgment; adoption revalidates or re-observes. The generation orders Jim's transitions, not observations. - The worldline-root attachment is conceptual, its layout pending echo#927 (index first); the fixture attaches two buffers. - Cost model counts the replacement tree's K leaves and K - 1 branches, K being fromBytes's actual leaf count, plus boundary and join reconstruction; construction work is separate from emitted effects; measurement covers sizes just above split thresholds. Also: branch normalization compares the stored definition (fact and child ids); the oracle compares within the shared supported domain; Reference.edict omits Root for empty text and uses its own resource profile; drafts build records explicitly instead of record spread; every draft construct has an owner issue (edict#264-#267 filed). --- docs/design/0159-edict-rope-representation.md | 115 ++++++++++++++---- edict/replace-range/draft/README.md | 36 +++--- edict/replace-range/draft/Reference.edict | 35 ++++-- edict/replace-range/draft/ReplaceRange.edict | 20 +-- edict/replace-range/draft/Rope.edict | 14 ++- edict/replace-range/draft/Text.edict | 6 +- 6 files changed, 160 insertions(+), 66 deletions(-) diff --git a/docs/design/0159-edict-rope-representation.md b/docs/design/0159-edict-rope-representation.md index 0b48b863..1fa6d556 100644 --- a/docs/design/0159-edict-rope-representation.md +++ b/docs/design/0159-edict-rope-representation.md @@ -168,7 +168,7 @@ contains the node itself, so no identity is circular. | Edge type | From → to | Meaning | | --- | --- | --- | -| `jedit.text.buffer` (per buffer, see Reachability) | worldline root → Buffer | attaches the buffer to the committed state | +| `jedit.text.buffer` (conceptual; layout pending echo#927) | worldline root → Buffer | attaches each buffer to the committed state | | `jedit.text.canonicalHead` | Buffer → Head | current head; retargeted by each edit | | `jedit.text.acceptedHostBasis` | Buffer → HostBasis | the host version Jim currently works against; retargeted by the transitions below | | `jedit.text.lastExport` | Buffer → Export | what Jim last exported; never the synchronization basis | @@ -249,14 +249,22 @@ witnessed per-node metric. ### Reachability A worldline holds many buffers, so the Buffer is not the worldline root. Each -Buffer is reached from the worldline root by its own typed edge, created in the -same proposal as the Buffer (echo#927). The committed current state is then: +Buffer must be reached from the worldline root, in the same proposal that +creates it. The relation is conceptual: its concrete layout is unresolved. +Under `ContentAddressV1` a mutable source has one slot edge per source and +type, so one fixed `jedit.text.buffer` type from the root admits only one +buffer. echo#927 owns the choice between a per-key slot type and a root-owned +index; the index is investigated first, because a derived per-buffer type id +must also satisfy the bridge's admitted schema and type allowlists. The +committed current state is then: the Buffer, its canonical Head and rope, the Head's Import, the `acceptedHostBasis` and `lastExport` targets, and declared current metadata, with no edge from any head to the head it replaced. The reachability fixture starts at the **actual worldline root**, never at a -conveniently chosen Buffer. +conveniently chosen Buffer, and attaches at least two buffers: both stay +reachable and committed, and editing one neither replaces nor disconnects the +other. A one-buffer fixture would pass while missing the problem. ### History, current state, and retained material @@ -285,17 +293,31 @@ it. Each limit is a lawpack constant: | Generated nodes and effects | `text.maxCreatedLeaves`, `text.maxCreatedBranches`, `text.maxEffects` | the proposal | | Evaluation work and allocation | `text.replaceRangeBudget` | the evaluator meter | -A proposal costs about `(h + 1)` path-copied branches plus -`ceil(replacement / 4096) + 2` fresh leaves, one head, and one Buffer update, -where `h ≤ 1.44 log2(leaves)`; each content node is one node, one atom, and up -to two edges. The equal-length no-op check reads the replaced range, so its -reads grow with the replacement, not only with boundary paths and spines; the -replacement bound bounds it. +A proposal's construction is three parts, where `h ≤ 1.44 log2(leaves)`: + +- **Replacement tree.** `fromBytes` produces K leaves for a non-empty + replacement and K − 1 internal branches. K is the constructor's actual leaf + count, not `ceil(replacement / 4096)`: it splits at character boundaries + near the midpoint, so 8,194 ASCII bytes split into two 4,097-byte halves and + then into four leaves and three branches, where `ceil(8194 / 4096) = 3`. +- **Boundary and join reconstruction.** Up to two split boundary leaves and + the branches the splits and joins path-copy, about `O(h)` per boundary and + per join spine. +- **Publication.** One head with its `root` and `anchor` edges and one Buffer + update. + +Each content node is one node, one atom, and up to two edges. Construction work +and emitted effects differ: normalization can merge equal-content targets, so +fewer effects may be emitted, but the work to build and recognize that content +is still spent and metered. The equal-length no-op check reads the replaced +range, so its reads grow with the replacement, not only with boundary paths and +spines; the replacement bound bounds it. Under Echo's current 128 patch operations per Action batch, a 1 MiB replacement (256 fresh leaves and 255 branches) is far outside any envelope. The v1 values -are chosen from a measurement fixture over generated trees and recorded with -their cost model before the representation gate; raising a cap without that +are chosen from a measurement fixture over generated trees, including sizes +just above split thresholds (4,097, 8,193, and 8,194 bytes, not only powers of +two), and recorded with their cost model before the representation gate; raising a cap without that model is out of scope. Larger edits are a separate operation family (#382). Three failures stay distinct, and none accuses valid data of corruption: @@ -332,7 +354,11 @@ Generic capabilities the representation gate needs: | `ContentAddressV1` inputs in Edict source | edict#260 | | Variant and `Option` types | edict#261 | | Bounded recursion over depth-bounded variants | edict#262 | -| Checked arithmetic, `min`, `max` | edict#263 | +| Checked arithmetic, `min`, `max`, division | edict#263 | +| Function preconditions for subtraction and slice | edict#264 | +| Typed failures in pure functions | edict#265 | +| Byte primitives (`at`, `count`, `isUtf8`) | edict#266 | +| Bounded effect-emitting loops lowered to Target IR | edict#267 | ## File-Crossing Contract @@ -386,8 +412,11 @@ its mapping. | Confirm an applicable export of S | the witnessed exported host version S | Each `HostBasis` names the evidence that made it current and a `generation` -that increases with every transition, so a stale evidence item can never be -mistaken for the current one by digest equality alone. +that increases with every transition. The generation orders Jim's own +transitions; it does not make an observation newer. Adopting a delayed older +observation would advance the generation while the accepted external version +went backward, so applicability is a separate rule (requirement 5 under +Observation, holding, and adoption). ### Versions and conditions @@ -412,12 +441,18 @@ mistaken for the current one by digest equality alone. or fences writes per binding: each intent carries a fencing generation, and an effector holding a stale generation does not write. - **Each export captures** its stable intent identity, the exact head - exported, the expected accepted host basis, the file binding and its - authorization, and the observations and host-attempt evidence that belong to - it. + exported, the file binding and its authorization, the observations and + host-attempt evidence that belong to it, and two separate preconditions: + - `expectedAcceptedBasis`: the identity and generation of the accepted host + basis B when the export was admitted. It decides whether the outcome still + applies to Jim's current state. + - `expectedHostContents`: the host version the write expects to replace, + enforced as far as the export profile allows. For an ordinary export it is + B. Only Overwrite sets it to an observed H ≠ B, and then also carries + `overwriteAuthority`, the authorization bound to H's observation. - **Outcomes are evidence first.** An outcome advances the accepted host basis - only if its intent is the binding's current one and the basis it expected is - still accepted. Otherwise it is retained as historical evidence and changes + only if its intent is the binding's current one and its + `expectedAcceptedBasis` is still accepted. Otherwise it is retained as historical evidence and changes no current state. A delayed older outcome never regresses a newer basis. - **Observation identity.** The intent keeps one identity across retries. Each physical read is a new observation with a new identity; retransmitting an @@ -465,6 +500,19 @@ turn a snapshot into an external editor's witnessed causal history. 4. **Adoption is a separate admitted forward transition** that creates a head anchored to the new `Import` and sets the accepted host basis. Automatic adoption is allowed only under a declared policy, and is still witnessed. +5. **Observation ordering and applicability.** This concerns the order of + Jim's own observations, not external writers' histories: + - An observation names its file binding and the receiving basis it was + captured against (the accepted host basis and its generation). + - Where the adapter can establish the order of its observations, it records + that order as epoch, sequence, or causal evidence. + - Historical observations may still enter history as evidence. + - An observation older than, or unordered with, the current host view + cannot automatically replace the current host view, the canonical head, or + a conflict judgment. + - Adoption and settlement revalidate the receiving basis and the + observation's applicability at admission. If applicability cannot be + established, Jim obtains a fresh observation instead. ### Path classification @@ -502,8 +550,12 @@ Settlements, each an admitted forward operation: - **Reload:** adopt H. L stays recoverable only if its material was retained before the Reload; that retention is acquired first, or Reload refuses. - **Keep local:** keep editing L; export stays obstructed by the divergence. -- **Overwrite:** an explicit export whose expected basis is H, recorded as - overwriting a known third-party change. +- **Overwrite:** an explicit export whose `expectedAcceptedBasis` is B, + whose `expectedHostContents` is the observed H, and whose + `overwriteAuthority` is bound to H's observation, recorded as overwriting a + known third-party change. H is never accepted just to satisfy the + applicability check. A confirmed Overwrite of S advances the accepted host + basis from B to S. - **Reconcile:** build M from B, L, and H and submit it as a forward edit; the accepted host basis becomes H. The base may be an observed host version that was never a Jim head. @@ -604,9 +656,13 @@ Representation gate: 3. The persistent rope (persistence target), with effect normalization and the three failure classes. 4. The resource-envelope measurement fixture and its recorded v1 values. -5. The schema 2 oracle: reference and persistent rope agree on text semantics; - representation invariants and admission/effect behavior are validated - separately. +5. The schema 2 oracle: reference and persistent rope agree on text semantics + within their shared supported domain; each implementation's resource + behavior is validated against its own declared profile, so a disagreement + between resource limits is never reported as an editing disagreement. + Representation invariants and admission/effect behavior are validated + separately. Stored-buffer size and the complete encoded invocation size are + separate limits. 6. Cutover, then deletion of the native schema 1 law. File-crossing gate: @@ -628,7 +684,8 @@ Representation gate: | Two equal-content leaves | the proposal has no duplicate targets; both text positions still exist | | `aa` as one shared leaf, edit the second `a` | the edit addresses the second position | | Exhaust a closure or effect budget, or fail the final effect | correctly classified outcome; no partial application | -| Traverse from the actual worldline root | all current representation is committed; no historical-head chain | +| Traverse from the actual worldline root with two buffers attached | both reachable and committed; editing one leaves the other attached; no historical-head chain | +| Replacements of 4,097, 8,193, and 8,194 bytes | leaf and branch counts match the constructor, not `ceil(n / 4096)` | | Restart after edits | recovered state equals the pre-restart state | File-crossing gate: @@ -638,6 +695,8 @@ File-crossing gate: | Read B → external write X → Jim writes L → read L | no claim that interference was detected or prevented | | Crash with final bytes equal to the intended or the prior bytes | recovery preserves uncertainty about the original write | | Adopt an external version after an earlier export | the next save uses the newly accepted basis | +| B ≠ H; authorize Overwrite against H; export S | the accepted basis advances to S; the next ordinary save does not rediscover the settled divergence | +| Two observations captured against the same B, delivered in reverse order | the older one cannot be adopted over the newer; adoption revalidates applicability or asks for a fresh observation | | H = L ≠ B | agreement accepted; no Export fabricated | | Reconcile to M, then save | the accepted basis is H; the same divergence is not rediscovered | | An older export outcome arrives after a newer one | evidence retained; current basis not regressed | @@ -652,7 +711,9 @@ File-crossing gate: implementations and the envelope recorded with its cost model. - File-crossing gate: slices 7–9 green, with every claim recorded at the strength its evidence supports. -- Every needed generic capability has an owner issue (listed above). +- Every needed generic capability has an owner issue (listed above and in the + draft README), or the first witness stops needing it. This stays a gate + criterion until the mapping is complete. ## Validation Plan diff --git a/edict/replace-range/draft/README.md b/edict/replace-range/draft/README.md index f4062de2..210de9c0 100644 --- a/edict/replace-range/draft/README.md +++ b/edict/replace-range/draft/README.md @@ -48,7 +48,7 @@ source on main, not by running it. | Construct | Used by | Status on main | | --- | --- | --- | -| Integer `+` on `U64` | both | refused, **confirmed** (`TypeMismatch`) | +| Integer `+` on `U64` | both | unsigned addition landed after the measured run (edict#259); checked overflow [edict#263](https://github.com/flyingrobots/edict/issues/263) | | Variant types and `match` | target 2 | refused, **confirmed** (`only record type declarations`); [edict#261](https://github.com/flyingrobots/edict/issues/261) | | Recursive types with a depth bound | target 2 | refused, **confirmed** (`UnresolvedType`) | | Recursive functions with a termination measure | target 2 | refused, **confirmed** (`ReferenceCycle`); [edict#262](https://github.com/flyingrobots/edict/issues/262) | @@ -58,12 +58,12 @@ source on main, not by running it. | Bytes literals `b"…"` | both | landed after the measured run (`6e6a0fa`, edict#249); not re-measured | | `\r` and explicit byte escapes | decoder only | landed after the measured run (`6e6a0fa`); not re-measured | | `Option`, `some`/`none`/`isSome`/`unwrap` | target 2 | refused, read; [edict#261](https://github.com/flyingrobots/edict/issues/261) | -| `List` construction, `++`, `len(list)` | target 2 | refused, read | -| `enum` declarations | target 2 | refused, read | -| Record spread `{ ...x, f: v }` | both | refused, read | -| Function preconditions and flow-sensitive proofs for `-` and `slice` | both | refused inside functions, read | -| Typed failure in pure functions (`fails`, `expect`) | target 2 | not in the spec; proposed | -| `U64` division, `min`/`max`, checked `+` | target 2 | refused, read; [edict#263](https://github.com/flyingrobots/edict/issues/263) | +| `List` construction, `++`, `len(list)` | target 2 | refused, read; [edict#262](https://github.com/flyingrobots/edict/issues/262) | +| `enum` declarations | target 2 | refused, read; payload-free variants, [edict#261](https://github.com/flyingrobots/edict/issues/261) | +| Record spread `{ ...x, f: v }` | none | removed from the drafts: records are built explicitly | +| Function preconditions and flow-sensitive proofs for `-` and `slice` | both | refused inside functions, read; [edict#264](https://github.com/flyingrobots/edict/issues/264) | +| Typed failure in pure functions (`fails`, `expect`) | target 2 | not in the spec; proposed; [edict#265](https://github.com/flyingrobots/edict/issues/265) | +| `U64` division, `min`/`max`, checked `+` and `-` | target 2 | refused, read; [edict#263](https://github.com/flyingrobots/edict/issues/263) | | `ContentAddressV1` inputs (type id, attachment digest, ordered edges) | both | absent; [edict#260](https://github.com/flyingrobots/edict/issues/260) | ### Generic data-structure primitives @@ -76,6 +76,8 @@ source on main, not by running it. | `echo.attachmentDigest(value)`, `echo.contentAddress(type, digest, edges)` | both | `ContentAddressV1` inputs, Echo's exact codec profile (edict#260) | None of these knows about text editing. They are byte and codec utilities. +The byte primitives are [edict#266](https://github.com/flyingrobots/edict/issues/266); +the identity inputs are [edict#260](https://github.com/flyingrobots/edict/issues/260). ### Runtime realization (Echo) @@ -85,22 +87,26 @@ whose implementation is [echo#921](https://github.com/flyingrobots/echo/pull/921 | Need | Used by | Status on main | | --- | --- | --- | -| Evaluated operation → proposed effects → atomic commit | both | absent (read) | -| `ensure` node: create, or require identical | both | absent; create obstructs on existing (read) | +| Evaluated operation → proposed effects → atomic commit | both | absent (read); [echo#921](https://github.com/flyingrobots/echo/pull/921) | +| `ensure` node: create, or require identical | both | absent; create obstructs on existing (read); [echo#921](https://github.com/flyingrobots/echo/pull/921) | | Edge read by type, edge `ensure`, edge compare-and-retarget | both | absent (read); edge reads [echo#926](https://github.com/flyingrobots/echo/issues/926) | -| Atom compare-and-replace from evaluation | both | only with caller-supplied bytes (read) | +| Atom compare-and-replace from evaluation | both | only with caller-supplied bytes (read); [echo#921](https://github.com/flyingrobots/echo/pull/921) | | Guided closure read with a pure Edict selector | target 2 | absent (read); [echo#926](https://github.com/flyingrobots/echo/issues/926) | | Buffers reachable from the worldline root | both | absent (read); [echo#927](https://github.com/flyingrobots/echo/issues/927) | -| `for` with effects lowered to Target IR | target 2 | Target refuses `For` (read) | +| `for` with effects lowered to Target IR | target 2 | Target refuses `For` (read); [edict#267](https://github.com/flyingrobots/edict/issues/267), runtime [echo#921](https://github.com/flyingrobots/echo/pull/921) | ### Performance and resources - Closure size: two boundary paths plus their inner spines, `O(h²)` nodes, with `h ≤ 1.44 log2(leaves)`. Bounded by `text.maxClosureNodes`. -- Patch size: about `(h + 1)` new branches, up to 2 new leaves plus - `ceil(replacement / 4096)` fresh leaves, two edges per branch, one head with - its `root` and `anchor` edges, and one retargeted `canonicalHead` edge. Echo - caps one Action batch at 128 patch operations; a 1 MiB replacement (256 fresh +- Patch size has three parts (DL-0159, Resource Envelope): the replacement tree, + K leaves and K − 1 branches where K is `fromBytes`'s actual leaf count (8,194 + ASCII bytes give four leaves and three branches, not `ceil(8194 / 4096) = 3` + leaves); boundary and join reconstruction, about `O(h)` path-copied branches + and up to two split boundary leaves; and publication, one head with its `root` + and `anchor` edges and one retargeted `canonicalHead` edge. Normalization can + reduce emitted effects but not construction work. Echo caps one Action batch + at 128 patch operations; a 1 MiB replacement (256 fresh leaves and 255 branches) is far outside it. The v1 operation supports an explicit envelope and refuses atomically outside it (DL-0159, Resource Envelope). diff --git a/edict/replace-range/draft/Reference.edict b/edict/replace-range/draft/Reference.edict index a551b664..5516a4cc 100644 --- a/edict/replace-range/draft/Reference.edict +++ b/edict/replace-range/draft/Reference.edict @@ -47,12 +47,15 @@ intent replaceRange(input: Input) returns Result let headRef = echo.ref(input.basisHeadId); let head = headRef.read() else text.FactMissing; - let textId = echo.edge(headRef) - .target() else text.FactMissing; let importId = echo.edge(headRef) .target() else text.FactMissing; - let old = echo.ref(textId).read() else text.FactMissing; - require len(old.bytes) == head.byteLength else text.MalformedRope; + // An empty head has no Root edge (DL-0159, Identity law). + let oldBytes = if head.byteLength == 0u64 then b"" + else (echo.ref( + echo.edge(headRef).target() else text.MalformedRope, + ).read() else text.FactMissing).bytes; + require len(oldBytes) == head.byteLength else text.MalformedRope; + let old = { bytes: oldBytes }; require input.endByte <= len(old.bytes) else text.RangeOutOfBounds; require v2.isCharBoundary(old.bytes, input.startByte) else text.Utf8BoundaryInvalid; @@ -64,30 +67,36 @@ intent replaceRange(input: Input) returns Result let bytes = slice(old.bytes, 0u64, input.startByte) + input.replacement + slice(old.bytes, input.endByte, len(old.bytes)); - require len(bytes) <= 1048576u64 else text.RangeOutOfBounds; // needs a bound proof + // The reference's own declared profile; the oracle compares outcomes only + // inside the domain both implementations support (DL-0159, slice 5). + require len(bytes) <= text.maxReferenceBufferBytes else text.ResourceLimitExceeded; let fact = { bytes, lineBreaks: v2.lineBreaks(bytes) }; let newTextId = v2.contentId(fact, []); - echo.ref(newTextId).ensure(fact) else text.ContentIdentityMismatch; let newHead = { byteLength: len(bytes), lineCount: fact.lineBreaks + 1u64, // needs checked + sequence: head.sequence + 1u64, }; - let newHeadId = v2.contentId(newHead, [ - { edgeType: typeId(), to: newTextId }, - { edgeType: typeId(), to: importId }, - ]); + let anchorEdge = { edgeType: typeId(), to: importId }; + let headEdges = if len(bytes) == 0u64 + then [anchorEdge] + else [{ edgeType: typeId(), to: newTextId }, anchorEdge]; + let newHeadId = v2.contentId(newHead, headEdges); let newHeadRef = echo.ref(newHeadId); newHeadRef.ensure(newHead) else text.ContentIdentityMismatch; - echo.edge(newHeadRef) - .ensure(newTextId) else text.ContentIdentityMismatch; // PROPOSED: edge ensure + if len(bytes) != 0u64 { + echo.ref(newTextId).ensure(fact) else text.ContentIdentityMismatch; + echo.edge(newHeadRef) + .ensure(newTextId) else text.ContentIdentityMismatch; // PROPOSED: edge ensure + } echo.edge(newHeadRef) .ensure(importId) else text.ContentIdentityMismatch; echo.edge(bufferRef) .replace(input.basisHeadId, newHeadId) else text.BasisNotCanonical; // PROPOSED: compare-and-retarget - bufferRef.replace({ ...buffer, version: buffer.version + 1u64 }) else text.BasisNotCanonical; + bufferRef.replace({ bufferKey: buffer.bufferKey, version: buffer.version + 1u64 }) + else text.BasisNotCanonical; return { headId: newHeadId, diff --git a/edict/replace-range/draft/ReplaceRange.edict b/edict/replace-range/draft/ReplaceRange.edict index 5df4abfa..e3e0890f 100644 --- a/edict/replace-range/draft/ReplaceRange.edict +++ b/edict/replace-range/draft/ReplaceRange.edict @@ -53,17 +53,19 @@ type Expansion = { left: Option, right: Option }; fn contains(lo: U64, hi: U64, at: U64) -> Bool { return lo <= at && at <= hi; } +fn withSpine(v: Visit, spine: Spine) -> Visit { return { lo: v.lo, hi: v.hi, spine }; } + fn expand(want: Want, visit: Visit, leftLength: U64) -> Expansion { let mid = visit.lo + leftLength; // needs checked + let left = { lo: visit.lo, hi: mid, spine: Spine::Boundary }; let right = { lo: mid, hi: visit.hi, spine: Spine::Boundary }; return match visit.spine { - RightSpine => { left: none(), right: some({ ...right, spine: Spine::RightSpine }) }, - LeftSpine => { left: some({ ...left, spine: Spine::LeftSpine }), right: none() }, - Range => { left: some({ ...left, spine: Spine::Range }), right: some({ ...right, spine: Spine::Range }) }, + RightSpine => { left: none(), right: some(withSpine(right, Spine::RightSpine)) }, + LeftSpine => { left: some(withSpine(left, Spine::LeftSpine)), right: none() }, + Range => { left: some(withSpine(left, Spine::Range)), right: some(withSpine(right, Spine::Range)) }, Boundary => { - left: some(if touches(want, left) then left else { ...left, spine: sideSpine(want, left, Spine::RightSpine) }), - right: some(if touches(want, right) then right else { ...right, spine: sideSpine(want, right, Spine::LeftSpine) }), + left: some(if touches(want, left) then left else withSpine(left, sideSpine(want, left, Spine::RightSpine))), + right: some(if touches(want, right) then right else withSpine(right, sideSpine(want, right, Spine::LeftSpine))), }, }; } @@ -128,7 +130,10 @@ intent replaceRange(input: Input) returns Result // Repeated text yields repeated content ids. Emit one effect per id, refuse // an id with two different contents, keep canonical order (DL-0159). let fresh = rope.normalized(rope.created(next)) - else { ConflictingContent => text.ContentIdentityMismatch }; + else { + ConflictingContent => text.ContentIdentityMismatch, + ClosureTooSmall => text.ClosureInsufficient, + }; for leaf in fresh.leaves bounded text.maxCreatedLeaves { echo.ref(leaf.id).ensure(leaf.fact) else text.ContentIdentityMismatch; @@ -167,7 +172,8 @@ intent replaceRange(input: Input) returns Result echo.edge(bufferRef) .replace(input.basisHeadId, newHeadId) else text.BasisNotCanonical; // PROPOSED: compare-and-retarget - bufferRef.replace({ ...buffer, version: buffer.version + 1u64 }) else text.BasisNotCanonical; + bufferRef.replace({ bufferKey: buffer.bufferKey, version: buffer.version + 1u64 }) + else text.BasisNotCanonical; return { headId: newHeadId, diff --git a/edict/replace-range/draft/Rope.edict b/edict/replace-range/draft/Rope.edict index 9b7a9b57..dccb81a0 100644 --- a/edict/replace-range/draft/Rope.edict +++ b/edict/replace-range/draft/Rope.edict @@ -261,14 +261,22 @@ fn created(t: Tree) -> Created // The proposal Echo receives may not name one target twice (DL-0159, effect // normalization). Equal text yields equal content ids, so keep the first of -// each id, refuse an id whose two occurrences differ, and sort by id. -fn normalized(c: Created) -> Created fails ConflictingContent { +// each id, refuse an id whose two occurrences have different stored +// definitions, and sort by id. A branch's stored definition is its fact and its +// child ids, never its view, expansion state, or `fresh` flag. +fn normalized(c: Created) -> Created fails ConflictingContent, ClosureTooSmall { return { leaves: expect dedupeById(c.leaves, _.id, _.fact), // PROPOSED generic list helper - branches: expect dedupeById(c.branches, _.id, _.fact), + branches: expect dedupeById(c.branches, _.id, branchDefinition(_)), }; } +type BranchDefinition = { fact: v2.BranchFact, left: NodeId, right: NodeId }; + +fn branchDefinition(b: BranchView) -> BranchDefinition fails ClosureTooSmall { + return { fact: b.fact, left: expect idOf(b.left), right: expect idOf(b.right) }; +} + // The bytes in [start, end), for the no-op check. Leaves in the range must be // expanded; the closure read expands them only when the range length equals // the replacement length, because otherwise the edit cannot be a no-op. diff --git a/edict/replace-range/draft/Text.edict b/edict/replace-range/draft/Text.edict index 7ac6921a..9752ed7b 100644 --- a/edict/replace-range/draft/Text.edict +++ b/edict/replace-range/draft/Text.edict @@ -62,7 +62,11 @@ type ExportFact = { // ---- Edge types (no payload; one edge per source node and type) ---- -type BufferSlot = Unit; // worldline root -> Buffer, one per buffer (echo#927) +// Conceptual relation only. One fixed slot type from the mutable worldline root +// admits one edge under ContentAddressV1, so this declaration cannot attach two +// buffers. The concrete layout (a root-owned index, investigated first, or a +// per-key slot type) is pending echo#927 (DL-0159, Reachability). +type BufferSlot = Unit; // worldline root -> Buffer: layout pending echo#927 type CanonicalHead = Unit; // Buffer -> Head type AcceptedHostBasis = Unit; // Buffer -> HostBasis, retargeted by basis transitions type Root = Unit; // Head -> Branch | Leaf