From 5327ab020e6d864df955387685f129f0d2fb569b Mon Sep 17 00:00:00 2001 From: James Ross Date: Sat, 18 Jul 2026 21:54:56 -0700 Subject: [PATCH 1/7] docs(architecture): define executable operation packages --- .../0015-registry-provider-host-boundary.md | 15 +- ...-admitted-executable-operation-packages.md | 347 ++++++++++++++++++ docs/adr/README.md | 3 +- .../application-contract-hosting.md | 9 + 4 files changed, 372 insertions(+), 2 deletions(-) create mode 100644 docs/adr/0023-admitted-executable-operation-packages.md diff --git a/docs/adr/0015-registry-provider-host-boundary.md b/docs/adr/0015-registry-provider-host-boundary.md index b4869136..db52dc0a 100644 --- a/docs/adr/0015-registry-provider-host-boundary.md +++ b/docs/adr/0015-registry-provider-host-boundary.md @@ -3,7 +3,8 @@ # ADR 0015: Registry, Provider, and Host Boundary -- **Status:** Accepted +- **Status:** Partially superseded +- **Superseded in part by:** ADR 0023 - **Date:** 2026-07-13 ## Context @@ -31,6 +32,18 @@ query, and compatibility mappings before mutating engine state. coordinates to the application. - Application nouns remain in contracts and adapters outside Echo core. +## Partial Supersession + +ADR 0023 governs newly authored executable operation packages. Their semantic +execution must come from an admitted program interpreted by Echo rather than a +host-supplied application matcher, executor, or footprint callback. + +This record remains authoritative for provider-v1 callback-shaped +compatibility infrastructure and for the separation between application, +runtime-owner, registry, and installation authority while that corridor is +retained. Provider v1 is not silently reinterpreted as the new executable +operation category. + ## Evidence Anchors - `docs/architecture/application-contract-hosting.md` diff --git a/docs/adr/0023-admitted-executable-operation-packages.md b/docs/adr/0023-admitted-executable-operation-packages.md new file mode 100644 index 00000000..360e8485 --- /dev/null +++ b/docs/adr/0023-admitted-executable-operation-packages.md @@ -0,0 +1,347 @@ + + + +# ADR 0023: Admitted Executable Operation Packages + +- **Status:** Accepted +- **Date:** 2026-07-18 +- **Partially supersedes:** ADR 0015 for newly authored executable operations + +## Context + +Echo's provider-v1 corridor witnesses an exact package, operation, Target IR, +and scheduler-rule identity, but it obtains application execution semantics +from host-supplied matcher, executor, and footprint function pointers. The +source explicitly says that matching callback claims do not prove callback +semantics. + +Edict's current Echo Target IR is a target review artifact. It names effects, +target intrinsics, requirements, budgets, obstruction mappings, and a result, +but it is not an executable graph-transformation program. Echo's current rule +type likewise stores native callbacks; its pattern metadata is not an +interpreted DPO rule. + +The first real convergence witness is Jedit's `ReplaceRange`. Its current +handwritten planner contains substantial application meaning: exact-basis +validation, fixed-width byte coordinates, range and UTF-8 checks, no-op +refusal, persistent-rope splitting and balancing, content-addressed fact +construction, version advancement, footprint derivation, and result facts. +Moving that planner into Echo or hiding it behind a native target intrinsic +would preserve the callback defect under another name. + +The new corridor is therefore not provider v2. Provider v1 remains stable +callback-shaped compatibility infrastructure while consumers migrate. The new +semantic category is an executable operation package whose admitted program is +interpreted by Echo without an application matcher, executor, footprint +callback, prebuilt mutation plan, or native operation implementation. + +## Decision + +### Executable operation category + +Echo will add an operation-oriented corridor with these provisional first- +version nouns: + +- `ExecutableOperationPackageV1`: exact publication material and provenance; +- `EchoOperationProgramV1`: the target-relative executable program artifact; +- `AdmittedExecutableOperationPackageV1`: package-admission evidence; +- `InstalledEchoOperationV1`: Echo-owned installed executable meaning; +- `PreparedEchoOperationV1`: one basis-bound private evaluation result; +- `EchoOperationExecutionEvidenceV1`: receipt and recovery evidence. + +These are new types and propositions. They are not aliases for provider-v1 +hooks or records. Lawful package-byte corroboration, registry conflict checks, +canonical codecs, scheduler integration, WAL framing, and recovery machinery +may be reused when their propositions remain exact. + +`EchoOperationProgramV1` is deliberately target-relative. It does not claim to +be the universal WARP wire noun or a runtime-neutral graph-program standard. +The name may be superseded after more than one real operation and runtime can +demonstrate a common portable boundary. + +The alternatives considered for the executable artifact name were: + +- `ContainedWarpOperationV1`: rejected for the first version because it implies + stronger recursive-WARP realization than the implementation demonstrates. + Version 1 has no durable child lane, child-local tick history, wormhole, or + recursively schedulable child runtime. +- `BoundedGraphOperationV1`: rejected for the first version because it reads as + a runtime-neutral or universal graph-operation contract before that claim has + cross-runtime evidence. +- `EchoOperationProgramV1`: selected because it states the current truth: this + is a bounded program for Echo's target profile. + +### First-version execution obligations + +Every `EchoOperationProgramV1` must declare and canonically bind: + +- one operation coordinate and exact input, output, and obstruction schemas; +- one invocation-to-graph binding; +- an explicit parent causal basis; +- a typed graph and attachment schema; +- a closed declarative rewrite/evaluation program; +- deterministic rule and match selection; +- only versioned, digest-locked, deterministic low-level intrinsics; +- a delegated step, allocation, and output budget; +- a declared footprint law or ceiling; +- a result projection and typed obstruction projection; +- one evaluator ABI and intrinsic-profile identity; +- atomic visibility as one parent patch or one obstruction. + +The evaluator may use private deterministic working state and several bounded +internal steps. That state is not parent history. A successful evaluation +exposes one normal Echo patch; an obstructed evaluation exposes no parent +mutation. Version 1 retains an execution or trace identity sufficient to bind +later evidence without claiming that a durable child worldline already exists. + +The program may use generic primitives for typed graph access, canonical scalar +operations, checked `u64` arithmetic, bounded byte manipulation, UTF-8 +validation, canonical hashing, content-address derivation, and graph-delta +construction. Echo must not provide an intrinsic whose native implementation +is Jedit `ReplaceRange`, persistent-rope replacement, or another application +semantic operation. + +### Prepared Operation Basis Law + +A prepared operation may commit only against the exact parent basis on which +it was evaluated. + +`PreparedEchoOperationV1` and its eventual receipt evidence must bind: + +- the exact Echo parent worldline, writer head, frontier/tick, commit or root, + and application basis named by the invocation; +- the program and package identities; +- the canonical input digest; +- the delegated budget and consumed budget; +- the declared footprint identity; +- the actual read/write footprint derived during evaluation; +- the resulting patch digest; +- the typed output or obstruction identity; +- the private execution or trace identity. + +Before commit, Echo must establish all of the following: + +```text +current parent basis == evaluated parent basis +installed program identity == evaluated program identity +canonical input identity == evaluated input identity +actual footprint is permitted by the declared footprint contract +committed patch identity == evaluated patch identity +``` + +If the parent basis changed, the prepared operation is ineligible to commit and +must yield a typed basis-changed posture without applying any patch. Echo must +not silently rebase, retarget, revalidate, or transport the preparation to the +new basis. A new evaluation is a new witnessed attempt unless an existing, +separately admitted Echo composition rule explicitly proves otherwise. + +An existing scheduler composition rule may combine independent preparations +evaluated from the same parent snapshot. That is not revalidation across a +changed basis; the composed tick remains bound to the common evaluation basis. + +### Jedit rope-law closure + +For the first `ReplaceRange` vertical, Jedit will use a digest-locked canonical +declarative executable semantic resource imported through a Jedit-owned Edict +lawpack. Campaign 1 will not expand Edict source until it can directly express +the complete recursive persistent-rope algorithm. + +The authoritative semantic closure consists of: + +```text +Jedit-owned ReplaceRange.edict ++ exact Jedit lawpack coordinate and digest ++ canonical declarative EchoOperationProgramV1 bytes ++ exact fact schemas, codec profile, identity domains, and obstruction map +``` + +The Edict intent remains the application-owned operation surface. Its canonical +meaning binds the lawpack resource and program digest. Changing the executable +resource changes the admitted semantic closure and package identity. + +The resource is acceptable only when it contains the executable meaning. It +must contain the declarative rewrite/control law needed to derive the rope +consequence from the invocation and parent graph. It may not contain or resolve +to: + +- a Rust function pointer; +- a callback coordinate; +- a host trait implementation; +- a generated `MutationPlan` supplied by Jedit; +- a native `replace-range` intrinsic; +- an assertion that ambient code implements the named operation. + +Jedit owns the resource and its exact fact/codec law. Edict binds it into +canonical source and Core meaning and routes it through the selected target. +The Echo target lowerer emits the target artifact and package bindings. Echo +validates, admits, installs, evaluates, schedules, commits, receipts, retains, +and recovers the exact program without learning Jedit semantics from ambient +host code. + +The current handwritten Jedit planner may remain temporarily as test-only +differential evidence. It must be unreachable from production execution after +cutover. + +## Alternatives for Expressing the Rope Law + +### Expand Edict source to express the full operation directly + +This route would add enough source and Core language to author persistent-rope +replacement directly: fixed-width values, bytes, variants, optionals, +conditionals, checked arithmetic, recursion or bounded iteration, typed graph +access, content-addressed construction, private work state, result projection, +and complete obstruction control. + +This is the preferable long-term authoring experience if repeated operations +demonstrate that those constructs belong in Edict. It is rejected for the first +vertical because the current compiler's initial lowerable subset is much +smaller. Implementing the entire language surface before any hook-free +operation runs would turn Campaign 1 into a broad language and runtime design +effort and would make `ReplaceRange` define unproven universal syntax. + +### Bind a canonical declarative executable resource from a Jedit lawpack + +This route adds only the Edict prerequisites needed to type the real operation, +name an explicit basis, import and bind the lawpack resource, preserve its +identity through Core and target lowering, and generate canonical client and +package artifacts. The persistent-rope execution law lives in declarative +program bytes rather than native code. + +This route is selected. It is the smallest route that closes the execution +proof chain without broad Edict expansion. It does not establish a permanent +rule that complex Edict operations must be authored as external resources. +Later Edict syntax may compile to the same target program boundary. + +## Verification Evidence Grades + +The word "independent" is reserved for an implementation that does not merely +enter the same logic through another crate or call path. The first vertical +will label evidence as follows. + +| Check | Evidence grade | First-version claim | +| ------------------------------------------------------------------------------------------------------------- | --------------------------------------------------------------------------------------------------------------------- | ------------------------------------------------------------------------------------------------------------------------------------ | +| Canonical decoding, schema closure, digest recomputation, supported instruction set, and static budget bounds | Deterministic self-validation | The exact bytes are internally well-formed under the installed ABI. | +| Installed package/program/input identity and exact-basis equality before commit | Deterministic self-validation | Echo committed only the admitted preparation against its evaluated basis. | +| Actual footprint against declared footprint law or ceiling | Deterministic self-validation | The evaluated support stayed within the admitted footprint contract. | +| Core to Target IR relation | Structurally separate verifier path | A separately invoked verifier path recomputed or checked the declared relation; separation alone is not implementation independence. | +| Target IR plus lawpack resource to `EchoOperationProgramV1` binding | Structurally separate verifier path | A separately invoked target verifier checked exact program/resource/schema/profile correspondence. | +| Generated codec and package golden bytes | Independently implemented conformance evidence only when the comparison implementation shares no encoder/lowerer path | The checked finite vectors agree; this is not a proof over all values. | +| Program result and patch versus the existing handwritten Jedit planner over a frozen differential corpus | Independently implemented conformance evidence for that finite corpus | Two separately implemented evaluators agree on the named cases; this is not complete semantic equivalence. | +| Repeated evaluation by the same Echo evaluator | Deterministic self-validation | The implementation is repeatable for the tested basis and inputs; it is not an independent implementation. | +| Receipt/WAL round-trip and fresh-host reconstruction | Deterministic self-validation | Retained bytes reconstruct the same installed and execution identities without callbacks. | + +A separate verifier crate is not, by itself, independently implemented +conformance evidence. The first vertical will not claim formal refinement, +complete semantic equivalence, a clean-room Echo interpreter, or a proof that +all possible `ReplaceRange` inputs agree with the legacy planner. + +The differential corpus counts as independently implemented evidence only +when its oracle path does not invoke the new program evaluator or generated +program implementation. Shared fact schemas and comparison codecs must be +named; agreement is asserted at the canonical output and patch boundary, not +by comparing two wrappers around the same algorithm. + +## Jurisdiction + +- **Jedit** owns `ReplaceRange.edict`, the rope-law resource, fact schemas, + codec/identity law, operation semantics, and the differential oracle corpus. +- **Edict** owns source parsing, typing, canonical meaning, Core, generic + resource binding, target invocation, package generation, clients, and + provenance orchestration. +- **Echo's target implementation** owns the target profile, target lowering, + structurally separate target verification, program ABI, and deterministic + low-level intrinsic profile. +- **Echo's runtime** owns package and invocation admission, byte corroboration, + installation, private evaluation, footprint enforcement, scheduling, + exact-basis commitment, receipts, WAL, retention, and recovery. +- **Current Jedit/Jim integration** may provide canonical events, known basis, + typed input, and external capabilities. It may not provide semantic execution + or Echo authority. + +## Sequencing Consequence + +Implementation proceeds in dependency order: + +1. minimal Edict operation prerequisites; +2. hook-free Echo bounded-operation evaluation with a tiny generic program; +3. the real Jedit `ReplaceRange` semantic artifact and differential oracle + corpus; +4. current Jim invocation and legacy `ReplaceRange` cutover. + +Each stage remains a separately reviewed and merged campaign. The first real +vertical is complete only when this chain is executable: + +```text +real Jim command +→ explicit basis-bearing generated invocation +→ admitted Edict-authored operation +→ Echo-owned deterministic evaluation +→ one committed buffer consequence or typed obstruction +→ receipt binding the executable semantics +``` + +Campaign 1 is bounded to the Edict capabilities required to type the real +operation surface, preserve exact fixed-width values and explicit basis, +canonically bind the lawpack program resource through Core and artifact +identity, and generate the operation-facing package/client inputs. It does not +add the Echo evaluator, author the Jedit rope program, or introduce general +recursion, iteration, graph-pattern syntax, observer syntax, or process +semantics. + +## Rejected Alternatives + +- Mutate provider v1 and describe it as provider v2. +- Treat matching callback claims as executable semantic evidence. +- Generate an application matcher, executor, or footprint callback. +- Install a host-supplied `MutationPlan` or parent patch. +- Implement Jedit rope replacement as an Echo native intrinsic. +- Call Target IR executable merely because it names a target intrinsic. +- Commit a preparation after its exact evaluation basis changed. +- Describe a separate verifier crate as independently implemented without + examining shared algorithms and dependencies. +- Build the general Cyber Kitten runtime before the operation seam works. + +## Consequences + +- Provider v1 remains byte- and API-stable compatibility infrastructure while + migrations proceed; it is not the authority model for new executable + operations. +- Echo gains one new program interpreter and installed-operation evidence + category rather than a callback-bearing provider revision. +- Campaign 1 stays bounded: it adds fixed-width and explicit-basis operation + prerequisites plus exact executable-resource binding, not a general recursive + Edict language. +- The first program format preserves contained-execution obligations without + claiming durable child lanes, child ticks, wormholes, or universal WARP wire + status. +- Receipts must distinguish package, program, input, basis, declared and actual + footprints, patch, output or obstruction, budget, and execution-trace + identities. +- A changed parent basis invalidates a preparation; automatic rebasing and + cross-basis transport remain separately witnessed future operations. +- The existing Jedit planner becomes migration evidence rather than production + execution authority. + +## Non-Goals + +- Cyber Kitten syntax or runtime; +- `TextWindow` or other optic migration; +- observer routing or event delivery; +- durable child worldlines or child-local ticks; +- wormholes, holograms, or Continuum transport; +- external effect execution; +- arbitrary native plugins, WASM, or a general-purpose VM; +- broad application authorization; +- create, checkpoint, inverse, save, or causal-topology migration. + +## Evidence Anchors + +- [Edict Target IR is a non-executing target review surface](https://github.com/flyingrobots/edict/blob/da5da887c1fa089a3f82f4d29d0799eb6e155f31/crates/edict-syntax/src/target_ir.rs#L1-L5) +- [Edict Core carries lawpack imports and bounded intent structure](https://github.com/flyingrobots/edict/blob/da5da887c1fa089a3f82f4d29d0799eb6e155f31/crates/edict-syntax/src/core_ir.rs#L14-L39) +- [Edict's initial compiler supports only one parameter and `basis none`](https://github.com/flyingrobots/edict/blob/da5da887c1fa089a3f82f4d29d0799eb6e155f31/crates/edict-syntax/src/compiler.rs#L608-L644) +- [Echo provider v1 stores host executor and footprint hooks](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/warp-core/src/provider_contract.rs#L35-L126) +- [Echo rewrite rules execute native matcher, executor, and footprint functions](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/warp-core/src/rule.rs#L11-L103) +- [Current provider evidence binds package, Target IR, and scheduler rule](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/warp-core/src/provider_contract.rs#L1181-L1263) +- [Jedit's current `ReplaceRange` semantic planner](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/rope.rs#L385-L475) +- [Jedit persistent-rope split and balance law](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/rope/tree.rs#L69-L193) +- [Jedit currently binds replacement to handwritten callbacks](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/contract.rs#L111-L142) diff --git a/docs/adr/README.md b/docs/adr/README.md index 441dfa4e..97504cb1 100644 --- a/docs/adr/README.md +++ b/docs/adr/README.md @@ -36,7 +36,7 @@ track work, progress, priority, or release readiness. | [0012](0012-repository-knowledge-model.md) | Accepted | Repository knowledge model after Method | | [0013](0013-echo-continuum-authority-boundary.md) | Accepted | Echo and Continuum authority boundary | | [0014](0014-generated-rule-authorship-and-footprints.md) | Accepted | Generated rule authorship and footprint honesty | -| [0015](0015-registry-provider-host-boundary.md) | Accepted | Compiler, registry, provider, and host responsibilities | +| [0015](0015-registry-provider-host-boundary.md) | Partially superseded | Compiler, registry, provider, and host responsibilities | | [0016](0016-continuum-transport-identity.md) | Accepted | Causal transport identity and idempotence | | [0017](0017-universal-little-endian-codec.md) | Accepted | Canonical little-endian binary boundary | | [0018](0018-sessions-causal-posture-and-authority.md) | Accepted | Sessions as causal contexts | @@ -44,6 +44,7 @@ track work, progress, priority, or release readiness. | [0020](0020-retained-reading-storage-and-proof-boundary.md) | Accepted | Retained reading storage and proof boundary | | [0021](0021-public-optic-observation-boundary.md) | Accepted | Public WARP optic over internal observation | | [0022](0022-application-requested-causal-anchor-admission.md) | Accepted | Application-requested, Echo-owned anchor admission | +| [0023](0023-admitted-executable-operation-packages.md) | Accepted | Admitted executable operation packages | ADR 0006 predates this index contract and did not declare a status. Its superseded tombstone preserves that fact without silently ratifying the old diff --git a/docs/architecture/application-contract-hosting.md b/docs/architecture/application-contract-hosting.md index 2aa1abd2..d32e01d3 100644 --- a/docs/architecture/application-contract-hosting.md +++ b/docs/architecture/application-contract-hosting.md @@ -66,6 +66,7 @@ Current authority for this boundary lives in: - [Runtime authority](../topics/RuntimeAuthority.md) - [Registry, provider, and host boundary](../adr/0015-registry-provider-host-boundary.md) - [Generated rule authorship and footprints](../adr/0014-generated-rule-authorship-and-footprints.md) +- [Admitted executable operation packages](../adr/0023-admitted-executable-operation-packages.md) - [Declarative rule authorship](../invariants/DECLARATIVE-RULE-AUTHORSHIP.md) ## Ownership Split @@ -144,6 +145,14 @@ mutation-specific; generated reads remain a separate bounded observer/optic crossing. Neither compiler path may claim that generated authority facts are Echo runtime authority. +The preceding paragraph describes the implemented provider-v1 compatibility +corridor. [ADR 0023](../adr/0023-admitted-executable-operation-packages.md) +accepts a distinct, not-yet-implemented executable-operation category for new +application mutations. That category installs a digest-bound declarative +program interpreted by Echo and exposes no application matcher, executor, or +footprint callback. Provider v1 remains stable while consumers migrate; it is +not renamed or silently reinterpreted as the executable-operation corridor. + ## External Edict Provider Artifacts Echo also owns the runtime-specific semantics supplied to Edict's generic From 1740d499b4ae9673939d4390829aaed466bed872 Mon Sep 17 00:00:00 2001 From: James Ross Date: Sat, 18 Jul 2026 21:55:29 -0700 Subject: [PATCH 2/7] docs(architecture): clarify operation program naming --- docs/adr/0023-admitted-executable-operation-packages.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/adr/0023-admitted-executable-operation-packages.md b/docs/adr/0023-admitted-executable-operation-packages.md index 360e8485..33389031 100644 --- a/docs/adr/0023-admitted-executable-operation-packages.md +++ b/docs/adr/0023-admitted-executable-operation-packages.md @@ -39,8 +39,8 @@ callback, prebuilt mutation plan, or native operation implementation. ### Executable operation category -Echo will add an operation-oriented corridor with these provisional first- -version nouns: +Echo will add an operation-oriented corridor with these provisional names for +the first version: - `ExecutableOperationPackageV1`: exact publication material and provenance; - `EchoOperationProgramV1`: the target-relative executable program artifact; From 96004787324dce85d7dc67ab032f56e0279012f0 Mon Sep 17 00:00:00 2001 From: James Ross Date: Sat, 18 Jul 2026 22:39:09 -0700 Subject: [PATCH 3/7] docs(architecture): enforce program substitution boundary --- ...-admitted-executable-operation-packages.md | 108 ++++++++++++++---- .../application-contract-hosting.md | 5 + 2 files changed, 91 insertions(+), 22 deletions(-) diff --git a/docs/adr/0023-admitted-executable-operation-packages.md b/docs/adr/0023-admitted-executable-operation-packages.md index 33389031..1d351dfa 100644 --- a/docs/adr/0023-admitted-executable-operation-packages.md +++ b/docs/adr/0023-admitted-executable-operation-packages.md @@ -71,20 +71,70 @@ The alternatives considered for the executable artifact name were: - `EchoOperationProgramV1`: selected because it states the current truth: this is a bounded program for Echo's target profile. +### Program Substitution Boundary Law + +An `EchoOperationProgramV1` digest is subordinate executable evidence. It is +not an operation coordinate, an installed operation, an invocation capability, +an authority token, or permission to invoke anything. Possessing, publishing, +or corroborating program bytes cannot make them independently installable or +invocable. + +The binding direction is explicit: + +```text +Edict intent / admitted executable-operation package +→ binds the canonical semantic closure +→ binds the exact Jedit lawpack coordinate and digest +→ binds the exact EchoOperationProgramV1 bytes and digest +``` + +The admitted Edict operation supplies the public operation coordinate, +invocation and result schemas, basis contract, budget and footprint contract, +authority requirements, result and obstruction interpretation, and the +runtime-recognized eligibility to invoke the operation. Echo still admits each +invocation against those requirements; package bytes do not authorize a +caller. The program supplies only the executable meaning used to evaluate an +already admitted invocation. + +Echo must therefore begin installation and invocation lookup from an admitted +operation-package identity, then follow its closed semantic bindings to the +program. It must not admit, install, or invoke a naked program digest. Any +operation or schema references carried inside program bytes are consistency +claims checked against the admitted package, not declarations that mint a +public contract. Reusing identical program bytes in another lawful package +does not merge operation identities, invocability, or authority. Substituting +different program bytes changes the semantic closure and package identity. + ### First-version execution obligations -Every `EchoOperationProgramV1` must declare and canonically bind: +Every `ExecutableOperationPackageV1` must canonically bind: + +- one public operation coordinate and exact invocation, output, and + obstruction schemas; +- the Edict source, canonical meaning, Core, and target identities that define + the admitted semantic closure; +- the exact lawpack resource coordinate and digest; +- the exact `EchoOperationProgramV1` bytes and digest; +- an explicit parent-basis contract; +- delegated budget and declared footprint contracts; +- authority requirements and invocation-admission requirements; +- result and obstruction interpretation; +- one evaluator ABI and intrinsic-profile identity. + +Every bound `EchoOperationProgramV1` must canonically bind its executable +meaning: -- one operation coordinate and exact input, output, and obstruction schemas; - one invocation-to-graph binding; -- an explicit parent causal basis; - a typed graph and attachment schema; - a closed declarative rewrite/evaluation program; - deterministic rule and match selection; - only versioned, digest-locked, deterministic low-level intrinsics; -- a delegated step, allocation, and output budget; -- a declared footprint law or ceiling; -- a result projection and typed obstruction projection; +- static resource requirements or ceilings checked against the delegated + budget; +- executable footprint derivation checked against the declared footprint + contract; +- typed result and obstruction construction checked against the public + operation schemas and interpretation; - one evaluator ABI and intrinsic-profile identity; - atomic visibility as one parent patch or one obstruction. @@ -110,7 +160,8 @@ it was evaluated. - the exact Echo parent worldline, writer head, frontier/tick, commit or root, and application basis named by the invocation; -- the program and package identities; +- the admitted operation and package identities plus the subordinate program + identity; - the canonical input digest; - the delegated budget and consumed budget; - the declared footprint identity; @@ -123,6 +174,8 @@ Before commit, Echo must establish all of the following: ```text current parent basis == evaluated parent basis +installed admitted-operation identity == evaluated admitted-operation identity +installed package identity == evaluated package identity installed program identity == evaluated program identity canonical input identity == evaluated input identity actual footprint is permitted by the declared footprint contract @@ -146,18 +199,22 @@ declarative executable semantic resource imported through a Jedit-owned Edict lawpack. Campaign 1 will not expand Edict source until it can directly express the complete recursive persistent-rope algorithm. -The authoritative semantic closure consists of: +The authoritative binding chain is: ```text Jedit-owned ReplaceRange.edict -+ exact Jedit lawpack coordinate and digest -+ canonical declarative EchoOperationProgramV1 bytes -+ exact fact schemas, codec profile, identity domains, and obstruction map +→ admitted executable-operation package and public operation contract +→ canonical semantic closure and exact fact/codec/identity law +→ exact Jedit lawpack coordinate and digest +→ exact canonical declarative EchoOperationProgramV1 bytes and digest ``` The Edict intent remains the application-owned operation surface. Its canonical meaning binds the lawpack resource and program digest. Changing the executable resource changes the admitted semantic closure and package identity. +The program digest alone does not confer the operation coordinate, +invocability, caller authority, result interpretation, or permission to enter +Echo admission. The resource is acceptable only when it contains the executable meaning. It must contain the declarative rewrite/control law needed to derive the rope @@ -218,17 +275,17 @@ The word "independent" is reserved for an implementation that does not merely enter the same logic through another crate or call path. The first vertical will label evidence as follows. -| Check | Evidence grade | First-version claim | -| ------------------------------------------------------------------------------------------------------------- | --------------------------------------------------------------------------------------------------------------------- | ------------------------------------------------------------------------------------------------------------------------------------ | -| Canonical decoding, schema closure, digest recomputation, supported instruction set, and static budget bounds | Deterministic self-validation | The exact bytes are internally well-formed under the installed ABI. | -| Installed package/program/input identity and exact-basis equality before commit | Deterministic self-validation | Echo committed only the admitted preparation against its evaluated basis. | -| Actual footprint against declared footprint law or ceiling | Deterministic self-validation | The evaluated support stayed within the admitted footprint contract. | -| Core to Target IR relation | Structurally separate verifier path | A separately invoked verifier path recomputed or checked the declared relation; separation alone is not implementation independence. | -| Target IR plus lawpack resource to `EchoOperationProgramV1` binding | Structurally separate verifier path | A separately invoked target verifier checked exact program/resource/schema/profile correspondence. | -| Generated codec and package golden bytes | Independently implemented conformance evidence only when the comparison implementation shares no encoder/lowerer path | The checked finite vectors agree; this is not a proof over all values. | -| Program result and patch versus the existing handwritten Jedit planner over a frozen differential corpus | Independently implemented conformance evidence for that finite corpus | Two separately implemented evaluators agree on the named cases; this is not complete semantic equivalence. | -| Repeated evaluation by the same Echo evaluator | Deterministic self-validation | The implementation is repeatable for the tested basis and inputs; it is not an independent implementation. | -| Receipt/WAL round-trip and fresh-host reconstruction | Deterministic self-validation | Retained bytes reconstruct the same installed and execution identities without callbacks. | +| Check | Evidence grade | First-version claim | +| ------------------------------------------------------------------------------------------------------------- | --------------------------------------------------------------------------------------------------------------------- | -------------------------------------------------------------------------------------------------------------------------------------------------------- | +| Canonical decoding, schema closure, digest recomputation, supported instruction set, and static budget bounds | Deterministic self-validation | The exact bytes are internally well-formed under the installed ABI. | +| Installed package/program/input identity and exact-basis equality before commit | Deterministic self-validation | Echo committed only the admitted preparation against its evaluated basis. | +| Actual footprint against declared footprint law or ceiling | Deterministic self-validation | The evaluated support stayed within the admitted footprint contract. | +| Core to Target IR relation | Structurally separate verifier path | A separately invoked verifier path recomputed or checked the declared relation; separation alone is not implementation independence. | +| Admitted operation package plus Target IR and lawpack resource to `EchoOperationProgramV1` binding | Structurally separate verifier path | A separately invoked target verifier checked exact package/program/resource/schema/profile correspondence without making the program an authority token. | +| Generated codec and package golden bytes | Independently implemented conformance evidence only when the comparison implementation shares no encoder/lowerer path | The checked finite vectors agree; this is not a proof over all values. | +| Program result and patch versus the existing handwritten Jedit planner over a frozen differential corpus | Independently implemented conformance evidence for that finite corpus | Two separately implemented evaluators agree on the named cases; this is not complete semantic equivalence. | +| Repeated evaluation by the same Echo evaluator | Deterministic self-validation | The implementation is repeatable for the tested basis and inputs; it is not an independent implementation. | +| Receipt/WAL round-trip and fresh-host reconstruction | Deterministic self-validation | Retained bytes reconstruct the same installed and execution identities without callbacks. | A separate verifier crate is not, by itself, independently implemented conformance evidence. The first vertical will not claim formal refinement, @@ -292,6 +349,10 @@ semantics. - Mutate provider v1 and describe it as provider v2. - Treat matching callback claims as executable semantic evidence. +- Treat a program digest as an operation coordinate, invocation capability, or + authority token. +- Install or invoke `EchoOperationProgramV1` without resolving it through an + admitted executable-operation package. - Generate an application matcher, executor, or footprint callback. - Install a host-supplied `MutationPlan` or parent patch. - Implement Jedit rope replacement as an Echo native intrinsic. @@ -317,6 +378,9 @@ semantics. - Receipts must distinguish package, program, input, basis, declared and actual footprints, patch, output or obstruction, budget, and execution-trace identities. +- A receipt's program digest identifies the executable meaning used only in + the context of the admitted operation and package that bind it; it does not + retroactively make the program independently invocable or authoritative. - A changed parent basis invalidates a preparation; automatic rebasing and cross-basis transport remain separately witnessed future operations. - The existing Jedit planner becomes migration evidence rather than production diff --git a/docs/architecture/application-contract-hosting.md b/docs/architecture/application-contract-hosting.md index d32e01d3..e8220722 100644 --- a/docs/architecture/application-contract-hosting.md +++ b/docs/architecture/application-contract-hosting.md @@ -152,6 +152,11 @@ application mutations. That category installs a digest-bound declarative program interpreted by Echo and exposes no application matcher, executor, or footprint callback. Provider v1 remains stable while consumers migrate; it is not renamed or silently reinterpreted as the executable-operation corridor. +The program digest supplies executable meaning only: it cannot independently +confer an operation coordinate, invocability, or authority, and Echo cannot +install or invoke it naked. The admitted Edict operation package binds the +public contract and semantic closure to the exact program, after which Echo +independently admits each invocation. ## External Edict Provider Artifacts From a4c8726965171ab4feda0c5564100af7f1dc1066 Mon Sep 17 00:00:00 2001 From: James Ross Date: Sat, 18 Jul 2026 23:49:08 -0700 Subject: [PATCH 4/7] docs(plans): preserve executable WARP campaign ledger --- ...im-edict-echo-executable-warp-semantics.md | 1281 +++++++++++++++++ 1 file changed, 1281 insertions(+) create mode 100644 docs/plans/2026-07-18-jim-edict-echo-executable-warp-semantics.md diff --git a/docs/plans/2026-07-18-jim-edict-echo-executable-warp-semantics.md b/docs/plans/2026-07-18-jim-edict-echo-executable-warp-semantics.md new file mode 100644 index 00000000..4515eb2d --- /dev/null +++ b/docs/plans/2026-07-18-jim-edict-echo-executable-warp-semantics.md @@ -0,0 +1,1281 @@ + + + +# Jim × Edict × Echo: Executable WARP Semantics Inventory + +Status: architectural discovery and source-grounded plan +Date: 2026-07-18 +Implementation status: halted pending architectural agreement + +## Source basis + +This report is based on source code, not repository documentation, at these +authoritative repository heads: + +- Jedit: c70e12d73b4b00bc92412bab67e1761f7dd22f82 +- Echo: 6615d3a97731a076fb4945bb6da083e82f55710d +- Edict: da5da887c1fa089a3f82f4d29d0799eb6e155f31 + +Historical commits in this report are immutable evidence coordinates. They are +not permission to assume that current repository heads remain unchanged. + +## Executive finding + +WARP is the right candidate for Echo's executable machine, but it is not yet +the executable machine implemented in the repositories. + +The source currently contains: + +```text +Edict meaning +→ Target IR naming a target intrinsic +→ generated registration/helper metadata +→ host-supplied Rust executor + footprint callbacks +→ TickDelta +→ Echo receipt +``` + +It does not yet contain: + +```text +Edict meaning +→ canonical executable WARP program +→ Echo-owned WARP interpreter +→ TickDelta +→ Echo receipt +``` + +This is not a documentation discrepancy. It identifies the missing +architectural center. + +Jim's Echo-facing needs fall into five jurisdictions: + +```text +Application mutations, authored by Jedit in Edict +├── CreateBufferWorldline +├── ReplaceRange +│ ├── Insert +│ └── Delete +└── DeclareCheckpoint + +Bounded observations, authored as optics +├── TextWindow +├── CausalLineDiff +├── WhyRange +└── FullTextSnapshot / export materialization + +Capability crossings +├── Read file / import bytes +└── Write file / export bytes + +Causal-topology operations, owned by Echo kernel law +├── Observe historical coordinate +├── Fork strand +├── Braid membership/lifecycle +├── Compare or plan settlement +└── Settle suffix as import, conflict, or lawful plurality + +Runtime judgments, exclusively Echo-owned +├── submit +├── admit +├── schedule +├── evaluate/apply +├── commit +├── emit outcome evidence +├── persist +└── recover +``` + +This is one algebra with multiple jurisdictions. + +Two prerequisites must be resolved before ReplaceRange can honestly become +executable Edict meaning: + +1. Jim does not yet have one canonical text-graph schema. +2. Echo does not yet have a serialized, independently verifiable DPO-program + interpreter. + +## 1. What Jim executes through Echo today + +The current GraphQL/Wesley corridor defines exactly three mutations and one +query: + +- createBufferWorldline +- replaceRangeAsTick +- declareCheckpoint +- textWindow + +Source: +[jedit/contracts/jedit/echo-text.graphql#L1-L71@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/contracts/jedit/echo-text.graphql#L1-L71) + +The TypeScript host port exposes precisely the same four operations. + +Sources: +[jedit/src/ports/echo-text-contract-host.ts#L9-L21@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/ports/echo-text-contract-host.ts#L9-L21), +[jedit/src/ports/echo-text-contract-host.ts#L140-L145@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/ports/echo-text-contract-host.ts#L140-L145) + +### 1.1 Open / CreateBufferWorldline + +Open is presently a composite operation: + +1. Jedit reads the file through its local EditorFilePort. +2. The loaded text becomes initialText. +3. Jedit calls the Echo host. +4. If the buffer already exists, the native host returns its current snapshot, + without a creation receipt. +5. Otherwise, it submits CreateBufferWorldline. +6. Jedit subsequently performs a TextWindow observation. + +The pre-Echo file read occurs here: +[jedit/src/app/workspace/workspace-text-open-basis.ts#L55-L80@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/app/workspace/workspace-text-open-basis.ts#L55-L80) + +The create-then-observe composition occurs here: +[jedit/src/app/workspace/workspace-text-commands.ts#L203-L234@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/app/workspace/workspace-text-commands.ts#L203-L234) + +The native existing-or-create behavior occurs here: +[jedit/native/jedit-echo-host/src/host.rs#L101-L134@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/host.rs#L101-L134) + +The actual create planner: + +- refuses an existing buffer; +- builds a persistent rope from initial UTF-8; +- creates an initial head; +- writes the mutable buffer record pointing at that head. + +Source: +[jedit/native/jedit-echo-host/src/rope.rs#L346-L383@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/rope.rs#L346-L383) + +The correct future expression is: + +```text +file-read capability +→ witnessed bytes or missing-file result +→ CreateBufferWorldline application operation +→ TextWindow optic +``` + +The file-read capability provides bytes. It must not define buffer semantics. + +### 1.2 Insert / Replace / Delete + +These are one semantic operation, not three runtime operations: + +```text +Insert(start, text) += ReplaceRange(start, start, text) + +Delete(start, end) += ReplaceRange(start, end, "") + +Replace(start, end, text) += ReplaceRange(start, end, text) +``` + +The adapter performs exactly these reductions: +[jedit/src/adapters/workspace-production-text-session.ts#L69-L84@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/adapters/workspace-production-text-session.ts#L69-L84) + +The product command layer independently presents all three edit kinds. + +Sources: +[jedit/src/app/workspace/workspace-text-commands.ts#L46-L58@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/app/workspace/workspace-text-commands.ts#L46-L58), +[jedit/src/app/workspace/workspace-text-commands.ts#L282-L305@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/app/workspace/workspace-text-commands.ts#L282-L305) + +The current handwritten ReplaceRange law: + +1. Resolves the buffer's canonical head. +2. Refuses a stale supplied basis. +3. Refuses malformed or out-of-bounds ranges. +4. Reads the replaced bytes. +5. Refuses exact no-ops. +6. Checked-increments head sequence and buffer version. +7. Splits the persistent rope at both range boundaries. +8. Builds a rope for the replacement text. +9. Deterministically joins and balances the resulting rope. +10. Creates a new immutable head. +11. Creates rewrite and diff facts. +12. Changes the buffer's canonical head and version. +13. Returns the exact read/write footprint and consequence. + +Source: +[jedit/native/jedit-echo-host/src/rope.rs#L385-L475@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/rope.rs#L385-L475) + +#### Persistent derivation, not destructive replacement + +ReplaceRange does not delete old rope nodes. + +Jim has a persistent rope. The implementation creates new content-addressed +nodes and a new head, reuses unaffected structure, and advances the buffer's +canonical-head reference. Old heads and old rope structure remain available as +historical support. + +The emitted patch contains only node upserts and attachment writes. It contains +no node deletion: +[jedit/native/jedit-echo-host/src/rope.rs#L217-L237@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/rope.rs#L217-L237) + +The future graph rewrite should therefore look like: + +```text +preserve old head and old rope +preserve all reusable subtrees +add replacement blobs/leaves/branches +add new head +add rewrite/diff evidence +replace Buffer ─canonicalHead→ OldHead + with Buffer ─canonicalHead→ NewHead +``` + +This is naturally expressible in DPO, but it is persistent derivation rather +than destructive replacement. + +### 1.3 DeclareCheckpoint + +Checkpoint declaration: + +- resolves a requested retained head; +- verifies that the head belongs to the requested buffer; +- creates a content-addressed checkpoint proposition from worldline, head, and + reason; +- does not advance the text head. + +Source: +[jedit/native/jedit-echo-host/src/rope.rs#L309-L344@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/rope.rs#L309-L344) + +This should be a small application-semantic graph write: + +```text +Buffer ─contains→ BasisHead ++ DeclareCheckpoint invocation +→ Checkpoint ─worldline→ Buffer + └─basis→ BasisHead + + reason +``` + +It is not a text mutation. + +The current source nevertheless wraps it in a MutationPlan, which is the false +vocabulary identified by Jedit issue #287: +[jedit/native/jedit-echo-host/src/rope.rs#L240-L256@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/rope.rs#L240-L256) + +The underlying checkpoint reason domain contains: + +- manual-save +- autosave +- retention-boundary +- export +- import + +Source: +[jedit/native/jedit-echo-host/src/contract.rs#L175-L195@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/contract.rs#L175-L195) + +The current product adapter maps only manual-save and autosave: +[jedit/src/adapters/workspace-production-text-session.ts#L43-L46@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/adapters/workspace-production-text-session.ts#L43-L46) + +### 1.4 TextWindow + +TextWindow is the one currently executing bounded observation. It: + +- takes a buffer and explicit basis head; +- verifies buffer/head ownership; +- checks the byte range; +- applies maxBytes; +- traverses only relevant rope support; +- returns the largest complete UTF-8 prefix; +- reports supporting leaf/blob identities; +- computes line projections. + +Sources: +[jedit/native/jedit-echo-host/src/rope/window.rs#L43-L102@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/rope/window.rs#L43-L102), +[jedit/native/jedit-echo-host/src/rope/window.rs#L129-L217@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/rope/window.rs#L129-L217) + +This is already shaped like a bounded optic: + +```text +basis ++ byte aperture ++ byte budget +→ text projection ++ exact supporting leaves/blobs ++ completeness posture +``` + +Its implementation is still a host-supplied observer closure, not executable +admitted semantics. The generated code accepts an arbitrary observing +function: +[jedit/native/jedit-echo-host/src/generated/contract.rs#L681-L753@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/generated/contract.rs#L681-L753) + +## 2. What Jim wants but cannot currently execute + +The broader ProductionTextSession asks for ten operations: + +- open buffer +- insert +- replace +- delete +- multi-range edit +- checkpoint +- text window +- causal line diff +- export snapshot +- explain range + +Source: +[jedit/src/app/workspace/production-text-session.ts#L196-L209@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/app/workspace/production-text-session.ts#L196-L209) + +Only open, insert/replace/delete, checkpoint, and text window are connected. +Multi-range edit, causal line diff, export, and range explanation explicitly +fail closed with a message saying that the current Wesley corridor does not +implement them: +[jedit/src/adapters/workspace-production-text-session.ts#L40-L62@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/adapters/workspace-production-text-session.ts#L40-L62) + +### 2.1 MultiRangeEdit + +The input is an ordered collection of byte ranges and replacement strings: +[jedit/src/app/workspace/production-text-session.ts#L104-L114@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/app/workspace/production-text-session.ts#L104-L114) + +It is declared but unsupported by the current adapter. + +Future choices must be explicit: + +- canonicalize ranges and perform one atomic bounded operation; +- lower it into a transaction containing multiple ReplaceRange applications; +- or refuse it as unsupported. + +It must not become an accidental loop whose result depends on caller iteration +order or intermediate canonical-head movement. + +### 2.2 CausalLineDiff + +The requested optic takes: + +- buffer; +- basis head; +- next head; +- maximum byte count; +- maximum line count; +- maximum rewrite count; +- maximum marker count. + +Source: +[jedit/src/app/workspace/production-text-causal-line-diff.ts#L6-L24@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/app/workspace/production-text-causal-line-diff.ts#L6-L24) + +The intended reading cites: + +- inserted and deleted line counts; +- tick receipts; +- rewrite identities; +- diff identities; +- per-line markers and deletion markers; +- observer version. + +Source: +[jedit/src/ports/text-authority-evidence.ts#L67-L95@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/ports/text-authority-evidence.ts#L67-L95) + +This should be a bounded causal optic over retained RopeRewrite and RopeDiff +evidence. It is not a mutation and should not be recomputed from two privileged +snapshots. + +### 2.3 ExplainRange / :why + +The intended range explanation includes: + +- exact queried basis and range; +- complete or partial coverage; +- continuation; +- fragments mapped to leaf/blob support; +- imported or rewrite origins; +- rewrite, diff, and tick receipt citations; +- related checkpoints; +- checkpoint-to-causal-anchor associations. + +Source: +[jedit/src/ports/jedit-why-range.ts#L34-L128@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/ports/jedit-why-range.ts#L34-L128) + +The UI computes a byte range around the cursor and requests explainRange. The +current adapter refuses it: +[jedit/src/app/workspace/workspace-why-range.ts#L70-L109@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/app/workspace/workspace-why-range.ts#L70-L109) + +This is another bounded optic: + +```text +basis head ++ byte range ++ evidence budget +→ origin fragments ++ rewrite/checkpoint evidence ++ partial/complete posture ++ continuation +``` + +### 2.4 Save / Export + +Save is currently a three-crossing composition: + +```text +exportSnapshot from Echo +→ local filesystem write +→ declare manual-save checkpoint +``` + +The export step invokes exportSnapshot, runs a materialization preflight, and +then directly calls saveEditorFile: +[jedit/src/app/workspace/workspace-text-commands.ts#L336-L368@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/app/workspace/workspace-text-commands.ts#L336-L368) + +After successful export, the reducer schedules checkpoint declaration: +[jedit/src/app/workspace/workspace-text-runtime-state.ts#L317-L348@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/app/workspace/workspace-text-runtime-state.ts#L317-L348) + +The current exportSnapshot session operation is unsupported, so the production +save chain cannot complete through the generated corridor. + +The correct future decomposition is: + +```text +FullText optic at explicit head +→ complete retained reading +→ FileWrite capability request +→ witnessed filesystem outcome +→ DeclareCheckpoint(manual-save or export) +``` + +The write capability performs the effect. It must not decide which text is +authoritative, which head was exported, or whether a checkpoint proposition is +lawful. + +## 3. Jim's causal command vocabulary + +Jim already presents these user-level commands: + +- ttd +- strand +- braid + +All three are deliberately unavailable. + +Sources: +[jedit/src/app/workspace/workspace-command-catalog.ts#L88-L119@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/app/workspace/workspace-command-catalog.ts#L88-L119), +[jedit/src/app/workspace/command-line-dispatch.ts#L52-L100@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/app/workspace/command-line-dispatch.ts#L52-L100) + +### 3.1 ttd + +The command vocabulary supports: + +- canonical head; +- current observer basis; +- previous tick; +- arbitrary tick or relative coordinate according to its usage. + +It explicitly promises historical observation without moving canonical head. + +Sources: +[jedit/src/app/workspace/workspace-command-catalog.ts#L88-L96@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/app/workspace/workspace-command-catalog.ts#L88-L96), +[jedit/src/app/workspace/workspace-command-catalog.ts#L143-L167@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/app/workspace/workspace-command-catalog.ts#L143-L167) + +This is a kernel-resolved historical observation coordinate followed by normal +optics. It is not an application mutation. + +### 3.2 strand + +The UI vocabulary includes: + +- list; +- create from the current observer basis; +- switch to main. + +Source: +[jedit/src/app/workspace/workspace-command-catalog.ts#L169-L191@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/app/workspace/workspace-command-catalog.ts#L169-L191) + +The source-backed mapping is: + +- strand list → causal-topology optic; +- strand new from here → Echo kernel fork; +- strand switch → client/runtime routing posture, not an application graph + rewrite. + +Echo implements a strand as a speculative lane relation over a child worldline, +with an immutable exact fork basis. It explicitly says that a strand is not a +separate scheduler or substrate. + +Sources: +[echo/crates/warp-core/src/strand.rs#L1-L27@6615d3a97731](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/warp-core/src/strand.rs#L1-L27), +[echo/crates/warp-core/src/strand.rs#L75-L117@6615d3a97731](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/warp-core/src/strand.rs#L75-L117) + +Echo's fork_strand: + +- replays the source at the requested historical tick; +- forks provenance; +- materializes the child frontier; +- creates child writer heads; +- registers the strand; +- rolls runtime and provenance back if anything fails. + +Source: +[echo/crates/warp-core/src/coordinator.rs#L1751-L1848@6615d3a97731](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/warp-core/src/coordinator.rs#L1751-L1848) + +This is kernel causal law. + +### 3.3 braid + +The UI vocabulary includes: + +- view; +- preview; +- admit. + +Source: +[jedit/src/app/workspace/workspace-command-catalog.ts#L193-L215@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/app/workspace/workspace-command-catalog.ts#L193-L215) + +Echo's actual braid is not a merge algorithm. It is an append-only coordination +log with these events: + +- braid created; +- member woven; +- settlement finalized; +- plural braid collapsed. + +Source: +[echo/crates/warp-core/src/braid.rs#L99-L128@6615d3a97731](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/warp-core/src/braid.rs#L99-L128) + +Its membership projections are explicitly read models, not admission +authority: +[echo/crates/warp-core/src/braid.rs#L130-L213@6615d3a97731](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/warp-core/src/braid.rs#L130-L213) + +Its fold validates lifecycle status, sequence, duplicate membership, disclosure +posture, settlement posture, and collapse witness: +[echo/crates/warp-core/src/braid.rs#L215-L335@6615d3a97731](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/warp-core/src/braid.rs#L215-L335) + +The accurate mapping is: + +```text +braid view +→ observe braid event log and membership projection + +braid preview +→ compare strand suffix + produce deterministic settlement plan + +braid admit +→ execute a named Echo settlement policy +``` + +Echo's settlement code already separates those acts: + +- compare is explicitly read-only inspection; +- plan_with_policy produces deterministic import/conflict/plural decisions; +- settle_with_policy appends corresponding causal consequences. + +Sources: +[echo/crates/warp-core/src/settlement.rs#L700-L757@6615d3a97731](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/warp-core/src/settlement.rs#L700-L757), +[echo/crates/warp-core/src/settlement.rs#L760-L956@6615d3a97731](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/warp-core/src/settlement.rs#L760-L956), +[echo/crates/warp-core/src/settlement.rs#L958-L1057@6615d3a97731](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/warp-core/src/settlement.rs#L958-L1057) + +The settlement decisions are: + +- import candidate; +- conflict artifact; +- plural alternative. + +Source: +[echo/crates/warp-core/src/settlement.rs#L225-L293@6615d3a97731](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/warp-core/src/settlement.rs#L225-L293) + +#### Reserve settle for causal-topology settlement + +The word settle should remain reserved for causal-topology settlement. + +The source already gives it a specific meaning: settling a strand suffix into +its base worldline as imports, conflicts, or retained plurality under a named +policy. Reusing settle to mean closing the disposition of every ordinary +invocation would introduce ambiguity. + +For ordinary submitted work, use a term such as: + +- recordOutcome; +- finalizeDisposition; +- commitOutcome. + +Retain settleStrand, settleBraid, and SettlementPolicy for the causal operation +already implemented. + +## 4. Latent concepts that are not Echo operations yet + +### 4.1 Undo and redo + +Undo and redo appear only as command/durability vocabulary and help text. There +is no ProductionTextSession or Echo operation for them. + +Source: +[jedit/src/app/workspace/workspace-buffer-durability.ts#L44-L105@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/app/workspace/workspace-buffer-durability.ts#L44-L105) + +Future undo should not silently rewind or rewrite causal history. It should be +one of: + +- a new admitted forward replacement; +- an explicitly authored inverse operation; +- a compensation; +- a new strand from an earlier basis. + +The exact law remains unimplemented. + +### 4.2 Point anchors + +Jedit has a local deterministic point-anchor transformation contract with +left/right bias and replacement-delta behavior: +[jedit/src/domain/anchor-transform-contract.ts#L7-L136@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/domain/anchor-transform-contract.ts#L7-L136) + +This is currently a local pure utility, not an Echo operation. + +Jedit also models a separate RopeCheckpointAnchored association containing +checkpoint, causal-anchor fact, and receipt identities: +[jedit/src/domain/graph-rope-types.ts#L250-L258@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/domain/graph-rope-types.ts#L250-L258) + +This supports the distinction: + +```text +declare checkpoint +≠ +anchor checkpoint to a causal coordinate +``` + +They should remain different propositions and operations. + +### 4.3 Structural maintenance + +The TypeScript domain models: + +- split leaf; +- merge leaves; +- rotate left; +- rotate right; +- rebalance branch. + +Source: +[jedit/src/domain/graph-rope-types.ts#L199-L219@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/domain/graph-rope-types.ts#L199-L219) + +The native rope performs splitting and deterministic height balancing +internally, but its admitted native fact inventory does not contain +RopeStructuralMaintenance and the planner emits no such facts. + +Sources: +[jedit/native/jedit-echo-host/src/records.rs#L7-L14@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/records.rs#L7-L14), +[jedit/native/jedit-echo-host/src/rope/tree.rs#L101-L193@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/rope/tree.rs#L101-L193) + +A future design must decide whether balancing steps are: + +- internal interpreter trace; +- retained structural-maintenance facts; +- or implied by the canonical rope-construction law. + +That decision affects receipts, replay, and :why. + +## 5. Jim's graph data model + +### 5.1 There is not currently one canonical Jim text graph + +The TypeScript semantic model contains ten fact kinds: + +1. BufferWorldline +2. RopeHead +3. RopeBranch +4. RopeLeaf +5. TextBlob +6. RopeRewrite +7. RopeDiff +8. RopeStructuralMaintenance +9. RopeCheckpoint +10. RopeCheckpointAnchored + +Sources: +[jedit/src/domain/graph-rope-types.ts#L12-L21@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/domain/graph-rope-types.ts#L12-L21), +[jedit/src/domain/graph-rope-types.ts#L85-L270@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/domain/graph-rope-types.ts#L85-L270) + +The native runtime contains only eight: + +1. buffer +2. blob +3. leaf +4. branch +5. head +6. rewrite +7. diff +8. checkpoint + +Source: +[jedit/native/jedit-echo-host/src/records.rs#L7-L14@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/records.rs#L7-L14) + +These are not merely two serializations of identical propositions. + +| Concept | TypeScript semantic model | Native runtime model | +| ----------------- | ---------------------------------------------------------------- | ---------------------------------------------------------------------------- | +| Buffer | Creation receipt and initial head | Buffer key, projection path, mutable canonical head, version | +| Head | Worldline, root, basis, receipt, byte/line metrics, content hash | Buffer, optional basis/root, byte/UTF-16/line metrics, root digest, sequence | +| Rewrite | Receipt, replacement blob, diff identity, full range | Buffer, basis/next head, range, inserted length | +| Diff | Ordered equal/delete/insert spans | Aggregate range and inserted/deleted lengths | +| Maintenance | Explicit modeled facts | Absent | +| Checkpoint anchor | Explicit modeled fact | Absent | + +Sources: +[jedit/src/domain/graph-rope-types.ts#L85-L270@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/domain/graph-rope-types.ts#L85-L270), +[jedit/native/jedit-echo-host/src/records.rs#L25-L106@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/records.rs#L25-L106) + +This must be resolved before writing authoritative .edict source. Otherwise, +Edict will canonize one side of an unresolved semantic fork by accident. + +### 5.2 Current graph relationships are opaque JSON fields + +Every native fact is serialized to JSON. Content-addressed identities hash +those JSON bytes. On read, the entire node attachment is decoded into a Rust +struct: +[jedit/native/jedit-echo-host/src/records.rs#L123-L173@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/records.rs#L123-L173) + +The planner emits: + +- an Echo node with a type; +- one atom attachment containing the JSON fact. + +It emits no Echo edges for: + +- head → root; +- branch → left/right; +- leaf → blob; +- rewrite → basis/next; +- checkpoint → head. + +Source: +[jedit/native/jedit-echo-host/src/rope.rs#L217-L237@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/rope.rs#L217-L237) + +The domain is conceptually graph-shaped, but the current WARP graph sees each +Jim fact largely as an opaque attributed node. A true DPO interpreter cannot +match Jim's semantic relationships if they exist only inside host-decoded +JSON. + +### 5.3 A plausible canonical graph shape + +After freezing the authoritative propositions, relationships could be +represented structurally: + +```text +BufferWorldline +├─ canonicalHead ───────────────→ RopeHead +├─ initialHead ─────────────────→ RopeHead +└─ attributes: bufferKey, projectionPath, version + +RopeHead +├─ worldline ───────────────────→ BufferWorldline +├─ basis ───────────────────────→ RopeHead? +├─ root ────────────────────────→ RopeBranch | RopeLeaf +└─ attributes: + byteLength, utf16Length, lineCount, sequence, rootDigest + +RopeBranch +├─ left ────────────────────────→ RopeBranch | RopeLeaf +├─ right ───────────────────────→ RopeBranch | RopeLeaf +└─ attributes: + byteLength, utf16Length, lineBreaks, height + +RopeLeaf +├─ blob ────────────────────────→ TextBlob +└─ attributes: + byteStart, byteLength, utf16Length, lineBreaks + +TextBlob +└─ attributes: + digest, canonical bytes or retained-content reference + +RopeRewrite +├─ worldline ───────────────────→ BufferWorldline +├─ basis ───────────────────────→ RopeHead +├─ next ────────────────────────→ RopeHead +├─ replacement ────────────────→ TextBlob +├─ diff ────────────────────────→ RopeDiff +└─ attributes: + startByte, endByte, receipt/evidence references + +RopeCheckpoint +├─ worldline ───────────────────→ BufferWorldline +├─ basis ───────────────────────→ RopeHead +└─ attributes: reason + +RopeCheckpointAnchored +├─ checkpoint ──────────────────→ RopeCheckpoint +└─ attributes: + causalAnchorId, anchorFactId, anchorReceiptId +``` + +Scalar fields can remain in canonical typed attachment records. Semantic +relationships should be typed edges, or the future WARP pattern algebra must +provide equally canonical typed-field matching. They cannot remain dependent +on arbitrary Rust JSON decoding. + +Echo's store already has typed nodes, outbound/inbound edge indexes, and +node/edge attachment planes: +[echo/crates/warp-core/src/graph.rs#L29-L64@6615d3a97731](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/warp-core/src/graph.rs#L29-L64) + +## 6. How ReplaceRange becomes a WARP program + +A single static DPO span is not enough for arbitrary ReplaceRange. + +The current operation performs variable-depth traversal and recursive +rebuilding: + +- leaves are capped at 4,096 UTF-8 bytes; +- leaf boundaries preserve UTF-8; +- splitting descends recursively by subtree metrics; +- joining recursively rebalances by height; +- hashes and aggregate metrics are recomputed. + +Sources: +[jedit/native/jedit-echo-host/src/rope/tree.rs#L9-L44@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/rope/tree.rs#L9-L44), +[jedit/native/jedit-echo-host/src/rope/tree.rs#L69-L193@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/rope/tree.rs#L69-L193) + +The executable unit therefore needs to be a bounded transactional WARP +program, not merely one rule: + +```text +WarpProgram ReplaceRange +│ +├─ bind invocation +│ ├─ buffer +│ ├─ explicit basis +│ ├─ start: u64 +│ ├─ end: u64 +│ └─ replacement: bytes +│ +├─ validate +│ ├─ operation/schema identity +│ ├─ basis belongs to buffer +│ ├─ basis is canonical where required +│ ├─ start ≤ end ≤ byteLength +│ ├─ UTF-8 boundaries +│ ├─ no arithmetic overflow +│ └─ no-op law +│ +├─ traverse/split +│ ├─ deterministic worklist +│ ├─ bounded rope descent +│ └─ exact read support +│ +├─ construct +│ ├─ replacement blobs and leaves +│ ├─ shared persistent subtrees +│ ├─ deterministic joins/rebalancing +│ └─ aggregate metrics and hashes +│ +├─ derive consequence +│ ├─ new RopeHead +│ ├─ RopeRewrite +│ ├─ RopeDiff +│ └─ new canonical-head relation +│ +├─ derive exact footprint +│ +└─ atomically emit one TickDelta +``` + +The intermediate traversal/work graph must not leak into authoritative history +step by step. It is private evaluation state. The entire successful program +produces one atomic tick consequence. + +The current planner already has the correct high-level separation: + +```text +read-only source +→ MutationPlan with exact reads/writes +→ footprint +→ one emitted TickDelta +``` + +Sources: +[jedit/native/jedit-echo-host/src/rope.rs#L79-L180@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/rope.rs#L79-L180), +[jedit/native/jedit-echo-host/src/rope.rs#L187-L237@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/rope.rs#L187-L237) + +That separation should survive. The handwritten Rust function determining the +plan must not. + +### 6.1 Closed attachment algebra + +The WARP interpreter needs a small, versioned, deterministic intrinsic profile +containing operations such as: + +- checked u64 arithmetic and comparison; +- canonical byte length; +- bounded byte slicing; +- UTF-8 validation and boundary checking; +- UTF-16 code-unit count; +- line-break count; +- canonical digest/content identity; +- height comparison and maximum; +- canonical ordered rule/work-item selection. + +It should not contain: + +```text +jedit_replace_range(...) +``` + +That would be the callback architecture renamed intrinsic. + +Generic intrinsics must be individually specified, bounded, and Echo-owned. The +Jedit lawpack composes them into rope semantics. + +## 7. The source proves the callback gap + +Echo's current RewriteRule contains: + +- a native matcher function pointer; +- a native executor function pointer; +- a native footprint function pointer. + +Its PatternGraph is only a vector of type identifiers, and the source says that +the left pattern is currently unused. + +Sources: +[echo/crates/warp-core/src/rule.rs#L11-L50@6615d3a97731](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/warp-core/src/rule.rs#L11-L50), +[echo/crates/warp-core/src/rule.rs#L73-L103@6615d3a97731](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/warp-core/src/rule.rs#L73-L103) + +Jedit's generated mutation code constructs an empty PatternGraph and accepts +host-supplied executor and footprint functions: +[jedit/native/jedit-echo-host/src/generated/contract.rs#L990-L1033@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/generated/contract.rs#L990-L1033) + +Jedit binds those callbacks to the handwritten planner. + +Sources: +[jedit/native/jedit-echo-host/src/contract.rs#L34-L77@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/contract.rs#L34-L77), +[jedit/native/jedit-echo-host/src/contract.rs#L111-L142@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/contract.rs#L111-L142) + +The provider-native Edict helper currently does the same thing with stronger +identity evidence. Its generated API asks for ProviderMutationHooksV1 and says +it is constructing a package proposal from an explicit host +executor/footprint binding: +[echo/crates/echo-edict-provider-lowerer/src/lib.rs#L1238-L1283@6615d3a97731](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/echo-edict-provider-lowerer/src/lib.rs#L1238-L1283) + +Echo's provider type states the limitation directly: identity equality detects +accidental cross-binding but does not prove that arbitrary Rust callbacks +semantically implement the claims. The hooks contain the executor and footprint +function pointers: +[echo/crates/warp-core/src/provider_contract.rs#L76-L126@6615d3a97731](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/warp-core/src/provider_contract.rs#L76-L126) + +This is the architectural defect, stated directly in source. + +## 8. What Edict currently lowers + +Edict's generic Target IR currently contains: + +- operation profile; +- input constraints; +- evaluation budget; +- requirements; +- ordered steps; +- each step's semantic effect and target intrinsic; +- result expression. + +Source: +[edict/crates/edict-syntax/src/target_ir.rs#L175-L214@da5da887c1fa](https://github.com/flyingrobots/edict/blob/da5da887c1fa089a3f82f4d29d0799eb6e155f31/crates/edict-syntax/src/target_ir.rs#L175-L214) + +Core already has fixed-width integer values represented by width plus canonical +textual value, record/field/call expressions, predicates, requirements, +effects, obstruction maps, and budgets: +[edict/crates/edict-syntax/src/core_ir.rs#L118-L234@da5da887c1fa](https://github.com/flyingrobots/edict/blob/da5da887c1fa089a3f82f4d29d0799eb6e155f31/crates/edict-syntax/src/core_ir.rs#L118-L234) + +This is a useful semantic foundation, but the current Echo-specific lowerer is +deliberately fixture-specific: + +- one Core coordinate, `a.b@1`; +- one operation, `a.b@1.t`; +- one effect, `target.replace`; +- one target intrinsic, `echo.dpo@1.replace`; +- one obstruction. + +Source: +[echo/crates/echo-edict-provider-lowerer/src/lib.rs#L23-L60@6615d3a97731](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/echo-edict-provider-lowerer/src/lib.rs#L23-L60) + +It accepts exactly one intent and one effect step. It refuses authored optics. + +Sources: +[echo/crates/echo-edict-provider-lowerer/src/lib.rs#L1580-L1690@6615d3a97731](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/echo-edict-provider-lowerer/src/lib.rs#L1580-L1690), +[echo/crates/echo-edict-provider-lowerer/tests/lowerer_contract.rs#L1263-L1293@6615d3a97731](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/echo-edict-provider-lowerer/tests/lowerer_contract.rs#L1263-L1293) + +The existing echo.span-ir/v1 must not yet be described as a complete executable +DPO program. Today it is a bounded effect/intrinsic plan plus identity evidence. + +## 9. The canonical executable object + +The executable unit can be called WarpProgramV1, while the publication +container remains a SemanticPackage. + +Conceptually: + +```text +SemanticPackage +├── application schema +├── operation schemas +├── WarpProgramV1[] +├── WarpOpticV1[] +├── attachment algebra profile +├── interpreter ABI requirement +├── package-wide limits +├── source/Core/program provenance +├── verifier evidence +└── digests +``` + +A mutation program needs at least: + +```text +WarpProgramV1 +├── jurisdiction/profile +├── entry operation coordinate +├── input and output schemas +├── invocation-to-graph binding +├── typed graph schema +├── DPO rules +│ ├── L +│ ├── K +│ ├── R +│ ├── positive conditions +│ └── negative conditions +├── bounded deterministic control law +├── match-selection law +├── private working-state schema +├── attachment intrinsic profile +├── footprint derivation and ceiling +├── resource bounds +├── obstruction map +├── result projection +└── interpreter ABI/version +``` + +A bounded optic needs a corresponding read-only form: + +```text +WarpOpticV1 +├── explicit causal basis +├── focus/aperture +├── traversal plan +├── support-evidence law +├── resource bounds +├── result projection +├── completeness/continuation posture +└── observer/interpreter ABI +``` + +The same algebra may encode kernel programs, but authority must remain +distinct: + +```text +Application package + may install application WarpProgramV1 + +Observation package + may install bounded WarpOpticV1 + +Causal policy package + may select or compose approved causal laws + under a stricter Echo profile + +Echo kernel package + owns submit/admit/schedule/commit/fork/settlement law + and cannot be replaced by an application package +``` + +This is one algebra with multiple jurisdictions. + +## 10. Receipt binding + +Current provider-native receipt evidence binds: + +- installed package; +- package reference/root; +- operation ID and coordinate; +- Target IR identity; +- scheduler rule ID. + +Source: +[echo/crates/warp-core/src/provider_contract.rs#L1181-L1262@6615d3a97731](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/warp-core/src/provider_contract.rs#L1181-L1262) + +It does not bind: + +- executable WARP program digest; +- WARP interpreter ABI/version; +- attachment intrinsic profile; +- deterministic program control law; +- executed rule/match trace or canonical patch identity. + +This is consistent with the present callback architecture because no admitted +executable artifact exists to bind. + +The future receipt should bind at least: + +```text +semantic package root +WarpProgram digest +interpreter ABI/version +intrinsic profile digest +canonical input digest +explicit causal basis +selected operation +derived footprint/support digest +committed TickPatch digest +result or obstruction identity +``` + +A full rule trace may be optional if the canonical input, program, basis, +interpreter profile, and resulting patch suffice for deterministic replay. The +exact executed program digest is not optional. + +## 11. Additional constraints exposed by the source + +### 11.1 Fixed-width coordinates remain unresolved end to end + +There are currently three coordinate representations: + +- native Rust uses u64; +- GraphQL/Wesley narrows values through Int/i32; +- TypeScript exposes branded structures whose value is number. + +The GraphQL narrowing is explicit: +[jedit/contracts/jedit/echo-text.graphql#L41-L60@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/contracts/jedit/echo-text.graphql#L41-L60) + +The native host converts u64 to i32 and refuses larger values: +[jedit/native/jedit-echo-host/src/host.rs#L420-L427@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/host.rs#L420-L427) + +The domain coordinate wrapper holds a TypeScript number: +[jedit/src/domain/graph-rope-types.ts#L36-L59@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/domain/graph-rope-types.ts#L36-L59) + +Removing GraphQL Int is necessary but insufficient. The generated JavaScript +client also needs an exact representation, likely bigint or a canonical +fixed-width wrapper rather than an unrestricted number. + +### 11.2 ReplaceRange's explicit basis is supplied by the host + +The GraphQL operation carries basisHeadId, but the TypeScript host request does +not: +[jedit/src/ports/echo-text-contract-host.ts#L40-L45@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/ports/echo-text-contract-host.ts#L40-L45) + +The native host snapshots the current canonical head and inserts it into the +generated intent: +[jedit/native/jedit-echo-host/src/host.rs#L136-L167@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/host.rs#L136-L167) + +In the future law, Jim's canonical command should name its basis explicitly. +Ambient host lookup must not silently determine which historical coordinate the +operation meant. + +### 11.3 Jim's native runtime is single-worldline + +The native host creates one hard-coded worldline and one AcceptAll default +writer: +[jedit/native/jedit-echo-host/src/host.rs#L375-L409@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/host.rs#L375-L409) + +The ttd, strand, and braid vocabulary is disconnected both at the operation +layer and at the host-session model. A future Jim/Echo boundary must carry +explicit worldline and causal coordinates. + +### 11.4 Tick patches are already the correct commit boundary + +Echo defines a tick patch as a replayable prescriptive delta sufficient to +reconstruct a tick without rerunning matching or scheduling: +[echo/crates/warp-core/src/tick_patch.rs#L3-L13@6615d3a97731](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/warp-core/src/tick_patch.rs#L3-L13) + +Its canonical operation vocabulary includes node, edge, attachment, and +warp-instance changes: +[echo/crates/warp-core/src/tick_patch.rs#L95-L165@6615d3a97731](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/warp-core/src/tick_patch.rs#L95-L165) + +The new interpreter does not need a second commit format. It needs to derive a +lawful TickPatch from an admitted WarpProgram. + +## 12. Constitutional laws + +### Executable Semantics Law + +Every observable consequence admitted by Echo must be derivable solely from: + +- admitted Edict meaning; +- its independently verified executable WARP program; +- Echo-owned runtime state; +- versioned deterministic Echo intrinsics; +- explicitly admitted capability results. + +Ambient host code, callbacks, plugins, or handwritten application +implementations must not determine semantic outcomes. + +### Application Meaning Law + +Application code authors meaning. Echo executes admitted meaning. + +A generated client may construct canonical input and submit it. It must not +know how to perform ReplaceRange. + +### Capability Law + +Executable semantics may request explicitly named capabilities. Echo owns +capability admission. Capabilities perform effects but do not define +application-semantic consequence. + +### Jurisdiction Law + +The transformation algebra may be uniform. Authority is not. + +- Echo kernel rules own runtime judgment. +- Echo causal rules own worldline and settlement topology. +- Edict-authored application rules own admitted application consequence. +- Edict-authored optics own bounded read plans. +- Capabilities own only their named effect crossing. + +### Atomic Program Law + +A multi-rule WARP program may use private deterministic evaluation state, but a +successful application operation commits one atomic TickPatch. Intermediate +work states do not become accidental application history. + +### Evidence Law + +Evidence from one crossing cannot stand in for another. + +Package identity, operation identity, Target IR identity, scheduler rule +identity, executable program identity, capability evidence, and committed +consequence are distinct propositions and must be bound explicitly where +required. + +## 13. Recommended design campaign + +Before authoring the real Jedit ReplaceRange .edict operation, produce a focused +architecture document named Executable Semantics for Echo. + +Use five orthogonal witnesses: + +1. DeclareCheckpoint — one finite application graph write. +2. ReplaceRange — bounded transactional multi-rule persistent-rope + transformation. +3. TextWindow — bounded optic with exact support evidence. +4. File save — explicit capability crossing. +5. Fork/braid/settlement — proof that shared algebra does not collapse + jurisdiction. + +The design must freeze: + +- the authoritative Jim text fact schema; +- structural relationships versus scalar attachments; +- canonical invocation binding; +- explicit worldline and basis semantics; +- WarpProgramV1; +- bounded deterministic control and matching; +- private intermediate evaluation state; +- atomic tick-patch emission; +- the intrinsic profile; +- typed obstructions; +- optic execution; +- package and receipt binding; +- interpreter recovery semantics; +- kernel/application/capability jurisdiction. + +## Final assessment + +WARP algebra should be Echo's executable semantics, provided WARP program means +a closed, typed, deterministic, resource-bounded, transactional +graph-transformation program—not merely one DPO span and not a named host +intrinsic. + +Fork, braid, and settlement belong to the same broad algebraic universe, but +they already operate under Echo's causal-kernel jurisdiction. They must not +become ordinary Jedit-authored application rules. + +Only after the executable WARP program contract and authoritative Jim schema +are defined should the real Jedit ReplaceRange .edict operation be authored. +Otherwise, Edict would be asked to compile into a target that still has no +complete executable constitutional meaning. From 73f73a6a1a25e67c3404caba588b79b6a6d3104d Mon Sep 17 00:00:00 2001 From: James Ross Date: Sat, 18 Jul 2026 23:49:33 -0700 Subject: [PATCH 5/7] test(docs): register ADR 0023 namespace --- tests/docs/test_adr_namespace.sh | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/tests/docs/test_adr_namespace.sh b/tests/docs/test_adr_namespace.sh index 364e5778..3de45c8e 100755 --- a/tests/docs/test_adr_namespace.sh +++ b/tests/docs/test_adr_namespace.sh @@ -33,9 +33,10 @@ readonly current_adrs=( "0020-retained-reading-storage-and-proof-boundary.md" "0021-public-optic-observation-boundary.md" "0022-application-requested-causal-anchor-admission.md" + "0023-admitted-executable-operation-packages.md" ) -readonly current_adr_last=22 +readonly current_adr_last=23 readonly superseded_legacy_adrs=( "ADR-0003-Materialization-Bus.md" From fc98855eccf6726af87855ec9a704fc8348bb343 Mon Sep 17 00:00:00 2001 From: James Ross Date: Sun, 19 Jul 2026 00:31:30 -0700 Subject: [PATCH 6/7] docs(architecture): tighten executable operation evidence --- .../0015-registry-provider-host-boundary.md | 3 +- ...-admitted-executable-operation-packages.md | 204 ++++++++++++------ docs/topics/GeneratedRules.md | 96 ++++++--- 3 files changed, 208 insertions(+), 95 deletions(-) diff --git a/docs/adr/0015-registry-provider-host-boundary.md b/docs/adr/0015-registry-provider-host-boundary.md index db52dc0a..94e038f2 100644 --- a/docs/adr/0015-registry-provider-host-boundary.md +++ b/docs/adr/0015-registry-provider-host-boundary.md @@ -4,7 +4,8 @@ # ADR 0015: Registry, Provider, and Host Boundary - **Status:** Partially superseded -- **Superseded in part by:** ADR 0023 +- **Superseded in part by:** + [ADR 0023](0023-admitted-executable-operation-packages.md) - **Date:** 2026-07-13 ## Context diff --git a/docs/adr/0023-admitted-executable-operation-packages.md b/docs/adr/0023-admitted-executable-operation-packages.md index 1d351dfa..cffb21fa 100644 --- a/docs/adr/0023-admitted-executable-operation-packages.md +++ b/docs/adr/0023-admitted-executable-operation-packages.md @@ -113,6 +113,8 @@ Every `ExecutableOperationPackageV1` must canonically bind: obstruction schemas; - the Edict source, canonical meaning, Core, and target identities that define the admitted semantic closure; +- the exact Jedit-owned canonical text-schema declaration coordinate and + digest; - the exact lawpack resource coordinate and digest; - the exact `EchoOperationProgramV1` bytes and digest; - an explicit parent-basis contract; @@ -156,54 +158,148 @@ semantic operation. A prepared operation may commit only against the exact parent basis on which it was evaluated. -`PreparedEchoOperationV1` and its eventual receipt evidence must bind: - -- the exact Echo parent worldline, writer head, frontier/tick, commit or root, - and application basis named by the invocation; -- the admitted operation and package identities plus the subordinate program +The first version names one canonical basis value, +`EchoOperationEvaluationBasisV1`. It is not a choice among a tick, commit, root, +or application coordinate. Every encoded value contains these fields in this +order: + +1. `writer_head.worldline_id`: the canonical 32 bytes of `WorldlineId`; +2. `writer_head.head_id`: the canonical 32 bytes of `HeadId`; +3. `worldline_tick`: one little-endian `u64`; +4. `commit_global_tick`: a required option encoded as tag `0` for the empty + `U0` frontier or tag `1` followed by one little-endian `u64`; +5. `state_root`: the exact 32-byte canonical graph-state root; +6. `commit_id`: the exact 32-byte canonical frontier/commit hash; +7. `application_basis_schema_digest`: the exact 32-byte digest of the basis + schema bound by the admitted operation package; +8. `application_basis_value_digest`: the exact 32-byte digest of the canonical + basis value carried in the package-declared invocation field. + +Its canonical byte encoding is the ASCII domain +`echo:operation-evaluation-basis:v1\0` followed by those fields without padding. +Its identity is the BLAKE3 digest of those bytes. The option tag is mandatory; +all other fields are mandatory. The admitted operation's basis contract names +exactly one invocation field and codec. Echo computes the application-basis +value digest from that field's canonical bytes and resolves the value to the +Jedit buffer head present at the named runtime frontier. A missing, foreign, +stale, or differently encoded application basis is a typed obstruction; Echo +does not choose or infer another basis. + +`PreparedEchoOperationV1` and its eventual execution evidence must bind: + +- the complete `EchoOperationEvaluationBasisV1` value and identity; +- the exact submission/invocation identity, canonical invocation digest, + caller-authority evidence identity, and Echo-owned invocation-admission + evidence identity; +- the admitted operation and package identities, package-admission evidence + identity, Echo-owned installed-operation identity, and subordinate program identity; -- the canonical input digest; - the delegated budget and consumed budget; - the declared footprint identity; - the actual read/write footprint derived during evaluation; -- the resulting patch digest; -- the typed output or obstruction identity; -- the private execution or trace identity. +- the private execution or trace identity; +- exactly one closed `PreparedEchoOperationOutcomeV1` variant: + - `Committable`, carrying a patch digest and typed output identity; or + - `Obstructed`, carrying a typed obstruction identity and, by its canonical + variant encoding, explicit evidence that no parent patch exists. + +An `Obstructed` outcome never enters parent commit or scheduler composition and +never carries a patch digest. It may produce retained typed execution evidence, +but it does not claim a committed consequence. -Before commit, Echo must establish all of the following: +Before any `Committable` outcome can commit, Echo must establish all of the +following: ```text -current parent basis == evaluated parent basis -installed admitted-operation identity == evaluated admitted-operation identity -installed package identity == evaluated package identity -installed program identity == evaluated program identity -canonical input identity == evaluated input identity +current EchoOperationEvaluationBasisV1 bytes == evaluated basis bytes +current installed admitted-operation identity == evaluated operation identity +current installed package identity == evaluated package identity +current installed program identity == evaluated program identity +admitted invocation identity and admission evidence == evaluated identities +canonical invocation identity == evaluated invocation identity +consumed budget <= delegated budget and evaluation completed within that budget actual footprint is permitted by the declared footprint contract -committed patch identity == evaluated patch identity ``` +An attempted evaluation that cannot complete without exceeding its delegated +budget yields a typed budget obstruction and no committable patch. A successful +evaluation may consume exactly its delegated budget if it completes without an +overrun. + +For a singleton commit, Echo must additionally establish: + +```text +committed patch identity == evaluated Committable patch identity +``` + +An existing scheduler composition rule may combine independent committable +preparations evaluated from the same basis. The committed receipt must then +bind the exact scheduler-rule identity, a canonical ordered list of member +preparation and patch identities, and the resulting composite `TickPatch` +identity. The scheduler law must verify that every member has identical +`EchoOperationEvaluationBasisV1` bytes and that the composite patch is the +canonical result of that exact ordered membership. A singleton commit uses the +same evidence shape with a one-member list. + If the parent basis changed, the prepared operation is ineligible to commit and must yield a typed basis-changed posture without applying any patch. Echo must not silently rebase, retarget, revalidate, or transport the preparation to the -new basis. A new evaluation is a new witnessed attempt unless an existing, -separately admitted Echo composition rule explicitly proves otherwise. +new basis. A new evaluation is a new witnessed attempt. Scheduler composition +from one unchanged common basis is not cross-basis revalidation. + +`EchoOperationExecutionEvidenceV1` has a separate closed terminal sum: + +- `Committed` binds the composite `TickPatch` digest, typed output identity, + resulting frontier identity, and scheduler composition evidence; or +- `NotCommitted` binds the evaluation obstruction or commit-ineligibility + identity, a canonical terminal-outcome digest, and canonical no-parent-patch + evidence. -An existing scheduler composition rule may combine independent preparations -evaluated from the same parent snapshot. That is not revalidation across a -changed basis; the composed tick remains bound to the common evaluation basis. +`NotCommitted` never carries a committed patch digest. A preparation that was +`Committable` but lost exact-basis eligibility is represented as +`NotCommitted`; its uncommitted prepared patch remains attributable but is not +misreported as a parent consequence. + +When an admitted package declares no application-specific caller-authorization +requirement, the caller-authority evidence field binds the versioned canonical +`None` identity selected by that package profile. It is never omitted or +silently replaced by package or program identity. This requirement binds the +admission posture without adding broad authorization policy to this decision. ### Jedit rope-law closure For the first `ReplaceRange` vertical, Jedit will use a digest-locked canonical declarative executable semantic resource imported through a Jedit-owned Edict -lawpack. Campaign 1 will not expand Edict source until it can directly express -the complete recursive persistent-rope algorithm. +lawpack. This decision does not require Edict source to express the complete +recursive persistent-rope algorithm directly. + +Before the real package can be generated or admitted, Jedit must publish one +versioned canonical text-schema declaration. That Jedit-owned declaration must +bind: + +- the exact fact, edge, and attachment proposition set and schema digest; +- the canonical codec and content-identity law for each proposition; +- whether the TypeScript-only structural-maintenance and checkpoint-anchor + propositions are authoritative retained facts, derived evidence, or excluded + from the first operation surface; +- the compatibility or migration posture for the current native JSON fact + model; and +- the exact rope-law resource coordinate and digest that consumes the selected + schema. + +The executable-operation package must bind that declaration's coordinate and +digest. Its public schemas, lawpack, and subordinate program must close exactly +over the declared propositions and codecs. Absence or disagreement produces a +typed schema-closure refusal before package admission or installation. Edict +and Echo validate the selected declaration; neither may choose between Jedit's +current TypeScript and native models. The authoritative binding chain is: ```text Jedit-owned ReplaceRange.edict → admitted executable-operation package and public operation contract +→ exact Jedit canonical text-schema declaration → canonical semantic closure and exact fact/codec/identity law → exact Jedit lawpack coordinate and digest → exact canonical declarative EchoOperationProgramV1 bytes and digest @@ -253,7 +349,7 @@ This is the preferable long-term authoring experience if repeated operations demonstrate that those constructs belong in Edict. It is rejected for the first vertical because the current compiler's initial lowerable subset is much smaller. Implementing the entire language surface before any hook-free -operation runs would turn Campaign 1 into a broad language and runtime design +operation runs would turn the first witness into a broad language and runtime design effort and would make `ReplaceRange` define unproven universal syntax. ### Bind a canonical declarative executable resource from a Jedit lawpack @@ -272,14 +368,17 @@ Later Edict syntax may compile to the same target program boundary. ## Verification Evidence Grades The word "independent" is reserved for an implementation that does not merely -enter the same logic through another crate or call path. The first vertical -will label evidence as follows. +enter the same logic through another crate or call path. Evidence claims use +the following grades. | Check | Evidence grade | First-version claim | | ------------------------------------------------------------------------------------------------------------- | --------------------------------------------------------------------------------------------------------------------- | -------------------------------------------------------------------------------------------------------------------------------------------------------- | | Canonical decoding, schema closure, digest recomputation, supported instruction set, and static budget bounds | Deterministic self-validation | The exact bytes are internally well-formed under the installed ABI. | | Installed package/program/input identity and exact-basis equality before commit | Deterministic self-validation | Echo committed only the admitted preparation against its evaluated basis. | +| Submission, caller-authority, and invocation-admission evidence identities | Deterministic self-validation | Preparation and retained execution evidence attribute evaluation to the exact Echo-admitted invocation. | +| Consumed budget against the delegated budget | Deterministic self-validation | An evaluation that cannot complete within budget obstructs without a committable patch. | | Actual footprint against declared footprint law or ceiling | Deterministic self-validation | The evaluated support stayed within the admitted footprint contract. | +| Scheduler rule, ordered preparation membership, and composite patch | Deterministic self-validation | The committed tick is attributable to the exact composition decision over one common basis. | | Core to Target IR relation | Structurally separate verifier path | A separately invoked verifier path recomputed or checked the declared relation; separation alone is not implementation independence. | | Admitted operation package plus Target IR and lawpack resource to `EchoOperationProgramV1` binding | Structurally separate verifier path | A separately invoked target verifier checked exact package/program/resource/schema/profile correspondence without making the program an authority token. | | Generated codec and package golden bytes | Independently implemented conformance evidence only when the comparison implementation shares no encoder/lowerer path | The checked finite vectors agree; this is not a proof over all values. | @@ -288,9 +387,9 @@ will label evidence as follows. | Receipt/WAL round-trip and fresh-host reconstruction | Deterministic self-validation | Retained bytes reconstruct the same installed and execution identities without callbacks. | A separate verifier crate is not, by itself, independently implemented -conformance evidence. The first vertical will not claim formal refinement, -complete semantic equivalence, a clean-room Echo interpreter, or a proof that -all possible `ReplaceRange` inputs agree with the legacy planner. +conformance evidence. This decision does not claim formal refinement, complete +semantic equivalence, a clean-room Echo interpreter, or a proof that all +possible `ReplaceRange` inputs agree with the legacy planner. The differential corpus counts as independently implemented evidence only when its oracle path does not invoke the new program evaluator or generated @@ -315,36 +414,6 @@ by comparing two wrappers around the same algorithm. typed input, and external capabilities. It may not provide semantic execution or Echo authority. -## Sequencing Consequence - -Implementation proceeds in dependency order: - -1. minimal Edict operation prerequisites; -2. hook-free Echo bounded-operation evaluation with a tiny generic program; -3. the real Jedit `ReplaceRange` semantic artifact and differential oracle - corpus; -4. current Jim invocation and legacy `ReplaceRange` cutover. - -Each stage remains a separately reviewed and merged campaign. The first real -vertical is complete only when this chain is executable: - -```text -real Jim command -→ explicit basis-bearing generated invocation -→ admitted Edict-authored operation -→ Echo-owned deterministic evaluation -→ one committed buffer consequence or typed obstruction -→ receipt binding the executable semantics -``` - -Campaign 1 is bounded to the Edict capabilities required to type the real -operation surface, preserve exact fixed-width values and explicit basis, -canonically bind the lawpack program resource through Core and artifact -identity, and generate the operation-facing package/client inputs. It does not -add the Echo evaluator, author the Jedit rope program, or introduce general -recursion, iteration, graph-pattern syntax, observer syntax, or process -semantics. - ## Rejected Alternatives - Mutate provider v1 and describe it as provider v2. @@ -369,15 +438,16 @@ semantics. operations. - Echo gains one new program interpreter and installed-operation evidence category rather than a callback-bearing provider revision. -- Campaign 1 stays bounded: it adds fixed-width and explicit-basis operation - prerequisites plus exact executable-resource binding, not a general recursive - Edict language. +- Edict needs fixed-width and explicit-basis operation support plus exact + executable-resource binding; this decision does not require a general + recursive language. - The first program format preserves contained-execution obligations without claiming durable child lanes, child ticks, wormholes, or universal WARP wire status. -- Receipts must distinguish package, program, input, basis, declared and actual - footprints, patch, output or obstruction, budget, and execution-trace - identities. +- Execution evidence must distinguish package, program, admitted invocation, + basis, declared and actual footprints, budget, scheduler composition, and + execution-trace identities. A successful commit binds its patch and output; + an obstruction binds a typed no-patch outcome instead. - A receipt's program digest identifies the executable meaning used only in the context of the admitted operation and package that bind it; it does not retroactively make the program independently invocable or authoritative. @@ -406,6 +476,10 @@ semantics. - [Echo provider v1 stores host executor and footprint hooks](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/warp-core/src/provider_contract.rs#L35-L126) - [Echo rewrite rules execute native matcher, executor, and footprint functions](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/warp-core/src/rule.rs#L11-L103) - [Current provider evidence binds package, Target IR, and scheduler rule](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/warp-core/src/provider_contract.rs#L1181-L1263) +- [Echo runtime coordinates have canonical identifier and counter representations](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/echo-runtime-schema/src/lib.rs#L82-L153) +- [Echo frontier evidence carries tick, state-root, and commit identities](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/echo-wasm-abi/src/kernel_port.rs#L364-L387) - [Jedit's current `ReplaceRange` semantic planner](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/rope.rs#L385-L475) - [Jedit persistent-rope split and balance law](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/rope/tree.rs#L69-L193) - [Jedit currently binds replacement to handwritten callbacks](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/contract.rs#L111-L142) +- [Jedit's TypeScript text-graph proposition set](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/domain/graph-rope-types.ts#L12-L21) +- [Jedit's native text-fact proposition set](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/records.rs#L7-L14) diff --git a/docs/topics/GeneratedRules.md b/docs/topics/GeneratedRules.md index 8d7eb63b..91370474 100644 --- a/docs/topics/GeneratedRules.md +++ b/docs/topics/GeneratedRules.md @@ -5,9 +5,10 @@ Product and application rules are authored in contract languages. Hand-written Rust rule registration is not a supported product authoring surface. The first -Edict mutation closure now reaches provider-native scheduling, receipts, and -WAL recovery. Wesley packaging and the generated bounded-read corridor remain -incomplete and must not borrow that mutation evidence. +Edict provider-v1 compatibility closure now reaches provider-native scheduling, +receipts, and WAL recovery. Its semantic implementation remains host-bound. +Wesley packaging and the generated bounded-read corridor remain incomplete and +must not borrow that mutation evidence. ## Current Implementation @@ -19,11 +20,13 @@ exercise package verification. The Edict provider path authenticates exact authored semantic source and generation settings, emits canonical provider artifacts, lowers the supported -mutation closure into `echo.span-ir/v1` Target IR, and independently verifies -that crossing. It publishes checked lowerer and verifier components inside a -digest-locked provider package with exact provenance and non-authoritative -review evidence. The lowerer also emits a requested-only Rust helper that binds -the exact Target IR, bundle propositions, profiles, schemas, ABI versions, +mutation closure into `echo.span-ir/v1` Target IR, and checks that crossing +through a structurally separate verifier path. That separation is not, by +itself, an independently implemented verifier. The path publishes checked +lowerer and verifier components inside a digest-locked provider package with +exact provenance and non-authoritative review evidence. The lowerer also emits +a requested-only Rust helper that binds the exact Target IR, bundle +propositions, profiles, schemas, ABI versions, footprint obligation, obstruction mapping, and semantic operation identity through a pure descriptor preflight. The generated-artifact profile owns the `le-binary-v1` value codec; the helper implements distinct typed `Id`, `Input`, @@ -86,15 +89,16 @@ a Rust dependency consumer can explicitly enable the feature. It is not an access-control or security seal. Echo product and adapter code must not use it as an application authoring escape hatch. -## Target Corridor +## Execution Corridors -The required end state is: +### Provider-v1 compatibility corridor + +The currently implemented Edict mutation corridor is: ```text -Wesley or Edict source --> verified mutation Target IR or lawful read/observer semantics --> generated Rust handlers, bounded observers, and footprints --> generated typed codecs, EINT helpers, registry, and package metadata +Edict source +-> reviewed mutation Target IR +-> generated Rust mutation handler, codecs, footprint, registry, and package metadata -> opaque provider package proposal with explicit host binding -> Echo-owned exact proposal-claim admission -> exact package corroboration @@ -105,20 +109,48 @@ Wesley or Edict source -> receipt / WAL evidence carrying package, operation, Target IR, and rule identity ``` -Wesley still needs a package emitter. Edict already emits a digest-locked -provider publication package, codec-bound mutation client, borrowed registry, -and fail-closed package proposal. Echo admits the exact proposal claim under -independent trusted-host policy; `echo-wesley-gen` corroborates that token with -independently admitted exact package bytes and consumes the proof into a -provider-native installed record with atomic Echo-owned indexes. Echo now -admits and dispatches that installed mutation through the shared scheduler with -provider-specific receipt and WAL evidence. It still needs the separate -generated bounded-observer path for authored reads. The current mutation -proposal intentionally rejects `Query`; that refusal does not turn a read into -a mutation or eliminate the independent observer/optic corridor. Installation -and invocation reuse Echo's existing indexes, scheduler, receipt, and WAL -machinery without fabricating Wesley metadata or creating a second execution -engine. +This is provider-v1 callback-shaped compatibility infrastructure, not the +required authoring path for newly authored executable operations. Edict already +emits a digest-locked provider publication package, codec-bound mutation client, +borrowed registry, and fail-closed package proposal. Echo admits the exact +proposal claim under a separate trusted-host policy; `echo-wesley-gen` +corroborates that token with separately admitted exact package bytes and +consumes the proof into a provider-native installed record with atomic +Echo-owned indexes. Echo admits and dispatches that installed mutation through +the shared scheduler with provider-specific receipt and WAL evidence. Those +identities prove exact wiring, not that the ambient callback implements the +authored meaning. + +Wesley's direct rule/bootstrap and bounded-read work remains a separate +compatibility corridor. Wesley still needs a package emitter and its own +installed generated-pack witness. The Edict mutation proposal intentionally +rejects `Query`; that refusal does not turn a read into a mutation or eliminate +the observer/optic crossing. + +### Required executable-operation corridor + +[ADR 0023](../adr/0023-admitted-executable-operation-packages.md) governs the +not-yet-implemented corridor required for newly authored application mutations: + +```text +Jedit-owned Edict operation source and public contract +-> canonical meaning, Core, and exact Jedit schema/lawpack closure +-> exact subordinate EchoOperationProgramV1 +-> structurally separate target verification +-> Echo-owned package admission, byte corroboration, and installation +-> exact basis-bearing invocation and Echo-owned invocation admission +-> bounded private Echo evaluation with no application callbacks +-> scheduler composition and exact-basis commit +-> committed TickPatch and result, or typed no-patch outcome +-> execution evidence / WAL carrying package, invocation, program, basis, + budget, footprint, scheduler, and terminal-outcome identities +``` + +The operation package owns the public contract and runtime-recognized +invocability. The subordinate program supplies executable meaning only. Echo +cannot install or invoke a naked program digest, and a generated artifact does +not confer caller authority. Provider v1 remains stable while existing +consumers migrate; it is not silently reinterpreted as this new category. ## Footprint Honesty @@ -146,10 +178,16 @@ trigger hidden retries or widen access. registration. - Product and adapter crates do not enable `native_rule_bootstrap`. - Generators emit artifacts, descriptors, and opaque proposals without - registering themselves. Trusted hosts independently admit proposal claims, + registering themselves. Trusted hosts separately admit proposal claims, corroborate exact package evidence, and register package-qualified generated material through the appropriate provider-native or Wesley compatibility record—not an app-specific engine escape hatch. +- Newly authored executable operations resolve installation and invocation from + an admitted `ExecutableOperationPackageV1`; a naked + `EchoOperationProgramV1` cannot install or invoke. +- Newly authored executable operations expose no application matcher, executor, + footprint callback, or prebuilt mutation plan. Provider-v1 callback bindings + remain explicitly labeled compatibility infrastructure. - Registry/package identity, operation identity, codec/schema compatibility, and footprint metadata are verified before the engine mutates registration state. From 3149892b486c3385a57ec19a1e8493980f61fac7 Mon Sep 17 00:00:00 2001 From: James Ross Date: Sun, 19 Jul 2026 00:31:39 -0700 Subject: [PATCH 7/7] docs(plans): align executable WARP campaign --- ...im-edict-echo-executable-warp-semantics.md | 449 ++++++++++-------- 1 file changed, 242 insertions(+), 207 deletions(-) diff --git a/docs/plans/2026-07-18-jim-edict-echo-executable-warp-semantics.md b/docs/plans/2026-07-18-jim-edict-echo-executable-warp-semantics.md index 4515eb2d..8ce16b5e 100644 --- a/docs/plans/2026-07-18-jim-edict-echo-executable-warp-semantics.md +++ b/docs/plans/2026-07-18-jim-edict-echo-executable-warp-semantics.md @@ -3,18 +3,24 @@ # Jim × Edict × Echo: Executable WARP Semantics Inventory -Status: architectural discovery and source-grounded plan -Date: 2026-07-18 -Implementation status: halted pending architectural agreement +- **Status:** Historical discovery reconciled by + [ADR 0023](../adr/0023-admitted-executable-operation-packages.md) +- **Date:** 2026-07-18 +- **Implementation status:** Campaign 1 has not started + +ADR 0023 is authoritative where this source inventory's earlier hypotheses +differ from the accepted executable-operation boundary. The accepted campaign +is recorded in section 13; the inventory of broader Jim and Echo capabilities +does not place those capabilities in scope for the first vertical. ## Source basis This report is based on source code, not repository documentation, at these authoritative repository heads: -- Jedit: c70e12d73b4b00bc92412bab67e1761f7dd22f82 -- Echo: 6615d3a97731a076fb4945bb6da083e82f55710d -- Edict: da5da887c1fa089a3f82f4d29d0799eb6e155f31 +- [Jedit `c70e12d73b4b`](https://github.com/flyingrobots/jedit/commit/c70e12d73b4b00bc92412bab67e1761f7dd22f82) +- [Echo `6615d3a97731`](https://github.com/flyingrobots/echo/commit/6615d3a97731a076fb4945bb6da083e82f55710d) +- [Edict `da5da887c1fa`](https://github.com/flyingrobots/edict/commit/da5da887c1fa089a3f82f4d29d0799eb6e155f31) Historical commits in this report are immutable evidence coordinates. They are not permission to assume that current repository heads remain unchanged. @@ -88,22 +94,25 @@ Runtime judgments, exclusively Echo-owned This is one algebra with multiple jurisdictions. -Two prerequisites must be resolved before ReplaceRange can honestly become +Two prerequisites must be resolved before `ReplaceRange` can honestly become executable Edict meaning: -1. Jim does not yet have one canonical text-graph schema. -2. Echo does not yet have a serialized, independently verifiable DPO-program - interpreter. +1. Jedit must select and bind one canonical text-graph schema and migration + posture; package generation or admission must refuse a missing or mismatched + declaration. +2. Echo does not yet have a serialized DPO-program interpreter with + deterministic self-validation and a structurally separate target-verifier + path. Independently implemented evidence is a separate, stronger grade. ## 1. What Jim executes through Echo today The current GraphQL/Wesley corridor defines exactly three mutations and one query: -- createBufferWorldline -- replaceRangeAsTick -- declareCheckpoint -- textWindow +- `createBufferWorldline` +- `replaceRangeAsTick` +- `declareCheckpoint` +- `textWindow` Source: [jedit/contracts/jedit/echo-text.graphql#L1-L71@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/contracts/jedit/echo-text.graphql#L1-L71) @@ -114,17 +123,17 @@ Sources: [jedit/src/ports/echo-text-contract-host.ts#L9-L21@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/ports/echo-text-contract-host.ts#L9-L21), [jedit/src/ports/echo-text-contract-host.ts#L140-L145@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/ports/echo-text-contract-host.ts#L140-L145) -### 1.1 Open / CreateBufferWorldline +### 1.1 Open / `CreateBufferWorldline` Open is presently a composite operation: -1. Jedit reads the file through its local EditorFilePort. -2. The loaded text becomes initialText. +1. Jedit reads the file through its local `EditorFilePort`. +2. The loaded text becomes `initialText`. 3. Jedit calls the Echo host. 4. If the buffer already exists, the native host returns its current snapshot, without a creation receipt. -5. Otherwise, it submits CreateBufferWorldline. -6. Jedit subsequently performs a TextWindow observation. +5. Otherwise, it submits `CreateBufferWorldline`. +6. Jedit subsequently performs a `TextWindow` observation. The pre-Echo file read occurs here: [jedit/src/app/workspace/workspace-text-open-basis.ts#L55-L80@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/app/workspace/workspace-text-open-basis.ts#L55-L80) @@ -180,7 +189,7 @@ Sources: [jedit/src/app/workspace/workspace-text-commands.ts#L46-L58@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/app/workspace/workspace-text-commands.ts#L46-L58), [jedit/src/app/workspace/workspace-text-commands.ts#L282-L305@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/app/workspace/workspace-text-commands.ts#L282-L305) -The current handwritten ReplaceRange law: +The current handwritten `ReplaceRange` law: 1. Resolves the buffer's canonical head. 2. Refuses a stale supplied basis. @@ -201,7 +210,7 @@ Source: #### Persistent derivation, not destructive replacement -ReplaceRange does not delete old rope nodes. +`ReplaceRange` does not delete old rope nodes. Jim has a persistent rope. The implementation creates new content-addressed nodes and a new head, reuses unaffected structure, and advances the buffer's @@ -227,7 +236,7 @@ replace Buffer ─canonicalHead→ OldHead This is naturally expressible in DPO, but it is persistent derivation rather than destructive replacement. -### 1.3 DeclareCheckpoint +### 1.3 `DeclareCheckpoint` Checkpoint declaration: @@ -252,7 +261,7 @@ Buffer ─contains→ BasisHead It is not a text mutation. -The current source nevertheless wraps it in a MutationPlan, which is the false +The current source nevertheless wraps it in a `MutationPlan`, which is the false vocabulary identified by Jedit issue #287: [jedit/native/jedit-echo-host/src/rope.rs#L240-L256@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/rope.rs#L240-L256) @@ -270,14 +279,14 @@ Source: The current product adapter maps only manual-save and autosave: [jedit/src/adapters/workspace-production-text-session.ts#L43-L46@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/adapters/workspace-production-text-session.ts#L43-L46) -### 1.4 TextWindow +### 1.4 `TextWindow` -TextWindow is the one currently executing bounded observation. It: +`TextWindow` is the one currently executing bounded observation. It: - takes a buffer and explicit basis head; - verifies buffer/head ownership; - checks the byte range; -- applies maxBytes; +- applies `maxBytes`; - traverses only relevant rope support; - returns the largest complete UTF-8 prefix; - reports supporting leaf/blob identities; @@ -305,7 +314,7 @@ function: ## 2. What Jim wants but cannot currently execute -The broader ProductionTextSession asks for ten operations: +The broader `ProductionTextSession` asks for ten operations: - open buffer - insert @@ -327,7 +336,7 @@ fail closed with a message saying that the current Wesley corridor does not implement them: [jedit/src/adapters/workspace-production-text-session.ts#L40-L62@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/adapters/workspace-production-text-session.ts#L40-L62) -### 2.1 MultiRangeEdit +### 2.1 `MultiRangeEdit` The input is an ordered collection of byte ranges and replacement strings: [jedit/src/app/workspace/production-text-session.ts#L104-L114@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/app/workspace/production-text-session.ts#L104-L114) @@ -337,13 +346,13 @@ It is declared but unsupported by the current adapter. Future choices must be explicit: - canonicalize ranges and perform one atomic bounded operation; -- lower it into a transaction containing multiple ReplaceRange applications; +- lower it into a transaction containing multiple `ReplaceRange` applications; - or refuse it as unsupported. It must not become an accidental loop whose result depends on caller iteration order or intermediate canonical-head movement. -### 2.2 CausalLineDiff +### 2.2 `CausalLineDiff` The requested optic takes: @@ -370,11 +379,11 @@ The intended reading cites: Source: [jedit/src/ports/text-authority-evidence.ts#L67-L95@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/ports/text-authority-evidence.ts#L67-L95) -This should be a bounded causal optic over retained RopeRewrite and RopeDiff +This should be a bounded causal optic over retained `RopeRewrite` and `RopeDiff` evidence. It is not a mutation and should not be recomputed from two privileged snapshots. -### 2.3 ExplainRange / :why +### 2.3 `ExplainRange` / `:why` The intended range explanation includes: @@ -390,7 +399,7 @@ The intended range explanation includes: Source: [jedit/src/ports/jedit-why-range.ts#L34-L128@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/ports/jedit-why-range.ts#L34-L128) -The UI computes a byte range around the cursor and requests explainRange. The +The UI computes a byte range around the cursor and requests `explainRange`. The current adapter refuses it: [jedit/src/app/workspace/workspace-why-range.ts#L70-L109@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/app/workspace/workspace-why-range.ts#L70-L109) @@ -416,14 +425,14 @@ exportSnapshot from Echo → declare manual-save checkpoint ``` -The export step invokes exportSnapshot, runs a materialization preflight, and -then directly calls saveEditorFile: +The export step invokes `exportSnapshot`, runs a materialization preflight, and +then directly calls `saveEditorFile`: [jedit/src/app/workspace/workspace-text-commands.ts#L336-L368@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/app/workspace/workspace-text-commands.ts#L336-L368) After successful export, the reducer schedules checkpoint declaration: [jedit/src/app/workspace/workspace-text-runtime-state.ts#L317-L348@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/app/workspace/workspace-text-runtime-state.ts#L317-L348) -The current exportSnapshot session operation is unsupported, so the production +The current `exportSnapshot` session operation is unsupported, so the production save chain cannot complete through the generated corridor. The correct future decomposition is: @@ -454,7 +463,7 @@ Sources: [jedit/src/app/workspace/workspace-command-catalog.ts#L88-L119@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/app/workspace/workspace-command-catalog.ts#L88-L119), [jedit/src/app/workspace/command-line-dispatch.ts#L52-L100@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/app/workspace/command-line-dispatch.ts#L52-L100) -### 3.1 ttd +### 3.1 `ttd` The command vocabulary supports: @@ -472,7 +481,7 @@ Sources: This is a kernel-resolved historical observation coordinate followed by normal optics. It is not an application mutation. -### 3.2 strand +### 3.2 `strand` The UI vocabulary includes: @@ -498,7 +507,7 @@ Sources: [echo/crates/warp-core/src/strand.rs#L1-L27@6615d3a97731](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/warp-core/src/strand.rs#L1-L27), [echo/crates/warp-core/src/strand.rs#L75-L117@6615d3a97731](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/warp-core/src/strand.rs#L75-L117) -Echo's fork_strand: +Echo's `fork_strand`: - replays the source at the requested historical tick; - forks provenance; @@ -512,7 +521,7 @@ Source: This is kernel causal law. -### 3.3 braid +### 3.3 `braid` The UI vocabulary includes: @@ -558,8 +567,8 @@ braid admit Echo's settlement code already separates those acts: - compare is explicitly read-only inspection; -- plan_with_policy produces deterministic import/conflict/plural decisions; -- settle_with_policy appends corresponding causal consequences. +- `plan_with_policy` produces deterministic import/conflict/plural decisions; +- `settle_with_policy` appends corresponding causal consequences. Sources: [echo/crates/warp-core/src/settlement.rs#L700-L757@6615d3a97731](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/warp-core/src/settlement.rs#L700-L757), @@ -586,11 +595,11 @@ invocation would introduce ambiguity. For ordinary submitted work, use a term such as: -- recordOutcome; -- finalizeDisposition; -- commitOutcome. +- `recordOutcome`; +- `finalizeDisposition`; +- `commitOutcome`. -Retain settleStrand, settleBraid, and SettlementPolicy for the causal operation +Retain `settleStrand`, `settleBraid`, and `SettlementPolicy` for the causal operation already implemented. ## 4. Latent concepts that are not Echo operations yet @@ -598,7 +607,7 @@ already implemented. ### 4.1 Undo and redo Undo and redo appear only as command/durability vocabulary and help text. There -is no ProductionTextSession or Echo operation for them. +is no `ProductionTextSession` or Echo operation for them. Source: [jedit/src/app/workspace/workspace-buffer-durability.ts#L44-L105@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/app/workspace/workspace-buffer-durability.ts#L44-L105) @@ -621,7 +630,7 @@ left/right bias and replacement-delta behavior: This is currently a local pure utility, not an Echo operation. -Jedit also models a separate RopeCheckpointAnchored association containing +Jedit also models a separate `RopeCheckpointAnchored` association containing checkpoint, causal-anchor fact, and receipt identities: [jedit/src/domain/graph-rope-types.ts#L250-L258@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/domain/graph-rope-types.ts#L250-L258) @@ -650,7 +659,7 @@ Source: The native rope performs splitting and deterministic height balancing internally, but its admitted native fact inventory does not contain -RopeStructuralMaintenance and the planner emits no such facts. +`RopeStructuralMaintenance` and the planner emits no such facts. Sources: [jedit/native/jedit-echo-host/src/records.rs#L7-L14@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/records.rs#L7-L14), @@ -662,7 +671,7 @@ A future design must decide whether balancing steps are: - retained structural-maintenance facts; - or implied by the canonical rope-construction law. -That decision affects receipts, replay, and :why. +That decision affects receipts, replay, and `:why`. ## 5. Jim's graph data model @@ -670,16 +679,16 @@ That decision affects receipts, replay, and :why. The TypeScript semantic model contains ten fact kinds: -1. BufferWorldline -2. RopeHead -3. RopeBranch -4. RopeLeaf -5. TextBlob -6. RopeRewrite -7. RopeDiff -8. RopeStructuralMaintenance -9. RopeCheckpoint -10. RopeCheckpointAnchored +1. `BufferWorldline` +2. `RopeHead` +3. `RopeBranch` +4. `RopeLeaf` +5. `TextBlob` +6. `RopeRewrite` +7. `RopeDiff` +8. `RopeStructuralMaintenance` +9. `RopeCheckpoint` +10. `RopeCheckpointAnchored` Sources: [jedit/src/domain/graph-rope-types.ts#L12-L21@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/domain/graph-rope-types.ts#L12-L21), @@ -714,8 +723,14 @@ Sources: [jedit/src/domain/graph-rope-types.ts#L85-L270@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/domain/graph-rope-types.ts#L85-L270), [jedit/native/jedit-echo-host/src/records.rs#L25-L106@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/records.rs#L25-L106) -This must be resolved before writing authoritative .edict source. Otherwise, -Edict will canonize one side of an unresolved semantic fork by accident. +ADR 0023 turns this discovery into a Jedit-owned admission prerequisite. Before +authoritative `.edict` source can produce an admissible real package, Jedit must +publish one versioned declaration that selects the canonical proposition, +identity, and codec law; classifies the TypeScript-only maintenance and anchor +facts; and states the compatibility or migration posture for the native JSON +model. The package, lawpack, program, and public schemas must close over that +exact declaration or fail with a typed schema-closure refusal. Edict and Echo +must not select a side of this semantic fork. ### 5.2 Current graph relationships are opaque JSON fields @@ -828,7 +843,7 @@ The executable unit therefore needs to be a bounded transactional WARP program, not merely one rule: ```text -WarpProgram ReplaceRange +EchoOperationProgramV1: ReplaceRange executable meaning │ ├─ bind invocation │ ├─ buffer @@ -865,7 +880,7 @@ WarpProgram ReplaceRange │ ├─ derive exact footprint │ -└─ atomically emit one TickDelta +└─ atomically prepare one TickPatch or one obstruction ``` The intermediate traversal/work graph must not leak into authoritative history @@ -893,7 +908,7 @@ plan must not. The WARP interpreter needs a small, versioned, deterministic intrinsic profile containing operations such as: -- checked u64 arithmetic and comparison; +- checked `u64` arithmetic and comparison; - canonical byte length; - bounded byte slicing; - UTF-8 validation and boundary checking; @@ -916,20 +931,20 @@ Jedit lawpack composes them into rope semantics. ## 7. The source proves the callback gap -Echo's current RewriteRule contains: +Echo's current `RewriteRule` contains: - a native matcher function pointer; - a native executor function pointer; - a native footprint function pointer. -Its PatternGraph is only a vector of type identifiers, and the source says that +Its `PatternGraph` is only a vector of type identifiers, and the source says that the left pattern is currently unused. Sources: [echo/crates/warp-core/src/rule.rs#L11-L50@6615d3a97731](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/warp-core/src/rule.rs#L11-L50), [echo/crates/warp-core/src/rule.rs#L73-L103@6615d3a97731](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/warp-core/src/rule.rs#L73-L103) -Jedit's generated mutation code constructs an empty PatternGraph and accepts +Jedit's generated mutation code constructs an empty `PatternGraph` and accepts host-supplied executor and footprint functions: [jedit/native/jedit-echo-host/src/generated/contract.rs#L990-L1033@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/generated/contract.rs#L990-L1033) @@ -940,7 +955,7 @@ Sources: [jedit/native/jedit-echo-host/src/contract.rs#L111-L142@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/contract.rs#L111-L142) The provider-native Edict helper currently does the same thing with stronger -identity evidence. Its generated API asks for ProviderMutationHooksV1 and says +identity evidence. Its generated API asks for `ProviderMutationHooksV1` and says it is constructing a package proposal from an explicit host executor/footprint binding: [echo/crates/echo-edict-provider-lowerer/src/lib.rs#L1238-L1283@6615d3a97731](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/echo-edict-provider-lowerer/src/lib.rs#L1238-L1283) @@ -991,90 +1006,69 @@ Sources: [echo/crates/echo-edict-provider-lowerer/src/lib.rs#L1580-L1690@6615d3a97731](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/echo-edict-provider-lowerer/src/lib.rs#L1580-L1690), [echo/crates/echo-edict-provider-lowerer/tests/lowerer_contract.rs#L1263-L1293@6615d3a97731](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/echo-edict-provider-lowerer/tests/lowerer_contract.rs#L1263-L1293) -The existing echo.span-ir/v1 must not yet be described as a complete executable +The existing `echo.span-ir/v1` must not yet be described as a complete executable DPO program. Today it is a bounded effect/intrinsic plan plus identity evidence. -## 9. The canonical executable object +## 9. The accepted first-version executable object -The executable unit can be called WarpProgramV1, while the publication -container remains a SemanticPackage. +[ADR 0023](../adr/0023-admitted-executable-operation-packages.md) retires +`WarpProgramV1` and `SemanticPackage` as normative first-version names. They +were discovery hypotheses, not compatibility aliases. The accepted public +container is `ExecutableOperationPackageV1`; its subordinate target-relative +executable artifact is `EchoOperationProgramV1`. A future portable WARP program +or broader semantic package needs a separate compatibility decision and cannot +silently alias either first-version identity. -Conceptually: +The admitted package owns the public contract: ```text -SemanticPackage -├── application schema -├── operation schemas -├── WarpProgramV1[] -├── WarpOpticV1[] -├── attachment algebra profile -├── interpreter ABI requirement -├── package-wide limits -├── source/Core/program provenance -├── verifier evidence -└── digests +ExecutableOperationPackageV1 +├── public operation coordinate +├── invocation, output, and obstruction schemas +├── explicit basis contract +├── budget and declared-footprint contracts +├── authority and invocation-admission requirements +├── result and obstruction interpretation +├── Edict source/Core/target semantic closure +├── Jedit canonical text-schema declaration +├── exact Jedit lawpack coordinate and digest +├── exact EchoOperationProgramV1 bytes and digest +├── evaluator ABI and intrinsic-profile requirement +├── provenance and verifier evidence grades +└── package root and digests ``` -A mutation program needs at least: +The bound program supplies only executable meaning: ```text -WarpProgramV1 -├── jurisdiction/profile -├── entry operation coordinate -├── input and output schemas -├── invocation-to-graph binding -├── typed graph schema -├── DPO rules +EchoOperationProgramV1 +├── invocation-to-graph binding checked against the package +├── typed graph and attachment schema identities +├── closed declarative DPO rewrite/evaluation rules │ ├── L │ ├── K │ ├── R -│ ├── positive conditions -│ └── negative conditions -├── bounded deterministic control law -├── match-selection law +│ ├── positive application conditions +│ └── negative application conditions +├── bounded deterministic control and match-selection laws ├── private working-state schema ├── attachment intrinsic profile -├── footprint derivation and ceiling -├── resource bounds -├── obstruction map -├── result projection -└── interpreter ABI/version -``` - -A bounded optic needs a corresponding read-only form: - -```text -WarpOpticV1 -├── explicit causal basis -├── focus/aperture -├── traversal plan -├── support-evidence law -├── resource bounds -├── result projection -├── completeness/continuation posture -└── observer/interpreter ABI +├── executable footprint derivation +├── static resource requirements or ceilings +├── typed result and obstruction construction checked against package schemas +└── evaluator ABI/version ``` -The same algebra may encode kernel programs, but authority must remain -distinct: - -```text -Application package - may install application WarpProgramV1 - -Observation package - may install bounded WarpOpticV1 - -Causal policy package - may select or compose approved causal laws - under a stricter Echo profile +An operation or schema coordinate carried inside program bytes is a consistency +claim, not a contract declaration. A program digest does not confer operation +identity, invocability, authority, or installation eligibility. Echo starts +installation and invocation lookup from an admitted operation-package identity +and follows its closed binding to the program. An application package does not +install itself, and Echo cannot install or invoke a naked program digest. -Echo kernel package - owns submit/admit/schedule/commit/fork/settlement law - and cannot be replaced by an application package -``` - -This is one algebra with multiple jurisdictions. +The broader optic and causal-policy ideas inventoried earlier are intentionally +non-normative here. `TextWindow`, capability execution, and causal-topology +migration are outside this vertical. ## 10. Receipt binding @@ -1089,10 +1083,10 @@ Current provider-native receipt evidence binds: Source: [echo/crates/warp-core/src/provider_contract.rs#L1181-L1262@6615d3a97731](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/warp-core/src/provider_contract.rs#L1181-L1262) -It does not bind: +Provider-v1 evidence does not bind: -- executable WARP program digest; -- WARP interpreter ABI/version; +- executable operation-program digest; +- evaluator ABI/version; - attachment intrinsic profile; - deterministic program control law; - executed rule/match trace or canonical patch identity. @@ -1100,24 +1094,43 @@ It does not bind: This is consistent with the present callback architecture because no admitted executable artifact exists to bind. -The future receipt should bind at least: +New executable-operation evidence must bind these common identities: ```text -semantic package root -WarpProgram digest -interpreter ABI/version +admitted public operation coordinate, package root, and package-admission evidence +Echo-owned installed-operation identity +exact submission/invocation and canonical input digest +caller-authority and Echo invocation-admission evidence +Jedit canonical text-schema declaration and lawpack digests +EchoOperationProgramV1 digest +evaluator ABI/version intrinsic profile digest -canonical input digest -explicit causal basis -selected operation -derived footprint/support digest -committed TickPatch digest -result or obstruction identity +EchoOperationEvaluationBasisV1 bytes and digest +delegated and consumed budgets +declared and actual footprint/support digests +private execution/trace identity +scheduler-rule and ordered composition-member identities ``` -A full rule trace may be optional if the canonical input, program, basis, -interpreter profile, and resulting patch suffice for deterministic replay. The -exact executed program digest is not optional. +It must then bind exactly one terminal variant: + +```text +Committed +├── committed composite TickPatch digest +├── typed result identity +└── resulting frontier identity + +NotCommitted +├── typed evaluation obstruction or commit-ineligibility identity +├── canonical outcome digest +└── canonical no-parent-patch evidence +``` + +`NotCommitted` never carries a committed patch digest. The exact executed +program digest is required but remains subordinate to the admitted operation +package. A full rule trace payload may be optional, but its retained identity is +not: recovery must be able to attribute the execution evidence without +rerunning ambient application code. ## 11. Additional constraints exposed by the source @@ -1125,26 +1138,26 @@ exact executed program digest is not optional. There are currently three coordinate representations: -- native Rust uses u64; -- GraphQL/Wesley narrows values through Int/i32; -- TypeScript exposes branded structures whose value is number. +- native Rust uses `u64`; +- GraphQL/Wesley narrows values through `Int`/`i32`; +- TypeScript exposes branded structures whose value is `number`. The GraphQL narrowing is explicit: [jedit/contracts/jedit/echo-text.graphql#L41-L60@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/contracts/jedit/echo-text.graphql#L41-L60) -The native host converts u64 to i32 and refuses larger values: +The native host converts `u64` to `i32` and refuses larger values: [jedit/native/jedit-echo-host/src/host.rs#L420-L427@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/host.rs#L420-L427) -The domain coordinate wrapper holds a TypeScript number: +The domain coordinate wrapper holds a TypeScript `number`: [jedit/src/domain/graph-rope-types.ts#L36-L59@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/domain/graph-rope-types.ts#L36-L59) Removing GraphQL Int is necessary but insufficient. The generated JavaScript -client also needs an exact representation, likely bigint or a canonical -fixed-width wrapper rather than an unrestricted number. +client also needs an exact representation, likely `bigint` or a canonical +fixed-width wrapper rather than an unrestricted `number`. -### 11.2 ReplaceRange's explicit basis is supplied by the host +### 11.2 `ReplaceRange`'s explicit basis is supplied by the host -The GraphQL operation carries basisHeadId, but the TypeScript host request does +The GraphQL operation carries `basisHeadId`, but the TypeScript host request does not: [jedit/src/ports/echo-text-contract-host.ts#L40-L45@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/src/ports/echo-text-contract-host.ts#L40-L45) @@ -1158,11 +1171,11 @@ operation meant. ### 11.3 Jim's native runtime is single-worldline -The native host creates one hard-coded worldline and one AcceptAll default +The native host creates one hard-coded worldline and one `AcceptAll` default writer: [jedit/native/jedit-echo-host/src/host.rs#L375-L409@c70e12d73b4b](https://github.com/flyingrobots/jedit/blob/c70e12d73b4b00bc92412bab67e1761f7dd22f82/native/jedit-echo-host/src/host.rs#L375-L409) -The ttd, strand, and braid vocabulary is disconnected both at the operation +The `ttd`, `strand`, and `braid` vocabulary is disconnected both at the operation layer and at the host-session model. A future Jim/Echo boundary must carry explicit worldline and causal coordinates. @@ -1176,17 +1189,20 @@ Its canonical operation vocabulary includes node, edge, attachment, and warp-instance changes: [echo/crates/warp-core/src/tick_patch.rs#L95-L165@6615d3a97731](https://github.com/flyingrobots/echo/blob/6615d3a97731a076fb4945bb6da083e82f55710d/crates/warp-core/src/tick_patch.rs#L95-L165) -The new interpreter does not need a second commit format. It needs to derive a -lawful TickPatch from an admitted WarpProgram. +The new evaluator does not need a second commit format. It needs to derive a +lawful `TickPatch` from an admitted package's subordinate +`EchoOperationProgramV1`. ## 12. Constitutional laws ### Executable Semantics Law -Every observable consequence admitted by Echo must be derivable solely from: +Every parent-visible consequence committed by Echo must be derivable solely +from: -- admitted Edict meaning; -- its independently verified executable WARP program; +- Jedit-owned application meaning preserved and lowered through an admitted + Edict operation package; +- that package's exact subordinate `EchoOperationProgramV1`; - Echo-owned runtime state; - versioned deterministic Echo intrinsics; - explicitly admitted capability results. @@ -1194,12 +1210,20 @@ Every observable consequence admitted by Echo must be derivable solely from: Ambient host code, callbacks, plugins, or handwritten application implementations must not determine semantic outcomes. +Evidence for this law must use ADR 0023's exact grades: deterministic +self-validation, structurally separate verification, or independently +implemented conformance evidence. A separate crate or call path does not, by +itself, establish implementation independence. + ### Application Meaning Law -Application code authors meaning. Echo executes admitted meaning. +Jedit owns application semantics. Edict preserves, canonicalizes, and lowers +that authored meaning. Echo admits packages and invocations, installs admitted +executable meaning, evaluates and schedules it, and commits parent-visible +consequences. A generated client may construct canonical input and submit it. It must not -know how to perform ReplaceRange. +know how to perform `ReplaceRange`. ### Capability Law @@ -1213,14 +1237,20 @@ The transformation algebra may be uniform. Authority is not. - Echo kernel rules own runtime judgment. - Echo causal rules own worldline and settlement topology. -- Edict-authored application rules own admitted application consequence. -- Edict-authored optics own bounded read plans. +- Jedit-owned, Edict-authored application rules define declarative application + meaning; they do not confer Echo admission or commitment authority. +- Edict preserves and lowers application meaning; it does not prove runtime + execution. +- Echo admits invocations and owns evaluation, scheduling, and commitment of + their consequences. +- Future Edict-authored optics may define bounded read plans, but optics are not + part of this campaign. - Capabilities own only their named effect crossing. ### Atomic Program Law A multi-rule WARP program may use private deterministic evaluation state, but a -successful application operation commits one atomic TickPatch. Intermediate +successful application operation commits one atomic `TickPatch`. Intermediate work states do not become accidental application history. ### Evidence Law @@ -1232,37 +1262,41 @@ identity, executable program identity, capability evidence, and committed consequence are distinct propositions and must be bound explicitly where required. -## 13. Recommended design campaign - -Before authoring the real Jedit ReplaceRange .edict operation, produce a focused -architecture document named Executable Semantics for Echo. - -Use five orthogonal witnesses: - -1. DeclareCheckpoint — one finite application graph write. -2. ReplaceRange — bounded transactional multi-rule persistent-rope - transformation. -3. TextWindow — bounded optic with exact support evidence. -4. File save — explicit capability crossing. -5. Fork/braid/settlement — proof that shared algebra does not collapse - jurisdiction. - -The design must freeze: - -- the authoritative Jim text fact schema; -- structural relationships versus scalar attachments; -- canonical invocation binding; -- explicit worldline and basis semantics; -- WarpProgramV1; -- bounded deterministic control and matching; -- private intermediate evaluation state; -- atomic tick-patch emission; -- the intrinsic profile; -- typed obstructions; -- optic execution; -- package and receipt binding; -- interpreter recovery semantics; -- kernel/application/capability jurisdiction. +## 13. Accepted bounded campaign + +ADR 0023 resolves the architecture question raised by this inventory. Campaign +1 implementation has not started. Work proceeds as four separately reviewed +and explicitly merged stages: + +1. add only the minimal Edict operation prerequisites: exact fixed-width + values, explicit basis, Jedit lawpack-resource binding through Core and + target identity, and generated operation-facing package/client artifacts; +2. add Echo's hook-free bounded-operation evaluator with one tiny generic + `EchoOperationProgramV1`, exact invocation admission, private evaluation, + budget and footprint enforcement, exact-basis commit, typed terminal + evidence, WAL, and recovery; +3. add the Jedit-owned canonical text-schema declaration, real `ReplaceRange` + lawpack resource and program, plus a finite independently implemented + differential oracle corpus whose limits are stated honestly; and +4. invoke the generated real operation from current Jim, prove the legacy + replacement route unreachable, and cut over `ReplaceRange` only. + +The first accepted witness is exactly: + +```text +real Jim command +→ explicit basis-bearing generated invocation +→ Echo-admitted Edict-authored operation +→ Echo-owned deterministic evaluation +→ one Echo-committed buffer consequence or typed no-patch outcome +→ execution evidence binding the admitted executable semantics +``` + +This campaign does not add checkpoint migration, `TextWindow`, save or other +capability execution, Cyber Kitten runtime machinery, observer routing, durable +child lanes or child-local ticks, wormholes, holograms, Continuum transport, or +fork/braid/settlement migration. Those remain useful inventory, not acceptance +witnesses for this vertical. ## Final assessment @@ -1275,7 +1309,8 @@ Fork, braid, and settlement belong to the same broad algebraic universe, but they already operate under Echo's causal-kernel jurisdiction. They must not become ordinary Jedit-authored application rules. -Only after the executable WARP program contract and authoritative Jim schema -are defined should the real Jedit ReplaceRange .edict operation be authored. -Otherwise, Edict would be asked to compile into a target that still has no -complete executable constitutional meaning. +Only after the admitted executable-operation contract and Jedit-owned canonical +text-schema declaration close exactly should the real Jedit +`ReplaceRange.edict` package become admissible. Otherwise, Edict would be asked +to compile into a target that still has no complete executable constitutional +meaning, or would canonize an unresolved Jedit schema fork.