Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
99afef6
WIP: R3 gate #22: int_lit_full_magnitude_consumer (T-Numeric-Construc…
briansrls May 14, 2026
8492715
docs(r3): name gate 22 predicate harness
briansrls May 14, 2026
13b78a9
docs(r3): tie gate 22 receipt to PR
briansrls May 14, 2026
4dc6ffe
Merge remote-tracking branch 'origin/main' into session/nimble-lark-725
briansrls May 14, 2026
020995d
Merge remote-tracking branch 'origin/main' into session/nimble-lark-725
briansrls May 14, 2026
3e42011
Merge remote-tracking branch 'origin/main' into session/nimble-lark-725
briansrls May 14, 2026
32aeee3
Merge remote-tracking branch 'origin/main' into session/nimble-lark-725
briansrls May 14, 2026
a09e8eb
Merge remote-tracking branch 'origin/main' into session/nimble-lark-725
briansrls May 14, 2026
9815302
Merge remote-tracking branch 'origin/main' into session/nimble-lark-725
briansrls May 14, 2026
db87d2f
Merge remote-tracking branch 'origin/main' into session/nimble-lark-725
briansrls May 14, 2026
2fb3444
docs(r3): refresh gate 22 audit counts
briansrls May 14, 2026
4c3fdbb
Merge remote-tracking branch 'origin/main' into session/nimble-lark-725
briansrls May 14, 2026
2394dc6
WIP: R3 gate #22: int_lit_full_magnitude_consumer (T-Numeric-Construc…
briansrls May 14, 2026
0255ace
docs(r3): reconcile close audit counts with main
briansrls May 14, 2026
eda28a6
Merge remote-tracking branch 'origin/main' into session/nimble-lark-725
briansrls May 14, 2026
6830f29
Merge remote-tracking branch 'origin/main' into session/nimble-lark-725
briansrls May 14, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 8 additions & 8 deletions docs/audit/r3-close-predicate-execution-2026-05-13.md
Original file line number Diff line number Diff line change
Expand Up @@ -25,11 +25,11 @@ Overall verdict remains **PENDING** until (a) every non-PASSING row transitions

## Verdict (Phase 2 index population)

**OVERALL: PENDING** — 48 of 106 gates have HARNESS_NAMED at this ledger snapshot; the remaining 58 gates are not at PASSING status and therefore have no predicate-execution obligation under §8 yet. **No execution receipt is asserted by this PR**; the §10 24h close-ceremony workspace re-sweep produces the receipts.
**OVERALL: PENDING** — 51 of 106 gates have HARNESS_NAMED at this ledger snapshot; the remaining 55 gates are not at PASSING status and therefore have no predicate-execution obligation under §8 yet. **No execution receipt is asserted by this PR**; the §10 24h close-ceremony workspace re-sweep produces the receipts.

## Ledger-snapshot anchor (boundary discipline, INVARIANTS P2)

This index was originally derived from `docs/r3-program-plan.md` §1.8 at commit `c055495c8` (the base commit of the Phase 2 PR). The 2026-05-14 follow-up re-derives row #15 (PR #3060 — `DECLARED` → `CONSUMER_LANDED`) and row #33 (this PR — `CONSUMER_LANDED` → `CONSUMER_LANDED + PASSING`, full §Acceptance receipt at HEAD via the four-category `canonical_lens_bridge_ratchet_test`, `bridge_retirement_demonstration` DeclarationRef-routed lens-output-equals, and `src/v3/std/bridge_ledger.dag` row `bridge_canonical_lens_name_patching_residual` `Retired`). If a future PR edits §1.8, that PR must re-derive any affected rows in the same change per the row-count parity check below.
This index was originally derived from `docs/r3-program-plan.md` §1.8 at commit `c055495c8` (the base commit of the Phase 2 PR). The current table re-derives affected rows present in the merged ledger snapshot, including row #15 (PR #3060 — `DECLARED` → `CONSUMER_LANDED`), row #22 (PR #3080 — `DECLARED` → `CONSUMER_LANDED + PASSING`), and row #33 (PR #3116 — `CONSUMER_LANDED` → `CONSUMER_LANDED + PASSING`, full §Acceptance receipt at HEAD via the four-category `canonical_lens_bridge_ratchet_test`, `bridge_retirement_demonstration` DeclarationRef-routed lens-output-equals, and `src/v3/std/bridge_ledger.dag` row `bridge_canonical_lens_name_patching_residual` `Retired`). If a future PR edits §1.8, that PR must re-derive any affected rows in the same change per the row-count parity check below.

