docs(design): revise DL-0159 after review

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.
+
 - `scripts/deps/echo-edict-relock.mjs` moves Jedit to new Echo and Edict commits in
   one command: Echo pins, regenerated host bindings, the ReplaceRange oracle, the
   republished `jedit.text` lawpack and import digest, and every proof lock,

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
@@ -41,23 +48,23 @@ 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`) |
+| 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`) |
+| 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 |
-| `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 |
+| 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; [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
 
@@ -66,41 +73,49 @@ 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.
+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)
 
-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) |
-| 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) |
-| `for` with effects lowered to Target IR | target 2 | Target refuses `For` (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); [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); [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
-  `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).
+- 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).
+- 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 +124,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.

edict/replace-range/draft/Reference.edict

@@ -47,12 +47,15 @@ intent replaceRange(input: Input) returns Result
 
   let headRef = echo.ref<v2.HeadFact>(input.basisHeadId);
   let head = headRef.read() else text.FactMissing;
-  let textId = echo.edge<v2.HeadFact, TextFact, v2.Root>(headRef)
-    .target() else text.FactMissing;
   let importId = echo.edge<v2.HeadFact, v2.ImportFact, v2.Anchor>(headRef)
     .target() else text.FactMissing;
-  let old = echo.ref<TextFact>(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<TextFact>(
+      echo.edge<v2.HeadFact, TextFact, v2.Root>(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,27 +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.nodeId("text", core.cbor.encode(fact), []);   // PROPOSED encode
-  echo.ref<TextFact>(newTextId).ensure(fact) else text.ContentIdentityMismatch;
+  let newTextId = v2.contentId(fact, []);
 
   let newHead = {
     byteLength: len(bytes),
     lineCount: fact.lineBreaks + 1u64,                       // needs checked +
     sequence: head.sequence + 1u64,
   };
-  let newHeadId = v2.nodeId("head", core.cbor.encode(newHead), [newTextId, importId]);
+  let anchorEdge = { edgeType: typeId<v2.Anchor>(), to: importId };
+  let headEdges = if len(bytes) == 0u64
+    then [anchorEdge]
+    else [{ edgeType: typeId<v2.Root>(), to: newTextId }, anchorEdge];
+  let newHeadId = v2.contentId(newHead, headEdges);
   let newHeadRef = echo.ref<v2.HeadFact>(newHeadId);
   newHeadRef.ensure(newHead) else text.ContentIdentityMismatch;
-  echo.edge<v2.HeadFact, TextFact, v2.Root>(newHeadRef)
-    .ensure(newTextId) else text.ContentIdentityMismatch;   // PROPOSED: edge ensure
+  if len(bytes) != 0u64 {
+    echo.ref<TextFact>(newTextId).ensure(fact) else text.ContentIdentityMismatch;
+    echo.edge<v2.HeadFact, TextFact, v2.Root>(newHeadRef)
+      .ensure(newTextId) else text.ContentIdentityMismatch;   // PROPOSED: edge ensure
+  }
   echo.edge<v2.HeadFact, v2.ImportFact, v2.Anchor>(newHeadRef)
     .ensure(importId) else text.ContentIdentityMismatch;
 
   echo.edge<v2.BufferFact, v2.HeadFact, v2.CanonicalHead>(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,