You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Author and prove ReplaceRange.edict as Jim's first real application operation.
This proves an operation law and compiler/runtime substrate; it does not by
itself prove the final Jim.edict observer composition.
jedit.text.schema@1 is the application ABI and fact/codec/identity contract.
jedit.text.ReplaceRange.oracle@1 is independent expected-behavior evidence.
ReplaceRange.edict is the authored executable semantics.
Edict Core/Target IR plus an independently verified package is executable
meaning.
Echo receipts are per-execution evidence.
Neither the schema nor oracle is a program. Echo must not synthesize a package
or evaluator from them.
Required first RED
Check in the exact Jim-owned source and complete lawpack closure, then build it
through Edict's public application-build boundary. The first honest failure
routes work to its owner:
missing expressivity or Core representation -> Edict;
source that cannot lower -> Edict target adapter/lawpack;
verified generic profile unsupported at runtime -> Echo;
execution disagrees with the oracle -> triangulate source/compiler/runtime.
Do not start by reverse-engineering an Echo evaluator from the schema/oracle.
Acceptance criteria
ReplaceRange.edict and its complete closure are checked in under a
Jim-owned application root.
Edict's public build emits exact Core, Target IR, package, manifest,
codecs, and structurally separate verification evidence.
Echo consumes the exact compiler-produced package without reconstruction.
Echo production code uses only generic bounded-program primitives and
contains no ReplaceRange, rope, split/join/balance, Buffer, or TextWindow branch or intrinsic.
One admitted execution produces the corpus-defined persistent-rope
consequence or typed obstruction with basis, budget, footprint, Tick, WAL,
receipt, reading, and recovery evidence.
All retained oracle cases agree through a separately implemented runtime
path that shares no native Jedit planner or algorithm.
Slice
Author and prove
ReplaceRange.edictas Jim's first real application operation.This proves an operation law and compiler/runtime substrate; it does not by
itself prove the final
Jim.edictobserver composition.Parent: #295.
Artifact boundary
jedit.text.schema@1is the application ABI and fact/codec/identity contract.jedit.text.ReplaceRange.oracle@1is independent expected-behavior evidence.ReplaceRange.edictis the authored executable semantics.meaning.
Neither the schema nor oracle is a program. Echo must not synthesize a package
or evaluator from them.
Required first RED
Check in the exact Jim-owned source and complete lawpack closure, then build it
through Edict's public application-build boundary. The first honest failure
routes work to its owner:
Do not start by reverse-engineering an Echo evaluator from the schema/oracle.
Acceptance criteria
ReplaceRange.edictand its complete closure are checked in under aJim-owned application root.
codecs, and structurally separate verification evidence.
contains no
ReplaceRange, rope, split/join/balance,Buffer, orTextWindowbranch or intrinsic.consequence or typed obstruction with basis, budget, footprint, Tick, WAL,
receipt, reading, and recovery evidence.
path that shares no native Jedit planner or algorithm.
MutationPlan, native callbacks, fake transports, and compatibility fallback.scaffolding and is unreachable from final production composition.
Source location
Use a Jim-owned application root such as:
The oracle remains under
contracts/jedit/lawpacks/replace-range-v1/and is notpart of executable semantic input.
Dependencies
lowering into Core. Current public-build probes stop there before provider
invocation.
necessary by the compiler-produced package.
Non-goals
Jim.edictobserver cutover in this slice.rope intrinsic, unrestricted VM, child lane, or wormhole.