Skip to content

Interpret compiler-produced bounded Edict graph programs #684

Description

@flyingrobots

Claim

Echo can independently verify and interpret compiler-produced bounded Edict
graph programs using a generic, deterministic, metered target profile. Jedit is
the first external conformance consumer, not part of Echo's runtime ontology.

Required input and RED

The first RED consumes an exact package and verification report produced from
real Jim-owned ReplaceRange.edict by Edict's public application-build
boundary. It fails because the verified generic Target IR requires a capability
the current EchoOperationProgramV1 profile does not support.

The RED must not construct a package from Jedit's schema or oracle, work
backward from expected outcomes, use a handwritten fixture builder, or link a
native Jedit planner. The Jedit oracle is test expectation only.

Generic scope

Add only capabilities proven necessary by the compiler-produced program, such
as:

  • typed records and tagged unions;
  • checked integer arithmetic;
  • deterministic byte and UTF-8 operations;
  • canonical encoding and hashing;
  • generic graph reads and staged node/attachment writes;
  • bounded control flow or metered worklists;
  • declared and actual footprints;
  • typed result and obstruction projection;
  • private evaluation followed by one atomic TickPatch;
  • WAL, receipt, recovery, and structurally separate verifier evidence.

Preserve existing program bytes and compatibility unless the compiler evidence
requires an explicitly versioned profile change.

Runtime ontology prohibition

Echo production code and public runtime APIs must not acquire:

  • ReplaceRange or any other Jedit operation variant;
  • rope, leaf, branch, split, join, balance, Buffer, or TextWindow semantics;
  • a Jedit planner callback, MutationPlan, caller-authored patch, or opaque host
    function;
  • an unrestricted VM, durable child lane, wormhole, or application-specific
    budget reinterpretation.

Application coordinates may appear opaquely in packages, receipts, fixtures,
and integration tests. Production Echo code may not interpret that vocabulary.

Acceptance criteria

  • The fixture is the exact Edict-produced package and accepted verification
    report from a checked-in Jedit application source revision.
  • The Jedit schema and oracle are retained only as ABI/conformance evidence,
    never executable semantic input.
  • Echo admits and interprets the program through a versioned generic target
    profile.
  • Evaluation is deterministic, budgeted, private before commit, and produces
    one atomic Tick or typed obstruction.
  • Declared and actual footprints, results, receipts, WAL evidence, and
    recovery corroborate.
  • A structurally separate verifier accepts the exact target program without
    reconstructing it.
  • Production source contains no application-specific branch, intrinsic, or
    callback.
  • Integration outcomes agree with the independent Jedit oracle without
    sharing the native planner or algorithm path.

Dependency

Blocked first on flyingrobots/edict#192 lowering bounded control flow and
digest-bound pure lawpack helpers into Core, then on flyingrobots/jedit#296
producing the exact Jim-owned compiler output. The compiler failure is the
routing table; do not implement speculative runtime capability before that
evidence exists.

Metadata

Metadata

Assignees

No one assigned

    Labels

    enhancementNew feature or requestfeatureFeature umbrella (epic)lane:up-nextMethod lane up-next.legend:testMethod legend test.priority:highMethod priority high.runtimeRuntime corespecSpec/Design documenttoolingTooling/CI/CLItype:enhancementMethod work type enhancement.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions