Repository navigation
feat(v3): totalize Int division with Result carrier #969
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Merged
Merged
Changes from all commits
Commits
Show all changes
128 commits
Select commit
Hold shift + click to select a range
3ffbb32
WIP: vivid-badger-729
briansrls 31bfb72
WIP: vivid-badger-729
briansrls e335311
chore: apply cargo fmt
briansrls f0edd3a
WIP: vivid-badger-729
briansrls 331c436
chore: apply cargo fmt
briansrls ca4084a
WIP: vivid-badger-729
briansrls 4f8130b
WIP: vivid-badger-729
briansrls 50fdc74
WIP: vivid-badger-729
briansrls b691688
chore: apply cargo fmt
briansrls 0d37ada
WIP: vivid-badger-729
briansrls 8f02992
WIP: vivid-badger-729
briansrls c20dc31
chore: apply cargo fmt
briansrls 7964dae
Merge remote-tracking branch 'origin/main' into session/vivid-badger-729
briansrls 33bf785
Merge remote-tracking branch 'origin/main' into session/vivid-badger-729
briansrls 2e2851c
Merge remote-tracking branch 'origin/main' into session/vivid-badger-729
briansrls 5a42fa3
WIP: vivid-badger-729
briansrls 7a045c6
WIP: vivid-badger-729
briansrls 911ba9d
chore: apply cargo fmt
briansrls 2d50fb1
WIP: vivid-badger-729
briansrls 7d195f5
chore: apply cargo fmt
briansrls 6490452
WIP: vivid-badger-729
briansrls 90fd100
WIP: vivid-badger-729
briansrls b5c2c2b
WIP: vivid-badger-729
briansrls e05bf26
WIP: vivid-badger-729
briansrls ca6b947
WIP: vivid-badger-729
briansrls 0b1cdf2
WIP: vivid-badger-729
briansrls 657471f
WIP: vivid-badger-729
briansrls 3659127
Merge remote-tracking branch 'origin/main' into session/vivid-badger-729
briansrls 28a51d6
WIP: vivid-badger-729
briansrls 120cc87
WIP: vivid-badger-729
briansrls 6c59e53
Merge remote-tracking branch 'origin/main' into session/vivid-badger-729
briansrls 13b6def
WIP: vivid-badger-729
briansrls 902f1b3
WIP: vivid-badger-729
briansrls be1a736
WIP: vivid-badger-729
briansrls bcdd0b8
WIP: vivid-badger-729
briansrls 1519ed5
WIP: vivid-badger-729
briansrls 83e848d
WIP: vivid-badger-729
briansrls 26ad966
chore: apply cargo fmt
briansrls f095b05
WIP: vivid-badger-729
briansrls 89b5e5b
WIP: vivid-badger-729
briansrls 2ca4dc9
WIP: vivid-badger-729
briansrls 17baffb
WIP: vivid-badger-729
briansrls 97bf18d
chore: apply cargo fmt
briansrls efcd87e
docs(spec): clarify Go Result carrier vs v3intdiv prelude (M1)
briansrls bae9937
WIP: vivid-badger-729
briansrls 1f4c442
docs(v3): clarify Result suppression, infer DAG mutation, Go M1 debt
briansrls 852fc60
WIP: vivid-badger-729
briansrls 9711332
WIP: valiant-lynx-650
briansrls 5ac371a
Merge remote-tracking branch 'origin/main' into session/vivid-badger-729
briansrls 24943ad
chore: apply cargo fmt
briansrls 1e765a2
Merge remote-tracking branch 'origin/session/vivid-badger-729' into s…
briansrls 9eeabd7
fix(v3): refresh division totality snapshots
briansrls 95f3fe0
fix(v3): refresh generated int div prelude visibility
briansrls 43cd006
docs(v3): correct Result authority references
briansrls 84e3a39
fix(v3): print Rust Result top-level values safely
briansrls 13c321b
Merge remote-tracking branch 'origin/session/vivid-badger-729' into s…
briansrls 993b65c
Merge remote-tracking branch 'origin/main' into subsume/pr-931
briansrls d6debeb
fix(v3): gate Rust division result emission
briansrls d018a06
Merge remote-tracking branch 'origin/main' into subsume/pr-931
briansrls c683b67
chore(v3): track Python div prelude gate
briansrls 4682440
fix: resolve PR-969 rustfmt + boundary test fixture issues
briansrls 36a6bbb
fix: anchor division prelude lookups and gate Go/Python division prel…
briansrls 7aa8ec6
WIP: valiant-lynx-650
briansrls 91ce8fe
chore: apply cargo fmt
briansrls 6fb6bcf
fix(v3): remove generated merge markers
briansrls 051fd6b
WIP: valiant-lynx-650
briansrls 528003e
chore: apply cargo fmt
briansrls 93e32ef
WIP: valiant-lynx-650
briansrls 7c57819
fix(v3): refresh std bootstrap cardinality snapshot
briansrls 2640d94
fix(v3): compile shared division prelude gate
briansrls 6cceef9
fix(v3): fail closed on Rust DivError prelude collision
briansrls b1996a7
WIP: valiant-lynx-650
briansrls d8e0d2a
Merge remote-tracking branch 'origin/main' into subsume/pr-931
briansrls 2fa4de4
WIP: valiant-lynx-650
briansrls 79da63b
WIP: valiant-lynx-650
briansrls 81619c5
WIP: valiant-lynx-650
briansrls 019f59d
fix(v3): fail closed division carrier collisions
briansrls 29e1678
Merge remote-tracking branch 'origin/main' into subsume/pr-931
briansrls bddf0a6
Merge remote-tracking branch 'origin/main' into subsume/pr-931
briansrls 9241aea
WIP: valiant-lynx-650
briansrls c6cea10
WIP: valiant-lynx-650
briansrls ab9c851
WIP: valiant-lynx-650
briansrls 756f34a
chore: apply cargo fmt
briansrls 2cb824c
ci: avoid target cache in v2 self-compile gate
briansrls 6c3d5ec
WIP: valiant-lynx-650
briansrls 2e33a52
WIP: valiant-lynx-650
briansrls c49d791
WIP: valiant-lynx-650
briansrls 78d1a8f
WIP: valiant-lynx-650
briansrls 34268ea
WIP: valiant-lynx-650
briansrls 6eda4d3
Merge remote-tracking branch 'origin/main' into subsume/pr-931
briansrls eeee2a0
chore: apply cargo fmt
briansrls 61babca
WIP: valiant-lynx-650
briansrls bf7eb35
WIP: valiant-lynx-650
briansrls 7d836e5
WIP: valiant-lynx-650
briansrls 65228f5
WIP: valiant-lynx-650
briansrls 94de338
WIP: valiant-lynx-650
briansrls 8cf0da1
fix v3 source filtering path normalization
briansrls 616aea5
fix v3 source filtering for absolute fixtures
briansrls 8f0c0ae
isolate v2 ci pass2 rebuild target
briansrls 4846ebd
WIP: valiant-lynx-650
briansrls 859016c
WIP: valiant-lynx-650
briansrls c2ee284
WIP: valiant-lynx-650
briansrls 0865888
WIP: valiant-lynx-650
briansrls 4bffcb2
WIP: valiant-lynx-650
briansrls 5d23999
WIP: valiant-lynx-650
briansrls 223a404
WIP: valiant-lynx-650
briansrls 2375242
WIP: valiant-lynx-650
briansrls 67094e8
WIP: valiant-lynx-650
briansrls ea05846
WIP: valiant-lynx-650
briansrls c53d0f2
WIP: valiant-lynx-650
briansrls a8b65d6
WIP: valiant-lynx-650
briansrls 9167e7d
WIP: valiant-lynx-650
briansrls 32c2dd6
Merge remote-tracking branch 'origin/main' into subsume/pr-931
briansrls b4a06f2
refresh parse corpus manifest after main merge
briansrls e5ed617
WIP: valiant-lynx-650
briansrls d342edd
fix go division overflow prelude test
briansrls 179c72c
WIP: valiant-lynx-650
briansrls b483d81
chore: apply cargo fmt
briansrls 260fb03
WIP: valiant-lynx-650
briansrls de34e3e
Merge remote-tracking branch 'origin/main' into subsume/pr-931
briansrls 02fca30
WIP: valiant-lynx-650
briansrls c390967
WIP: valiant-lynx-650
briansrls 03d0995
WIP: valiant-lynx-650
briansrls 68a12ca
WIP: valiant-lynx-650
briansrls 53d3edc
WIP: valiant-lynx-650
briansrls 07a96e0
WIP: valiant-lynx-650
briansrls 2e2a59b
Merge remote-tracking branch 'origin/main' into subsume/pr-931
briansrls d866808
Merge remote-tracking branch 'origin/main' into subsume/pr-931
briansrls File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,18 @@ | ||
| // std/error_primitives.dag — minimal error carriers with **no** dependency on | ||
| // `Int` / `String` / other `std.types` surface, so this module can load in the | ||
| // v3 std bootstrap seed *before* `algebra.dag` (which needs `Result` / `DivError` | ||
| // for `OrderedRing.div`). | ||
|
|
||
| module std.error_primitives | ||
|
|
||
| // 🟡 STRUCTURAL-CARRIER: algebraic Result sum for fallible std operations | ||
| // (e.g. `OrderedRing.div` totality). It is substrate-owned until target | ||
| // realizations can consume this declaration directly instead of filtering it | ||
| // from emitted std surfaces and reintroducing per-target carriers. | ||
| type Result<ok, err> = Ok { value: ok } | Err { value: err } | ||
|
|
||
| // 🟡 STRUCTURAL-CARRIER: signed integer division (`Int / Int`) failure modes | ||
| // (C-8): zero divisor vs MIN / -1 signed overflow. The target preludes mirror | ||
| // this declaration until `std.error_primitives` is emitted through the normal | ||
| // filtered-type path. | ||
| type DivError = DivideByZero | Overflow |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,26 @@ | ||
| // Generated by v2 compiler -- do not edit. | ||
| // Source module: std.error_primitives | ||
|
|
||
| #![allow(non_camel_case_types)] | ||
|
|
||
| use self::DivError::*; | ||
| use self::Result::*; | ||
| use crate::v2_rt; | ||
| use crate::NonEmptyBTreeSet; | ||
| use crate::NonEmptyVec; | ||
| use std::collections::HashMap; | ||
| use std::rc::Rc; | ||
|
|
||
| #[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] | ||
| #[serde(tag = "_variant")] | ||
| pub enum Result<ok, err> { | ||
| Ok { value: Box<ok> }, | ||
| Err { value: Box<err> }, | ||
| } | ||
|
|
||
| #[derive(Debug, Clone, Copy, PartialEq, serde::Serialize, serde::Deserialize)] | ||
| #[serde(tag = "_variant")] | ||
| pub enum DivError { | ||
| DivideByZero, | ||
| Overflow, | ||
| } |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
BLOCKING: M9/modeling faithfulness: generic OrderedRing.div now returns the signed-Int-specific DivError, so every OrderedRing inhabitant inherits Int overflow semantics that the algebra itself does not define.