diff --git a/docs/adr/0015-registry-provider-host-boundary.md b/docs/adr/0015-registry-provider-host-boundary.md index b4869136..94e038f2 100644 --- a/docs/adr/0015-registry-provider-host-boundary.md +++ b/docs/adr/0015-registry-provider-host-boundary.md @@ -3,7 +3,9 @@ # ADR 0015: Registry, Provider, and Host Boundary -- **Status:** Accepted +- **Status:** Partially superseded +- **Superseded in part by:** + [ADR 0023](0023-admitted-executable-operation-packages.md) - **Date:** 2026-07-13 ## Context @@ -31,6 +33,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..cffb21fa --- /dev/null +++ b/docs/adr/0023-admitted-executable-operation-packages.md @@ -0,0 +1,485 @@ + + + +# 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 names for +the first version: + +- `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. + +### 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 `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 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; +- 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 invocation-to-graph binding; +- 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; +- 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. + +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. + +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 delegated budget and consumed budget; +- the declared footprint identity; +- the actual read/write footprint derived during evaluation; +- 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 any `Committable` outcome can commit, Echo must establish all of the +following: + +```text +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 +``` + +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. 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. + +`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. 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 +``` + +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 +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 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 + +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. 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. | +| 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. 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 +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. + +## Rejected Alternatives + +- 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. +- 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. +- 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. +- 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. +- 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) +- [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/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..e8220722 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,19 @@ 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. +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 Echo also owns the runtime-specific semantics supplied to Edict's generic 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..8ce16b5e --- /dev/null +++ b/docs/plans/2026-07-18-jim-edict-echo-executable-warp-semantics.md @@ -0,0 +1,1316 @@ + + + +# Jim × Edict × Echo: Executable WARP Semantics Inventory + +- **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 `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. + +## 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. 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` + +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) + +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 + +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 +EchoOperationProgramV1: ReplaceRange executable meaning +│ +├─ 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 prepare one TickPatch or one obstruction +``` + +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 accepted first-version executable object + +[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. + +The admitted package owns the public contract: + +```text +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 +``` + +The bound program supplies only executable meaning: + +```text +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 application conditions +│ └── negative application conditions +├── bounded deterministic control and match-selection laws +├── private working-state schema +├── attachment intrinsic profile +├── executable footprint derivation +├── static resource requirements or ceilings +├── typed result and obstruction construction checked against package schemas +└── evaluator ABI/version +``` + +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. + +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 + +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) + +Provider-v1 evidence does not bind: + +- executable operation-program digest; +- evaluator 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. + +New executable-operation evidence must bind these common identities: + +```text +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 +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 +``` + +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 + +### 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 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 parent-visible consequence committed by Echo must be derivable solely +from: + +- 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. + +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 + +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`. + +### 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. +- 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 +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. 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 + +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 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. 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. 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"