Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
84 changes: 82 additions & 2 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -168,9 +168,87 @@ jobs:
- name: Run Echo release gate
run: npm run release-gate:jedit-echo

edict-replace-range:
name: edict / replace-range package chain
runs-on: ubuntu-latest
timeout-minutes: 20

steps:
- name: Checkout Jedit
uses: actions/checkout@v6.0.2
with:
ref: ${{ github.event.pull_request.head.sha || github.sha }}
path: jedit

- name: Verify literal submitted head
working-directory: jedit
env:
EXPECTED_JEDIT_HEAD: ${{ github.event.pull_request.head.sha || github.sha }}
run: test "$(git rev-parse HEAD)" = "$EXPECTED_JEDIT_HEAD"

- name: Read pinned toolchain commits
id: toolchain
working-directory: jedit
run: |
node --input-type=module <<'NODE' >> "$GITHUB_OUTPUT"
import { readFileSync } from "node:fs";
const lock = JSON.parse(
readFileSync("edict/replace-range/edict.toolchain-lock.json", "utf8"),
);
console.log(`edict_commit=${lock.edict.commit}`);
console.log(`echo_commit=${lock.echo.commit}`);
console.log(`rust_toolchain=${lock.rust.toolchain}`);
console.log(`node_version=${lock.validation.nodeVersion}`);
NODE

- name: Checkout pinned Edict
uses: actions/checkout@v6.0.2
with:
repository: flyingrobots/edict
ref: ${{ steps.toolchain.outputs.edict_commit }}
path: edict

- name: Checkout pinned Echo
uses: actions/checkout@v6.0.2
with:
repository: flyingrobots/echo
ref: ${{ steps.toolchain.outputs.echo_commit }}
path: echo

- name: Setup Node.js
uses: actions/setup-node@v6.4.0
with:
node-version: ${{ steps.toolchain.outputs.node_version }}
cache: 'npm'
cache-dependency-path: jedit/package-lock.json

- name: Setup pinned Rust
run: rustup toolchain install '${{ steps.toolchain.outputs.rust_toolchain }}' --profile minimal

- name: Install Jedit dependencies
working-directory: jedit
run: npm ci

- name: Verify exact package chain and adversarial regressions
working-directory: jedit
env:
EDICT_REPO: ${{ github.workspace }}/edict
ECHO_REPO: ${{ github.workspace }}/echo
run: node --test edict/replace-range/tests/proof-harness.spec.mjs

- name: Verify authoritative checkouts remain clean
run: |
for repository in jedit edict echo; do
if [[ -n "$(git -C "$repository" status --porcelain=v1 --untracked-files=all)" ]]; then
echo "$repository changed during the package-chain gate" >&2
git -C "$repository" status --short >&2
exit 1
fi
done

check:
name: check
needs: [ plan, build, test-shards, quality, release-gate ]
needs: [ plan, build, test-shards, quality, release-gate, edict-replace-range ]
if: always()
runs-on: ubuntu-latest

Expand All @@ -182,9 +260,10 @@ jobs:
TEST_SHARDS_RESULT: ${{ needs.test-shards.result }}
QUALITY_RESULT: ${{ needs.quality.result }}
RELEASE_GATE_RESULT: ${{ needs.release-gate.result }}
EDICT_REPLACE_RANGE_RESULT: ${{ needs.edict-replace-range.result }}
run: |
failed=0
for result in "$PLAN_RESULT" "$BUILD_RESULT" "$QUALITY_RESULT"; do
for result in "$PLAN_RESULT" "$BUILD_RESULT" "$QUALITY_RESULT" "$EDICT_REPLACE_RANGE_RESULT"; do
if [[ "$result" != "success" ]]; then
failed=1
fi
Expand All @@ -205,5 +284,6 @@ jobs:
echo "| test shards | $TEST_SHARDS_RESULT |"
echo "| quality | $QUALITY_RESULT |"
echo "| release gate | $RELEASE_GATE_RESULT |"
echo "| edict / replace-range package chain | $EDICT_REPLACE_RANGE_RESULT |"
} >> "$GITHUB_STEP_SUMMARY"
exit "$failed"
3 changes: 3 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,9 @@ title-recordings/
.wesley-cache/
.jedit-cache/
.jedit/
.build/
.vendor.edict-lawpack-build.lock
.jedit-text.edict-lawpack-build.lock
.obsidian/
.claude/
src/generated/jedit/structural-history-replace-text-range.wesley.generated.ts
10 changes: 10 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,16 @@

## Unreleased

- Added the Jedit-owned `ReplaceRange.edict` application root and canonical
`jedit.text@1` lawpack publication. With Edict #201, its executable integration
gate now proves that real source lowers into generic pure Target IR and reaches
Echo's checked lowerer through the exact generic pure target configuration.
Echo's generic pure-program lowerer now emits the exact compiler-produced
package, and its structurally separate verifier independently accepts the
package relation. The integration gate pins clean Edict and Echo revisions,
verifies the committed lawpack closure without repairing it, and rejects
authoritative-input mutation outside its disposable build root. Runtime
evaluation and rope mutation remain unimplemented.
- Made `ReplaceRange` corroborate the selected Head/root byte extent and exact
requested-range materialization before no-op classification, so truncated or
absent retained roots fail with a typed malformed-rope obstruction.
Expand Down
85 changes: 85 additions & 0 deletions edict/replace-range/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,85 @@
# ReplaceRange Edict application

This directory is the Jedit-owned application root for issue #296. It keeps
the authored, built, and evidentiary artifact classes separate:

- `edict.lawpack.json` is the reviewable `jedit.text@1` authoring input;
- `vendor/jedit-text/` is Edict's canonical published lawpack closure;
- `src/ReplaceRange.edict` is the application-owned source;
- `edict.toolchain-lock.json` pins the exact build implementations and
provider;
- `edict.build-lock.json` pins the exact source closure and emitted artifact
chain;
- `edict.executable-subject-lock.json` pins the verified executable meaning;
- `.build/` contains disposable provider and compiler outputs;
- `contracts/jedit/lawpacks/replace-range-v1/` remains the independent schema
and oracle corpus and is not executable input.

## Current executable boundary

The checked-in source is the first compiler-pressure slice, not a completed
text mutation. It binds exact-length nominal identities, the selected basis,
range, replacement bytes, operation profile, budget, imported helper
implementation, and a pure conditional into Edict Core. It intentionally does
not claim to traverse or rewrite a rope yet.

With Edict #201, the public application build lowers those Core `let` nodes into
generic, source-ordered Target IR and independently verifies the compiler-owned
result projection. Echo #724 now emits a distinct
`compiler-produced-bounded-pure/v1` executable package containing the exact
Core, lawpack exports, Target IR, and result projection. Echo's structurally
separate verifier independently reconstructs that package relation and emits an
accepted report bound to retained canonical `echo.executable-subject/v1` bytes.

That accepted package is the current routing evidence required by #296: Edict
preserves the bounded pure program without learning Jedit vocabulary, and Echo
packages it without learning `ReplaceRange`. No Echo evaluator runs, no graph
or rope is mutated, and no Tick is settled. This is not evidence that
`ReplaceRange` mutates a rope or that Jim runs end to end.

## Reproduce

The build script requires exact local Edict and Echo checkouts:

```bash
EDICT_REPO=/path/to/edict \
ECHO_REPO=/path/to/echo \
./edict/replace-range/tests/build.sh
```

`edict.toolchain-lock.json` pins the exact Edict commit and CLI release, Rust
toolchain, Echo commit, provider identity, provider manifest bytes, and lowerer
and verifier components. It also pins the Node and npm releases, the resolved
`cbor-x` package and integrity, and the package, lockfile, and CI invocation
bytes that perform validation. The script refuses non-Git roots, wrong commits,
dirty checkouts, or validation-environment drift before invoking either
toolchain. GitHub's package-chain job checks out and verifies the literal pull
request head; ordinary matrix jobs may separately exercise the synthetic merge.

`edict.build-lock.json` binds the exact source and validation closure to the
Core, Target IR, result projection, executable package, verification report,
and executable-subject identities. The raw Echo report remains a separately
identified artifact. A canonical-JSON Jedit evidence envelope binds that artifact
and subject to the exact provider release, verifier component, diagnostic ABI,
report ABI, and outcome; that verifier-specific envelope is the transitional
`VerificationReportId`. `edict.executable-subject-lock.json` separately records
the subject identity and the exact package, Target IR, and result-projection
references it contains. The harness recomputes every digest from emitted bytes
and refuses a valid report paired with a substituted package or verifier. The
locks contain no self-referential Jedit commit; an exact PR head remains an
external review coordinate.

