Repository navigation
Conversation
WF19: Generator workflow capability port (bootstrap/makegen/pragma) - Add universal compilation_ensure + codegen_ensure capabilities to process registry, shared across all tool workflows via canonical WorkIdentity dedup - Create bootstrap workflow spec (8 nodes, 2 parallel upsert chains) - Create makegen workflow spec (6 nodes, linear chain) - Create pragma workflow spec (9 nodes, 3 parallel render+upsert chains) WF20: Remaining tool capability port (deps/dag-viz/dag-snapshot) - Create deps workflow spec (10 nodes, parallel install+generate chains) - Create dag-viz workflow spec (8 nodes, shared base with gist family) - Create dag-snapshot workflow spec (9 nodes, mirrors gist-snapshot) - dag-viz and dag-snapshot share branch_resolution + credential_resolve capabilities via global ledger dedup WF21: Makefile thinning for all tool targets - Add planner_managed flag to ToolInfo struct - Planner-managed tools dispatch via gunbc-workflow --plan <tool> - Remove ensure-codegen prerequisite for planner-managed tools - Mark bootstrap, makegen, pragma, deps, dag-viz*, dag-snapshot WF22: Capability minimization verification - Extend PlanExplain with capability_status per-capability breakdown - Add CapabilityStatus/CapabilityAction types for hit/miss/execute - CLI text output includes capabilities section - CLI JSON output includes capabilities array with action/detail/node_ids Integration tests verify: - Universal capabilities deduped across all 6 tool workflows - Global plan non-redundancy proof holds with all 8 workflows - Projection equivalence maintained across full workflow set https://claude.ai/code/session_01X5CzTeZdjtsAVcz696jme4
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 34dfc8ac61
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| "dag-viz-diff", | ||
| "dag-viz-recent", |
There was a problem hiding this comment.
Keep unsupported dag-viz variants off planner dispatch
Including dag-viz-diff and dag-viz-recent in the planner-managed list makes their Make targets invoke gunbc-workflow --plan <name>, but the workflow builder only supports dag-viz/dag-snapshot names, so these two existing targets now fail with an unknown-workflow error instead of executing their binaries.
Useful? React with 👍 / 👎.
| let cli_args = render_cli_args(&tool.entrypoints); | ||
| if dry_run { | ||
| format!( | ||
| "@target/release/gunbc-workflow --plan {} --dry-run strict{}", | ||
| tool.short_name, cli_args |
There was a problem hiding this comment.
Stop forwarding tool entrypoint flags to gunbc-workflow
This planner command still appends render_cli_args(&tool.entrypoints), but gunbc-workflow only parses planner flags and rejects unknown arguments; for planner-managed dag-viz targets, setting Make vars like REPO/FMT/BASE now emits flags such as --repo-path and --base-ref that cause immediate CLI parse failure.
Useful? React with 👍 / 👎.
| if tool.planner_managed { | ||
| return Vec::new(); |
There was a problem hiding this comment.
Retain a prerequisite that builds the planner binary
Returning no dependencies for planner-managed tools removes all build prerequisites, but their recipes execute target/release/gunbc-workflow directly; in a clean workspace (or after cargo clean) that binary is absent, so targets like make bootstrap fail before any planner logic runs.
Useful? React with 👍 / 👎.
…penai-pro BLOCKING fix) openai-pro REQUEST_CHANGES at sha 8f5483b on PR #1817 caught a real internal inconsistency: ratification text said "Faithful representation of the concept is the closure criterion; pair-counting is not" but the actual closure predicates across r3-structure.md / r3-program-plan.md / r3-design-schedule-2026-05-06.md still phrased Pass as "≥3 pairs emit to target primitives". This violated single-authority + facts-flow-forward. Fix: align all 5 Pass-condition / closure-predicate locations to the faithful-modeling criterion ratified in Q-MachineConstraint sub-decision 5: - docs/r3-program-plan.md:74 (gate #60 Pass condition in §1.4 ledger): "Gate Pass = concept faithfully modeled (per Brian directive 2026-05-06) — once substrate carries algebra + machine-constraint as independent composing axes with .dag-generated interaction substrate, all valid pairs work by construction. Minimum existence-proof evidence: 3 pairs lower without v2-fallback (evidence, not target)." - docs/r3-program-plan.md:257 (§1.8 canonical ledger row): "concept faithfully modeled... min existence-proof = Int<64>/Real<64>/Nat<8> lower without v2-fallback (evidence, not target)" - docs/r3-program-plan.md:430 (§1.4 Class 1 representative gap-test): "Representative gap-test (minimum existence-proof, NOT target) — substrate faithfully modeling algebra + machine-constraint separation IS the closure criterion; the 3 pairs below are the minimum existence-proof" - docs/r3-structure.md:173 (canonical gate description): "Pass condition: concept faithfully modeled... Minimum existence-proof evidence (not closure target): 3 pairs lower without v2-fallback" - docs/r3-design-schedule-2026-05-06.md:60 (S3 closure predicate cite): "Pass = concept faithfully modeled... 3-pair set is minimum existence-proof evidence, NOT the closure target" Sub-decision 5 explanatory text retains "≥3 pairs land" as anti-reference to the prior phrasing for traceability of the change. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…+ 5 PM defaults (#1817) * docs(r3): Q-MachineConstraint-Carrier RATIFIED — universal substrate + 5 PM defaults (Brian directive) Brian directive 2026-05-06: "universal substrate, ratify defaults". Resolves Q-MachineConstraint-Carrier (was OPEN per r3-program-plan.md §10.3) with 6 sub-decisions ratified: 1. Axes in R3 scope: MachineWidth<bits> only. RegisterClass<R> / EndianMode<E> / alignment / signedness-as-axis deferred post-R3. 2. Interaction substrate shape: parametric Compose<Algebra, MachineConstraint> type-level construction. Closed-enumeration lookup-maps rejected (bridges). 3. Type-level spelling: Int<64> = Compose<AbelianGroup, MachineWidth<64>> parametrically. Equivalent under both algebra-side options per PR #1815. 4. Approximate-algebra layering: algebra approx + machine approx are independent composing axes. Real<64> = Compose<ApproximateField<Rational>, MachineWidth<64>> carries both layers per S8 discipline. 5. Class 1 demonstration breadth: ≥3 algebra×constraint pairs is minimum, not target. Broader coverage follows automatically once parser handles generic interaction syntax. 6. Target-specificity: MachineConstraint<C> is UNIVERSAL substrate (Brian directive). Every target carries machine-constraint facts as substrate; targets lacking native machine-width semantics (Python int/float) handle omission at Grounding-level discharge — target-conditioned lowering, NOT target-conditioned substrate. Substrate Mgr S3 dispatch unblocked on machine-constraint side; independent of T-Numeric-Construction algebra-side Option A vs B selection per PR #1815 (interaction semantics carries through under either). Updates: - docs/r3-program-plan.md §10.3 Q-MachineConstraint-Carrier row: OPEN → RATIFIED 2026-05-06 with all 6 sub-decisions named. - docs/r3-design-schedule-2026-05-06.md §S3: drops "open scope" framing; explicit ratified-scope block citing the 6 decisions; S3 dispatch noted as unblocked on machine-constraint side. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): Q-MachineConstraint sub-decisions 1/2/5/6 elaborated per Brian clarifying inline Brian clarifying directive 2026-05-06 on the 6 sub-decisions: 1. AXES — accept MachineWidth<bits> only; add separation-of-facts/concerns discipline note: algebra/machine-constraint/target-lowering are distinct axes. Integer modeling is the canonical exercise. 2. INTERACTION SHAPE (revised from "parametric Compose<...>" framing): "these models interact a la rest apis interacting — scalable / no dual representations (.dag generated)". The interaction substrate is .dag-DECLARED + .dag-GENERATED, never hand-coded. Hard constraint: no dual representations — any Rust counterpart must be generated, never hand-maintained (feedback_isomorphism_or_generation_for_mirrors + feedback_no_generated_code_on_disk). 3. SPELLING — Compose<AbelianGroup, MachineWidth<64>> ratified ("ok fine"). Note added: the interaction substrate elaborating Compose<...> is .dag-generated per sub-decision 2. 4. LAYERING — independent composing axes ratified ("ok fine"). Real<64> = Compose<ApproximateField<Rational>, MachineWidth<64>> stays. 5. DEMONSTRATION BREADTH — strengthened: "3 is not a target, we shouldn't be 'targeting' modeling, we are just doing our best job to faithfully represent the concepts". Closure criterion is "concept is faithfully modeled", not "≥3 pairs land". 3-pair demonstration is minimum existence proof, not closure target. 6. TARGET-SPECIFICITY — universal substrate stays. Python lowering uses faithful target-available primitives (numpy.uint8 / ctypes.c_uint8 / explicit literal-bits), NOT omission. "if python lacks — we would have to actually represent the struct using something that python faithfully provides — i.e. either literal bits or otherwise". Faithful representation > target-conditioned omission. Updates docs/r3-program-plan.md §10.3 Q-MachineConstraint-Carrier row + docs/r3-design-schedule-2026-05-06.md §S3 ratified-scope block to reflect clarifying inline. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): closure predicate aligned to faithful-modeling criterion (openai-pro BLOCKING fix) openai-pro REQUEST_CHANGES at sha 8f5483b on PR #1817 caught a real internal inconsistency: ratification text said "Faithful representation of the concept is the closure criterion; pair-counting is not" but the actual closure predicates across r3-structure.md / r3-program-plan.md / r3-design-schedule-2026-05-06.md still phrased Pass as "≥3 pairs emit to target primitives". This violated single-authority + facts-flow-forward. Fix: align all 5 Pass-condition / closure-predicate locations to the faithful-modeling criterion ratified in Q-MachineConstraint sub-decision 5: - docs/r3-program-plan.md:74 (gate #60 Pass condition in §1.4 ledger): "Gate Pass = concept faithfully modeled (per Brian directive 2026-05-06) — once substrate carries algebra + machine-constraint as independent composing axes with .dag-generated interaction substrate, all valid pairs work by construction. Minimum existence-proof evidence: 3 pairs lower without v2-fallback (evidence, not target)." - docs/r3-program-plan.md:257 (§1.8 canonical ledger row): "concept faithfully modeled... min existence-proof = Int<64>/Real<64>/Nat<8> lower without v2-fallback (evidence, not target)" - docs/r3-program-plan.md:430 (§1.4 Class 1 representative gap-test): "Representative gap-test (minimum existence-proof, NOT target) — substrate faithfully modeling algebra + machine-constraint separation IS the closure criterion; the 3 pairs below are the minimum existence-proof" - docs/r3-structure.md:173 (canonical gate description): "Pass condition: concept faithfully modeled... Minimum existence-proof evidence (not closure target): 3 pairs lower without v2-fallback" - docs/r3-design-schedule-2026-05-06.md:60 (S3 closure predicate cite): "Pass = concept faithfully modeled... 3-pair set is minimum existence-proof evidence, NOT the closure target" Sub-decision 5 explanatory text retains "≥3 pairs land" as anti-reference to the prior phrasing for traceability of the change. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): apply 2 claude APPROVE-with-observations precisions on Q-MachineConstraint Claude review at sha e1ea7cf (post-BLOCKING-fix) APPROVE with two exploratory observations. Both worth applying: 1. Sub-decision 3: clarify Compose<...> elaboration vs interaction substrate. Sub-decision 2 says the *interaction substrate* (composition/projection/ coercion machinery) is .dag-generated, not the Compose<...> type itself. Avoid an S3 worker reading "the Compose type is generated." 2. Closure predicate: explicit note that §1.4 conjunctive-closure rule still binds. Sub-decision 5 narrows what counts as Pass (concept faithfully modeled, not pair-counting), but does NOT relax the conjunctive form (representative gap-test executes AND class-bridge enumeration = 0). Both are tightening clarifications; no disposition change. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…s unification (post-#1817) (#1821) * docs(r3): Q-MachineConstraint-Carrier RATIFIED — universal substrate + 5 PM defaults (Brian directive) Brian directive 2026-05-06: "universal substrate, ratify defaults". Resolves Q-MachineConstraint-Carrier (was OPEN per r3-program-plan.md §10.3) with 6 sub-decisions ratified: 1. Axes in R3 scope: MachineWidth<bits> only. RegisterClass<R> / EndianMode<E> / alignment / signedness-as-axis deferred post-R3. 2. Interaction substrate shape: parametric Compose<Algebra, MachineConstraint> type-level construction. Closed-enumeration lookup-maps rejected (bridges). 3. Type-level spelling: Int<64> = Compose<AbelianGroup, MachineWidth<64>> parametrically. Equivalent under both algebra-side options per PR #1815. 4. Approximate-algebra layering: algebra approx + machine approx are independent composing axes. Real<64> = Compose<ApproximateField<Rational>, MachineWidth<64>> carries both layers per S8 discipline. 5. Class 1 demonstration breadth: ≥3 algebra×constraint pairs is minimum, not target. Broader coverage follows automatically once parser handles generic interaction syntax. 6. Target-specificity: MachineConstraint<C> is UNIVERSAL substrate (Brian directive). Every target carries machine-constraint facts as substrate; targets lacking native machine-width semantics (Python int/float) handle omission at Grounding-level discharge — target-conditioned lowering, NOT target-conditioned substrate. Substrate Mgr S3 dispatch unblocked on machine-constraint side; independent of T-Numeric-Construction algebra-side Option A vs B selection per PR #1815 (interaction semantics carries through under either). Updates: - docs/r3-program-plan.md §10.3 Q-MachineConstraint-Carrier row: OPEN → RATIFIED 2026-05-06 with all 6 sub-decisions named. - docs/r3-design-schedule-2026-05-06.md §S3: drops "open scope" framing; explicit ratified-scope block citing the 6 decisions; S3 dispatch noted as unblocked on machine-constraint side. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): Q-MachineConstraint sub-decisions 1/2/5/6 elaborated per Brian clarifying inline Brian clarifying directive 2026-05-06 on the 6 sub-decisions: 1. AXES — accept MachineWidth<bits> only; add separation-of-facts/concerns discipline note: algebra/machine-constraint/target-lowering are distinct axes. Integer modeling is the canonical exercise. 2. INTERACTION SHAPE (revised from "parametric Compose<...>" framing): "these models interact a la rest apis interacting — scalable / no dual representations (.dag generated)". The interaction substrate is .dag-DECLARED + .dag-GENERATED, never hand-coded. Hard constraint: no dual representations — any Rust counterpart must be generated, never hand-maintained (feedback_isomorphism_or_generation_for_mirrors + feedback_no_generated_code_on_disk). 3. SPELLING — Compose<AbelianGroup, MachineWidth<64>> ratified ("ok fine"). Note added: the interaction substrate elaborating Compose<...> is .dag-generated per sub-decision 2. 4. LAYERING — independent composing axes ratified ("ok fine"). Real<64> = Compose<ApproximateField<Rational>, MachineWidth<64>> stays. 5. DEMONSTRATION BREADTH — strengthened: "3 is not a target, we shouldn't be 'targeting' modeling, we are just doing our best job to faithfully represent the concepts". Closure criterion is "concept is faithfully modeled", not "≥3 pairs land". 3-pair demonstration is minimum existence proof, not closure target. 6. TARGET-SPECIFICITY — universal substrate stays. Python lowering uses faithful target-available primitives (numpy.uint8 / ctypes.c_uint8 / explicit literal-bits), NOT omission. "if python lacks — we would have to actually represent the struct using something that python faithfully provides — i.e. either literal bits or otherwise". Faithful representation > target-conditioned omission. Updates docs/r3-program-plan.md §10.3 Q-MachineConstraint-Carrier row + docs/r3-design-schedule-2026-05-06.md §S3 ratified-scope block to reflect clarifying inline. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): closure predicate aligned to faithful-modeling criterion (openai-pro BLOCKING fix) openai-pro REQUEST_CHANGES at sha 8f5483b on PR #1817 caught a real internal inconsistency: ratification text said "Faithful representation of the concept is the closure criterion; pair-counting is not" but the actual closure predicates across r3-structure.md / r3-program-plan.md / r3-design-schedule-2026-05-06.md still phrased Pass as "≥3 pairs emit to target primitives". This violated single-authority + facts-flow-forward. Fix: align all 5 Pass-condition / closure-predicate locations to the faithful-modeling criterion ratified in Q-MachineConstraint sub-decision 5: - docs/r3-program-plan.md:74 (gate #60 Pass condition in §1.4 ledger): "Gate Pass = concept faithfully modeled (per Brian directive 2026-05-06) — once substrate carries algebra + machine-constraint as independent composing axes with .dag-generated interaction substrate, all valid pairs work by construction. Minimum existence-proof evidence: 3 pairs lower without v2-fallback (evidence, not target)." - docs/r3-program-plan.md:257 (§1.8 canonical ledger row): "concept faithfully modeled... min existence-proof = Int<64>/Real<64>/Nat<8> lower without v2-fallback (evidence, not target)" - docs/r3-program-plan.md:430 (§1.4 Class 1 representative gap-test): "Representative gap-test (minimum existence-proof, NOT target) — substrate faithfully modeling algebra + machine-constraint separation IS the closure criterion; the 3 pairs below are the minimum existence-proof" - docs/r3-structure.md:173 (canonical gate description): "Pass condition: concept faithfully modeled... Minimum existence-proof evidence (not closure target): 3 pairs lower without v2-fallback" - docs/r3-design-schedule-2026-05-06.md:60 (S3 closure predicate cite): "Pass = concept faithfully modeled... 3-pair set is minimum existence-proof evidence, NOT the closure target" Sub-decision 5 explanatory text retains "≥3 pairs land" as anti-reference to the prior phrasing for traceability of the change. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): apply 2 claude APPROVE-with-observations precisions on Q-MachineConstraint Claude review at sha e1ea7cf (post-BLOCKING-fix) APPROVE with two exploratory observations. Both worth applying: 1. Sub-decision 3: clarify Compose<...> elaboration vs interaction substrate. Sub-decision 2 says the *interaction substrate* (composition/projection/ coercion machinery) is .dag-generated, not the Compose<...> type itself. Avoid an S3 worker reading "the Compose type is generated." 2. Closure predicate: explicit note that §1.4 conjunctive-closure rule still binds. Sub-decision 5 narrows what counts as Pass (concept faithfully modeled, not pair-counting), but does NOT relax the conjunctive form (representative gap-test executes AND class-bridge enumeration = 0). Both are tightening clarifications; no disposition change. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): codex BLOCKING fix — Compose<concept, MachineWidth<...>> not Compose<witness, ...> Codex BLOCKING at sha 8099ace on PR #1817 caught a real type-level error: Compose<AbelianGroup, MachineWidth<64>> composes the *algebra witness shape* rather than the integer carrier. Per dsl/std/algebra.dag:148-150: "T = GroupCompletion<M> is the carrier; AbelianGroup<T> carries op/identity/inverse over that carrier" AbelianGroup<T> is a witness shape generic over carrier T, not a carrier constructor. The bare AbelianGroup (without args) is just the kind/ constructor — putting it in Compose<...> slot-1 doesn't yield an integer carrier. Correct form: first slot of Compose<...> holds the **algebraic concept** (the fully-applied carrier+witness composite that IS the Int / UInt / Real / Nat type), second slot holds the machine-constraint: - Int<64> = Compose<Int, MachineWidth<64>> (Int = AbelianGroup<GroupCompletion<Nat>> per #1466) - UInt<64> = Compose<UInt, MachineWidth<64>> (UInt = CommutativeMonoid<Nat> per #1818) - Real<64> = Compose<Real, MachineWidth<64>> (Real = ApproximateField<Rational>) - Nat<8> = Compose<Nat, MachineWidth<8>> Updates sub-decision 3 (type-level spelling) + sub-decision 4 (approximate- algebra layering) in both r3-design-schedule-2026-05-06.md §S3 and r3-program-plan.md §10.3 Q-MachineConstraint-Carrier row. Wrong-form references retained as anti-references only ("prior phrasing was wrong"; critical correction note + dsl/std/algebra.dag citation). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): flag Python width-lowering divergence with design-numeric-construction.md (codex non-blocking) Codex non-blocking improvement at sha 83be121: sub-decision 6's Python faithful-lowering directive (numpy.uint8 / ctypes.c_uint8 / literal-bits) competes with the existing default at docs/design-numeric-construction.md: 194-198 which lowers Nat<N> for any N to plain Python int with size-hint metadata (width-omission default). Brian's directive ("represent the struct using something that python faithfully provides") shifts the standing default to faithful concrete representation, but the existing design doc isn't updated yet. Fix: explicit "Tracked divergence" callout in sub-decision 6 (both r3-design- schedule.md §S3 and r3-program-plan.md §10.3 row). Routes reconciliation to T-Numeric-Construction / Grounding lane paydown — update design-numeric-construction.md Python row when the Grounding-side per-target lowering authority lands. Not bundled in this PR per scope; the divergence is tracked-not-silent. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): sub-decision 6 unified with cost lens — universal faithful representation, cost as discriminator (Brian directive) Brian directive 2026-05-06 elaborated 2x: "basically this would be represented by cost right - in all cases we should be able to represent the structure with literal bits/objects or whatever - the cost would be enormous - in those cases, we would look for alternatives like better modeling/libraries/int & 0xFF" This unifies sub-decision 6 with T-CostLens-Composition: faithful representation is universal (every target CAN represent every concept, literal-bits is the always-available floor); the cost lens is the discriminator that orders the alternatives. Reframing: - Universality of faithful representation: every target carries every concept faithfully (literal-bits as the floor) - Cost lens (T-CostLens-Composition gates cost_lens_reads_target_realization + coercion_cost_equals_complexity_by_construction) reads per-primitive realization cost from target language spec - Grounding selects the lowest-cost faithful representation by reading cost-lens output - For Python u8: cost-tier 1 = numpy.uint8 (low cost), cost-tier 2 = ctypes.c_uint8 (medium), cost-tier 3 = int & 0xFF discipline (universal floor, high cost). All three faithful; cost lens orders. Implication: existing docs/design-numeric-construction.md:194-198 Python row (Nat<N> → int with size-hint metadata) is NON-FAITHFUL — drops width structure to opaque metadata, cost lens cannot read what isn't there. Reframe routes to T-Numeric-Construction / Grounding lane paydown: replace with cost-tiered faithful-representation table. This is the structurally-elegant unification: faithful-representation universality + cost-lens-as-discriminator. Sub-decision 6 IS an instance of "coercion cost = complexity by construction" thesis (T-CostLens-Composition load-bearing claim). Updates both r3-design-schedule-2026-05-06.md §S3 and r3-program-plan.md §10.3 Q-MachineConstraint-Carrier row sub-decision 6. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…-06 (#1824) * docs(r3): Q-MachineConstraint-Carrier RATIFIED — universal substrate + 5 PM defaults (Brian directive) Brian directive 2026-05-06: "universal substrate, ratify defaults". Resolves Q-MachineConstraint-Carrier (was OPEN per r3-program-plan.md §10.3) with 6 sub-decisions ratified: 1. Axes in R3 scope: MachineWidth<bits> only. RegisterClass<R> / EndianMode<E> / alignment / signedness-as-axis deferred post-R3. 2. Interaction substrate shape: parametric Compose<Algebra, MachineConstraint> type-level construction. Closed-enumeration lookup-maps rejected (bridges). 3. Type-level spelling: Int<64> = Compose<AbelianGroup, MachineWidth<64>> parametrically. Equivalent under both algebra-side options per PR #1815. 4. Approximate-algebra layering: algebra approx + machine approx are independent composing axes. Real<64> = Compose<ApproximateField<Rational>, MachineWidth<64>> carries both layers per S8 discipline. 5. Class 1 demonstration breadth: ≥3 algebra×constraint pairs is minimum, not target. Broader coverage follows automatically once parser handles generic interaction syntax. 6. Target-specificity: MachineConstraint<C> is UNIVERSAL substrate (Brian directive). Every target carries machine-constraint facts as substrate; targets lacking native machine-width semantics (Python int/float) handle omission at Grounding-level discharge — target-conditioned lowering, NOT target-conditioned substrate. Substrate Mgr S3 dispatch unblocked on machine-constraint side; independent of T-Numeric-Construction algebra-side Option A vs B selection per PR #1815 (interaction semantics carries through under either). Updates: - docs/r3-program-plan.md §10.3 Q-MachineConstraint-Carrier row: OPEN → RATIFIED 2026-05-06 with all 6 sub-decisions named. - docs/r3-design-schedule-2026-05-06.md §S3: drops "open scope" framing; explicit ratified-scope block citing the 6 decisions; S3 dispatch noted as unblocked on machine-constraint side. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): Q-MachineConstraint sub-decisions 1/2/5/6 elaborated per Brian clarifying inline Brian clarifying directive 2026-05-06 on the 6 sub-decisions: 1. AXES — accept MachineWidth<bits> only; add separation-of-facts/concerns discipline note: algebra/machine-constraint/target-lowering are distinct axes. Integer modeling is the canonical exercise. 2. INTERACTION SHAPE (revised from "parametric Compose<...>" framing): "these models interact a la rest apis interacting — scalable / no dual representations (.dag generated)". The interaction substrate is .dag-DECLARED + .dag-GENERATED, never hand-coded. Hard constraint: no dual representations — any Rust counterpart must be generated, never hand-maintained (feedback_isomorphism_or_generation_for_mirrors + feedback_no_generated_code_on_disk). 3. SPELLING — Compose<AbelianGroup, MachineWidth<64>> ratified ("ok fine"). Note added: the interaction substrate elaborating Compose<...> is .dag-generated per sub-decision 2. 4. LAYERING — independent composing axes ratified ("ok fine"). Real<64> = Compose<ApproximateField<Rational>, MachineWidth<64>> stays. 5. DEMONSTRATION BREADTH — strengthened: "3 is not a target, we shouldn't be 'targeting' modeling, we are just doing our best job to faithfully represent the concepts". Closure criterion is "concept is faithfully modeled", not "≥3 pairs land". 3-pair demonstration is minimum existence proof, not closure target. 6. TARGET-SPECIFICITY — universal substrate stays. Python lowering uses faithful target-available primitives (numpy.uint8 / ctypes.c_uint8 / explicit literal-bits), NOT omission. "if python lacks — we would have to actually represent the struct using something that python faithfully provides — i.e. either literal bits or otherwise". Faithful representation > target-conditioned omission. Updates docs/r3-program-plan.md §10.3 Q-MachineConstraint-Carrier row + docs/r3-design-schedule-2026-05-06.md §S3 ratified-scope block to reflect clarifying inline. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): closure predicate aligned to faithful-modeling criterion (openai-pro BLOCKING fix) openai-pro REQUEST_CHANGES at sha 8f5483b on PR #1817 caught a real internal inconsistency: ratification text said "Faithful representation of the concept is the closure criterion; pair-counting is not" but the actual closure predicates across r3-structure.md / r3-program-plan.md / r3-design-schedule-2026-05-06.md still phrased Pass as "≥3 pairs emit to target primitives". This violated single-authority + facts-flow-forward. Fix: align all 5 Pass-condition / closure-predicate locations to the faithful-modeling criterion ratified in Q-MachineConstraint sub-decision 5: - docs/r3-program-plan.md:74 (gate #60 Pass condition in §1.4 ledger): "Gate Pass = concept faithfully modeled (per Brian directive 2026-05-06) — once substrate carries algebra + machine-constraint as independent composing axes with .dag-generated interaction substrate, all valid pairs work by construction. Minimum existence-proof evidence: 3 pairs lower without v2-fallback (evidence, not target)." - docs/r3-program-plan.md:257 (§1.8 canonical ledger row): "concept faithfully modeled... min existence-proof = Int<64>/Real<64>/Nat<8> lower without v2-fallback (evidence, not target)" - docs/r3-program-plan.md:430 (§1.4 Class 1 representative gap-test): "Representative gap-test (minimum existence-proof, NOT target) — substrate faithfully modeling algebra + machine-constraint separation IS the closure criterion; the 3 pairs below are the minimum existence-proof" - docs/r3-structure.md:173 (canonical gate description): "Pass condition: concept faithfully modeled... Minimum existence-proof evidence (not closure target): 3 pairs lower without v2-fallback" - docs/r3-design-schedule-2026-05-06.md:60 (S3 closure predicate cite): "Pass = concept faithfully modeled... 3-pair set is minimum existence-proof evidence, NOT the closure target" Sub-decision 5 explanatory text retains "≥3 pairs land" as anti-reference to the prior phrasing for traceability of the change. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): apply 2 claude APPROVE-with-observations precisions on Q-MachineConstraint Claude review at sha e1ea7cf (post-BLOCKING-fix) APPROVE with two exploratory observations. Both worth applying: 1. Sub-decision 3: clarify Compose<...> elaboration vs interaction substrate. Sub-decision 2 says the *interaction substrate* (composition/projection/ coercion machinery) is .dag-generated, not the Compose<...> type itself. Avoid an S3 worker reading "the Compose type is generated." 2. Closure predicate: explicit note that §1.4 conjunctive-closure rule still binds. Sub-decision 5 narrows what counts as Pass (concept faithfully modeled, not pair-counting), but does NOT relax the conjunctive form (representative gap-test executes AND class-bridge enumeration = 0). Both are tightening clarifications; no disposition change. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): codex BLOCKING fix — Compose<concept, MachineWidth<...>> not Compose<witness, ...> Codex BLOCKING at sha 8099ace on PR #1817 caught a real type-level error: Compose<AbelianGroup, MachineWidth<64>> composes the *algebra witness shape* rather than the integer carrier. Per dsl/std/algebra.dag:148-150: "T = GroupCompletion<M> is the carrier; AbelianGroup<T> carries op/identity/inverse over that carrier" AbelianGroup<T> is a witness shape generic over carrier T, not a carrier constructor. The bare AbelianGroup (without args) is just the kind/ constructor — putting it in Compose<...> slot-1 doesn't yield an integer carrier. Correct form: first slot of Compose<...> holds the **algebraic concept** (the fully-applied carrier+witness composite that IS the Int / UInt / Real / Nat type), second slot holds the machine-constraint: - Int<64> = Compose<Int, MachineWidth<64>> (Int = AbelianGroup<GroupCompletion<Nat>> per #1466) - UInt<64> = Compose<UInt, MachineWidth<64>> (UInt = CommutativeMonoid<Nat> per #1818) - Real<64> = Compose<Real, MachineWidth<64>> (Real = ApproximateField<Rational>) - Nat<8> = Compose<Nat, MachineWidth<8>> Updates sub-decision 3 (type-level spelling) + sub-decision 4 (approximate- algebra layering) in both r3-design-schedule-2026-05-06.md §S3 and r3-program-plan.md §10.3 Q-MachineConstraint-Carrier row. Wrong-form references retained as anti-references only ("prior phrasing was wrong"; critical correction note + dsl/std/algebra.dag citation). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): flag Python width-lowering divergence with design-numeric-construction.md (codex non-blocking) Codex non-blocking improvement at sha 83be121: sub-decision 6's Python faithful-lowering directive (numpy.uint8 / ctypes.c_uint8 / literal-bits) competes with the existing default at docs/design-numeric-construction.md: 194-198 which lowers Nat<N> for any N to plain Python int with size-hint metadata (width-omission default). Brian's directive ("represent the struct using something that python faithfully provides") shifts the standing default to faithful concrete representation, but the existing design doc isn't updated yet. Fix: explicit "Tracked divergence" callout in sub-decision 6 (both r3-design- schedule.md §S3 and r3-program-plan.md §10.3 row). Routes reconciliation to T-Numeric-Construction / Grounding lane paydown — update design-numeric-construction.md Python row when the Grounding-side per-target lowering authority lands. Not bundled in this PR per scope; the divergence is tracked-not-silent. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): sub-decision 6 unified with cost lens — universal faithful representation, cost as discriminator (Brian directive) Brian directive 2026-05-06 elaborated 2x: "basically this would be represented by cost right - in all cases we should be able to represent the structure with literal bits/objects or whatever - the cost would be enormous - in those cases, we would look for alternatives like better modeling/libraries/int & 0xFF" This unifies sub-decision 6 with T-CostLens-Composition: faithful representation is universal (every target CAN represent every concept, literal-bits is the always-available floor); the cost lens is the discriminator that orders the alternatives. Reframing: - Universality of faithful representation: every target carries every concept faithfully (literal-bits as the floor) - Cost lens (T-CostLens-Composition gates cost_lens_reads_target_realization + coercion_cost_equals_complexity_by_construction) reads per-primitive realization cost from target language spec - Grounding selects the lowest-cost faithful representation by reading cost-lens output - For Python u8: cost-tier 1 = numpy.uint8 (low cost), cost-tier 2 = ctypes.c_uint8 (medium), cost-tier 3 = int & 0xFF discipline (universal floor, high cost). All three faithful; cost lens orders. Implication: existing docs/design-numeric-construction.md:194-198 Python row (Nat<N> → int with size-hint metadata) is NON-FAITHFUL — drops width structure to opaque metadata, cost lens cannot read what isn't there. Reframe routes to T-Numeric-Construction / Grounding lane paydown: replace with cost-tiered faithful-representation table. This is the structurally-elegant unification: faithful-representation universality + cost-lens-as-discriminator. Sub-decision 6 IS an instance of "coercion cost = complexity by construction" thesis (T-CostLens-Composition load-bearing claim). Updates both r3-design-schedule-2026-05-06.md §S3 and r3-program-plan.md §10.3 Q-MachineConstraint-Carrier row sub-decision 6. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): Q-PAFS Path A ACCEPTED — Brian Director countersignature 2026-05-06 Per Brian directive 2026-05-06: "approved path A countersign". Resolves three bundled §10.3 questions to ACCEPTED: - Q-PAFS: TC1 first slice = static representative via E6-G1.a (Path A); Path B (TC1 generic G1.b/X1.b) deferred; Path C (RustDagIsomorphism before TC1) deferred under Q-PAFS default. - Q-Pattern-A-First-Slice-Subscope: G1.a static representative ratified; TC1-generic via X1.b S1/S3 + G1.b deferred-not-blocked. - Q-EVAL-Lens-Fold-First-Slice: G1.a first-slice shape locked for Evaluator E3 sequencing. Implementation dispatch unblocked simultaneously across two lanes (same release step): - Verification V1 — Pattern-A executable cluster, TC1 first slice - Evaluator E3 — E6-G1.a static lens fold Both Mgrs (cool-owl-579 #1740, merry-gull-128 #1743) author worker briefs and dispatch in same release step. Substrate/evaluator carrier-shape changes remain STOP+PING until routed implementation PRs land — ACCEPTED closes the policy-layer scope fork (which slice first), not the substrate routing. Updates: - docs/r3-program-plan.md §10.3: Q-PAFS / Q-Pattern-A-First-Slice-Subscope / Q-EVAL-Lens-Fold-First-Slice rows from PENDING DIRECTOR COUNTERSIGNATURE to ACCEPTED 2026-05-06 (Path A / G1.a). - docs/r3-design-schedule-2026-05-06.md §V1 + §E3: dispatch trigger updated from "pending Director countersignature" to "DISPATCH UNBLOCKED 2026-05-06" with cross-references to the bundled gate. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Promotes 4 §1.8 rows with PR-evidence on main. PB Mgr post-merge ledger-receipt sync per Director ratification at gunbc#828 (c#4415884211; same pattern as PR #2399). Promotions: - #6 lens_testgen_dot_rs_retired DECLARED -> CONSUMER_LANDED + PASSING (PR #2392 producer + PR #2594 regression-guard; lens_testgen.rs absent on disk; consumer-side ratchet test landed) - #33 bridge_canonical_lens_name_dispatch_retired DECLARED -> CONSUMER_LANDED (PR #2449) - #34 bridge_include_str_side_channels_retired DECLARED -> CONSUMER_LANDED (slice scope) (PR #2459 pipeline.dag slice; standalone closure brief #1976 STOP-BLOCKED on Substrate T1) - #66 lens_producer_retirement_executable_witness Notes-update only (PR #2595 substrate-impl landed: TestRunner executes .dag PB census claim and reports residual; closure-receipt remains F3-DEFERRED per PB Mgr disposition) Excluded (out of charter): - #31 -> Substrate (#2068) - #36 -> Verification (#2075) Excluded (T-V2-Retirement HELD on PM-authored S-1 brief #1974): - #41 / #42 / #60 / #71 Pre-authored brief at docs/briefs/r3-pb-status-drift-sweep-post-tlp.md covers the post-T-LP cascade wave (G5/G7/G8). Closes PB Mgr drift-sweep obligation for already-merged evidence; G5/G7/G8 remain queued per pre-authored brief. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…2631) * docs(audit): land R-3 + R-7 ratifications (T-Tier3 perf budget) §5.1 designation in canonical-bench-host-decision-matrix: Option A ubicloud-standard-2 ratified 2026-05-08 per PB Manager (warm-dove-618); Director ratification at gunbc#828 c#4403509523. §2 capture procedure: multi-run discipline addendum — N=5 preferred, median-of-medians for median_ns, max-p99-across-runs for p99_ns, per-run intermediates committed alongside final tier3_baseline.json. Both lines unblock #2204 slice dispatch (Substrate-side PerfWithinBaseline variant + PerfBaselineMeasurement carrier); PB consumer slice queues post-#2204 land. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * PB Item 5 brief — encode substrate disposition (#2068 P1 RATIFIED) Substrate Mgr (warm-wolf-698) ratified §7.3 disposition at gunbc#2068 c#4411574142: shape (b) CensusSubsetCount filter with closed predicate BinShimFilesSubsetPredicate, mirroring existing LensProducerFilesSubsetPredicate precedent. Per feedback_strict_mirror_vs_novel_substrate_fact, strict-mirror ratifies directly (no canvas needed). Updates r3-pb-binshim-retirement-worker.md: - New §"Substrate landings (locked shape)" with the 4 required artifacts (substrate marker type + value, runtime predicate body, dispatch branch). - §7.3 acceptance now authorable; locked TestClaim shape recorded. - Dispatch precondition (5): unauthorable → RESOLVED. - STOP condition: §7.3 disposition not-yet-live → drift-detection. - Status header: PROPOSAL → READY-FOR-DISPATCH posture (pending only the standard R2/R2-Evaluator close signal; both Item-4 sub-gates met via PR #2282 / #2227 close). Bin-shim file inventory at main 5a13ed8: 9 files in src/v3/compiler/src/bin/; closure when CensusSubsetCount predicate count == 0. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: R3 PB Mgr — lane through R3 close * brief: clarify §7.3 TestClaim is zero-only (not schedule-bound) Addresses non-blocking improvement on PR #2334 (codex review sha=68977425): the prior wording called CensusSubsetCount a schedule-bound gate, but the runtime predicate (test_runner.rs:3290-3296) is zero-only — Pass iff count==0. Interim per-PR shrink receipts are PR-level milestones outside this TestClaim, not TestClaim verdicts. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * brief: reconcile §"Substrate landings" with Non-goals (PB strict-mirror authoring authorized post-#2068) Addresses non-blocking improvement on PR #2334 (codex review sha=363cf799): the new §"Substrate landings (locked shape)" worker-owned list contradicted the unchanged "out of scope" entries that still said PB lane does not author §7.3 substrate shape. Resolution: per #2068 c#4411574142 ratification + feedback_strict_mirror_vs_ novel_substrate_fact, strict-mirror declarations (mirroring the existing LensProducerFilesSubsetPredicate precedent) are PB-lane-authorable. The non-goal still applies to *novel* shape (extra fields, alternative coproducts) which would re-escalate to Substrate Mgr. Updates: - "PB does not own and must not edit" entry (line 29): clarifies shape question is Substrate-territory but strict-mirror authoring is authorized. - Non-goals (line 155): same reconciliation; novel shape still gates back to Substrate Mgr. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * PB Item 5 follow-on brief — batch retirement for 8 remaining bin-shims Director re-task at gunbc#828 c#4413892216 Task A: author per-shim retirement worker briefs for the 9 bin-shims; 1 covered by gate #7 (warm-crab-600 working regen_lens.rs); 8 unscoped (emit_method_template_projection, r1c_e_emit_gates, regen_bootstrap, regen_parse, regen_parse_tables, regen_tokenize, regen_v3, self_host_fixed_point). This brief governs the 8-shim batch follow-on against the canonical r3-pb-binshim-retirement-worker.md template. Status PROPOSAL — dispatch-gated on: - smart-tern-649 Stage A landing (BinShimFilesSubsetPredicate carriers + runtime predicate) - warm-crab-600 gate #7 first-cut precedent on main Three staging shapes documented (mega-PR / serial-per-shim / batched-2-3); PB Mgr leans batched-by-regen-family. Worker chooses at dispatch. STOP-AND-PING conditions enumerated (substrate-carrier absent / carrier shape pressure / emit-pattern divergence / substrate-grep mismatch). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * fix-forward (PR #2471 codex REQUEST_CHANGES) Two findings addressed: 1. Carrier-shape mismatch (line 43): brief template said `name:` but the locked BinShim carrier per design-pb-runtime-interpreter.md:200-204 uses `entrypoint_name`, `description`, `entry`. P2 single-authority violation would have routed workers against wrong shape. Fixed: template now matches locked shape verbatim with explicit no-additional-fields clause. 2. Dispatch-gate dilution (lines 33, 98): brief reduced operative dispatch gate to "Stage A landing + gate #7 precedent" but parent brief enumerates 5 preconditions (R2 close + R2-Evaluator landed + Item 4 sub-gate green + BinShim carrier live + §7.3 disposition). P5 fail-closed violation. Fixed: full readiness prerequisite inherited verbatim from parent brief; gate #7 precedent demoted to implementation-pattern reference (not gate). Worker dispatch posture updated to require all 5 preconditions verified on main at dispatch time per feedback_substrate_grep_before_authoring. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: R3 PB Mgr — lane through R3 close * docs(r3): §1.8 ledger Status drift sweep — post-T-LP / T-Bridge wave Promotes 4 §1.8 rows with PR-evidence on main. PB Mgr post-merge ledger-receipt sync per Director ratification at gunbc#828 (c#4415884211; same pattern as PR #2399). Promotions: - #6 lens_testgen_dot_rs_retired DECLARED -> CONSUMER_LANDED + PASSING (PR #2392 producer + PR #2594 regression-guard; lens_testgen.rs absent on disk; consumer-side ratchet test landed) - #33 bridge_canonical_lens_name_dispatch_retired DECLARED -> CONSUMER_LANDED (PR #2449) - #34 bridge_include_str_side_channels_retired DECLARED -> CONSUMER_LANDED (slice scope) (PR #2459 pipeline.dag slice; standalone closure brief #1976 STOP-BLOCKED on Substrate T1) - #66 lens_producer_retirement_executable_witness Notes-update only (PR #2595 substrate-impl landed: TestRunner executes .dag PB census claim and reports residual; closure-receipt remains F3-DEFERRED per PB Mgr disposition) Excluded (out of charter): - #31 -> Substrate (#2068) - #36 -> Verification (#2075) Excluded (T-V2-Retirement HELD on PM-authored S-1 brief #1974): - #41 / #42 / #60 / #71 Pre-authored brief at docs/briefs/r3-pb-status-drift-sweep-post-tlp.md covers the post-T-LP cascade wave (G5/G7/G8). Closes PB Mgr drift-sweep obligation for already-merged evidence; G5/G7/G8 remain queued per pre-authored brief. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(briefs): fix gate #64 → #66 mislabel in drift-sweep brief Per cursor/composer-2 review on PR #2631: brief table + dispatch-trigger parenthetical labeled lens_producer_retirement_executable_witness as gate #64. Authoritative §1.8 row is #66; #64 is substrate_gap_reflection_closure_closed (separate predicate). Aligns brief with r3-program-plan.md §1.8 row identity per INVARIANTS.md P1 (single authoritative facts). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): row #66 DECLARED → CONSUMER_LANDED per §1.7 taxonomy Per codex/codex-default review on PR #2631 (REQUEST_CHANGES, review 9150): leaving row #66 at DECLARED while the Notes cell describes an executable consumer that runs through TestRunner contradicts the §1.7 status taxonomy and INVARIANTS P2 single-authority discipline. Promoting #66 to CONSUMER_LANDED with explicit PASSING gate on residual = 0 (cascades from T-LensProducer-Retirement gates #5 + #6 + #7). The F3 deferral is on PASSING, not CONSUMER_LANDED; the executable receipt src/v3/compiler/tests/integration/r3_lens_producer_retirement_executable_witness_test.rs already exists and runs the .dag PB census claim through TestRunner. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…tax (gate #60) Add SurfaceType::PhantomWidthLit, parse numeric type args per S3 Phase-2, lower Algebra<N> / MachineWidth<N> to Compose<Algebra, MachineWidth<Word*>> for the canonical R3 bit widths. Integration receipt covers Int<64>, Real<64>, Nat<8>. Refresh handwritten parse corpus manifest. Co-authored-by: Cursor <cursoragent@cursor.com>
INTERNAL __phantom_* UnresolvedIdentifier stubs tripped resolve_pending_identifiers_strict after the authoritative unsupported-width diagnostic. Lowering now reuses prelude Bool by declaration id instead. Adds regression asserting no stray ResolveErrors on gate #60 negatives. Co-authored-by: Cursor <cursoragent@cursor.com>
Adds assert_phantom_machine_width_lit_lowers_to_word plus happy-path fixture Gate60_MachineWidth128_Lit addressing openai-pro APPROVE_WITH_COMMENTS test gap (distinct lowering branch). Co-authored-by: Cursor <cursoragent@cursor.com>
Matches TESTING.md guidance: pin Diagnostic::ParseError + source slice for the offending literal and file binding, instead of message().contains full strings. Co-authored-by: Cursor <cursoragent@cursor.com>
Fail-closed ParseError if peek/bump mismatch; regen_parse. Addresses review feedback on hiding panic surface in gate #60 phantom width atom parsing. Co-authored-by: Cursor <cursoragent@cursor.com>
AtomTypePolicy was retired; phantom magnitudes are gated via SurfaceTypeArg and parse_generic_type_arg. Co-authored-by: Cursor <cursoragent@cursor.com>
…tion (#2767) * docs(r3): gate-60 substrate_gap_parser_grammar_closed scope decomposition Decomposes gate #60 into 6 named work-slices (A: Word8 carrier, B: Nat8 alias, C: parser desugar [brief already authored], D: class-bridge=0 receipt, E: 3-pair existence-proof demo, F: v2-oracle parity). Maps each slice to owner-role + Mgr authority + brief status; flags PB Mgr role unfilled for Slice F and recommends PM escalation. No code change. Authoring node: adhoc-e48c09a4-8d9 (bold-heron-632). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): reconcile gate-60 decomposition with on-main Byte/UInt8 + ratified MachineWidth<N> Address codex BLOCKING review on PR #2767: - Withdraw Slice A (Word8): Byte already defines the 8-bit carrier at dsl/std/bit.dag:26; Word8 would introduce parallel authority (P1). - Withdraw Slice B (Nat8 alias): Int8/UInt8 already on main at dsl/std/integer.dag:45,52; with UInt = Nat (line 148), Nat<8> substrate is structurally UInt8. - Retarget Slice C from MachineWidth<WordN> to literal-Nat MachineWidth<N> per Q-MC sub-decision 3 ratified spelling (gunbc#828 #issuecomment-4385530115). - Add Slice Z: retire IntW*/UIntW* aliases and MachineWidth<WordN> slot-2 spellings per the in-substrate named dissolution trigger at dsl/std/integer.dag:71-78. Without Z, gate-60 would Pass against a substrate carrying two slot-2 spellings (P2 dual-authority). - Refresh dependency graph + routing table accordingly. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): correct line citations in gate-60 decomposition Address cursor APPROVE_WITH_COMMENTS on PR #2767: - `type Int =` / `type UInt =` live at lines 123/124, not 147/148 (147-148 are inside the IntPlatform comment block). - Lines 45-56 hold canonical `Int8..Int128` / `UInt8..UInt128` fixed- width rows, NOT the `IntW*` / `UIntW*` aliases. Aliases are at 79-84. - Split the table row accordingly and update inline citations elsewhere in the document. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Register r3_gate_60_phase2_width_nat_parser_test.rs in the SG-0 integration test receipt table per §P5. Narrow bare-width parse assertion to the IntLit Debug discriminant (ParseError still has no stable error code). Co-authored-by: Cursor <cursoragent@cursor.com>
* WIP: substrate_gap_parser_grammar_closed * WIP: substrate_gap_parser_grammar_closed * WIP: substrate_gap_parser_grammar_closed * WIP: substrate_gap_parser_grammar_closed * WIP: substrate_gap_parser_grammar_closed * WIP: substrate_gap_parser_grammar_closed * WIP: substrate_gap_parser_grammar_closed * WIP: substrate_gap_parser_grammar_closed * WIP: substrate_gap_parser_grammar_closed * WIP: substrate_gap_parser_grammar_closed * WIP: substrate_gap_parser_grammar_closed * WIP: substrate_gap_parser_grammar_closed * WIP: substrate_gap_parser_grammar_closed * WIP: substrate_gap_parser_grammar_closed * WIP: substrate_gap_parser_grammar_closed * WIP: substrate_gap_parser_grammar_closed * style(v3): drop stray blank lines in gate-60 Parameterized lowering Cosmetic cleanup from review: keep Declaration struct literals compact in the Int<N> sugar allocation path (type_to_declaration_id). Co-authored-by: Cursor <cursoragent@cursor.com> * refactor(lower): avoid expect in Compose width-nat materialization compose_algebra_machine_width_connective now returns Option and threads template_param_id through ? so a drifted Compose template fails closed via the same Option path as other gate-60 helpers instead of panicking. Co-authored-by: Cursor <cursoragent@cursor.com> * docs: P5 receipt row for gate #60 hand-authored test (INVARIANTS) Register r3_gate_60_phase2_width_nat_parser_test.rs in the SG-0 integration test receipt table per §P5. Narrow bare-width parse assertion to the IntLit Debug discriminant (ParseError still has no stable error code). Co-authored-by: Cursor <cursoragent@cursor.com> --------- Co-authored-by: Cursor <cursoragent@cursor.com>
- dsl/std/integer.dag: fixed-width rows use MachineWidth<16|32|64|128> (8-bit stays MachineWidth<Byte>); remove IntW*/UIntW* aliases. - dsl/std/float.dag: Real32/Real64 use MachineWidth<32|64>. - Regenerate bootstrap_*_generated.rs; substrate_receipt helpers match literal-Nat phantom widths. - Integration: Real<64> lowering receipt (type alias); refactor compose-shape assertion. Class-bridge census (Slice D) and v2 parity (Slice F) remain per docs/audit/r3-gate-60-decomposition.md. Co-authored-by: Cursor <cursoragent@cursor.com>
…-Numeric-Construction + Substra) (#3102) * WIP: R3 gate #60: substrate_gap_parser_grammar_closed (T-V2-Retirement + T-Nu * WIP: R3 gate #60: substrate_gap_parser_grammar_closed (T-V2-Retirement + T-Nu * R3 gate #60: literal-Nat MachineWidth slot-2 (Slice Z) - dsl/std/integer.dag: fixed-width rows use MachineWidth<16|32|64|128> (8-bit stays MachineWidth<Byte>); remove IntW*/UIntW* aliases. - dsl/std/float.dag: Real32/Real64 use MachineWidth<32|64>. - Regenerate bootstrap_*_generated.rs; substrate_receipt helpers match literal-Nat phantom widths. - Integration: Real<64> lowering receipt (type alias); refactor compose-shape assertion. Class-bridge census (Slice D) and v2 parity (Slice F) remain per docs/audit/r3-gate-60-decomposition.md. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: R3 gate #60: substrate_gap_parser_grammar_closed (T-V2-Retirement + T-Nu * WIP: R3 gate #60: substrate_gap_parser_grammar_closed (T-V2-Retirement + T-Nu * WIP: R3 gate #60: substrate_gap_parser_grammar_closed (T-V2-Retirement + T-Nu * WIP: R3 gate #60: substrate_gap_parser_grammar_closed (T-V2-Retirement + T-Nu * fix(infer): unify literal-Nat MachineWidth phantom decls across sites bind_expected_decl_to_actual_context fell through to walk_to_type_shape for anonymous LiteralBits width atoms; walk returns None, so UInt8 arrows (Compose<UInt, MachineWidth<8>>) failed signature validation when literal ids differed. Resolve both sides, then compare literal payloads before shape identity. Tests: remove dead assert_int_value_port_resolves_to_uint8 wrapper; restore direct compile_to_dag expect for call-site harness. Co-authored-by: Cursor <cursoragent@cursor.com> --------- Co-authored-by: Cursor <cursoragent@cursor.com>
End-to-end Int<32> + Real<64> (construction syntax): infer integral literals for fixed-width reals, structural Compose→i32/f64 emit for gate-#60 sugar, rustc-friendly float literal fragment, rust.dag Real32/64 realizations + regen_bootstrap, boundary emit+rustc test. Co-authored-by: Cursor <cursoragent@cursor.com>
WF19: Generator workflow capability port (bootstrap/makegen/pragma)
WF20: Remaining tool capability port (deps/dag-viz/dag-snapshot)
WF21: Makefile thinning for all tool targets
WF22: Capability minimization verification
Integration tests verify:
https://claude.ai/code/session_01X5CzTeZdjtsAVcz696jme4