Author ReplaceRange as Jedit-owned Edict source

[flyingrobots]

Goal

Author and prove ReplaceRange.edict as the first Jedit-owned text operation,
compiled by Edict and ultimately realized by Echo without moving rope semantics
into Echo or TypeScript.

Tracks #296.

Plan

• Publish the canonical jedit.text@1 lawpack closure through Edict's public authoring boundary.
• Check in the first real ReplaceRange.edict source and application manifest.
• Lower the source through Edict and emit an independently verified generic Echo package.
• Pin clean Edict/Echo toolchains and make lawpack reproduction non-mutating.
• Preserve distinct nominal 32-byte BufferId and HeadId contracts.
• Bind raw verifier output to a verifier-specific transitional evidence identity.
• Pin the complete Core → Target IR → projection → package → report → subject chain.
• Pin the Node/npm/CBOR validation environment and literal PR-head CI checkout.
• Make the calibrated substitution and drift attacks permanent regressions.
• Refresh against merged Edict main and prove repeated public-build byte identity.
• Obtain a fresh independent exact-head operational audit.
• Implement Echo's generic pure runtime evaluator and the application-owned rope algorithm.
• Execute through Echo and prove agreement with the independent Jedit oracle.

Current status

The repaired package-proof candidate is published at:

• Jedit: a894c7c4c6d150c0fb210d2e0ca4c27bf518b4c7
• Edict: 3f81f759e921a69b04fe8cf8e62e62f8f3dc7b7e
• Echo: 49e9efb68001dfd78563d18bac9359a87671e431

jedit.text@1 now exports deliberate nominal BufferId and HeadId
contracts over one exact 32-byte representation. Edict preserves their contract
coordinates in Core and refuses cross-assignment across the imported lawpack
boundary. Echo's lowerer and verifier consume the generic nominal Core form
without acquiring any Jedit vocabulary.

The raw Echo verifier report remains a separately identified artifact. Jedit's
canonical-JSON evidence envelope binds that report and its exact executable
subject to the provider release, verifier component, verifier contract, target
profile, report ABI, diagnostic ABI, and outcome. Changing only the verifier
identity changes the transitional VerificationReportId.

The toolchain and build locks pin exact Rust, Node, npm, Edict, Echo, provider,
cbor-x, package, lockfile, workflow, source, lawpack, Core, Target IR,
projection, executable-package, report-artifact, verifier-evidence, and
executable-subject identities. Validation uses Edict's non-mutating
checkOnly publication boundary and snapshots authoritative inputs before and
after the build.

Permanent local witnesses are green:

• rejects_non_git_toolchain_inputs
• rejects_wrong_commit_toolchain_inputs
• lawpack_check_only_rejects_drift_without_repairing_it
• rejects_package_whose_recomputed_identity_differs_from_report_subject
• preserves_nominal_exact_length_buffer_and_head_identities
• repeated_public_builds_preserve_core_and_package_bytes
• rejects_buffer_id_head_id_substitution
• verification_report_identity_is_verifier_specific
• rejects_drifted_build_and_executable_subject_locks
• rejects_drifted_executable_subject_lock
• required_ci_executes_the_exact_package_chain

The dedicated package-chain job now checks out and asserts the literal pull
request head. Ordinary matrix jobs remain separate integration evidence.
Hosted CI run 34168569421 is green for exact head a894c7c4c6d150c0fb210d2e0ca4c27bf518b4c7, including the literal-head package-chain job.

This remains a Draft and is not a completed text mutation. No Echo evaluator
runs, no graph or rope is mutated, and no Tick is settled. The source does not
invoke the native Jedit planner, construct a caller-authored patch, or treat the
schema/oracle as executable input. Echo remains free of Jim, Jedit, rope,
buffer, range, and editor semantics.

Compiler pin refresh evidence

Edict is now pinned to merged main 3f81f759e921a69b04fe8cf8e62e62f8f3dc7b7e; Echo remains the exact open #724 candidate 49e9efb68001dfd78563d18bac9359a87671e431.

The original harness refused that compiler as an exact-commit mismatch. After the deliberate pin refresh and real artifact rebuild, its nominal witness failed because it looked for obsolete synthetic per-field type entries. The corrected witness follows each actual record field to the named BufferId/HeadId contract and then to the shared exact 32-byte representation. Cross-assignment rejection remains covered.