## Row-count parity (ledger source of truth)

Expand All @@ -41,16 +41,16 @@ grep -cE '^\| [0-9]+ \| `' docs/r3-program-plan.md

At the ledger-snapshot anchor commit `c055495c8`, that count is **106** (skeleton row count of 105 + row #106 `show_correct_code_diagnostic_coverage` added by merged PR #3020 per Gap 9 of `docs/r3-actual-close-plan.md`). The table below contains 106 rows mirroring that ledger one-for-one.

## Status-bucket distribution after row #15 + row #33 re-derivation
## Status-bucket distribution after current re-derivation

Derived from the `c055495c8` §1.8 status snapshot plus the 2026-05-14 row #15 delta (`DECLARED` → `CONSUMER_LANDED`, PR #3060) and the row #33 delta (`CONSUMER_LANDED` → `CONSUMER_LANDED + PASSING`, this PR) recorded in this follow-up:
Derived from the one-row-per-gate table below after applying the current merged §1.8 deltas, including row #15 (`DECLARED` → `CONSUMER_LANDED`, PR #3060), row #22 (`DECLARED` → `CONSUMER_LANDED + PASSING`, PR #3080), and row #33 (`CONSUMER_LANDED` → `CONSUMER_LANDED + PASSING`, PR #3116):

| Bucket | Count | Predicate-execution requirement (§8) |
|---|---:|---|
| `PASSING` | 45 | HARNESS_NAMED → §10 close-ceremony sweep produces EXECUTED receipt |
| `PASSING` | 48 | HARNESS_NAMED → §10 close-ceremony sweep produces EXECUTED receipt |
| `SATISFIED-BY-CONSTRUCTION` | 3 | HARNESS_NAMED → §10 close-ceremony sweep produces EXECUTED receipt |
| `CONSUMER_LANDED` | 20 | not yet — not at PASSING |
| `DECLARED` | 30 | not yet — not at PASSING |
| `CONSUMER_LANDED` | 18 | not yet — not at PASSING |
| `DECLARED` | 29 | not yet — not at PASSING |
| `R3-LOAD-BEARING` (declaration-stage) | 3 | not yet — not at PASSING |
| `INTEGRATION_RECEIPT` | 3 | not yet — not at PASSING |
| `CANVAS_RATIFIED` | 2 | not yet — not at PASSING |
Expand Down Expand Up @@ -85,7 +85,7 @@ Close-time canonical predicate harness for `PASSING` / `SATISFIED-BY-CONSTRUCTIO
| 19 | `numeric_aliases_align_to_refinements` | substrate-shape | **N/A_NOT_PASSING** | Predicate not yet load-bearing: §1.8 Status `DECLARED` (no PASSING claim at HEAD) per §1.8 row #19 Notes. | NOT_APPLICABLE_AT_HEAD — §8 predicate-execution requirement attaches only to PASSING gates. |
| 20 | `numeric_inherited_bake_ins_dissolved` | substrate-shape | **N/A_NOT_PASSING** | Predicate not yet load-bearing: §1.8 Status `DECLARED` (no PASSING claim at HEAD) per §1.8 row #20 Notes. | NOT_APPLICABLE_AT_HEAD — §8 predicate-execution requirement attaches only to PASSING gates. |
| 21 | `int_refinement_overflow_proven_parametric` | structural-fold | **N/A_NOT_PASSING** | Predicate not yet load-bearing: §1.8 Status `DECLARED` (no PASSING claim at HEAD) per §1.8 row #21 Notes. | NOT_APPLICABLE_AT_HEAD — §8 predicate-execution requirement attaches only to PASSING gates. |
| 22 | `int_lit_full_magnitude_consumer` | substrate-shape | **N/A_NOT_PASSING** | Predicate not yet load-bearing: §1.8 Status `DECLARED` (no PASSING claim at HEAD) per §1.8 row #22 Notes. | NOT_APPLICABLE_AT_HEAD — §8 predicate-execution requirement attaches only to PASSING gates. |
| 22 | `int_lit_full_magnitude_consumer` | substrate-shape | **HARNESS_NAMED** | `cargo test -p v3-compiler --test integration int_literal_full_magnitude_carrier_rejects_beyond_documented_boundary` plus sibling endpoint ratchets named in §1.8 row #22 Notes; cross-ref `docs/r3-structure.md` §Acceptance gate #22. | Harness named; execution receipt is produced by the §10 close-ceremony 24h workspace re-sweep, not by this Phase 2 audit. |
| 23 | `string_audit_receipt` | state-check | **N/A_NOT_PASSING** | Predicate not yet load-bearing: §1.8 Status `DECLARED` (no PASSING claim at HEAD) per §1.8 row #23 Notes. | NOT_APPLICABLE_AT_HEAD — §8 predicate-execution requirement attaches only to PASSING gates. |
| 24 | `numeric_reframe_no_parallel_authority` | state-check | **HARNESS_NAMED** | `cargo test --workspace --exclude gunbc-dag-tests` (HEAD ratchet `numeric_reframe_no_parallel_authority` and sibling ratchets cited under §1.8 row #24 Notes); cross-ref `docs/r3-structure.md` §Acceptance gate #24. | Harness named; execution receipt is produced by the §10 close-ceremony 24h workspace re-sweep, not by this Phase 2 PR. See §Workspace batch receipt for the partial fmt + clippy receipts captured during Phase 2 authoring. |
| 25 | `omni_openapi_backend_emission_demo` | demonstration | **HARNESS_NAMED** | `cargo test --workspace --exclude gunbc-dag-tests` (HEAD ratchet `omni_openapi_backend_emission_demo` and sibling ratchets cited under §1.8 row #25 Notes); cross-ref `docs/r3-structure.md` §Acceptance gate #25. | Harness named; execution receipt is produced by the §10 close-ceremony 24h workspace re-sweep, not by this Phase 2 PR. See §Workspace batch receipt for the partial fmt + clippy receipts captured during Phase 2 authoring. |
Expand Down
2 changes: 1 addition & 1 deletion docs/r3-program-plan.md
Original file line number Diff line number Diff line change
Expand Up @@ -246,7 +246,7 @@ This principle is NOT a separate lane; it's a per-lane gate-shape requirement ap
| 19 | `numeric_aliases_align_to_refinements` | substrate-shape | T-Numeric-Construction | **CONSUMER_LANDED + PASSING for bootstrap substrate receipt** (2026-05-14) | Fixed public numeric aliases align to width-refinement substrate, not parallel primitive authority. Producer-side substrate: `Int8/16/32/64/128 = Compose<Int, MachineWidth<Byte\|Word16\|Word32\|Word64\|Word128>>` and `UInt8/16/32/64/128 = Compose<UInt, MachineWidth<Byte\|Word16\|Word32\|Word64\|Word128>>` in `dsl/std/integer.dag`; `Float32/Float64` alias `Real32/Real64`, whose canonical entries are `Compose<Real, MachineWidth<Word32\|Word64>>` in `dsl/std/float.dag`. Consumer evidence: `bootstrap_numeric_aliases_align_to_refinements_per_gate_19` loads the bootstrap DAG and asserts every Int/UInt alias has `Compose<abstract-carrier, MachineWidth<width>>`; the same receipt asserts Float aliases resolve to the canonical Real width-refinement entries. |
| 20 | `numeric_inherited_bake_ins_dissolved` | substrate-shape | T-Numeric-Construction | DECLARED | Char/EpochMs/Duration consume abstract Int |
| 21 | `int_refinement_overflow_proven_parametric` | structural-fold | T-Numeric-Construction | **CONSUMER_LANDED + PASSING** (2026-05-14 — `src/v3/compiler/tests/integration/int_literal_cardinality_test.rs` `int_refinement_overflow_is_proven_parametric_for_representable_widths`: every fixed-width `Int*`/`UInt*` refinement with a source-representable out-of-range decimal literal emits exactly one root-cause `Diagnostic::MagnitudeOutOfRange` carrying the typed Rust primitive `target` plus inclusive min/max strings; includes `Int128::MAX+1`, `UInt128` lower-bound overflow (`-1`), and representative `type Alias = …` chains for selected widths) | overflow caught for any width refinement |
| 22 | `int_lit_full_magnitude_consumer` | substrate-shape | T-Numeric-Construction | DECLARED | IntLit accepts full magnitude range |
| 22 | `int_lit_full_magnitude_consumer` | substrate-shape | T-Numeric-Construction | **CONSUMER_LANDED + PASSING** (PR #3080 — full-magnitude carrier ratchet in `int_literal_cardinality_test.rs`: `uint64_upper_half_literal_tokenizes_and_narrows`, `uint128_full_magnitude_literal_tokenizes_and_narrows`, `int128_max_literal_tokenizes_and_narrows`, `int128_min_literal_tokenizes_and_narrows`, and `int_literal_full_magnitude_carrier_rejects_beyond_documented_boundary`) | IntLit accepts full host narrowing range as decimal `String`: unsigned through `u128::MAX`, signed unary `-` through `i128::MIN`; one-step-beyond magnitudes fail closed at tokenization instead of truncating through narrower host integers. |
| 23 | `string_audit_receipt` | state-check | T-Numeric-Construction | DECLARED | String audit landed |
| 24 | `numeric_reframe_no_parallel_authority` | state-check | T-Numeric-Construction | **CONSUMER_LANDED + PASSING for Grounding G2 primitive rows** (2026-05-10, PR #2570 squash `b96a51a2`) | old exact-field primitive authority is no longer consumed by Rust Grounding rows. **Per-arm HEAD evidence:** **Int arm** — `type Int = AbelianGroup<GroupCompletion<Nat>>` at `dsl/std/integer.dag:147` (Slice 3 PR #1466 Q6 single-authority form); no `type Int = Int64` residue in `dsl/std/` or `src/v3/std/`. **UInt arm** — `type UInt = Nat` at `dsl/std/integer.dag:148` (PR #1818 canonical-instance form); no `type UInt = UInt64` residue at HEAD. **Float arm** — `dsl/std/float.dag` defines `Real32/Real64` as `Compose<Real, MachineWidth<Word32|Word64>>`, `Float32/Float64` as compatibility aliases to those Real-width entries, and `Real = ApproximateField<FieldOfFractions<Int>>`; Rust Grounding rows consume `ApproximateFieldAlgebra` for `f32`/`f64` and `grounding_engine` validates those rows through the loaded pilot list. The default alias `type Float = Float64` remains explicit and ratified as a default-width alias for this G2 consumer receipt, not the former `Field<Word64>` parent authority; physical alias deletion, if required, is outside this G2 primitive-row closure. |
| 25 | `omni_openapi_backend_emission_demo` | demonstration | T-Omni-Shape-B | **CONSUMER_LANDED + PASSING** (PR #2251 — Shape B OpenAPI 3.1 projection demo via `src/v3/compiler/src/omni_shape_b_openapi.rs` + `tests/integration/m1_5_omni_shape_b_openapi_test.rs`; **PR #2587** squash `77678c04` — runnable Rust backend emission demo extension landed 2026-05-10; orphan PR #2410 closed as superseded) | one workflow → OpenAPI + backend |
Expand Down
2 changes: 1 addition & 1 deletion docs/r3-structure.md
Original file line number Diff line number Diff line change
Expand Up @@ -95,7 +95,7 @@ L6 (`l6_structural_form_coverage`) was moved out of this lane during the engine-
- `numeric_aliases_align_to_refinements` — `Int8`/.../`Int128`, `Float32`/`Float64`, `UInt8`/.../`UInt128` are refinements, not parallel substrate
- `numeric_inherited_bake_ins_dissolved` — `Char`, `EpochMs`, `Duration`, `Milliseconds`, `Seconds` consume abstract `Int` (or appropriate refinement)
- `int_refinement_overflow_proven_parametric` — replaces `tier2_int128_overflow_proven`; overflow caught structurally for any width refinement
- `int_lit_full_magnitude_consumer` — replaces `int_lit_full_int128_word128_consumer`; IntLit accepts full magnitude range
- `int_lit_full_magnitude_consumer` — replaces `int_lit_full_int128_word128_consumer`; IntLit accepts full magnitude range. **CONSUMER_LANDED + PASSING** (PR #3080): `LiteralBits::LitInt(String)` documents the full host narrowing range in `src/v3/std/substrate.dag`; tokenizer/lowering consumers preserve decimal magnitudes through `UInt64` upper-half, `UInt128::MAX`, `Int128::MAX`, and unary `Int128::MIN`, with one-step-beyond values failing closed at tokenization (`int_literal_cardinality_test.rs`).
- `string_audit_receipt` — Substrate Mgr String audit landed (per Director scope-add 2026-05-01); documented-no-change in [`docs/audit/t-numeric-construction-string-audit-receipt.md`](audit/t-numeric-construction-string-audit-receipt.md): `String = FreeMonoid<Char>` already, with only `Char` retained in inherited numeric-refinement scope
- `numeric_reframe_no_parallel_authority` — old exact-field primitive authority removed from Grounding consumer rows. **CONSUMER_LANDED + PASSING for Grounding G2 primitive rows** (PR #2570 squash `b96a51a2`): Int arm — `type Int = AbelianGroup<GroupCompletion<Nat>>` at `dsl/std/integer.dag:147` (PR #1466); UInt arm — `type UInt = Nat` at `dsl/std/integer.dag:148` (PR #1818); no `Int = Int64` / `UInt = UInt64` residue at HEAD. Float arm — `dsl/std/float.dag` defines `Real32/Real64` as `Compose<Real, MachineWidth<Word32|Word64>>`, `Float32/Float64` as compatibility aliases to those Real-width entries, and `Real = ApproximateField<FieldOfFractions<Int>>`; Rust Grounding rows consume `ApproximateFieldAlgebra` for `f32`/`f64`. `type Float = Float64` remains explicitly as a default-width alias for this G2 consumer receipt, not the former `Field<Word64>` parent authority; physical alias deletion, if required, is outside this primitive-row closure. See §1.8 row #24 for full receipt.
- **T-Omni-Shape-B** (Director-locked target pair 2026-04-28: OpenAPI + Markdown drift-lock primary; SQL DDL alternative).
Expand Down
32 changes: 32 additions & 0 deletions src/v3/compiler/tests/integration/int_literal_cardinality_test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -479,6 +479,38 @@ fn int128_min_literal_tokenizes_and_narrows() {
);
}

#[test]
fn int_literal_full_magnitude_carrier_rejects_beyond_documented_boundary() {
// R3 gate #22: the surface carrier intentionally accepts the full host narrowing range
// and then fails closed immediately past it, before any narrower host integer parse.
let cases = [
(
"data x: UInt128 = 340282366920938463463374607431768211456",
"invalid integer literal `340282366920938463463374607431768211456`",
),
(
"data x: Int128 = -170141183460469231731687303715884105729",
"integer literal out of range for signed decimal literal",
),
];

for (source, expected) in cases {
let err = compile_to_dag(source, "int_literal_full_magnitude_boundary.v3")
.expect_err("literal just beyond the full-magnitude carrier must fail closed");
let CompileError::Tokenize(v3_compiler::diagnostics::Diagnostic::TokenizerError {
message,
..
}) = err
else {
panic!("expected tokenizer diagnostic for `{source}`, got {err:?}");
};
assert!(
message.contains(expected),
"expected tokenizer diagnostic containing `{expected}`, got `{message}`"
);
}
}

#[test]
fn out_of_range_uint8_literal_emits_magnitude_diagnostic() {
let err = compile_to_dag("data x: UInt8 = 256", "int_literal_u8_oob.v3")
Expand Down
Loading