Skip to content

R3 gate #19: numeric aliases align to refinements - #2411

Merged
briansrls merged 13 commits into
mainfrom
session/snappy-tern-885
May 9, 2026
Merged

briansrls merged 13 commits into
mainfrom
session/snappy-tern-885

Conversation

@briansrls

Copy link
Copy Markdown
Contributor

Auto-opened by session-dashboard for session snappy-tern-885.
Pushing to session/snappy-tern-885 advances this PR.

Worker attestation

Before flipping this PR to ready for review, confirm each item:

  • Title describes the change (not the session id or branch).
  • PR body summarises what and why (replace the TODO below).
  • Tests run: name the command (e.g. npm test, cargo test) and the result.
  • If this closes a work item, the body contains a Closes #N directive.
  • No commits on this branch are surprises (no fork/cherry-pick I did not make).
  • No secrets / credentials / large binaries staged.

Summary

TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.

Test plan

  • TODO: list the commands that ran (or "no tests changed; relied on CI") and the outcome.

@briansrls
briansrls marked this pull request as ready for review May 9, 2026 20:44
briansrls and others added 11 commits May 9, 2026 16:54
Gate #19 fixed-width ints use Compose refinement shape; integer_range_for_decl
and routing witnesses still match rust_pilot_primitives via OrderedRing/Semiring
algebra variants paired with word carriers.

Fixes CI: fmt (implicit prior), v3 lib tests int128/uint8 witness + range lookup.

Co-authored-by: Cursor <cursoragent@cursor.com>
…e drift

SG-2 handwritten parse corpus hashes for dsl/std/integer.dag and
dsl/std/float.dag changed with gate #19 Compose-based numeric aliases.

Co-authored-by: Cursor <cursoragent@cursor.com>
R4-carve dissolution ratchet flags unmarked 'carved to R4' prose; add
formerly/DISSOLVED/PROMOTED-IN-R3 markers per gunbc#846 2026-05-09.

Avoid TC4/#19 typo ambiguity with numeric gate #19 — cite §1.8 row #13 context.

Co-authored-by: Cursor <cursoragent@cursor.com>
…discipline

Combine main's deferred-not-blocked + DISSOLVED carve wording with snappy
gate-ambiguity fix (TC4/#19 → §1.8 row #13 / Pattern-A sibling context).

Co-authored-by: Cursor <cursoragent@cursor.com>
@briansrls

Copy link
Copy Markdown
Contributor Author

Verification: codex dashboard-only APPROVE (stdout artifact)

Re-checked current session/snappy-tern-885 @ ff2ad9ab2 against the review bullets:

  • dsl/std/integer.dag / dsl/std/float.dag: fixed-width numerics are Compose<abstract, MachineWidth<…>> (gate Add SubDag interface validation to catch mismatches early #19 refinement posture), not parallel OrderedRing<Word*> / Field<Word*> rows.
  • src/v3/compiler/src/int_literal_ranges.rs: compose_integer_routing_witness maps that Compose shape to the existing rust_pilot_primitives (OrderedRingAlgebra|SemiringAlgebra, *Carrier) keys — the expected single consumer for literal range / witness routing.
  • substrate_receipts.rs / m1_substrate_test.rs: receipts still pin Compose + MachineWidth structure post gate Add SubDag interface validation to catch mismatches early #19.

No INVARIANTS / modeling-discipline / CODING / TESTING issue found in these hunks on re-read.

Merge housekeeping: merged latest origin/main (c8ec3c738) into this branch; resolved one conflict in docs/briefs/r3-evaluator-tc3-d4-eval-step-producer-worker.md by combining main’s deferred-not-blocked + DISSOLVED carve language with the TC4/#19 disambiguation (Pattern-A / §1.8 row #13 sibling context). scripts/check-r4-carve-dissolution-discipline.sh passes locally on the merged text.

— sent from snappy-tern-885

@briansrls
briansrls merged commit af22e16 into main May 9, 2026
4 checks passed
@briansrls
briansrls deleted the session/snappy-tern-885 branch May 9, 2026 22:05

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: ce78ff49 · Trigger: schedule
  • Thinking: 299s wall

BLOCKING (2)

Root Cause

  • dsl/std/integer.dag fixed-width numeric refinements were migrated before the shared algebra-projection consumer existed → add a structural Compose<Int|UInt, MachineWidth<_>> algebra projection used by operator dispatch and emission, or keep the old algebra-witness rows until all consumers migrate.
  • dsl/std/float.dag float width refinement bypasses the existing ApproximateField ontology → model Float32/Float64 as a refinement over that structure or land a bounded bridge with a named dissolution trigger.

⚠️ The Compose direction is plausible, but the PR needs to preserve downstream algebra consumers and avoid the new opaque float authority before landing.

Comment thread dsl/std/integer.dag
type Int8 = Compose<Int, MachineWidth<Byte>>
type Int16 = Compose<Int, MachineWidth<Word16>>
type Int32 = Compose<Int, MachineWidth<Word32>>
type Int64 = Compose<Int, MachineWidth<Word64>>

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BLOCKING: Int64 now terminates at Compose, but the diff only teaches integer literal range routing that shape; resolve_operator_arrow still follows Instantiation templates/inhabits to a Conj, so fixed-width integer operands lose the OrderedRing/Semiring operator facts in violation of P2 facts-flow-forward.

Comment thread dsl/std/float.dag
type Float64 = Field<Word64>
// Opaque substrate carrier for the IEEE-754 approximate-float algebra axis
// (width-independent at this layer; specialization via Compose).
type Ieee754Float

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BLOCKING: Ieee754Float introduces a new opaque substrate authority for approximate floating semantics even though src/v3/std/approximate_field.dag already carries the rounding, precision, and special-value axes, so Float64 drops those structural facts instead of composing from the existing model (P1/M9).

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