The newly emitted Core, Target, package, report, and subject identities were recomputed from accepted output bytes. The lawpack release and result projection identities stayed unchanged. The new repeated-build test compares embedded Core/Target/projection and emitted package/report bytes after two public builds from the same authored closure. It exercises already landed behavior and required no compiler or provider implementation change.

Validation at this head:

• RED: PATH=/Users/james/.local/share/mise/installs/node/22.23.1/bin:$PATH EDICT_REPO=/path/to/edict-main ECHO_REPO=/path/to/pinned-echo node --test edict/replace-range/tests/proof-harness.spec.mjs produced 9 passes / 1 failure in the old nominal witness after the compiler pin refresh.
• GREEN: the same command with the updated witness and repeated-build case passed all 11 tests.
• npm run check: 782 Node tests passed, 12 intentional skips, all native Rust suites passed, quality gate reported no regressions.
• git diff --check and git verify-commit HEAD passed.

No rope algorithm, evaluator, production runtime, oracle, authored source, or lawpack was changed in this refresh. The PR remains a draft under its existing full-operation scope.

[coderabbitai]

Important

Draft PR not reviewed

Draft PRs are not automatically reviewed by default.

• Trigger a manual review

To automatically review draft PRs, update your CodeRabbit configuration:

reviews:
  auto_review:
    drafts: true

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}

[flyingrobots]

@codex review please, focus on the three unmet plan items and whether they are reachable at these exact heads.

Requesting the fresh independent exact-head operational audit that is item 11 of this PR's plan. Please state the exact commits you audited rather than accepting the ones quoted below.

Heads as I read them right now

repo	commit
jedit (PR head)	a894c7c4c6d150c0fb210d2e0ca4c27bf518b4c7
edict (PR body pin)	3f81f759e921a69b04fe8cf8e62e62f8f3dc7b7e
echo (PR body pin)	49e9efb68001dfd78563d18bac9359a87671e431
edict (my local main)	e4fa81dd772a88fa50b5272da627716e7ea56214
echo (my local main)	490134c0753a3df6a74da366cc71c1248764dc5a

The pins in the PR body are behind both upstreams, so part of what I need is whether the closure still reproduces byte-identically at current heads or only at the pinned ones.

Findings I want checked, not trusted. These are my reads from source this session and I would rather you contradict them than confirm them politely:

1. No loop-carried result in Edict. crates/edict-syntax/src/compiler.rs builds every bounded for with result: CoreExpr::Const(CoreValue::Null) (~line 1815), and return is rejected inside a bounded-for body (~line 1798). If that is right, a rope traversal that accumulates cannot be expressed in Edict source today, which blocks the "application-owned rope algorithm" half of item 12 on an Edict language change rather than on authoring effort.

2. No generic pure evaluator in Echo. crates/warp-core/src/edict_target_ir.rs::execute_accepted_edict_echo_target_ir evaluates no program: it checks a single BasisFresh predicate and returns a receipt, never touching the intent body. If that is right, item 12's evaluator half is a new warp-core component, not a wiring task, and item 13 cannot start until it exists.

3. The current source is a boundary record, not an algorithm. edict/replace-range/src/ReplaceRange.edict is 41 lines: one maxCreatedLeafCount() call, one rangeIsEmpty conditional, one returned record. No traversal.

What would help most

• Confirm or refute 1 and 2 with file and line, at the heads you actually audited.
• If 1 is right: the smallest Edict language capability that unblocks the algorithm — general loop-carried result, or something narrower that still expresses replace-range.
• Whether the maintainer position that Echo must not learn ropes is satisfiable with a generic evaluator, or whether it forces a different split.
• Anything in items 1-10 that has silently regressed since they were ticked.

Not asking you to implement anything. James has asked me to finish this PR and I want an independent read on what finishing actually requires before I touch three repos.

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-09-08T06:02:22.133141Z	a894c7c	Manual request

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

[chatgpt-codex-connector]

Codex Review: Didn't find any major issues. Breezy!

Reviewed commit: a894c7c4c6

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".