From e93d07883fbfa80d7173428b6d751cf64dab1e4c Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 6 May 2026 16:56:01 +0000 Subject: [PATCH 1/4] docs(evaluator): add E3 option3 feasibility probe --- .../r3-pr-e6-g1a-option3-feasibility-probe.md | 193 ++++++++++++++++++ 1 file changed, 193 insertions(+) create mode 100644 docs/briefs/r3-pr-e6-g1a-option3-feasibility-probe.md diff --git a/docs/briefs/r3-pr-e6-g1a-option3-feasibility-probe.md b/docs/briefs/r3-pr-e6-g1a-option3-feasibility-probe.md new file mode 100644 index 00000000000..0b67cd93639 --- /dev/null +++ b/docs/briefs/r3-pr-e6-g1a-option3-feasibility-probe.md @@ -0,0 +1,193 @@ +# R3 PR-E E6-G1.a — Option 3 Static Representative Feasibility Probe + +**Status:** Director-authorized feasibility probe. This is not an +implementation brief. Do not dispatch implementation from this packet until +Director review accepts the representative. + +**Director ratification:** 2026-05-06, Option 3 for the E3/G1.a STOP: +revise the static representative so E6-G1.a can exercise static lens function +fields and report construction over already-evaluator-shaped inputs, while +deferring reflected-program `Dag` folding to a separate carrier question. + +**Supersedes for dispatch:** the representative assumption in +[`r3-pr-e6-g1a-static-lens-fold-worker.md`](r3-pr-e6-g1a-static-lens-fold-worker.md) +until this probe either lands a Director-accepted revision or reports STOP. + +## Problem + +The first E6-G1.a implementation attempt proved that the original static TC1 +representative still needed a substrate-shaped `Dag` value at runtime. The only +worker-found path was a local bridge: + +- compiled `Dag` to evaluator `Value` reification; +- whole-Dag reflection added through `lens_apply.rs`; +- `DeclarationId` encoded as `Int` because evaluator `Value` has no typed + declaration-reference inhabitant. + +That path is rejected. It creates local authority instead of executing the +existing body-evaluator surface. + +## Probe Goal + +Find a finite static `Lens` representative that proves the E6-G1.a +evaluator facts that are already in scope: + +1. static top-level `data ... : Lens` value consumption; +2. static function-field calls lowered through X1.a to + `TransformTarget::Callable`; +3. non-function field reads through `TransformTarget::FieldProject` over + `Value::RecordValue`; +4. `Witness`, `OptionalDiagnostic`, and `DimensionReport` construction + through declared constructors and existing evaluator `Value` carriers. + +The representative must use input values the evaluator can already supply +without compiled-program reflection. Because the live `Lens` carrier fixes +`read` and `validate` to `Dag`-typed inputs, this likely means opaque +already-evaluator-shaped `Dag` / `Behavior` arguments whose structure is not +inspected by the representative. + +The representative does not need to prove reflected-program folding. That is +now a separate `ReflectedProgram` / declaration-reference carrier question. + +## Hard Scope Bars + +The probe and any follow-up implementation brief must not: + +- require compiled `Dag` to evaluator `Value` reification; +- add an `eval_substrate_reify.rs`-shaped local authority; +- extend `lens_apply.rs` reflection to whole-Dag or route through + `lens_apply.rs`; +- encode `DeclarationId` as `Int`, `String`, or any other existing scalar + carrier; +- introduce new evaluator `Value` variants; +- add parser, lowerer, or substrate carrier changes; +- claim generic `fold_lens` or runtime-sourced callee dispatch. + +If one of those is required, STOP. The next action becomes Q-Reification / +reflected-program carrier design, not E3 implementation. + +## HEAD Check + +`src/v3/std/lens.dag` fixes the `Lens` carrier to: + +```text +read: fn(Dag, Behavior) -> Witness +validate: fn(Dag, C) -> OptionalDiagnostic +``` + +Therefore Option 3 cannot honestly change the representative to a different +subject type such as `MiniSubject` while still claiming to exercise the live +`Lens` carrier. A subject-typed mini lens would be a parallel `LensLike` +fixture, not E6-G1.a. + +The only plausible Option 3 probe is narrower: keep the live `Lens` +signature, but choose a static representative whose `read` and `validate` +functions do not inspect the `Dag` or `Behavior` arguments. The evaluator test +would supply already-evaluator-shaped opaque argument values for those ports. +That can prove static lens field calls and report construction, but it does +not prove reflected-program folding. + +If Director judges that an argument-opaque representative is too weak for +Path A, this probe should STOP immediately and route Q-Reification. + +## Candidate Representative Shape + +Prefer a tiny static lens that keeps the live `Lens` signature but avoids +reading reflected-program structure: + +```text +fn mini_read(d: Dag, b: Behavior) -> Witness = + Inhabits(1) + +fn int_add(a: Int, b: Int) -> Int = a + b +fn int_max(a: Int, b: Int) -> Int = if a > b then a else b +fn mini_iterate(c: Int, bound: LoopBound) -> Int = c +fn mini_validate(d: Dag, c: Int) -> OptionalDiagnostic = + NoDiagnostic + +data mini_lens: Lens = { + name: "mini_static", + read: mini_read, + sequential: { op: int_add, identity: 0 }, + branch: int_max, + iterate: mini_iterate, + validate: mini_validate +} + +fn mini_report(d: Dag, b: Behavior) -> DimensionReport = + match mini_lens.validate(d, 1) { + NoDiagnostic => + DimensionOk { + dimension_name: mini_lens.name, + composed: 1, + witnesses: ... + } + SomeDiagnostic { value: _diag } => + DimensionFail { ... } + } +``` + +The implementation test may bind `d` and `b` directly in the evaluator frame +using existing `Value` carriers, but the representative must not inspect either +argument. If any body needs to project fields from `d` or `b`, the probe has +crossed back into reflected-program reification and must STOP. + +## Feasibility Checks + +Before authoring an implementation brief, verify at HEAD: + +1. The proposed representative keeps the live `Lens` signature from + `src/v3/std/lens.dag`; no alternate lens carrier or subject-typed fixture. +2. The proposed `data ... : Lens` value lowers static function fields to + `TransformTarget::Callable` through the existing X1.a path. +3. The proposed opaque `Dag` / `Behavior` arguments can be supplied to + `evaluate_body` using existing + `Value::LiteralValue`, `Value::RecordValue`, or `Value::VariantValue` + carriers only, and no executed body inspects them. +4. Report constructors for `Witness`, `OptionalDiagnostic`, and + `DimensionReport` execute through E6-G0d constructor runtime support. +5. The representative avoids `LoopBound::Descent`; any iteration uses + cardinality-only behavior or no loop. + +## Feasibility Outcomes + +### Outcome A — Viable Representative Found + +Author a revised worker brief that replaces the original `Dag`/TC1-reflection +representative with the accepted already-evaluator-shaped representative. +That brief may dispatch an implementation PR only after Director review. + +Acceptance for the implementation brief: + +- compile-to-evaluate test proves the static lens value is consumed; +- lens function fields execute through `TransformTarget::Callable`; +- non-function field reads execute through `FieldProject` where the live + representative uses them, such as `mini_lens.name` or + `mini_lens.sequential.identity`; +- report values are `Value::VariantValue` / `Value::RecordValue` built through + declared constructors; +- test fails if it imports `lens_apply`, `eval_substrate_reify`, or reflection + helpers; +- PR body explicitly says reflected-program `Dag` folding remains deferred. + +### Outcome B — No Honest Representative Exists + +STOP and report the exact blocker: + +- Director rejects an argument-opaque `Dag` / `Behavior` representative as too + weak for Path A; or +- the evaluator cannot bind opaque `Dag` / `Behavior` arguments without + reflection or new carriers; or +- report construction still requires a typed reference carrier absent from + evaluator `Value`; or +- static lens function fields cannot be authored without parser/lowerer or + substrate changes. + +This STOP triggers Director's Q-Reification design audit and the +Substrate-side reflected-program carrier calibration. + +## Worker Pin Recommendation + +Use valiant-carp-10 only after Director accepts a revised implementation brief. +Until then, this is manager-authored feasibility/design work, not a worker +implementation task. From 99b56a6785134cd942101010001e2ddcaa5d00cd Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 6 May 2026 17:05:13 +0000 Subject: [PATCH 2/4] docs(evaluator): carve E3 option3 acceptance scope --- .../r3-pr-e6-g1a-option3-feasibility-probe.md | 23 ++++++++++++++++--- 1 file changed, 20 insertions(+), 3 deletions(-) diff --git a/docs/briefs/r3-pr-e6-g1a-option3-feasibility-probe.md b/docs/briefs/r3-pr-e6-g1a-option3-feasibility-probe.md index 0b67cd93639..e958f119498 100644 --- a/docs/briefs/r3-pr-e6-g1a-option3-feasibility-probe.md +++ b/docs/briefs/r3-pr-e6-g1a-option3-feasibility-probe.md @@ -154,11 +154,16 @@ Before authoring an implementation brief, verify at HEAD: ### Outcome A — Viable Representative Found Author a revised worker brief that replaces the original `Dag`/TC1-reflection -representative with the accepted already-evaluator-shaped representative. -That brief may dispatch an implementation PR only after Director review. +representative with the accepted argument-opaque representative. Director +review accepted this representative shape as sufficient for E6-G1.a's narrow +mechanism-demonstration scope: static lens value consumption, static +function-field calls, field projection, and report construction. Acceptance for the implementation brief: +- acceptance gate explicitly says: lens consumer-wiring mechanism + demonstration; lens-over-`Dag` folding is deferred to + `ReflectedProgram` / typed declaration-reference carrier work; - compile-to-evaluate test proves the static lens value is consumed; - lens function fields execute through `TransformTarget::Callable`; - non-function field reads execute through `FieldProject` where the live @@ -168,7 +173,19 @@ Acceptance for the implementation brief: declared constructors; - test fails if it imports `lens_apply`, `eval_substrate_reify`, or reflection helpers; -- PR body explicitly says reflected-program `Dag` folding remains deferred. +- PR body explicitly says reflected-program `Dag` folding remains deferred; +- cementing-test discipline for static lenses is not part of E6-G1.a Outcome A + acceptance. It waits behind Q-Reification and the reflected-program carrier + landing. + +Verification V1 cascade routing: + +- If Verification can demonstrate TC1 eta-equivalence with the + argument-opaque representative, V1 and E3 remain paired in the same release + step. +- If TC1 eta-equivalence requires a real lens-over-`Dag` fold, V1 unpairs from + this E3 slice and waits for Q-Reification / carrier landing. This does not + block the E6-G1.a Outcome A mechanism demonstration. ### Outcome B — No Honest Representative Exists From ad8dc645cf1d79c9b924621f36531aca5e028b96 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 6 May 2026 13:08:28 -0400 Subject: [PATCH 3/4] WIP: R3 Evaluator --- .../r3-pr-e6-g1a-option3-feasibility-probe.md | 43 +++++++++++++++---- 1 file changed, 35 insertions(+), 8 deletions(-) diff --git a/docs/briefs/r3-pr-e6-g1a-option3-feasibility-probe.md b/docs/briefs/r3-pr-e6-g1a-option3-feasibility-probe.md index e958f119498..ffea3e67c47 100644 --- a/docs/briefs/r3-pr-e6-g1a-option3-feasibility-probe.md +++ b/docs/briefs/r3-pr-e6-g1a-option3-feasibility-probe.md @@ -115,15 +115,28 @@ data mini_lens: Lens = { } fn mini_report(d: Dag, b: Behavior) -> DimensionReport = - match mini_lens.validate(d, 1) { - NoDiagnostic => - DimensionOk { + match mini_lens.read(d, b) { + Inhabits(c) => + match mini_lens.validate(d, c) { + NoDiagnostic => + DimensionOk { + dimension_name: mini_lens.name, + composed: c, + witnesses: singleton_witness(Inhabits(c)) + } + SomeDiagnostic { value: diag } => + DimensionFail { + dimension_name: mini_lens.name, + violations: singleton_diagnostic(diag), + witnesses: singleton_witness(Inhabits(c)) + } + } + Violates { reason: diag, at: beh } => + DimensionFail { dimension_name: mini_lens.name, - composed: 1, - witnesses: ... + violations: singleton_diagnostic(diag), + witnesses: singleton_witness(Violates { reason: diag, at: beh }) } - SomeDiagnostic { value: _diag } => - DimensionFail { ... } } ``` @@ -132,6 +145,13 @@ using existing `Value` carriers, but the representative must not inspect either argument. If any body needs to project fields from `d` or `b`, the probe has crossed back into reflected-program reification and must STOP. +The `singleton_witness` / `singleton_diagnostic` helpers above are placeholders +for whatever declared list constructor surface is live at implementation time. +The implementation may choose an equivalent already-declared list producer, but +it must not replace the witness list with an unrelated literal or empty list: +the `Witness` returned by `mini_lens.read(d, b)` must flow into the +`DimensionReport`. + ## Feasibility Checks Before authoring an implementation brief, verify at HEAD: @@ -146,7 +166,11 @@ Before authoring an implementation brief, verify at HEAD: carriers only, and no executed body inspects them. 4. Report constructors for `Witness`, `OptionalDiagnostic`, and `DimensionReport` execute through E6-G0d constructor runtime support. -5. The representative avoids `LoopBound::Descent`; any iteration uses +5. `mini_report` or its final equivalent calls `mini_lens.read(d, b)` and uses + the returned `Witness` to choose the report path and populate report + witnesses/composed/fail fields as appropriate. A report built from only + literals is not sufficient. +6. The representative avoids `LoopBound::Descent`; any iteration uses cardinality-only behavior or no loop. ## Feasibility Outcomes @@ -166,6 +190,9 @@ Acceptance for the implementation brief: `ReflectedProgram` / typed declaration-reference carrier work; - compile-to-evaluate test proves the static lens value is consumed; - lens function fields execute through `TransformTarget::Callable`; +- the implementation test fails if `mini_lens.read(d, b)` is removed, bypassed, + or replaced by a literal carrier; the returned `Witness` must feed the + `DimensionReport`; - non-function field reads execute through `FieldProject` where the live representative uses them, such as `mini_lens.name` or `mini_lens.sequential.identity`; From b2eaa2b39c9bc480d12e9c8bcb5ddb60fc93a64a Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 6 May 2026 18:08:47 +0000 Subject: [PATCH 4/4] docs(evaluator): stop read violation diagnostic lift --- .../r3-pr-e6-g1a-option3-feasibility-probe.md | 29 ++++++++++++++----- 1 file changed, 22 insertions(+), 7 deletions(-) diff --git a/docs/briefs/r3-pr-e6-g1a-option3-feasibility-probe.md b/docs/briefs/r3-pr-e6-g1a-option3-feasibility-probe.md index ffea3e67c47..f804a7c8e67 100644 --- a/docs/briefs/r3-pr-e6-g1a-option3-feasibility-probe.md +++ b/docs/briefs/r3-pr-e6-g1a-option3-feasibility-probe.md @@ -131,12 +131,8 @@ fn mini_report(d: Dag, b: Behavior) -> DimensionReport = witnesses: singleton_witness(Inhabits(c)) } } - Violates { reason: diag, at: beh } => - DimensionFail { - dimension_name: mini_lens.name, - violations: singleton_diagnostic(diag), - witnesses: singleton_witness(Violates { reason: diag, at: beh }) - } + Violates { reason: _reason, at: _behavior } => + STOP } ``` @@ -152,6 +148,15 @@ it must not replace the witness list with an unrelated literal or empty list: the `Witness` returned by `mini_lens.read(d, b)` must flow into the `DimensionReport`. +The read-channel `Violates` branch is deliberately a STOP in the candidate. +`Witness::Violates` carries `reason: String` and `at: Behavior`, while +`DimensionFail.violations` carries `List`. The probe must not +invent a `String` / `Behavior` to `Diagnostic` lift. Outcome A may only include +a read-violation report path if an existing declared diagnostic-construction +path is identified and exercised; otherwise the first representative must keep +`mini_read` on the `Inhabits` path and leave read-channel violation lifting to +Q-Reification / diagnostic carrier follow-up. + ## Feasibility Checks Before authoring an implementation brief, verify at HEAD: @@ -170,7 +175,11 @@ Before authoring an implementation brief, verify at HEAD: the returned `Witness` to choose the report path and populate report witnesses/composed/fail fields as appropriate. A report built from only literals is not sufficient. -6. The representative avoids `LoopBound::Descent`; any iteration uses +6. Any read-channel `Violates` to `DimensionFail.violations` path uses an + existing declared diagnostic-construction path. If no such path exists, the + candidate must STOP on read-channel violations and the first representative + must exercise the `Inhabits` path only. +7. The representative avoids `LoopBound::Descent`; any iteration uses cardinality-only behavior or no loop. ## Feasibility Outcomes @@ -193,6 +202,10 @@ Acceptance for the implementation brief: - the implementation test fails if `mini_lens.read(d, b)` is removed, bypassed, or replaced by a literal carrier; the returned `Witness` must feed the `DimensionReport`; +- the implementation either identifies and uses an existing declared + diagnostic-construction path for read-channel `Violates`, or proves the first + representative stays on the `Inhabits` path and fails closed if `Violates` + would need to be lifted into `DimensionFail.violations`; - non-function field reads execute through `FieldProject` where the live representative uses them, such as `mini_lens.name` or `mini_lens.sequential.identity`; @@ -222,6 +235,8 @@ STOP and report the exact blocker: weak for Path A; or - the evaluator cannot bind opaque `Dag` / `Behavior` arguments without reflection or new carriers; or +- read-channel `Violates` must be lifted into `DimensionFail.violations` but no + declared `Diagnostic` construction path exists; or - report construction still requires a typed reference carrier absent from evaluator `Value`; or - static lens function fields cannot be authored without parser/lowerer or