The script verifies the committed `jedit.text@1` closure through Edict's public
lawpack `checkOnly` boundary. It never republishes or repairs that authoritative
tree. It then copies Echo's checked provider package into `.build/`, invokes
Edict's public application build, and requires the generic pure package and an
accepted independent-verifier report. Snapshots cover the application inputs
outside `.build/`, the pinned project validation files, and every tracked Edict
and Echo file; any content, identity, or timestamp mutation fails the run. Only
`.build/` is disposable output. Distinct nominal `BufferId` and `HeadId`
contracts retain the same exact 32-byte representation, while a negative
compiler witness proves that neither can cross the imported lawpack boundary as
the other.

The gate must advance again when Echo implements generic pure evaluation;
package acceptance is not a permanent substitute for runtime evidence.
20 changes: 20 additions & 0 deletions edict/replace-range/edict.application.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
{
"schema": "edict.application/v1",
"coordinate": "jedit.text.replace_range@1",
"sources": [
"src/ReplaceRange.edict"
],
"lawpacks": [
{
"manifest": "vendor/jedit-text/manifest.cbor",
"exports": "vendor/jedit-text/exports.cbor",
"adapter": "vendor/jedit-text/adapter.cbor",
"targetConfiguration": "vendor/jedit-text/echo-operation-configuration.cbor"
}
],
"target": {
"profile": "echo.dpo@1",
"providerPackage": ".build/echo-provider"
},
"outputDirectory": ".build/application"
}
128 changes: 128 additions & 0 deletions edict/replace-range/edict.build-lock.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,128 @@
{
"schema": "jedit.edict-build-lock/v1",
"applicationCoordinate": "jedit.text.replace_range@1",
"operationCoordinate": "jedit.text.replace_range@1.replaceRange",
"toolchainLockSha256": "3396bb91bea7e51d1e4b9f7385421d865d9e5a8f1c7ee1eaf330592143925fa0",
"sourceClosure": {
"schema": "jedit.edict-source-closure/v1",
"digest": "sha256:b6e247a612dd30b62db8b72d5063cbc29c762ffa91f8462fe57b1aadbdda521b",
"files": [
{
"path": "application/edict.application.json",
"sha256": "3182577627cd1f88bf590f3a8481ef53476c83d783aa142182e7c65eb1f72f8b"
},
{
"path": "application/edict.lawpack.json",
"sha256": "150abd5971b40ed70d2b1a1765a1a690e120ad9e44239dae732dc54e6ae04f99"
},
{
"path": "application/edict.toolchain-lock.json",
"sha256": "3396bb91bea7e51d1e4b9f7385421d865d9e5a8f1c7ee1eaf330592143925fa0"
},
{
"path": "application/src/ReplaceRange.edict",
"sha256": "51797e77062585a9f59083ee8a1da3faaf486ef7691e1b62203369a9d9356ee0"
},
{
"path": "application/tests/assert-build-output.mjs",
"sha256": "cc54e77a7a5923bb6496817b4822dfd38d5077501f6e12ab55129cf8cfcc86d9"
},
{
"path": "application/tests/build.sh",
"sha256": "b5827a1e2a4b64b214406ee3d0cdc9499059922f9878649946c0358fbbd6ea6d"
},
{
"path": "application/tests/package-chain.mjs",
"sha256": "28615de79aa645fa7c3a9cd098865e02af666fa86f49b251d5fe6c919329d141"
},
{
"path": "application/tests/proof-harness.spec.mjs",
"sha256": "a60012f744cff26095a451fe74f984b41a48551e8b47d6f2e5d8e128e1dcd643"
},
{
"path": "application/tests/verification-evidence.mjs",
"sha256": "3022f86f5c96d61f32ced3bec211d08ef7bbcdbc6e772cc61e2019eba0e42218"
},
{
"path": "application/vendor/jedit-text/edict.lawpack-output.json",
"sha256": "141c0000932ba19cff687e4173e40b0a38410f70bd511c9bc51f3fb3f73ee62b"
},
{
"path": "application/vendor/jedit-text/exports.cbor",
"sha256": "cab9c575da49cb33289e45fc45afb9d7f05558dada734be7eb3acfbbabb1d4db"
},
{
"path": "application/vendor/jedit-text/exports.sha256",
"sha256": "9bb11d9f8153c18af53b484526d9980b05c27eb20aa97e7623d1bf1ed5a69aea"
},
{
"path": "application/vendor/jedit-text/manifest.cbor",
"sha256": "0323ed8e9510e473d329166d421dc7d8e1da353065c1cd2dee77e6313ba9bf91"
},
{
"path": "application/vendor/jedit-text/manifest.sha256",
"sha256": "316cf602502a45cbab89b77b6344854edee750eaf1f0c8167da48d19ead75c22"
},
{
"path": "project/.github/workflows/ci.yml",
"sha256": "d4100140562e160bd897f9af9fc5d4ee8d7ea9285ba5d0734c620a38cf2d2ea5"
},
{
"path": "project/package.json",
"sha256": "735a70d8e48f118695529446780d547f8f200dcb0fa453099aa2241d820d9eb5"
},
{
"path": "project/package-lock.json",
"sha256": "d39f4b39e262e55355315e0a38ad2d10953ae5f6cd48b9fe3a530a128afd01d2"
}
]
},
"lawpackRelease": {
"coordinate": "jedit.text@1",
"digest": "sha256:95758c1605894672cc9069fde01bb8b6e11842b053102660c9cd4f4d6f34d64e"
},
"provider": {
"coordinate": "echo.edict-provider@1",
"digest": "sha256:b065242a81179df02cd450763c8266e866bbca959308f5198b791a919050e0c2"
},
"artifacts": {
"core": {
"coordinate": "jedit.text.replace_range@1",
"domain": "edict.core.module/v1",
"digest": "sha256:d965643ff78c4f321af538f086329fee53c22b21dc1de9e5f9914d6cb69e609f"
},
"targetIr": {
"coordinate": "echo.span-ir/v1",
"domain": "edict.target-ir.artifact/v1",
"digest": "sha256:8a5243fef0aea029df1b6a56eb65f199703e10143d5e0cec5b73603455284229"
},
"resultProjection": {
"coordinate": "jedit.text.replace_range@1.replaceRange",
"domain": "edict.result-projection.artifact/v1",
"digest": "sha256:f804baa01c357e5ed54e86f752ea7f8201e454ad0b47c10813fde8c7dc2aeba6"
},
"executablePackage": {
"coordinate": "executable-operation-package.echo",
"domain": "echo.operation-package/v1",
"digest": "sha256:9a9e26e10dabf9175889fb2ef50bd463dd08ea95e9a377e0a39eb4663acd409b",
"rawSha256": "f339cf8e52621df4a9b644c83770932df5c01c52e70d1bd271c0e6519cda2998"
},
"verificationReportArtifact": {
"coordinate": "verifier-report.echo-operation",
"domain": "echo.operation-package-verifier-report/v1",
"digest": "sha256:c8f1e52216f248022a884c822d577c479b3a68b0f5ad69f21db3288a00e474a1",
"rawSha256": "124cfca3449d19684a169a4fe62898dfb76124854d0f0ef57ea3ed9f606a4ce0"
},
"verificationReport": {
"coordinate": "jedit.edict-verification-evidence/v1",
"domain": "jedit.edict-verification-evidence/v1",
"digest": "sha256:54f4bc09addabf3236478c891aa8ced4f13a2738e007f95c96f547b6b36dcd80",
"rawSha256": "6a6420061353e34a8a8db21025b9eeed7a0802c720b4e865e8f6218448f5be4e"
},
"executableSubject": {
"coordinate": "echo.executable-subject/v1",
"domain": "echo.executable-subject/v1",
"digest": "sha256:9738fc187d8507b64bc7c01a536c8eb2b99fb550380db878d49ebb7e130267aa"
}
}
}
20 changes: 20 additions & 0 deletions edict/replace-range/edict.executable-subject-lock.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
{
"schema": "jedit.edict-executable-subject-lock/v1",
"reference": {
"coordinate": "echo.executable-subject/v1",
"digest": "sha256:9738fc187d8507b64bc7c01a536c8eb2b99fb550380db878d49ebb7e130267aa"
},
"rawSha256": "46255257cc23601a10f2dd1fd5d7bc86fc4bb13612eb2b3ac5f633ded159aa88",
"package": {
"coordinate": "executable-operation-package.echo",
"digest": "sha256:9a9e26e10dabf9175889fb2ef50bd463dd08ea95e9a377e0a39eb4663acd409b"
},
"targetIr": {
"coordinate": "echo.span-ir/v1",
"digest": "sha256:8a5243fef0aea029df1b6a56eb65f199703e10143d5e0cec5b73603455284229"
},
"resultProjection": {
"coordinate": "jedit.text.replace_range@1.replaceRange",
"digest": "sha256:f804baa01c357e5ed54e86f752ea7f8201e454ad0b47c10813fde8c7dc2aeba6"
}
}
Loading