Fix bounded integer encoding with overflow checking - #1015

Draft

jcp19 wants to merge 82 commits into

claude/improve-int-type-inference-UFkBefrom

claude/integer-type-semantics-RUVTQ

Commits on Apr 15, 2026

Add domain-based encoding for bounded integer types
claude
committed
746d119
Fix two runtime bugs in BoundedIntEncoding and add regression tests
claude
committed
5204674

Commits on Apr 16, 2026

Revert equal override in BoundedIntEncoding (fixed in base branch)
claude
committed
d7c3c65
Merge remote-tracking branch 'origin/claude/improve-int-type-inference-UFkBe' into claude/integer-type-semantics-RUVTQ
claude
committed
9dce304
Encode each bounded integer kind as its own Viper domain type
claude
committed
4f0f2ab
Fix type mismatch: use partial FuncApp constructor with withSrc
claude
committed
ce8fde6
Normalise unbounded-int operands to domain values
claude
committed
1317e4e
Fix MBQI divergence by making arithmetic functions return Int
claude
committed
1292b3d
Prefix bounded int domain names to avoid Silicon sort clash
claude
committed
161bf8f

Commits on Apr 19, 2026

fix byte.go
jcp19
committed
d6b5557
Merge branch 'master' into claude/integer-type-semantics-RUVTQ
jcp19
committed
83b7e4f
Propagate IntegerKind through desugaring and align mixed-kind operands

jcp19
and
claude
committed
24166a6
Register `integer` as a built-in type so it resolves in conversions

jcp19
and
claude
committed
cf59992
Add `from` injectivity axiom; require `integer` for perm operands; reject bitwise on integer

jcp19
and
claude
committed
f5469bf
Emit well-founded order axioms for each bounded integer domain

jcp19
and
claude
committed
cba0e19
Distinguish typed `integer` from untyped int constant via separate kind

jcp19
and
claude
committed
145530d
fix byte test
jcp19
committed
cefbf0e
Make bounded arithmetic functions return the domain type, not Int+wrap

jcp19
and
claude
committed
51b592c

Commits on Apr 27, 2026

Replace pair-trigger from-injectivity with unary `to` domain axiom

jcp19
and
claude
committed
682bf20

Commits on Jun 2, 2026

Commits on Jun 13, 2026

Fix e-matching matching loop in bounded-int arithmetic encoding
claude
committed
b61e057

Commits on Jun 14, 2026

Add INFO-level per-phase progress logging to the pipeline
jcp19
committed
dbcfe3f

Commits on Jul 18, 2026

Prevent e-matching blowups from bounded-int from-triggers and literal roundtrips

jcp19
and
claude
committed
10823ed
Reinstate loop-safe from-injectivity; handle bounded operands on either side

jcp19
and
claude
committed
10a4753
Align integer kinds at all remaining encoding boundaries

jcp19
and
claude
committed
eb4c443

Commits on Jul 19, 2026

Type ghost-collection sizes, multiplicities, and range elements as `integer`

jcp19
and
claude
committed
deb220d
Keep from(to(c)) literal anchors; allow int-to-integer assignability

jcp19
and
claude
committed
567b2d6
Use Skolem-inverse form for the from-injectivity axiom

jcp19
and
claude
committed
d6d716b
Make small-operand multiplication robustly linear via sqrt-box lemmas

jcp19
and
claude
committed
5623067

Commits on Jul 20, 2026

Align integer kinds at channel-invariant args and the close built-in

jcp19
and
claude
committed
745c1ed
Add a math stub with the concrete-type integer limit constants

jcp19
and
claude
committed
1e910cd
Align set-multiplicity element kind; bound overflow-dependent test specs

jcp19
and
claude
committed
5cf0a5b
Negate WaitGroup debt permission in exact integer arithmetic

jcp19
and
claude
committed
3834a82
Quantify bounded-integer variables over the mathematical integer sort

jcp19
and
claude
committed
193ddab
Bound example-2-1's incr spec against loop-counter and element overflow

jcp19
and
claude
committed
a133aea
Align option element kinds in mixed comparisons

jcp19
and
claude
committed
e834cdd
Bound n in the tutorial sum examples so the result cannot overflow

jcp19
and
claude
committed
de00d25
Bound quantified-permissions addToSlice against loop-counter/element overflow

jcp19
and
claude
committed
d1404df
Rewrite tour/Test2 sum invariant to keep multiplication operands small

jcp19
and
claude
committed
fc092aa
Bound switch/channels examples against increment/negation overflow

jcp19
and
claude
committed
5f626a6
Bound zune's day-conversion input so its year products stay exact

jcp19
and
claude
committed
2e52e1e
Bound ghost-code's slice lengths so index arithmetic stays exact

jcp19
and
claude
committed
62dcbce
Type list_of_interfaces' recursion-depth result as ghost integer

jcp19
and
claude
committed
1486c3a
Type visitor_pattern's permission-scaling depth as ghost integer

jcp19
and
claude
committed
f45c953
Adapt collection feature tests to sound bounded-int + mathematical quantifiers

jcp19
and
claude
committed
4be64b5
Use the configured int/uint kinds for explicit conversions

jcp19
and
claude
committed
9b70fe3
Adapt misc feature tests to sound bounded-int + mathematical quantifiers

jcp19
and
claude
committed
965836f
Adapt closure tests to sound bounded-int semantics

jcp19
and
claude
committed
1eb2f3c
Fix unsigned-shift constant evaluation overflow; bound wand traversal counters

jcp19
and
claude
committed
7fd380d
Claim mixed comparisons only when both operands are integer-typed

jcp19
and
claude
committed
d2ab93c
Mirror sound-semantics adaptations into impl_errors/spec_errors variants

jcp19
and
claude
committed
b2a098c
Adapt suite-only failing tests: bounds, integer results, overflow annotations

jcp19
and
claude
committed
a48663b

Commits on Jul 21, 2026

Maintain relaxed_prefix's prefix equalities at the sequence level

jcp19
and
claude
committed
1b7610b
Add --unboundedIntegers flag to restore unbounded integer encoding
claude
committed
7ac4d1c
Adapt seq-convert-fail3 to mathematical integer len result
claude
committed
d521500
Opt 000659 and termination-fail-01 out of bounded-int semantics
claude
committed
73c5948
Opt trusted-functions out of bounded-int semantics
claude
committed
cbb75bf

Commits on Jul 22, 2026

Opt evaluation examples out of bounded-int semantics

jcp19
and
claude
committed
c3309c3
Convert ghost-sequence length to int in parallel_search_replace

jcp19
and
claude
committed
bbfd2e0
Assert that no range axioms are emitted under --unboundedIntegers

jcp19
and
claude
committed
e770cc7

Commits on Aug 3, 2026

Quantify bounded-integer variables over their type's domain

jcp19
and
claude
committed
05a76fd
Merge defined types with any integer kind in internal binary expressions

jcp19
and
claude
committed
6d66c9b
Type bit-negation with its operand's type

jcp19
and
claude
committed
097ab45

Commits on Aug 4, 2026

Keep existential bound variables at the domain sort

jcp19
and
claude
committed
e91239c
Axiomatize that array, slice, and string lengths fit in int

jcp19
and
claude
committed
015e1c8
Exclude bounded-int arithmetic helpers from quantifier triggers

jcp19
and
claude
committed
1614b6c
Normalize resolved package paths before deriving package ids

jcp19
and
claude
committed
ff51547
Lower quantified domain occurrences via inv and add its surjectivity axiom

jcp19
and
claude
committed
99a0b08
Add missing termination measures to closures-calldesc1

jcp19
and
claude
committed
47b2e1a
Type let binders at the frontend type and align let bindings' sorts

jcp19
and
claude
committed
220a909
Require termination measure on closures-calldesc1's closure literal

jcp19
and
claude
committed
cd19c82
Align pure function bodies with the declared result sort

jcp19
and
claude
committed
f24f0e7

Commits on Aug 6, 2026

push current pathc for scion
jcp19
committed
14a119c
backup intermediate changes
jcp19
committed
32aa59b

Commits on Aug 8, 2026

Merge branch 'master' into claude/new-ints-verifiedscion
jcp19
committed
84a7fe2
Bridge bounded integers across int<->float conversions

jcp19
and
claude
committed
b77d775
Adapt integer unit tests to master's PFunctionSpec signature

jcp19
and
claude
committed
f19ccbf

Commits on Aug 9, 2026