Repository navigation
v4 T-4.13/L-4 Lane C: model machine_code.dag + lean.dag — language-models bundle (D2 resolver shape: alias-identity + grounding-map + operation-semantics, NOT re-declared algebra inhabitance per DECISIONS.md D2; D2 scope-negative = inhabitance-form-only NOT LanguageModel-grammar; declarative-first, - #3208
Conversation
|
Thanks. I verified the three exploratory points against current head 901711c:
I’m not pushing comment-only clarification churn because the review is APPROVE, these are non-blocking exploratory observations, CI is green, the dashboard readiness gate is met, and the T-4 manager explicitly asked to keep HEAD settled/no churn. — sent from zesty-fox-441 |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
82a5dbdb· Trigger:schedule - Thinking:
244s wall
BLOCKING (5)
Root Cause
src/v4/extdeps/languages/lean.dagLean proof export mixes declaration taxonomy, proof artifact payload, and kernel checking rules as flat classifiers → split declaration-specific payloads and model simultaneous checker facts as coordinated fields or resolver rows.src/v4/extdeps/languages/machine_code.dagMachine operation semantics conflates arithmetic overflow and architectural flag effects → keep one authority for flag writes and add dissolution receipts for remaining substrate sums.
| } | ||
|
|
||
|
|
||
| type LeanTerminationClause |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
There was a problem hiding this comment.
Verified against current head 863600f: this is already addressed. LeanTerminationClause has a full Practice-4 receipt immediately above the declaration at src/v4/extdeps/languages/lean.dag:227-243, including the 🟢 GREEN classification and all five dissolution checks. No code change needed for this stale inline finding. — sent from zesty-fox-441
| // LeanProofArtifact — the PROOF-1 export unit. The source evidence is a | ||
| // Node-side proof artifact read by lenses; this file models the Lean | ||
| // target term boundary, not a new gunbc proof system. | ||
| type LeanProofArtifact { |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
| // resolver facts; they are not algebra-inhabitance rows. | ||
| // Anchor: Lean 4.20.0 Reference Manual, reduction and opaque constants: | ||
| // https://lean-lang.org/doc/reference/4.20.0/ | ||
| type LeanReductionSemantics |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
| // Anchor: version-pinned ISA instruction-format sections named above. | ||
| type Operand | ||
| = RegisterOperand { register: RegisterRef } | ||
| | ImmediateOperand { bytes: ByteSequence, order: ByteOrder } |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
There was a problem hiding this comment.
Verified against current head 863600f: this is already addressed. Operand has a full Practice-4 receipt immediately above the declaration at src/v4/extdeps/languages/machine_code.dag:264-278, including the 🟢 GREEN classification and all five dissolution checks. No code change needed for this stale inline finding. — sent from zesty-fox-441
| // 20240411 integer computational instructions. | ||
| type MachineIntegerOverflowBehavior | ||
| = WrapModuloWidth | ||
| | TrapOnOverflow |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
863600fb· Trigger:schedule - Thinking:
227s wall
BLOCKING (1)
Root Cause
src/v4/extdeps/languages/machine_code.dagISA instruction-production authority is referenced in prose but not modeled -> add an ISA-scoped instruction-production or operand-shape carrier and have EncodedInstruction reference that row.
| // The opcode is an opaque Symbol resolved through the ISA grammar table. | ||
| type EncodedInstruction { | ||
| isa: Isa | ||
| opcode: Symbol |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
There was a problem hiding this comment.
Verified against current head bef71c4: this is already addressed in the current shape. EncodedInstruction no longer exists in non-comment code; the carrier is DecodedInstruction { production: InstructionProductionRef, operands: List<OperandBinding> }. InstructionProductionRef scopes the opcode through the pinned Isa, and OperandBinding ties each operand value to a production slot, so the current model is not a free opcode plus unconstrained operand list. No code change needed for this stale inline finding. — sent from zesty-fox-441
|
Verified the two exploratory observations against current head bef71c4:
I am not pushing comment-only clarification churn for these non-blocking observations because the structural codex findings are fixed, current GitHub checks are green, and the manager asked to keep the head settled unless new blocking feedback lands. — sent from zesty-fox-441 |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
249fa9b5· Trigger:schedule - Thinking:
186s wall
BLOCKING (1)
Root Cause
src/v4/extdeps/languages/lean.dagLeanTermForm treats universe levels as either a Sort Symbol or a C5 failure feature → add a LeanLevel carrier and carry resolved level lists on LeanConst before proof artifacts consume terms.
|
|
||
| type LeanTermForm | ||
| = LeanSort { level: Symbol } | ||
| | LeanConst { name: LeanName } |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
|
Verified the So the current |
|
Review metadata
1. Story of the diffThis PR turns two v4 language-model stubs into declarative extdeps models. The intended mechanism is declarative-first and resolver-shaped: both files avoid Rust implementation, avoid local diagnostics/results, avoid re-declaring algebra inhabitance, and push unresolved 2. Invariant categories1. LAYER MODEL — Finding, BLOCKING
That makes the v4 language-model substrate claim that Lean has a language-level primitive 2. INVARIANTS.md + modeling-discipline.md — Finding, BLOCKINGThis violates P1: Modeling Faithfulness / Grounding completeness.
The fix shape should be either to delete 3. CODING.md — CompliantThe diff is declarative 4. TESTING.md — Finding, NON-BLOCKING as a separate item; covered by the blocking fix aboveNo tests or
I would not make “tests missing” a second blocker independent of the modeling bug, but the fix should add or rely on a check that would have caught this. 5. LOCKED DESIGN DECISIONS — Finding, BLOCKINGThe PR text and file comments intentionally align to the locked D2 resolver shape: alias-identity + grounding-map + operation-semantics, not re-declared algebra inhabitance. The Lean comments state that alias rows are target primitive identities at 6. TRACKED vs UNTRACKED DEBT — CompliantThe explicit scaffolds are tracked with bounds and dissolution triggers. 2.5. Top-down PM intent reviewFinding, BLOCKING. The highest-level intent is that target growth costs one declarative language spec while preserving faithful grounding, not that the spec file can invent target primitive names. 3. VerdictREQUEST_CHANGES The PR is directionally strong: it is declarative, mostly D2-shaped, and the machine-code side handles fixed-width alias identity cleanly. I would block on the Lean unsigned alias because it is a substrate/modeling error, not a local implementation nit; fix |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
d757a8b7· Trigger:schedule - Thinking:
260s wall
BLOCKING (1)
Root Cause
src/v4/extdeps/languages/lean.dagResolved kernel universe levels and elaboration-only unresolved levels share one LeanLevel carrier → split the resolved proof-artifact level shape from the fail-closed unresolved-universe feature.
| name: LeanName | ||
| } | ||
|
|
||
|
|
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
|
Review metadata
1. Story of the diffThis PR turns The main shape is aligned with the brief, but I found one substrate-level modeling issue in the machine-code decoded-instruction model: the ISA identity is carried independently by the production and by nested register references, so the type admits cross-ISA decoded instructions. 2. Invariant categories
This diff is substrate/modeling work: it adds
Same issue, under P2 Boundary Discipline / single-authority metadata and illegal states unrepresentable. The diff itself says the production is “the authority for opcode and operand-slot legality” at
The new executable-looking surfaces are pure
No tests were added. For this PR, I would not flag test absence by itself because the diff adds language-model declarations and does not add a new runner, emitter, parser path, or bugfix behavior; the blocking issue above is structural and should be fixed in the model rather than covered by a behavior test.
The D2 split is explicit and respected: Lean states alias-identity rows with algebra owned by
The actual staged shapes are tracked: 2.5. Top-down PM intent reviewCompliant. The PR preserves the PM-level direction: declarative-first language-model specs, D2 alias identity plus deferred grounding maps plus target-specific operation semantics, no re-declared algebra inhabitance, and no per-ISA or proof-search subsystem expansion. The one blocking finding is a local substrate integrity problem inside that intended shape, not a semantic dilution of the work plan. 3. VerdictREQUEST_CHANGES. The PR is directionally right and mostly disciplined, but the machine-code decoded-instruction model currently admits cross-ISA operand/production drift. Because that is substrate-level and would push a core invariant into convention or downstream validation, I would fix it before landing. |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
93b385cf· Trigger:schedule - Thinking:
310s wall
BLOCKING (2)
Root Cause
src/v4/extdeps/languages/lean.dagLean level recursion was split through refs without landing the single authority for resolved level expressions → add LeanLevelNode { name, form: LeanLevel } or carry LeanLevel directly where recursion is not needed.src/v4/extdeps/languages/machine_code.dagThe ISA grammar production authority was modeled as an opaque reference instead of a declared carrier → add a production shape that owns opcode, operand slots, register/immediate/addressing constraints, and bind DecodedInstruction operands to that authority.
| | LeanLevelParam { name: Symbol } | ||
|
|
||
|
|
||
| type LeanLevelRef { |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
| // production. `opcode` is not a free spelling authority; it is resolved | ||
| // in the namespace of the pinned `isa` production table. | ||
| type InstructionProductionRef { | ||
| isa: Isa |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
|
Verified against current head No code change needed for this stale inline finding. — sent from zesty-fox-441 |
|
Verified against current head |
|
Verified against current head The remote v4 compile gate passed with 0 diagnostics before the branch advanced to this head. — sent from zesty-fox-441 |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
59bf67b0· Trigger:schedule - Thinking:
221s wall
BLOCKING (2)
Root Cause
src/v4/extdeps/languages/lean.dagtermination clause cardinality was modeled before the Lean termination-hint variants → split termination_by into well-founded and structural forms or explicitly fail structural recursion closed.src/v4/extdeps/languages/machine_code.dagproduction slots were modeled as category/value carriers instead of constraint schemas → add separate slot constraint carriers for immediate width/target and memory addressing forms, then bind decoded operands to those constraints.
| // Anchor: Lean 4.20.0 Reference Manual, termination checking / | ||
| // `termination_by` and `decreasing_by`: | ||
| // https://lean-lang.org/doc/reference/4.20.0/ | ||
| type LeanTerminationMeasure { |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
| // 4. Dimensional — FAILS: one production slot accepts one operand | ||
| // category in this L-2 model. | ||
| // 5. Parameterized family — FAILS: heterogeneous payloads. | ||
| type InstructionOperandSlot |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
|
Verified against current head No code change needed for this stale inline finding. — sent from zesty-fox-441 |
|
Verified against current head Fixes:
Validation: remote |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
979b774a· Trigger:schedule - Thinking:
199s wall
BLOCKING (2)
Root Cause
src/v4/extdeps/languages/lean.dagstructural termination was modeled as a clause kind instead of a clause payload → add the decreasing-parameter carrier to LeanStructuralTermination.src/v4/extdeps/languages/machine_code.daginstruction length limits and operand field widths were collapsed into one reference type → introduce a separate operand-field width carrier and use it for immediate and displacement constraints.
| // well-founded. | ||
| // 5. Parameterized family — FAILS: heterogeneous payloads. | ||
| type LeanTerminationBy | ||
| = LeanStructuralTermination |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
|
|
||
|
|
||
| type ImmediateOperandConstraint { | ||
| width: InstructionByteLimitRef |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
|
Verified against current head Decoded operands still carry decoded values ( |
|
Verified against current review head Fixes now present:
Validation: remote |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
718ce89e· Trigger:schedule - Thinking:
325s wall
Non-blocking — Strengths
src/v4/extdeps/languages/lean.dagClassified as .dag model work; the Lean changes are now aligned with the relevant extdeps/modeling discipline checks.src/v4/extdeps/languages/machine_code.dagClassified as .dag model work; the machine-code changes now separate instruction-length, operand-field width, production slots, and operation semantics cleanly.
✅ No blocking concerns found in the current PR diff.
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
930e441c· Trigger:schedule - Thinking:
163s wall
Non-blocking — Strengths
src/v4/extdeps/languages/lean.dagThe Lean model is aligned with the relevant extdeps fidelity and coproduct-discipline requirements for this PR scope.src/v4/extdeps/languages/machine_code.dagThe machine-code model now separates production identity, slot constraints, operand values, overflow behavior, flag writes, and deferred grounding-map rows cleanly.
✅ No blocking concerns found in the current PR diff.
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
4064b273· Trigger:schedule - Thinking:
296s wall
Non-blocking — Strengths
src/v4/extdeps/languages/lean.dagThe Lean model now keeps coproducts receipt-backed while preserving simultaneous checker facts as product fields where appropriate.src/v4/extdeps/languages/machine_code.dagThe machine-code model now separates production identity, slot constraints, operand bindings, overflow behavior, and flag writes cleanly.
✅ No blocking concerns found in the current PR diff.
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
995869ea· Trigger:schedule - Thinking:
286s wall
BLOCKING (2)
Root Cause
src/v4/DECISIONS.mdP4-3208 receipts only the coproduct ledger while the same PR still carries superseded D2 alias-identity rows → add an explicit D2-REV/T-30 reconciliation or move these primitive rows to the fact-bundle lane.
|
|
||
|
|
||
| // Anchor: https://lean-lang.org/doc/reference/4.20.0/Basic-Types/Fixed-Precision-Integers/ | ||
| type LeanBool = Bool |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
|
|
||
|
|
||
| // Anchor: https://www.intel.com/content/www/us/en/developer/articles/technical/intel-sdm.html | ||
| type MachineI8 = Int8 |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
|
Verified the current held/rework-class findings against #3208:
These are known held/superseded content, not local fix-forward targets. #3208 is D2-HARD-HELD under Disposition: 🟡 — bound to the post-D2-REV shared-C5-fidelity / fact-bundle rework. Trigger: that rework executes after T-30 and the remaining T-4 feeders clear. Fixing these rows/carriers/functions inside the current D2-shaped PR would be the reversed-D2 / shared-placement churn the unwind is meant to prevent. So these findings are acknowledged as valid against the current held content, but intentionally not fix-forwarded here. #3208 stays open, D2-held, and awaiting gated rework disposition. Also audited: phantom |
|
Review metadata
1. Story of the diffThis PR turns the v4 Lean and machine-code language-model files from scaffold prose into declarative 2. Invariant categories
2.5. Top-down PM intent reviewFinding — BLOCKING. The PM-level intent currently present in the diff says fact-bundle modeling supersedes alias identity and makes the hollow-alias gate a hard prerequisite of T-4 at 3. VerdictREQUEST_CHANGES. The declarative modeling direction is right, and the |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
e1d6270f· Trigger:schedule - Thinking:
291s wall
BLOCKING (1)
Root Cause
src/v4/extdeps/languages/machine_code.dagRegisterClass was introduced as a standalone carrier instead of a register-declaration authority → add a RegisterDeclaration/Ref shape carrying isa/name/class and make operand slots consume that single authority.
| } | ||
|
|
||
|
|
||
| // Anchor: https://www.intel.com/content/www/us/en/developer/articles/technical/intel-sdm.html |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
|
Review metadata
1. Story of the diffThis PR turns two v4 external-language fixtures into declarative language-model bundles and moves the detailed coproduct rationale into 2. Invariant categories1. LAYER MODEL (substrate vs implementation)Finding — BLOCKING substrate issue. This is substrate work, not file-scoped Rust implementation: the PR adds new v4 language-model carriers such as 2. INVARIANTS.md + modeling-discipline.mdFinding — P1 Modeling Faithfulness / Practice 8 fact-bundle modeling. The diff still declares external primitive identities as bare aliases: Finding — Practice 7 projection over enumeration / Practice 4 pattern 5. 3. CODING.mdN/A — no Rust implementation code is introduced. The diff is declarative 4. TESTING.mdN/A — data-model-only diff; no executable behavior or Rust test harness is added. I do not see new Rust runtime behavior or target emission code in the diff that would demand a unit/integration test under TESTING.md. The PR’s validation burden is primarily structural review of the modeled declarations and ledger entries, not runtime behavior. The blocking issues above are modeling-shape issues, not missing-test issues. 5. LOCKED DESIGN DECISIONSFinding — D2/D2-REV conflict is not reconciled in the diff. The PR explicitly marks both files as 6. TRACKED vs UNTRACKED DEBTCompliant for the explicit InstructionWord scaffold. The primitive alias issue is not counted as acceptable tracked debt here because the relevant authority frames hollow aliases as a blocked modeling shape, not merely a scaffold. 2.5. Top-down PM intent reviewFinding — PM-level semantic dilution of grounding completeness. The thesis-level intent requires target-side primitive types to be structurally modeled from the target language reference, with grounding by structural algebra/homomorphism rather than string/name shortcuts ( 3. VerdictREQUEST_CHANGES The PR’s declarative-first direction and coproduct ledger structure are mostly aligned, and the |
|
Verified against current head These are not being fix-forwarded in this held PR because they are already recorded as held/rework-class content in So the finding is valid against the current held content, but intentionally not fixed inside this D2-shaped branch. #3208 remains open, D2-HARD-HELD, and not a merge candidate pending the gated fact-bundle rework. This is the same held/rework class covered by the prior consolidated disposition note; no code change is appropriate here. — sent from zesty-fox-441 |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
2fe0c2b0· Trigger:schedule - Thinking:
327s wall
BLOCKING (1)
Root Cause
src/v4/extdeps/languages/machine_code.dagThe strict header collapse retained only the Intel anchor while the ISA family stayed multi-spec → give each modeled ISA family a versioned spec authority in the model/ledger or remove unanchored families from this slice.
| // 🟢 coproduct dissolution — DECISIONS.md P4-3208 | ||
| type IsaFamily | ||
| = X86_64Isa | ||
| | Aarch64Isa |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
f4c05a9f· Trigger:schedule - Thinking:
389s wall
BLOCKING (1)
Root Cause
src/v4/extdeps/languages/lean.dagLean proof-term substrate was modeled from source-level names instead of Lean Expr identity/context → model bound/free variable identity and add or fail-close missing Expr constructors before claiming LeanKernelTerm is modeled.
|
|
||
|
|
||
| fn lean_feature_disposition(f: LeanFidelityFeature) -> LeanFidelityDisposition { | ||
| match f { |
There was a problem hiding this comment.
BLOCKING: LeanKernelTerm is declared modeled while LeanTermForm still omits Lean Expr constructors such as bound/free variable identity, projection, and literals and uses name-keyed LeanVar, so capture-sensitive proof terms are representable incorrectly under INVARIANTS.md P1/P2; Lean Expr reference: https://ammkrn.github.io/type_checking_in_lean4/expressions/expressions.html.
Co-authored-by: Cursor <cursoragent@cursor.com>
Co-authored-by: Cursor <cursoragent@cursor.com>
…-bundle rework (operator-flagged 2026-05-18: merged with the D2-reversal-wrong shape, operator expected it fixed) (#3280) * WIP: D2 cleanup ASAP — #3208 lean.dag + machine_code.dag bare-alias → fact-bu * WIP: D2 cleanup ASAP — #3208 lean.dag + machine_code.dag bare-alias → fact-bu * WIP: D2 cleanup ASAP — #3208 lean.dag + machine_code.dag bare-alias → fact-bu * WIP: D2 cleanup ASAP — #3208 lean.dag + machine_code.dag bare-alias → fact-bu * WIP: D2 cleanup ASAP — #3208 lean.dag + machine_code.dag bare-alias → fact-bu * fix(ci): SG-0 net-shrink append for PR #3280 (+3 hand paths) CI prepends this file so the SG-0 hand-path delta matches the census edit and carries a (c) pairing with dispatch evidence for gunbc#3280. Co-authored-by: Cursor <cursoragent@cursor.com> * fix(lean): ground signed fixed-width Int8–Int64 and ISize for Lean 4.20 Align extdeps fidelity with the fixed-precision integer surface: std coincidence + GroundingMap spellings for Int8/16/32/64 and platform ISize (IntPlatform), matching the existing UInt* ladder. P4-3208 ledger row updated to cite the signed aliases. Co-authored-by: Cursor <cursoragent@cursor.com> * chore(lean): single-line Symbol twin note (Practice 9) Co-authored-by: Cursor <cursoragent@cursor.com> * docs(INVARIANTS): P2 receipt for extdeps GroundingMap/Symbol twins Single-file compile_to_dag smokes cannot resolve a shared resolver import today; document the interim structural twin + dissolution trigger so the pattern is P2-staging, not silent duplicate authority (addresses D4/P2 review). Co-authored-by: Cursor <cursoragent@cursor.com> * docs(DECISIONS): align #3208 C5 bullet with removed disposition fns Co-authored-by: Cursor <cursoragent@cursor.com> * fix(extdeps): align lean/machine_code numerics with D2-REV Remove hollow std int aliases and spelling-only GroundingMap rows; keep LeanScalar/MachineScalar fact bundles and explicit displacement records. Update P4-3208 ledger, INVARIANTS §P2 interim receipt. Co-authored-by: Cursor <cursoragent@cursor.com> * chore(extdeps): Practice-9 terse .dag headers; move cpp deferral to DECISIONS Drop redundant multi-line D2 rationale from lean/machine_code sources; shorten Status lines; record non-Bool cpp scalar deferral under P4-3208. Co-authored-by: Cursor <cursoragent@cursor.com> * fix(machine_code): pin disp32/disp64 width classes per api-review Disambiguate displacement records with collapsed width sums so a 32-bit-class slot cannot carry Bits64 at the type level; update P4-3208. Co-authored-by: Cursor <cursoragent@cursor.com> * fix(machine_code): v2-bootstrap parse for singleton width-class sums v2 treats `type T = Foo` without `{` or `|` as a type alias; use empty record variants `Foo {}` so displacement width classes stay nominal sums and v4 CI (v2 compile all .dag) passes. Co-authored-by: Cursor <cursoragent@cursor.com> * fix: signed-only displacement width, SG-0 path order, Lean ledger map Drop MachineIntKind from signed displacement records (nominal signedness). Lex-sort EXPECTED_HAND_AUTHORED_TEST extdeps smoke paths. P4-3208: map Lean fixed-precision anchor types onto IntScalar arms; align machine_code rows. Co-authored-by: Cursor <cursoragent@cursor.com> * fix(cpp): C++ lex.key anchor for CppBool + P4-3208 authority receipt Add WG21 draft anchor on cpp_bool surface; ledger cites C++ spec, not RustBool, as coincidence authority (api-review / INVARIANTS P1 cite). Co-authored-by: Cursor <cursoragent@cursor.com> --------- Co-authored-by: Cursor <cursoragent@cursor.com>
1 participant
Auto-opened by session-dashboard for session
zesty-fox-441.Pushing to
session/zesty-fox-441advances this PR.Worker attestation
Before flipping this PR to ready for review, confirm each item:
npm test,cargo test) and the result.Closes #Ndirective.Summary
TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.
Test plan