diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b8fc974..d90ea2c 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -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 @@ -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 @@ -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" diff --git a/.gitignore b/.gitignore index 733790b..ff1f05b 100644 --- a/.gitignore +++ b/.gitignore @@ -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 diff --git a/CHANGELOG.md b/CHANGELOG.md index e968747..c36e201 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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. diff --git a/edict/replace-range/README.md b/edict/replace-range/README.md new file mode 100644 index 0000000..da488a0 --- /dev/null +++ b/edict/replace-range/README.md @@ -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. diff --git a/edict/replace-range/edict.application.json b/edict/replace-range/edict.application.json new file mode 100644 index 0000000..f3e59f8 --- /dev/null +++ b/edict/replace-range/edict.application.json @@ -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" +} diff --git a/edict/replace-range/edict.build-lock.json b/edict/replace-range/edict.build-lock.json new file mode 100644 index 0000000..63a1834 --- /dev/null +++ b/edict/replace-range/edict.build-lock.json @@ -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" + } + } +} diff --git a/edict/replace-range/edict.executable-subject-lock.json b/edict/replace-range/edict.executable-subject-lock.json new file mode 100644 index 0000000..d0605bb --- /dev/null +++ b/edict/replace-range/edict.executable-subject-lock.json @@ -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" + } +} diff --git a/edict/replace-range/edict.lawpack.json b/edict/replace-range/edict.lawpack.json new file mode 100644 index 0000000..2652d16 --- /dev/null +++ b/edict/replace-range/edict.lawpack.json @@ -0,0 +1,214 @@ +{ + "schema": "edict.lawpack-build/v1", + "outputDirectory": "vendor/jedit-text", + "lawpack": { + "schema": "edict.lawpack-authoring/v1", + "id": "jedit.text", + "version": "1", + "acceptedCoreAbi": [ + "edict.core/v1" + ], + "dependencies": [], + "exportsCoordinate": "jedit.text.exports/v1", + "exports": { + "types": [ + { + "coordinate": "jedit.text@1.NodeId", + "definition": "Bytes" + }, + { + "coordinate": "jedit.text@1.BufferId", + "definition": "Nominal" + }, + { + "coordinate": "jedit.text@1.HeadId", + "definition": "Nominal" + }, + { + "coordinate": "jedit.text@1.ReplacementBytes", + "definition": "Bytes" + }, + { + "coordinate": "jedit.text@1.ObstructionDetail", + "definition": "String" + } + ], + "constants": [ + { + "coordinate": "jedit.text@1.maxCreatedLeaves", + "type": "U64", + "value": 4096 + }, + { + "coordinate": "jedit.text@1.maxCreatedBranches", + "type": "U64", + "value": 4096 + } + ], + "pureFunctions": [ + { + "source": "edict", + "coordinate": "jedit.text@1.maxCreatedLeafCount", + "typeParameters": [], + "parameterTypes": [], + "returnType": "U64", + "costTemplate": "jedit.text@1.replaceRangeBudget", + "determinismClass": "total", + "body": { + "params": [], + "body": { + "locals": [], + "bindings": [], + "result": { + "kind": "const", + "value": { + "kind": "int", + "width": "U64", + "value": 4096 + } + } + } + } + } + ], + "effects": [], + "obstructions": [ + { + "coordinate": "jedit.text@1.RangeOrderInvalid", + "authorityClass": "domainMappable", + "payloadSchema": "jedit.text@1.ObstructionDetail" + }, + { + "coordinate": "jedit.text@1.RangeOutOfBounds", + "authorityClass": "domainMappable", + "payloadSchema": "jedit.text@1.ObstructionDetail" + }, + { + "coordinate": "jedit.text@1.Utf8BoundaryInvalid", + "authorityClass": "domainMappable", + "payloadSchema": "jedit.text@1.ObstructionDetail" + }, + { + "coordinate": "jedit.text@1.NoOp", + "authorityClass": "domainMappable", + "payloadSchema": "jedit.text@1.ObstructionDetail" + }, + { + "coordinate": "jedit.text@1.BasisNotCanonical", + "authorityClass": "domainMappable", + "payloadSchema": "jedit.text@1.ObstructionDetail" + }, + { + "coordinate": "jedit.text@1.ArithmeticOverflow", + "authorityClass": "integrityFault", + "payloadSchema": "jedit.text@1.ObstructionDetail" + }, + { + "coordinate": "jedit.text@1.FactMissing", + "authorityClass": "resourceFault", + "payloadSchema": "jedit.text@1.ObstructionDetail" + }, + { + "coordinate": "jedit.text@1.FactMalformed", + "authorityClass": "integrityFault", + "payloadSchema": "jedit.text@1.ObstructionDetail" + }, + { + "coordinate": "jedit.text@1.ContentIdentityMismatch", + "authorityClass": "integrityFault", + "payloadSchema": "jedit.text@1.ObstructionDetail" + }, + { + "coordinate": "jedit.text@1.MalformedRope", + "authorityClass": "integrityFault", + "payloadSchema": "jedit.text@1.ObstructionDetail" + } + ], + "operationProfiles": { + "jedit.text@1.replaceRange": { + "opticTemplate": { + "opticKind": "affectReintegration", + "boundaryKind": "affect", + "supportPolicy": "jedit.text@1.basisBoundSupport", + "lossDisposition": "jedit.text@1.lossless", + "basisTemplate": "jedit.text@1.exactHeadBasis", + "apertureRequirement": { + "kind": "abstractFootprintObligation", + "reference": "jedit.text@1.replaceRangeFootprint" + } + }, + "effectPredicate": "jedit.text@1.replaceRangeEffects" + } + } + }, + "targetAdapters": [ + { + "coordinate": "jedit.text.echo-adapter/v1", + "output": "adapter.cbor", + "acceptedTargetProfile": { + "id": "echo.dpo@1", + "digest": "sha256:2e2494121aecf5e6a2d920f5fb85408825d394765fad41484c416397c920fb04" + }, + "acceptedTargetIr": { + "id": "echo.span-ir/v1", + "digest": "sha256:0057167e68f50c99dcce087b3e1cd677d17c5d1dc238bdb52d89469e1472fc2f" + }, + "operationProfiles": { + "jedit.text@1.replaceRange": { + "core": "continuum.profile.read-write/v1", + "semanticEffects": [], + "budgetObligation": "jedit.text@1.replaceRangeBudget", + "targetConfiguration": { + "local": "echo-config" + } + } + }, + "effectImplementations": {}, + "budgets": { + "jedit.text@1.replaceRangeBudget": { + "maxSteps": 1048576, + "maxAllocatedBytes": 16777216, + "maxOutputBytes": 8388608 + } + } + } + ], + "verifier": { + "class": "declarative", + "ruleset": { + "local": "verifier-rules" + } + }, + "compatibility": { + "id": "jedit.text.compatibility/v1", + "digest": "sha256:2adf83f798205f52636ad64ca45178f33a8e1cc663874f8a6113484c945e3052" + }, + "conformanceFixtureCorpus": { + "id": "jedit.text.ReplaceRange.oracle@1", + "digest": "sha256:b9b4707dd5e07897cbe7af36d88928401887e6af5d167d1a88a8d6181b4dbb0e" + }, + "localResources": [ + { + "name": "echo-config", + "coordinate": "echo.operation-lowering-configuration/v1", + "output": "echo-operation-configuration.cbor", + "value": { + "apiVersion": "echo.operation-lowering-configuration/v1", + "programKind": "compiler-produced-bounded-pure/v1" + } + }, + { + "name": "verifier-rules", + "coordinate": "jedit.text.verifier-rules/v1", + "output": "verifier-rules.cbor", + "value": { + "schema": "jedit.text.schema@1", + "schemaDigest": "sha256:f49b0ff6c9c7010d3a72b46734d47832853f496739a083edc41dddec3431bac7", + "oracleIsExecutableInput": false, + "runtimeOntology": "generic-bounded-graph" + } + } + ] + }, + "dependencyBundles": [] +} diff --git a/edict/replace-range/edict.toolchain-lock.json b/edict/replace-range/edict.toolchain-lock.json new file mode 100644 index 0000000..110a908 --- /dev/null +++ b/edict/replace-range/edict.toolchain-lock.json @@ -0,0 +1,59 @@ +{ + "schema": "jedit.edict-toolchain-lock/v1", + "rust": { + "toolchain": "1.94.0", + "rustcVersion": "rustc 1.94.0 (4a4ef493e 2026-03-02)", + "cargoVersion": "cargo 1.94.0 (85eff7c80 2026-01-15)" + }, + "validation": { + "nodeVersion": "22.23.1", + "processVersion": "v22.23.1", + "npmVersion": "10.9.8", + "cborX": { + "version": "1.6.4", + "integrity": "sha512-UGKHjp6RHC6QuZ2yy5LCKm7MojM4716DwoSaqwQpaH4DvZvbBTGcoDNTiG9Y2lByXZYFEs9WRkS5tLl96IrF1Q==" + }, + "files": [ + { + "path": "package.json", + "sha256": "735a70d8e48f118695529446780d547f8f200dcb0fa453099aa2241d820d9eb5" + }, + { + "path": "package-lock.json", + "sha256": "d39f4b39e262e55355315e0a38ad2d10953ae5f6cd48b9fe3a530a128afd01d2" + }, + { + "path": ".github/workflows/ci.yml", + "sha256": "d4100140562e160bd897f9af9fc5d4ee8d7ea9285ba5d0734c620a38cf2d2ea5" + } + ] + }, + "edict": { + "commit": "39a796de04b3400f569880da06878da50d8ed0ee", + "cliVersion": "0.11.0-alpha.1" + }, + "echo": { + "commit": "49e9efb68001dfd78563d18bac9359a87671e431", + "provider": { + "coordinate": "echo.edict-provider@1", + "digest": "sha256:b065242a81179df02cd450763c8266e866bbca959308f5198b791a919050e0c2", + "manifestSha256": "c5b9fb2fe3a0dc4dad282621a97413225c555be0071f3502b3272952069d42dc", + "targetProfile": { + "coordinate": "echo.dpo@1", + "digest": "sha256:2e2494121aecf5e6a2d920f5fb85408825d394765fad41484c416397c920fb04" + }, + "lowerer": { + "coordinate": "echo.dpo.lowerer/component@1", + "sha256": "e842063bd8d8ec12fff5b392a9d6bc646e2e3025c7a0c93726f53eed3cb5a0bf" + }, + "verifier": { + "coordinate": "echo.dpo.verifier/component@1", + "sha256": "174cf8758815bf2b9f2ef575517aa6d144ed3f2d1995fc65d25a211b9dea82d9", + "contract": { + "coordinate": "echo.dpo.verifier/v1", + "digest": "sha256:ca96b190728de3d668072ec1bd37d24e5197e7bd9bd54f70966d8c566b9b67f2" + } + } + } + } +} diff --git a/edict/replace-range/src/ReplaceRange.edict b/edict/replace-range/src/ReplaceRange.edict new file mode 100644 index 0000000..6079dbe --- /dev/null +++ b/edict/replace-range/src/ReplaceRange.edict @@ -0,0 +1,41 @@ +package jedit.text.replace_range@1; + +use lawpack jedit.text@1 digest "sha256:95758c1605894672cc9069fde01bb8b6e11842b053102660c9cd4f4d6f34d64e" as text; + +type ReplaceRangeInput = { + bufferId: text.BufferId, + basisHeadId: text.HeadId, + startByte: U64, + endByte: U64, + replacement: text.ReplacementBytes, +}; + +type ReplaceRangeBoundary = { + bufferId: text.BufferId, + basisHeadId: text.HeadId, + startByte: U64, + endByte: U64, + replacement: text.ReplacementBytes, + rangeIsEmpty: U32, + createdLeafCeiling: U64, +}; + +intent replaceRange(input: ReplaceRangeInput) returns ReplaceRangeBoundary + profile text.replaceRange + basis input.basisHeadId + budget <= text.replaceRangeBudget + where input.startByte <= input.endByte +{ + let createdLeafCeiling: U64 = text.maxCreatedLeafCount(); + let rangeIsEmpty = if input.startByte == input.endByte then 1u32 else 0u32; + + return { + bufferId: input.bufferId, + basisHeadId: input.basisHeadId, + startByte: input.startByte, + endByte: input.endByte, + replacement: input.replacement, + rangeIsEmpty, + createdLeafCeiling, + }; +} diff --git a/edict/replace-range/tests/assert-build-output.mjs b/edict/replace-range/tests/assert-build-output.mjs new file mode 100644 index 0000000..fc0d14a --- /dev/null +++ b/edict/replace-range/tests/assert-build-output.mjs @@ -0,0 +1,316 @@ +// SPDX-License-Identifier: Apache-2.0 OR LicenseRef-MIND-UCAL-1.0 +// © James Ross Ω FLYING•ROBOTS + +import assert from "node:assert/strict"; +import { createHash } from "node:crypto"; +import { readFile, writeFile } from "node:fs/promises"; +import path from "node:path"; + +import { decode } from "cbor-x"; + +import { + canonicalArtifactDigest, + digestText, + verificationEvidence, +} from "./verification-evidence.mjs"; + +function assertResourceReference(reference, coordinate, digest) { + assert.equal(reference.id, coordinate); + assert.deepEqual(reference.digest, ["sha256", digest]); +} + +const SOURCE_CLOSURE_INPUTS = [ + ["application/edict.application.json", "edict.application.json"], + ["application/edict.lawpack.json", "edict.lawpack.json"], + ["application/edict.toolchain-lock.json", "edict.toolchain-lock.json"], + ["application/src/ReplaceRange.edict", "src/ReplaceRange.edict"], + ["application/tests/assert-build-output.mjs", "tests/assert-build-output.mjs"], + ["application/tests/build.sh", "tests/build.sh"], + ["application/tests/package-chain.mjs", "tests/package-chain.mjs"], + ["application/tests/proof-harness.spec.mjs", "tests/proof-harness.spec.mjs"], + [ + "application/tests/verification-evidence.mjs", + "tests/verification-evidence.mjs", + ], + [ + "application/vendor/jedit-text/edict.lawpack-output.json", + "vendor/jedit-text/edict.lawpack-output.json", + ], + ["application/vendor/jedit-text/exports.cbor", "vendor/jedit-text/exports.cbor"], + [ + "application/vendor/jedit-text/exports.sha256", + "vendor/jedit-text/exports.sha256", + ], + ["application/vendor/jedit-text/manifest.cbor", "vendor/jedit-text/manifest.cbor"], + [ + "application/vendor/jedit-text/manifest.sha256", + "vendor/jedit-text/manifest.sha256", + ], + ["project/.github/workflows/ci.yml", "../../.github/workflows/ci.yml"], + ["project/package.json", "../../package.json"], + ["project/package-lock.json", "../../package-lock.json"], +]; + +function sha256(bytes) { + return createHash("sha256").update(bytes).digest(); +} + +function lengthPrefix(length) { + const prefix = Buffer.alloc(8); + prefix.writeBigUInt64LE(BigInt(length)); + return prefix; +} + +async function sourceClosure(applicationRoot) { + const hasher = createHash("sha256"); + hasher.update("jedit.edict-source-closure/v1\0"); + const files = []; + for (const [identityPath, relative] of SOURCE_CLOSURE_INPUTS) { + const bytes = await readFile(path.join(applicationRoot, relative)); + const relativeBytes = Buffer.from(identityPath, "utf8"); + hasher.update(lengthPrefix(relativeBytes.length)); + hasher.update(relativeBytes); + hasher.update(lengthPrefix(bytes.length)); + hasher.update(bytes); + files.push({ path: identityPath, sha256: sha256(bytes).toString("hex") }); + } + return { + schema: "jedit.edict-source-closure/v1", + digest: `sha256:${hasher.digest("hex")}`, + files, + }; +} + +const [outputDirectory, mode] = process.argv.slice(2); +assert.ok(outputDirectory, "pass the Edict application output directory"); +assert.ok( + mode === undefined || mode === "--write-locks", + "the only supported mode is --write-locks", +); +const applicationRoot = path.resolve(outputDirectory, "../.."); + +const packageBytes = await readFile( + path.join(outputDirectory, "executable-operation-package.cbor"), +); +const reportBytes = await readFile( + path.join(outputDirectory, "verification-report.cbor"), +); +const executablePackage = decode(packageBytes); +const report = decode(reportBytes); +const program = decode(executablePackage.program); + +const packageDigest = canonicalArtifactDigest( + "echo.operation-package/v1", + packageBytes, +); +assertResourceReference( + report.package, + "executable-operation-package.echo", + packageDigest, +); + +assert.equal(executablePackage.schema, "echo.operation-package/v1"); +assert.equal( + executablePackage.package_kind, + "compiler-produced-bounded-pure/v1", +); +assert.equal( + executablePackage.operation_coordinate, + "jedit.text.replace_range@1.replaceRange", +); +assert.equal(program.schema, "echo.compiler-produced-pure-program/v1"); +assert.equal(program.kind, "compiler-produced-bounded-pure/v1"); +assert.equal(program.intent, "replaceRange"); +for (const artifact of [ + "core_artifact", + "lawpack_exports_artifact", + "result_projection_artifact", + "target_ir_artifact", +]) { + assert.ok(Buffer.isBuffer(program[artifact]), `${artifact} must be retained`); + assert.ok(program[artifact].length > 0, `${artifact} must not be empty`); +} + +const coreDigest = canonicalArtifactDigest( + "edict.core.module/v1", + program.core_artifact, +); +const coreArtifact = decode(program.core_artifact); +assert.deepEqual(executablePackage.semantic_closure.core_identity, coreDigest); +assert.deepEqual( + executablePackage.semantic_closure.canonical_meaning_identity, + coreDigest, +); + +const targetIrDigest = canonicalArtifactDigest( + "edict.target-ir.artifact/v1", + program.target_ir_artifact, +); +assert.deepEqual( + executablePackage.semantic_closure.target_ir_identity, + targetIrDigest, +); +assertResourceReference(report.targetIr, "echo.span-ir/v1", targetIrDigest); + +const resultProjectionDigest = canonicalArtifactDigest( + "edict.result-projection.artifact/v1", + program.result_projection_artifact, +); + +assert.equal( + report.apiVersion, + "echo.operation-package-verifier-report/v1", +); +assert.equal(report.outcome, "accepted"); +assert.equal(report.diagnosticBytes.length, 0); +assert.equal( + report.applicationResultProjection.id, + "jedit.text.replace_range@1.replaceRange", +); +assertResourceReference( + report.applicationResultProjection, + "jedit.text.replace_range@1.replaceRange", + resultProjectionDigest, +); + +assert.equal( + report.executableSubject.reference.id, + "echo.executable-subject/v1", +); +assert.ok( + Buffer.isBuffer(report.executableSubject.bytes), + "the verifier report must retain the executable subject bytes", +); +const executableSubjectDigest = canonicalArtifactDigest( + "echo.executable-subject/v1", + report.executableSubject.bytes, +); +assertResourceReference( + report.executableSubject.reference, + "echo.executable-subject/v1", + executableSubjectDigest, +); +const executableSubject = decode(report.executableSubject.bytes); +assert.equal(executableSubject.apiVersion, "echo.executable-subject/v1"); +assert.deepEqual(executableSubject.package, report.package); +assert.deepEqual(executableSubject.targetIr, report.targetIr); +assert.deepEqual( + executableSubject.applicationResultProjection, + report.applicationResultProjection, +); + +const toolchainLockBytes = await readFile( + path.join(applicationRoot, "edict.toolchain-lock.json"), +); +const toolchainLock = JSON.parse(toolchainLockBytes); +const lawpackReleaseDigest = ( + await readFile( + path.join(applicationRoot, "vendor", "jedit-text", "manifest.sha256"), + "utf8", + ) +).trim(); +const reportDigest = canonicalArtifactDigest( + "echo.operation-package-verifier-report/v1", + reportBytes, +); +const reportArtifactId = { + coordinate: "verifier-report.echo-operation", + domain: "echo.operation-package-verifier-report/v1", + digest: digestText(reportDigest), + rawSha256: sha256(reportBytes).toString("hex"), +}; +const evidence = verificationEvidence({ + executableSubjectId: { + coordinate: report.executableSubject.reference.id, + digest: digestText(executableSubjectDigest), + }, + provider: toolchainLock.echo.provider, + reportArtifactId, + report, +}); +const computedBuildLock = { + schema: "jedit.edict-build-lock/v1", + applicationCoordinate: coreArtifact.coordinate, + operationCoordinate: executablePackage.operation_coordinate, + toolchainLockSha256: sha256(toolchainLockBytes).toString("hex"), + sourceClosure: await sourceClosure(applicationRoot), + lawpackRelease: { + coordinate: executablePackage.semantic_closure.lawpack_coordinate, + digest: lawpackReleaseDigest, + }, + provider: { + coordinate: toolchainLock.echo.provider.coordinate, + digest: toolchainLock.echo.provider.digest, + }, + artifacts: { + core: { + coordinate: coreArtifact.coordinate, + domain: "edict.core.module/v1", + digest: digestText(coreDigest), + }, + targetIr: { + coordinate: report.targetIr.id, + domain: "edict.target-ir.artifact/v1", + digest: digestText(targetIrDigest), + }, + resultProjection: { + coordinate: report.applicationResultProjection.id, + domain: "edict.result-projection.artifact/v1", + digest: digestText(resultProjectionDigest), + }, + executablePackage: { + coordinate: report.package.id, + domain: "echo.operation-package/v1", + digest: digestText(packageDigest), + rawSha256: sha256(packageBytes).toString("hex"), + }, + verificationReportArtifact: reportArtifactId, + verificationReport: evidence.identity, + executableSubject: { + coordinate: report.executableSubject.reference.id, + domain: "echo.executable-subject/v1", + digest: digestText(executableSubjectDigest), + }, + }, +}; +const computedSubjectLock = { + schema: "jedit.edict-executable-subject-lock/v1", + reference: { + coordinate: report.executableSubject.reference.id, + digest: digestText(executableSubjectDigest), + }, + rawSha256: sha256(report.executableSubject.bytes).toString("hex"), + package: { + coordinate: report.package.id, + digest: digestText(packageDigest), + }, + targetIr: { + coordinate: report.targetIr.id, + digest: digestText(targetIrDigest), + }, + resultProjection: { + coordinate: report.applicationResultProjection.id, + digest: digestText(resultProjectionDigest), + }, +}; + +const buildLockPath = path.join(applicationRoot, "edict.build-lock.json"); +const subjectLockPath = path.join( + applicationRoot, + "edict.executable-subject-lock.json", +); +if (mode === "--write-locks") { + await writeFile(buildLockPath, `${JSON.stringify(computedBuildLock, null, 2)}\n`); + await writeFile(subjectLockPath, `${JSON.stringify(computedSubjectLock, null, 2)}\n`); +} else { + assert.deepEqual( + JSON.parse(await readFile(buildLockPath, "utf8")), + computedBuildLock, + "the exact build closure differs from edict.build-lock.json", + ); + assert.deepEqual( + JSON.parse(await readFile(subjectLockPath, "utf8")), + computedSubjectLock, + "the executable subject differs from edict.executable-subject-lock.json", + ); +} diff --git a/edict/replace-range/tests/build.sh b/edict/replace-range/tests/build.sh new file mode 100755 index 0000000..00009a3 --- /dev/null +++ b/edict/replace-range/tests/build.sh @@ -0,0 +1,7 @@ +#!/usr/bin/env bash +set -euo pipefail + +project_root=$(cd "$(dirname "${BASH_SOURCE[0]}")/../../.." && pwd) +application_root="$project_root/edict/replace-range" + +exec node "$application_root/tests/package-chain.mjs" diff --git a/edict/replace-range/tests/package-chain.mjs b/edict/replace-range/tests/package-chain.mjs new file mode 100644 index 0000000..b521798 --- /dev/null +++ b/edict/replace-range/tests/package-chain.mjs @@ -0,0 +1,317 @@ +// SPDX-License-Identifier: Apache-2.0 OR LicenseRef-MIND-UCAL-1.0 +// © James Ross Ω FLYING•ROBOTS + +import assert from "node:assert/strict"; +import { spawnSync } from "node:child_process"; +import { createHash } from "node:crypto"; +import { + cp, + lstat, + mkdir, + readFile, + readlink, + realpath, + readdir, + rm, +} from "node:fs/promises"; +import path from "node:path"; +import { fileURLToPath } from "node:url"; + +import { decode } from "cbor-x"; + +const testsDirectory = path.dirname(fileURLToPath(import.meta.url)); +const applicationRoot = path.resolve(testsDirectory, ".."); +const projectRoot = path.resolve(applicationRoot, "../.."); +const lockPath = path.join(applicationRoot, "edict.toolchain-lock.json"); +const edictRepository = process.env.EDICT_REPO; +const echoRepository = process.env.ECHO_REPO; + +function run(command, arguments_, options = {}) { + const result = spawnSync(command, arguments_, { + cwd: options.cwd, + encoding: "utf8", + env: process.env, + input: options.input, + timeout: options.timeout ?? 120_000, + }); + if (options.emit !== false && result.stdout) { + process.stdout.write(result.stdout); + } + if (options.emit !== false && result.stderr) { + process.stderr.write(result.stderr); + } + if (result.error) { + throw result.error; + } + if (result.status !== 0) { + throw new Error(`${command} exited with status ${result.status}`); + } + return result.stdout.trim(); +} + +function git(repository, ...arguments_) { + return run("git", ["-C", repository, ...arguments_], { emit: false }); +} + +async function sha256(filePath) { + return createHash("sha256").update(await readFile(filePath)).digest("hex"); +} + +async function verifyGitCheckout(repository, expectedCommit, label) { + assert.ok(repository, `${label} repository path is required`); + const [requestedRoot, discoveredRoot] = await Promise.all([ + realpath(repository), + realpath(git(repository, "rev-parse", "--show-toplevel")), + ]); + assert.equal(discoveredRoot, requestedRoot, `${label} path must be the checkout root`); + assert.equal(git(repository, "rev-parse", "HEAD"), expectedCommit, `${label} commit mismatch`); + assert.equal( + git(repository, "status", "--porcelain=v1", "--untracked-files=all"), + "", + `${label} checkout must be clean`, + ); +} + +function providerArtifact(manifest, role) { + const matches = manifest.artifacts.filter((artifact) => artifact.role === role); + assert.equal(matches.length, 1, `provider must contain one ${role} artifact`); + return matches[0]; +} + +async function verifyProvider(lock) { + const providerRoot = path.join( + echoRepository, + "schemas", + "edict-provider", + "package", + "v1", + ); + await rejectSymlinks(providerRoot); + const manifestPath = path.join(providerRoot, "provider-manifest.echo.json"); + const manifest = JSON.parse(await readFile(manifestPath, "utf8")); + assert.equal(manifest.provider.coordinate, lock.coordinate); + assert.equal(manifest.provider.digest, lock.digest); + assert.equal(await sha256(manifestPath), lock.manifestSha256); + + for (const [role, fileName, expected] of [ + ["lowerer.echo-dpo", "lowerer.echo-dpo.component.wasm", lock.lowerer], + ["verifier.echo-dpo", "verifier.echo-dpo.component.wasm", lock.verifier], + ]) { + const artifact = providerArtifact(manifest, role); + assert.equal(artifact.resource.coordinate, expected.coordinate); + assert.equal(artifact.resource.digest, `sha256:${expected.sha256}`); + assert.equal( + await sha256(path.join(providerRoot, "components", fileName)), + expected.sha256, + ); + } + const targetProfileArtifact = providerArtifact( + manifest, + "target-profile.echo-dpo", + ); + assert.equal( + targetProfileArtifact.resource.coordinate, + lock.targetProfile.coordinate, + ); + assert.equal(targetProfileArtifact.resource.digest, lock.targetProfile.digest); + const targetProfile = decode( + await readFile( + path.join( + providerRoot, + "generated", + "primary", + "target-profile.echo-dpo.cbor", + ), + ), + ); + assert.equal(targetProfile.verifier.id, lock.verifier.contract.coordinate); + assert.equal( + `sha256:${Buffer.from(targetProfile.verifier.digest[1]).toString("hex")}`, + lock.verifier.contract.digest, + ); + return providerRoot; +} + +async function rejectSymlinks(root) { + for (const entry of await readdir(root, { withFileTypes: true })) { + const entryPath = path.join(root, entry.name); + assert.equal(entry.isSymbolicLink(), false, `symbolic link is forbidden: ${entryPath}`); + if (entry.isDirectory()) { + await rejectSymlinks(entryPath); + } + } +} + +async function collectDirectoryFiles(root, relative = "") { + const files = []; + const directory = path.join(root, relative); + for (const entry of await readdir(directory, { withFileTypes: true })) { + if (relative === "" && entry.name === ".build") { + continue; + } + const entryRelative = path.join(relative, entry.name); + if (entry.isDirectory()) { + files.push(...(await collectDirectoryFiles(root, entryRelative))); + } else { + files.push(entryRelative); + } + } + return files; +} + +function trackedFiles(repository) { + return git(repository, "ls-files", "-z") + .split("\0") + .filter(Boolean) + .sort(); +} + +async function snapshotFile(namespace, root, relative) { + const filePath = path.join(root, relative); + const metadata = await lstat(filePath, { bigint: true }); + const common = { + path: `${namespace}/${relative.split(path.sep).join("/")}`, + mode: metadata.mode.toString(), + size: metadata.size.toString(), + modifiedNanoseconds: metadata.mtimeNs.toString(), + inode: metadata.ino.toString(), + }; + if (metadata.isSymbolicLink()) { + return { ...common, kind: "symlink", target: await readlink(filePath) }; + } + if (metadata.isFile()) { + return { ...common, kind: "file", sha256: await sha256(filePath) }; + } + return { ...common, kind: "other" }; +} + +async function snapshotAuthoritativeInputs(lock) { + const roots = [ + ["jedit", applicationRoot, (await collectDirectoryFiles(applicationRoot)).sort()], + [ + "jedit-project", + projectRoot, + lock.validation.files.map((file) => file.path).sort(), + ], + ["edict", edictRepository, trackedFiles(edictRepository)], + ["echo", echoRepository, trackedFiles(echoRepository)], + ]; + const snapshot = []; + for (const [namespace, root, files] of roots) { + for (const relative of files) { + snapshot.push(await snapshotFile(namespace, root, relative)); + } + } + return snapshot; +} + +async function verifyVersions(lock) { + assert.equal(process.version, lock.validation.processVersion); + assert.equal(run("npm", ["--version"]), lock.validation.npmVersion); + const packageLock = JSON.parse( + await readFile(path.join(projectRoot, "package-lock.json")), + ); + assert.equal( + packageLock.packages["node_modules/cbor-x"].version, + lock.validation.cborX.version, + ); + assert.equal( + packageLock.packages["node_modules/cbor-x"].integrity, + lock.validation.cborX.integrity, + ); + for (const file of lock.validation.files) { + assert.equal( + await sha256(path.join(projectRoot, file.path)), + file.sha256, + `${file.path} differs from the validation-environment lock`, + ); + } + assert.equal( + run("rustc", [`+${lock.rust.toolchain}`, "--version"]), + lock.rust.rustcVersion, + ); + assert.equal( + run("cargo", [`+${lock.rust.toolchain}`, "--version"]), + lock.rust.cargoVersion, + ); + run( + "cargo", + [`+${lock.rust.toolchain}`, "build", "--locked", "-p", "edict-cli"], + { cwd: edictRepository }, + ); + const edictBinary = path.join(edictRepository, "target", "debug", "edict"); + const version = JSON.parse(run(edictBinary, ["--version"])); + assert.equal(version.version, lock.edict.cliVersion); + return edictBinary; +} + +async function build() { + const lock = JSON.parse(await readFile(lockPath, "utf8")); + assert.equal(lock.schema, "jedit.edict-toolchain-lock/v1"); + await verifyGitCheckout(edictRepository, lock.edict.commit, "Edict"); + await verifyGitCheckout(echoRepository, lock.echo.commit, "Echo"); + const providerSource = await verifyProvider(lock.echo.provider); + const before = await snapshotAuthoritativeInputs(lock); + let failure; + try { + const edictBinary = await verifyVersions(lock); + run(edictBinary, [], { + cwd: applicationRoot, + input: `${JSON.stringify({ + schema: "edict.compiler.settings/v1", + type: "compilerSettings", + operation: "build", + lawpack: "edict.lawpack.json", + checkOnly: true, + })}\n`, + }); + + const buildRoot = path.join(applicationRoot, ".build"); + const providerDestination = path.join(buildRoot, "echo-provider"); + const applicationOutput = path.join(buildRoot, "application"); + await rm(providerDestination, { recursive: true, force: true }); + await rm(applicationOutput, { recursive: true, force: true }); + await mkdir(providerDestination, { recursive: true }); + await cp(providerSource, providerDestination, { recursive: true }); + await rejectSymlinks(providerDestination); + + run(edictBinary, [], { + cwd: applicationRoot, + input: `${JSON.stringify({ + schema: "edict.compiler.settings/v1", + type: "compilerSettings", + operation: "build", + application: "edict.application.json", + })}\n`, + }); + run( + process.execPath, + [path.join(testsDirectory, "assert-build-output.mjs"), applicationOutput], + { cwd: applicationRoot }, + ); + } catch (error) { + failure = error; + } + + const after = await snapshotAuthoritativeInputs(lock); + let mutationFailure; + try { + assert.deepEqual(after, before, "authoritative inputs changed during package-chain build"); + } catch (error) { + mutationFailure = error; + } + if (failure && mutationFailure) { + throw new AggregateError( + [failure, mutationFailure], + "build failed and authoritative inputs changed", + ); + } + if (mutationFailure) { + throw mutationFailure; + } + if (failure) { + throw failure; + } +} + +await build(); diff --git a/edict/replace-range/tests/proof-harness.spec.mjs b/edict/replace-range/tests/proof-harness.spec.mjs new file mode 100644 index 0000000..c860a4c --- /dev/null +++ b/edict/replace-range/tests/proof-harness.spec.mjs @@ -0,0 +1,396 @@ +// SPDX-License-Identifier: Apache-2.0 OR LicenseRef-MIND-UCAL-1.0 +// © James Ross Ω FLYING•ROBOTS + +import assert from "node:assert/strict"; +import { spawnSync } from "node:child_process"; +import { cp, mkdtemp, mkdir, readFile, rm, symlink, writeFile } from "node:fs/promises"; +import os from "node:os"; +import path from "node:path"; +import test from "node:test"; +import { fileURLToPath } from "node:url"; + +import { decode, encode } from "cbor-x"; + +import { verificationEvidence } from "./verification-evidence.mjs"; + +const testDirectory = path.dirname(fileURLToPath(import.meta.url)); +const applicationRoot = path.resolve(testDirectory, ".."); +const projectRoot = path.resolve(applicationRoot, "../.."); +const edictRepository = process.env.EDICT_REPO; +const echoRepository = process.env.ECHO_REPO; + +function requireToolchainEnvironment() { + assert.ok(edictRepository, "EDICT_REPO must name the exact Edict checkout"); + assert.ok(echoRepository, "ECHO_REPO must name the exact Echo checkout"); +} + +async function fixture() { + const root = await mkdtemp(path.join(os.tmpdir(), "jedit-replace-range-proof-")); + const fixtureProject = path.join(root, "jedit"); + const fixtureApplication = path.join(fixtureProject, "edict", "replace-range"); + await mkdir(path.dirname(fixtureApplication), { recursive: true }); + await cp(applicationRoot, fixtureApplication, { recursive: true }); + await mkdir(path.join(fixtureProject, ".github", "workflows"), { + recursive: true, + }); + for (const relative of [ + ".github/workflows/ci.yml", + "package.json", + "package-lock.json", + ]) { + await cp(path.join(projectRoot, relative), path.join(fixtureProject, relative)); + } + await symlink( + path.join(projectRoot, "node_modules"), + path.join(fixtureProject, "node_modules"), + "dir", + ); + return { + root, + project: fixtureProject, + application: fixtureApplication, + async dispose() { + await rm(root, { recursive: true, force: true }); + }, + }; +} + +function runBuild(fixtureProject, overrides = {}) { + return spawnSync("bash", ["edict/replace-range/tests/build.sh"], { + cwd: fixtureProject, + encoding: "utf8", + env: { + ...process.env, + EDICT_REPO: edictRepository, + ECHO_REPO: echoRepository, + ...overrides, + }, + timeout: 120_000, + }); +} + +function assertCommandCompleted(result) { + assert.equal(result.error, undefined, result.error?.message); + assert.notEqual(result.status, null, `command terminated by ${result.signal}`); +} + +test("rejects_non_git_toolchain_inputs", { timeout: 120_000 }, async () => { + requireToolchainEnvironment(); + const subject = await fixture(); + try { + const fakeEdict = path.join(subject.root, "fake-edict"); + const fakeEcho = path.join(subject.root, "fake-echo"); + const fakeEdictBinary = path.join(fakeEdict, "target", "debug", "edict"); + const providerSource = path.join( + echoRepository, + "schemas", + "edict-provider", + "package", + "v1", + ); + const fakeProvider = path.join( + fakeEcho, + "schemas", + "edict-provider", + "package", + "v1", + ); + await mkdir(path.dirname(fakeEdictBinary), { recursive: true }); + await mkdir(path.dirname(fakeProvider), { recursive: true }); + await symlink(path.join(edictRepository, "target", "debug", "edict"), fakeEdictBinary); + await cp(providerSource, fakeProvider, { recursive: true }); + + const result = runBuild(subject.project, { + EDICT_REPO: fakeEdict, + ECHO_REPO: fakeEcho, + }); + assertCommandCompleted(result); + assert.notEqual( + result.status, + 0, + "non-Git toolchain directories must be rejected before publication or application build", + ); + } finally { + await subject.dispose(); + } +}); + +test("rejects_wrong_commit_toolchain_inputs", { timeout: 120_000 }, async () => { + requireToolchainEnvironment(); + const subject = await fixture(); + try { + const lockPath = path.join(subject.application, "edict.toolchain-lock.json"); + const lock = JSON.parse(await readFile(lockPath, "utf8")); + lock.edict.commit = "0".repeat(40); + await writeFile(lockPath, `${JSON.stringify(lock, null, 2)}\n`); + + const result = runBuild(subject.project); + assertCommandCompleted(result); + assert.notEqual(result.status, 0, "a wrong Edict commit must be rejected"); + } finally { + await subject.dispose(); + } +}); + +test("lawpack_check_only_rejects_drift_without_repairing_it", { timeout: 120_000 }, async () => { + requireToolchainEnvironment(); + const subject = await fixture(); + try { + const digestPath = path.join( + subject.application, + "vendor", + "jedit-text", + "manifest.sha256", + ); + const corruptDigest = `sha256:${"0".repeat(64)}\n`; + await writeFile(digestPath, corruptDigest); + + const result = runBuild(subject.project); + assertCommandCompleted(result); + assert.notEqual(result.status, 0, "drift must fail instead of being repaired"); + assert.equal( + await readFile(digestPath, "utf8"), + corruptDigest, + "check-only validation must leave the drifted artifact untouched", + ); + } finally { + await subject.dispose(); + } +}); + +test( + "rejects_package_whose_recomputed_identity_differs_from_report_subject", + { timeout: 120_000 }, + async () => { + requireToolchainEnvironment(); + const subject = await fixture(); + try { + const build = runBuild(subject.project); + assertCommandCompleted(build); + assert.equal(build.status, 0, build.stderr); + + const outputDirectory = path.join(subject.application, ".build", "application"); + const packagePath = path.join(outputDirectory, "executable-operation-package.cbor"); + const executablePackage = decode(await readFile(packagePath)); + const program = decode(executablePackage.program); + const alteredCore = Buffer.from(program.core_artifact); + alteredCore[0] ^= 1; + program.core_artifact = alteredCore; + executablePackage.program = encode(program); + await writeFile(packagePath, encode(executablePackage)); + + const assertion = spawnSync( + process.execPath, + [path.join(subject.application, "tests", "assert-build-output.mjs"), outputDirectory], + { cwd: subject.project, encoding: "utf8", timeout: 30_000 }, + ); + assertCommandCompleted(assertion); + assert.notEqual( + assertion.status, + 0, + "a report for the original package must not authorize altered embedded Core bytes", + ); + } finally { + await subject.dispose(); + } + }, +); + +test( + "preserves_nominal_exact_length_buffer_and_head_identities", + { timeout: 120_000 }, + async () => { + requireToolchainEnvironment(); + const subject = await fixture(); + try { + const build = runBuild(subject.project); + assertCommandCompleted(build); + assert.equal(build.status, 0, build.stderr); + + const packageBytes = await readFile( + path.join( + subject.application, + ".build", + "application", + "executable-operation-package.cbor", + ), + ); + const executablePackage = decode(packageBytes); + const program = decode(executablePackage.program); + const core = decode(program.core_artifact); + for (const typeName of [ + "ReplaceRangeInput.bufferId", + "ReplaceRangeInput.basisHeadId", + "ReplaceRangeBoundary.bufferId", + "ReplaceRangeBoundary.basisHeadId", + ]) { + assert.deepEqual( + core.types[typeName], + { + kind: "Nominal", + contract: + typeName.endsWith("bufferId") + ? "jedit.text@1.BufferId" + : "jedit.text@1.HeadId", + representation: "Bytes", + }, + `${typeName} must preserve its nominal exact 32-byte contract in Core`, + ); + } + } finally { + await subject.dispose(); + } + }, +); + +test("rejects_buffer_id_head_id_substitution", { timeout: 120_000 }, async () => { + requireToolchainEnvironment(); + const subject = await fixture(); + try { + const sourcePath = path.join( + subject.application, + "src", + "ReplaceRange.edict", + ); + const source = await readFile(sourcePath, "utf8"); + const crossed = source + .replace("bufferId: input.bufferId,", "bufferId: input.basisHeadId,") + .replace("basisHeadId: input.basisHeadId,", "basisHeadId: input.bufferId,"); + assert.notEqual( + crossed, + source, + "the negative witness must cross the two identities", + ); + await writeFile(sourcePath, crossed); + + const result = runBuild(subject.project); + assertCommandCompleted(result); + assert.notEqual(result.status, 0, "BufferId and HeadId must not be substitutable"); + assert.match( + `${result.stdout}\n${result.stderr}`, + /TypeMismatch/, + "the imported nominal boundary must reject the crossed assignment", + ); + } finally { + await subject.dispose(); + } +}); + +test("verification_report_identity_is_verifier_specific", () => { + const common = { + executableSubjectId: { + coordinate: "echo.executable-subject/v1", + digest: `sha256:${"1".repeat(64)}`, + }, + reportArtifactId: { + coordinate: "verifier-report.echo-operation", + domain: "echo.operation-package-verifier-report/v1", + digest: `sha256:${"2".repeat(64)}`, + rawSha256: "3".repeat(64), + }, + report: { + apiVersion: "echo.operation-package-verifier-report/v1", + diagnosticAbi: { + id: "edict.diagnostics/v1", + digest: ["sha256", Buffer.alloc(32, 4)], + }, + outcome: "accepted", + }, + }; + const provider = { + coordinate: "echo.edict-provider@1", + digest: `sha256:${"5".repeat(64)}`, + verifier: { + coordinate: "echo.dpo.verifier/component@1", + sha256: "6".repeat(64), + contract: { + coordinate: "echo.dpo.verifier/v1", + digest: `sha256:${"8".repeat(64)}`, + }, + }, + targetProfile: { + coordinate: "echo.dpo@1", + digest: `sha256:${"9".repeat(64)}`, + }, + }; + const original = verificationEvidence({ ...common, provider }); + const changed = verificationEvidence({ + ...common, + provider: { + ...provider, + verifier: { ...provider.verifier, sha256: "7".repeat(64) }, + }, + }); + assert.notEqual( + original.identity.digest, + changed.identity.digest, + "different verifier identities must produce different VerificationReportIds", + ); +}); + +test("rejects_drifted_build_and_executable_subject_locks", { timeout: 120_000 }, async () => { + requireToolchainEnvironment(); + const subject = await fixture(); + try { + const lockPath = path.join(subject.application, "edict.build-lock.json"); + const lock = JSON.parse(await readFile(lockPath, "utf8")); + lock.artifacts.core.digest = `sha256:${"0".repeat(64)}`; + await writeFile(lockPath, `${JSON.stringify(lock, null, 2)}\n`); + + const build = runBuild(subject.project); + assertCommandCompleted(build); + assert.notEqual( + build.status, + 0, + "a changed exact-artifact expectation must fail the package-chain gate", + ); + } finally { + await subject.dispose(); + } +}); + +test("rejects_drifted_executable_subject_lock", { timeout: 120_000 }, async () => { + requireToolchainEnvironment(); + const subject = await fixture(); + try { + const lockPath = path.join( + subject.application, + "edict.executable-subject-lock.json", + ); + const lock = JSON.parse(await readFile(lockPath, "utf8")); + lock.reference.digest = `sha256:${"0".repeat(64)}`; + await writeFile(lockPath, `${JSON.stringify(lock, null, 2)}\n`); + + const build = runBuild(subject.project); + assertCommandCompleted(build); + assert.notEqual( + build.status, + 0, + "a changed executable-subject expectation must fail the package-chain gate", + ); + } finally { + await subject.dispose(); + } +}); + +test("required_ci_executes_the_exact_package_chain", async () => { + const workflow = await readFile( + path.join(projectRoot, ".github", "workflows", "ci.yml"), + "utf8", + ); + assert.match(workflow, /^ edict-replace-range:\n/m); + assert.match(workflow, /name: edict \/ replace-range package chain/); + assert.match( + workflow, + /node --test edict\/replace-range\/tests\/proof-harness\.spec\.mjs/, + ); + assert.match( + workflow, + /ref: \$\{\{ github\.event\.pull_request\.head\.sha \|\| github\.sha \}\}/, + ); + assert.match(workflow, /git rev-parse HEAD/); + assert.match( + workflow, + /needs: \[ plan, build, test-shards, quality, release-gate, edict-replace-range \]/, + ); +}); diff --git a/edict/replace-range/tests/verification-evidence.mjs b/edict/replace-range/tests/verification-evidence.mjs new file mode 100644 index 0000000..2286e29 --- /dev/null +++ b/edict/replace-range/tests/verification-evidence.mjs @@ -0,0 +1,83 @@ +// SPDX-License-Identifier: Apache-2.0 OR LicenseRef-MIND-UCAL-1.0 +// © James Ross Ω FLYING•ROBOTS + +import { createHash } from "node:crypto"; + +import { encode } from "cbor-x"; + +export function canonicalArtifactDigest(domain, canonicalArtifactBytes) { + const preimage = Buffer.concat([ + Buffer.from([0x83]), + Buffer.from(encode("edict.digest/v1")), + Buffer.from(encode(domain)), + Buffer.from(canonicalArtifactBytes), + ]); + return createHash("sha256").update(preimage).digest(); +} + +export function digestText(bytes) { + return `sha256:${Buffer.from(bytes).toString("hex")}`; +} + +function canonicalJson(value) { + if (Array.isArray(value)) { + return value.map(canonicalJson); + } + if (value !== null && typeof value === "object") { + return Object.fromEntries( + Object.keys(value) + .sort() + .map((key) => [key, canonicalJson(value[key])]), + ); + } + return value; +} + +function resourceReference(reference) { + return { + coordinate: reference.id, + digest: digestText(reference.digest[1]), + }; +} + +export function verificationEvidence({ + executableSubjectId, + provider, + reportArtifactId, + report, +}) { + const envelope = { + apiVersion: "jedit.edict-verification-evidence/v1", + reportArtifact: reportArtifactId, + executableSubject: executableSubjectId, + providerRelease: { + coordinate: provider.coordinate, + digest: provider.digest, + }, + verifierComponent: { + coordinate: provider.verifier.coordinate, + digest: `sha256:${provider.verifier.sha256}`, + }, + verificationPolicy: { + apiVersion: "jedit.edict-verification-policy/v1", + verifierContract: provider.verifier.contract, + targetProfile: provider.targetProfile, + reportAbi: report.apiVersion, + diagnosticAbi: resourceReference(report.diagnosticAbi), + }, + outcome: report.outcome, + }; + const bytes = Buffer.from(JSON.stringify(canonicalJson(envelope)), "utf8"); + return { + envelope, + bytes, + identity: { + coordinate: "jedit.edict-verification-evidence/v1", + domain: "jedit.edict-verification-evidence/v1", + digest: digestText( + canonicalArtifactDigest("jedit.edict-verification-evidence/v1", bytes), + ), + rawSha256: createHash("sha256").update(bytes).digest("hex"), + }, + }; +} diff --git a/edict/replace-range/vendor/jedit-text/adapter.cbor b/edict/replace-range/vendor/jedit-text/adapter.cbor new file mode 100644 index 0000000..99e3ce6 Binary files /dev/null and b/edict/replace-range/vendor/jedit-text/adapter.cbor differ diff --git a/edict/replace-range/vendor/jedit-text/adapter.sha256 b/edict/replace-range/vendor/jedit-text/adapter.sha256 new file mode 100644 index 0000000..4260e28 --- /dev/null +++ b/edict/replace-range/vendor/jedit-text/adapter.sha256 @@ -0,0 +1 @@ +sha256:b8d9f15ef18dc99691ab1e034ca40a8b8ac52a1bc1b27597284f1edbaf84f049 diff --git a/edict/replace-range/vendor/jedit-text/echo-operation-configuration.cbor b/edict/replace-range/vendor/jedit-text/echo-operation-configuration.cbor new file mode 100644 index 0000000..ee60987 --- /dev/null +++ b/edict/replace-range/vendor/jedit-text/echo-operation-configuration.cbor @@ -0,0 +1 @@ +¢japiVersionx(echo.operation-lowering-configuration/v1kprogramKindx!compiler-produced-bounded-pure/v1 \ No newline at end of file diff --git a/edict/replace-range/vendor/jedit-text/echo-operation-configuration.sha256 b/edict/replace-range/vendor/jedit-text/echo-operation-configuration.sha256 new file mode 100644 index 0000000..a708943 --- /dev/null +++ b/edict/replace-range/vendor/jedit-text/echo-operation-configuration.sha256 @@ -0,0 +1 @@ +sha256:bcb811b2d00d9824a256a26e48c14401c87fff509f2f75deb2ba703003a3f6d4 diff --git a/edict/replace-range/vendor/jedit-text/edict.lawpack-output.json b/edict/replace-range/vendor/jedit-text/edict.lawpack-output.json new file mode 100644 index 0000000..5907953 --- /dev/null +++ b/edict/replace-range/vendor/jedit-text/edict.lawpack-output.json @@ -0,0 +1,67 @@ +{ + "schema": "edict.lawpack-output/v1", + "lawpackId": "jedit.text", + "lawpackVersion": "1", + "artifacts": [ + { + "path": "manifest.cbor", + "kind": "manifest", + "coordinate": "edict.lawpack/v1", + "digest": "sha256:95758c1605894672cc9069fde01bb8b6e11842b053102660c9cd4f4d6f34d64e" + }, + { + "path": "manifest.sha256", + "kind": "manifestDigest", + "coordinate": "edict.lawpack/v1", + "digest": "sha256:95758c1605894672cc9069fde01bb8b6e11842b053102660c9cd4f4d6f34d64e" + }, + { + "path": "exports.cbor", + "kind": "exports", + "coordinate": "jedit.text.exports/v1", + "digest": "sha256:cbbc79fd92f09f341a1fae221a2a869bb64e15c511af39333e0453cd87fe456a" + }, + { + "path": "exports.sha256", + "kind": "exportsDigest", + "coordinate": "jedit.text.exports/v1", + "digest": "sha256:cbbc79fd92f09f341a1fae221a2a869bb64e15c511af39333e0453cd87fe456a" + }, + { + "path": "echo-operation-configuration.cbor", + "kind": "localResource", + "coordinate": "echo.operation-lowering-configuration/v1", + "digest": "sha256:bcb811b2d00d9824a256a26e48c14401c87fff509f2f75deb2ba703003a3f6d4" + }, + { + "path": "echo-operation-configuration.sha256", + "kind": "localResourceDigest", + "coordinate": "echo.operation-lowering-configuration/v1", + "digest": "sha256:bcb811b2d00d9824a256a26e48c14401c87fff509f2f75deb2ba703003a3f6d4" + }, + { + "path": "verifier-rules.cbor", + "kind": "localResource", + "coordinate": "jedit.text.verifier-rules/v1", + "digest": "sha256:364fb4ff98ae64fcd8d793aae3d7cb133ff8a1ce661330cea47688b13a0a823f" + }, + { + "path": "verifier-rules.sha256", + "kind": "localResourceDigest", + "coordinate": "jedit.text.verifier-rules/v1", + "digest": "sha256:364fb4ff98ae64fcd8d793aae3d7cb133ff8a1ce661330cea47688b13a0a823f" + }, + { + "path": "adapter.cbor", + "kind": "adapter", + "coordinate": "jedit.text.echo-adapter/v1", + "digest": "sha256:b8d9f15ef18dc99691ab1e034ca40a8b8ac52a1bc1b27597284f1edbaf84f049" + }, + { + "path": "adapter.sha256", + "kind": "adapterDigest", + "coordinate": "jedit.text.echo-adapter/v1", + "digest": "sha256:b8d9f15ef18dc99691ab1e034ca40a8b8ac52a1bc1b27597284f1edbaf84f049" + } + ] +} diff --git a/edict/replace-range/vendor/jedit-text/exports.cbor b/edict/replace-range/vendor/jedit-text/exports.cbor new file mode 100644 index 0000000..8092549 Binary files /dev/null and b/edict/replace-range/vendor/jedit-text/exports.cbor differ diff --git a/edict/replace-range/vendor/jedit-text/exports.sha256 b/edict/replace-range/vendor/jedit-text/exports.sha256 new file mode 100644 index 0000000..87a0814 --- /dev/null +++ b/edict/replace-range/vendor/jedit-text/exports.sha256 @@ -0,0 +1 @@ +sha256:cbbc79fd92f09f341a1fae221a2a869bb64e15c511af39333e0453cd87fe456a diff --git a/edict/replace-range/vendor/jedit-text/manifest.cbor b/edict/replace-range/vendor/jedit-text/manifest.cbor new file mode 100644 index 0000000..7bbc2c4 Binary files /dev/null and b/edict/replace-range/vendor/jedit-text/manifest.cbor differ diff --git a/edict/replace-range/vendor/jedit-text/manifest.sha256 b/edict/replace-range/vendor/jedit-text/manifest.sha256 new file mode 100644 index 0000000..be4e2d8 --- /dev/null +++ b/edict/replace-range/vendor/jedit-text/manifest.sha256 @@ -0,0 +1 @@ +sha256:95758c1605894672cc9069fde01bb8b6e11842b053102660c9cd4f4d6f34d64e diff --git a/edict/replace-range/vendor/jedit-text/verifier-rules.cbor b/edict/replace-range/vendor/jedit-text/verifier-rules.cbor new file mode 100644 index 0000000..ef8836e --- /dev/null +++ b/edict/replace-range/vendor/jedit-text/verifier-rules.cbor @@ -0,0 +1 @@ +¤fschemasjedit.text.schema@1lschemaDigestxGsha256:f49b0ff6c9c7010d3a72b46734d47832853f496739a083edc41dddec3431bac7oruntimeOntologyugeneric-bounded-graphworacleIsExecutableInputô \ No newline at end of file diff --git a/edict/replace-range/vendor/jedit-text/verifier-rules.sha256 b/edict/replace-range/vendor/jedit-text/verifier-rules.sha256 new file mode 100644 index 0000000..f8f7a38 --- /dev/null +++ b/edict/replace-range/vendor/jedit-text/verifier-rules.sha256 @@ -0,0 +1 @@ +sha256:364fb4ff98ae64fcd8d793aae3d7cb133ff8a1ce661330cea47688b13a0a823f diff --git a/package-lock.json b/package-lock.json index 801e5a1..d76f6e8 100644 --- a/package-lock.json +++ b/package-lock.json @@ -22,6 +22,7 @@ "@flyingrobots/bijou-i18n-tools-node": "^7.0.0", "@flyingrobots/bijou-i18n-tools-xlsx": "^7.0.0", "@types/node": "^22.0.0", + "cbor-x": "^1.6.4", "semver": "^7.8.5", "tsx": "^4.22.4", "typescript": "^5.9.3" diff --git a/package.json b/package.json index d0490ec..8161bb2 100644 --- a/package.json +++ b/package.json @@ -41,6 +41,7 @@ "@flyingrobots/bijou-i18n-tools-node": "^7.0.0", "@flyingrobots/bijou-i18n-tools-xlsx": "^7.0.0", "@types/node": "^22.0.0", + "cbor-x": "^1.6.4", "semver": "^7.8.5", "tsx": "^4.22.4", "typescript": "^5.9.3"