Skip to content

R3 gate #67: numeric construction demonstration - #2457

Merged
briansrls merged 11 commits into
mainfrom
session/loyal-eagle-130
May 10, 2026
Merged

briansrls merged 11 commits into
mainfrom
session/loyal-eagle-130

Conversation

@briansrls

@briansrls briansrls commented May 9, 2026 •

Copy link
Copy Markdown
Contributor

Summary

R3 gate #67 now demonstrates the numeric construction chain through the bootstrapped substrate: Magnitude -> Nat -> Int -> Rational -> Real, with Int32 and Real64 represented as machine-width refinements via Compose<..., MachineWidth<...>>. The float substrate now exposes Real32/Real64 as width refinements of abstract Real, while Float32/Float64 remain compatibility aliases to those construction rows.

Test plan

R3 / P5 receipt

  • Gate receipt: m1_substrate_test now carries focused receipts for Nat, Int, Rational, Real, Int32, Real64, and the Float64 compatibility alias, so each numeric-construction edge is checkable without bundling unrelated claims into one test.
  • Debt receipt: this PR pays down the prior endpoint-only numeric construction receipt by making the full chain structural and checkable. No new tracked debt is introduced.

@briansrls
briansrls marked this pull request as ready for review May 9, 2026 23:21
@briansrls
briansrls force-pushed the session/loyal-eagle-130 branch from 601b9cb to 2af78d0 Compare May 10, 2026 00:12
@briansrls

Copy link
Copy Markdown
Contributor Author

Addressed the review's P5 receipt concern by replacing the template PR body with a concrete summary, focused test plan, and explicit R3/P5 debt receipt for gate #67. — sent from loyal-eagle-130

@briansrls

Copy link
Copy Markdown
Contributor Author

Verified the review against current head 352ba42. The PR description already includes the explicit ## R3 / P5 receipt with both gate and debt receipts. The optional Ieee754Float note is accurate: current search shows only the compatibility declaration in dsl/std/float.dag and generated bootstrap entries, with Float32/Float64 routed through Real32/Real64. No code change needed for this APPROVE review. — sent from loyal-eagle-130

@briansrls
briansrls force-pushed the session/loyal-eagle-130 branch from 6642f18 to 32c4ee3 Compare May 10, 2026 01:12
@briansrls

Copy link
Copy Markdown
Contributor Author

Verified against current head 32c4ee3. The optional Ieee754Float observation is accurate and non-blocking: search shows the compatibility declaration in dsl/std/float.dag plus generated bootstrap entries only; the public Float32/Float64 rows route through Real32/Real64, and the header explicitly documents Float<N> = Real<N> = Compose<Real, MachineWidth<Word*>>. No code change needed for this APPROVE review. — sent from loyal-eagle-130

@briansrls
briansrls force-pushed the session/loyal-eagle-130 branch from 32c4ee3 to 4963ea2 Compare May 10, 2026 01:22
@briansrls

Copy link
Copy Markdown
Contributor Author

Verified against current head b4f17f2. Both optional observations match the tree: Ieee754Float appears only as the compatibility declaration in dsl/std/float.dag plus generated bootstrap entries, and the alias walkers intentionally retain the existing loud-at-16 bound. I agree both are follow-up/policy questions rather than blockers for this APPROVE review. — sent from loyal-eagle-130

@briansrls

Copy link
Copy Markdown
Contributor Author

Verified against current head 78a849e. The APPROVE review's optional P5 note is satisfied out of band: the PR body includes ## R3 / P5 receipt with a gate receipt for m1_substrate_test::numeric_construction_demonstration_gate_67 and a debt receipt stating the prior endpoint-only receipt is paid down with no new tracked debt. No code change needed for this APPROVE review. — sent from loyal-eagle-130

@briansrls

Copy link
Copy Markdown
Contributor Author

Verified against current head ad8ce44. The APPROVE review matches the tree: dsl/std/float.dag routes Float<N> through Real<N>, the gate #19 and #67 receipts are split in m1_substrate_test.rs / substrate_receipts.rs, CI is green, and the PR body includes the ## R3 / P5 receipt gate/debt receipt. No code change needed for this APPROVE review. — sent from loyal-eagle-130

@briansrls

Copy link
Copy Markdown
Contributor Author

Verified against current head f6585e9. The APPROVE review's optional observations match the current tree: Ieee754Float appears only as the compatibility declaration plus generated bootstrap entries, and assert_numeric_construction_demonstration_gate_67 is the single named gate receipt bundling the construction-chain checks. No code change needed for this APPROVE review. — sent from loyal-eagle-130

@briansrls
briansrls force-pushed the session/loyal-eagle-130 branch from f6585e9 to dfdad73 Compare May 10, 2026 02:25
@briansrls
briansrls merged commit 59c9073 into main May 10, 2026
4 checks passed
@briansrls
briansrls deleted the session/loyal-eagle-130 branch May 10, 2026 02:55
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant