Fix bounded integer encoding with overflow checking - #1015
Draft
jcp19 wants to merge 82 commits into
Draft
Conversation
Replace the broken OverflowChecksTransform with a clean encoding-level approach for bounded integer type semantics: - Add ghost `integer` type (PIntegerGhostType) for unbounded mathematical integers in specifications and ghost code - Delete OverflowChecksTransform (Viper-level AST rewrite that was unmaintainable) - Add BoundedIntEncoding: each bounded integer type (int8, uint8, int16, etc.) gets abstract Viper functions for arithmetic with range postconditions, Go truncation-towards-zero div/mod semantics, and abstract bitwise operations - Restrict IntEncoding to only handle unbounded integers (UnboundedInt pattern), preventing combiner conflicts with BoundedIntEncoding - Add BoundedInt/UnboundedInt extractor patterns in TypePatterns - Add naming helpers in Names.scala for per-kind function generation - Repurpose --overflow flag: when enabled, arithmetic functions on bounded types gain preconditions making overflow a verification error - Add type-checking errors for bitwise operations on the `integer` type - Register BoundedIntEncoding in DfltTranslatorConfig before IntEncoding https://claude.ai/code/session_01VLNTKs1NTzfhQjBz8u5y1U
Bug 1: DefaultPureMethodEncoding did not apply `fixResultvar` to postconditions produced by `varPostcondition`, causing "local variable P0_PO0 not found" errors in Viper when pure functions or methods have bounded integer result types. Fixed by transforming `vResultPosts` through `fixResultvar` in both `pureMethodDefault` and `pureFunctionDefault`. Bug 2: BoundedIntEncoding lacked an `equal` override for mixed bounded/unbounded comparisons (e.g., `x == 0` where `x: int` and `0` is an untyped integer literal with UnboundedInteger kind). The default `equal` in TypeEncoding requires both sides to be handled by the same encoding's `typ`, which fails for this mixed case. Fixed by overriding `equal` in BoundedIntEncoding to handle (BoundedInt, UnboundedInt) and (UnboundedInt, BoundedInt) pairs. Also add three regression test files: - integers/bounded_int_semantics.gobra: verifies range semantics, equality with literals, and pure function postcondition handling without overflow checking - integers/integer_ghost_type.gobra: verifies the ghost `integer` type for unbounded mathematical integer arithmetic in ghost code - overflow_checks/bounded_int_overflow.gobra: verifies overflow detection using the new domain-based encoding (with --overflow flag) https://claude.ai/code/session_01VLNTKs1NTzfhQjBz8u5y1U
The mixed bounded/unbounded equal case (e.g. `x == 0` where x: int and 0 is an untyped integer literal) is already handled in the base branch claude/improve-int-type-inference-UFkBe. https://claude.ai/code/session_01VLNTKs1NTzfhQjBz8u5y1U
…e-UFkBe' into claude/integer-type-semantics-RUVTQ
Previously BoundedIntEncoding translated all bounded int types (int8,
uint8, etc.) to vpr.Int, making them indistinguishable in Viper. This
change gives each kind an opaque domain type with from/to functions:
domain int8 {}
function int8$from(x: int8): Int ensures -128 <= result <= 127
function int8$to(x: Int): int8 requires -128 <= x <= 127
ensures int8$from(result) == x
Arithmetic/bitwise/shift functions now operate on domain types and
express their contracts through from(). The varPrecondition/
varPostcondition overrides are removed since the from postcondition
universally axiomatises the range for all domain values.
Supporting changes:
- IntEncoding.scala: guard IntLit to unbounded-only to avoid
SafeTypeEncodingCombiner duplicate errors
- MemoryEncoding.scala: guard LessCmp/AtMostCmp/GreaterCmp/AtLeastCmp
to non-bounded operands; BoundedIntEncoding now intercepts these and
converts via from() before the Int comparison
https://claude.ai/code/session_01VLNTKs1NTzfhQjBz8u5y1U
fromApp returns a fully-applied vpr.Exp; withSrc expects a partial constructor (pos,info,errT)=>T. Inline the FuncApp to fix the mismatch in the bounded→unbounded conversion case. https://claude.ai/code/session_01VLNTKs1NTzfhQjBz8u5y1U
Gobra's internal AST mixes unbounded-integer IntLits (kind=UnboundedInteger) with bounded-integer operands without inserting explicit conversions. For example, \`u + 1\` where \`u: int\` has Add.typ = int (via merge(int, integer)), but the right operand \`1\` is still IntLit(UnboundedInteger) and encodes to vpr.Int rather than the int domain type. With the old vpr.Int encoding this coincidence worked; with domain types it causes sort mismatches — Silicon crashed on \`int\$from\` being called with an Int value when instantiating the postcondition of int\$add. Fix: - New \`asDomain(ctx)(k, expr, v)\` helper — wraps v with \`to(k, _)\` when the source Gobra expression is not a bounded integer; identity when it is. - \`handleBoundedBinOp\`, bitwise binary ops, and the left operand of shifts now route both operands through asDomain before the domain-typed call. - New \`assignment\` override for bounded LHS + non-bounded RHS: wraps the RHS with \`to(k, _)\` for both exclusive (LocalVarAssign) and shared (FieldAssign) assignments. This fixes returns like \`return 0\` where the assignee is bounded and the literal is still UnboundedInteger. https://claude.ai/code/session_01VLNTKs1NTzfhQjBz8u5y1U
The previous encoding had arithmetic functions with signature (dom, dom): dom, which caused Z3's MBQI to proliferate domain-typed terms indefinitely: each new int8$add(x, y) term of domain type created new pairs for MBQI to consider, producing int8$add(x, int8$add(x, y)), int8$add(x, int8$add(x, int8$add(x, y))), and so on. This manifested as Gobra hanging forever on tests like StatsCollector's pkg2.gobra (`return r.width * r.height`). Fix: arithmetic, bitwise, and shift functions now return Int. A new abstract function `int8$wrap(x: Int): int8` (no precondition, postcondition inRange(x) ==> from(result) == x) lifts the Int result back into the domain at explicit encoding positions. Because wrap is applied only at explicit call sites — not inside axiom bodies — the set of domain-typed terms remains finite and MBQI terminates. Also switches asDomain to use wrap instead of to, avoiding the need to discharge a precondition when normalising unbounded RHS operands. https://claude.ai/code/session_01VLNTKs1NTzfhQjBz8u5y1U
Go's int type maps to a Viper domain named "int", whose Silicon/Z3 sort name "int~_int" is visually and structurally too close to Viper's built-in Int sort "Int~_Int". When Silicon generates tuple sorts (e.g. for 2-argument function axioms), using Tuple2<int~_int> alongside Tuple2<Int~_Int> produces a Z3 sort incompatibility error: Sorts Tuple2<int~_int> and Tuple2<Int~_Int> are incompatible Fix: prefix every bounded integer domain name with "Bounded_", so Go's int becomes domain "Bounded_int", int8 becomes "Bounded_int8", etc. This is a domain-level renaming only — all function names (int8$from, int8$wrap, etc.) are unchanged. https://claude.ai/code/session_01VLNTKs1NTzfhQjBz8u5y1U
The domain-based bounded-integer encoding introduced in this branch
treats each kind (int, int8, ..., uintptr) as its own opaque Viper
sort. The legacy desugarer relied on the encoding's vpr.Int-based
representation to silently bridge mixed-kind operands; with domain
types every kind boundary needs an explicit conversion or the Viper
output fails its consistency check (or Z3 reports a sort mismatch at
SMT time).
Changes:
- PrettyPrinter (frontend): add the missing case for `PIntegerGhostType`
in `showGhostType`, so any program using the ghost `integer` type can
be printed (the test harness pretty-prints every parsed input).
- Desugar.litD: propagate the frontend-inferred IntegerKind to in.IntLit
using `info.typ(lit)`. constSpecD does the same from the global
constant's declared type. Constant-fold any pure integer expression
whose inferred type is a bounded kind and whose value fits in that
kind — handles the unary-negation pattern `PSub(IntLit(0), IntLit(v))`
representing `-v`, where naively wrapping `v` is lossy if `v` is itself
out of range (e.g. `-128` in int8). Constant-fold shift expressions
with the inferred kind too.
- IntKindAlignment (new utility): two helpers used wherever the AST
brings together expressions of different IntegerKinds:
- `alignIntKinds(l, r)`: prefer retyping an in.IntLit operand to
match the other side when the literal's value fits; otherwise
demote the bounded operand to UnboundedInteger via in.Conversion
(the `from` bridge is total).
- `asUnboundedInt(e)`: wrap a bounded int with Conversion-to-integer.
Used at sites that consume vpr.Int (slice/sequence/array bounds,
perm-constructor numerator/denominator).
- Desugar uses these for: every comparison desugar (PEquals/PUnequals/
PLess/PAtMost/PGreater/PAtLeast and the Ghost variants), PConditional
branches, indexedExprD (slice/array/sequence/string index demoted to
integer; map/mathmap key retyped to the container's key kind), slice
bounds (low/high/cap), PermConstructorFromInt arguments, PElem element
vs. container element type, and an extended implicitConversion that
inserts an in.Conversion whenever an assignment crosses IntegerKinds.
- BoundedIntEncoding.typ: touch funcsOf(k) so the domain is registered
even for kinds reachable only via the type translation (e.g. a `byte`
parameter that is never used in arithmetic). Without this, the Viper
output references `Bounded_byte` without declaring the domain.
- StringEncoding: stringIndexFunc declares its index parameter as
UnboundedInteger so it matches the call-site Viper Int produced by
the encoding's bound variables.
- SliceEncoding (Make): align lenArg/capArg with in.Length/in.Capacity
(which are hardcoded integer-kinded in the internal AST) before the
programmatic ctx.equal call.
Verified focused suites pass:
- regressions/features/integers (21/21)
- regressions/features/overflow_checks (3/5; the two remaining failures
are spec-position vs body-position annotation mismatches that the
user said are intended behaviour)
Remaining suite-wide failures fall into two buckets that are out of
scope for this commit:
- semantic verification errors caused by the lossy `wrap` postcondition
on bounded arithmetic results (without --overflow, the verifier can't
reason precisely about `n + 1` etc.) — needs a follow-up encoding
redesign;
- the chopper Tuple2 sort clash in StatsCollectorTests, which is
upstream Silicon behaviour.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The frontend's parser already mapped the identifier "integer" to PIntegerGhostType in `visitTypeIdentifier` (used in explicit type positions like field declarations), but the resolver had no entry for "integer" in `BuiltInMemberTag.builtInMembers`. As a result, using `integer` in a value position — most commonly the conversion `integer(x)` — failed name resolution with "got unknown identifier integer" instead of being treated as a bounded → unbounded conversion. Add `IntegerType` as a ghost BuiltInTypeTag (identifier "integer", typ IntT(UnboundedInteger), node PIntegerGhostType()) and include it in the `builtInMembers()` vector. With this, expressions such as ensures integer(ret) == integer(u) + 1 resolve `integer` to the ghost type and route through the existing bounded → unbounded conversion encoding (which extracts the Int via the kind's `from` bridge). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…ject bitwise on integer Three independent improvements: 1. **`from` is now a domain function with range + injectivity axioms.** Previously `int8$from` was a top-level `vpr.Function` with a postcondition `-128 <= result <= 127`. There was no axiom expressing that two distinct domain values must have distinct `from`-images, so the verifier could not conclude that `to(n) == to(m)` (i.e. equal numeric values) implied equal domain values. With both axioms in place — together with `to`'s `from(to(n)) == n` postcondition — `from` is now characterised as a bijection between the kind's domain and `[lower, upper]` ⊂ Int. Implementation: `from` becomes a `vpr.DomainFunc` declared inside the per-kind `Bounded_<k>` domain, alongside two `NamedDomainAxiom`s: `<k>$from_in_range` (forall x: D :: lower <= from(x) && from(x) <= upper) and `<k>$from_injective` (forall x, y: D :: from(x) == from(y) ==> x == y). `fromApp` now produces a `DomainFuncApp`; the few sites that previously used `vpr.FuncApp(funcsOf(k).from, ...)` (the conv-cache builders for bounded↔bounded and integer→bounded) route through `fromApp` instead. 2. **`perm(x, y)` requires `integer` operands, not arbitrary int.** The conceptual signature of the fractional-permission constructor is `perm(integer, integer): perm`. The previous typing rule used `assignableTo.errors(numT, UNTYPED_INT_CONST, ...)`, which silently accepted any bounded integer kind because `assignableTo` treats bounded ints as assignable to UNTYPED_INT_CONST. The new rule requires `numT == IntT(UnboundedInteger)` (or `PermissionT` for the numerator) and emits a clear error otherwise. Affected stub: `stubs/sync/waitgroup.gobra` previously called `perm(-n, 1)` and `perm(n, 1)` with `n: int`; both call sites now wrap the bounded-int operand with an explicit `integer(...)`. 3. **Bitwise ops on `integer` are rejected — regression test added.** `regressions/features/integers/integer_bitwise_rejected.gobra` covers `&`, `|`, `^`, `&^`, unary `^`, `<<`, `>>` on `integer` operands; each is annotated `ExpectedOutput(type_error)`. Also pulled in the user's test-file edit to overflow_int64.gobra adding `incrementOverflows2` (overflow inside an `integer(...)`-wrapped spec expression) and aligning the `incrementOverflows` annotation with the spec-position report. Verified focused suites: - `regressions/features/integers` 22/22 pass. - `regressions/features/overflow_checks` 3/5 (same as before; the two remaining failures are the spec-position annotation mismatches that are intended behaviour). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Termination measures over bounded integer values (e.g. `decreases n`
where `n: int`) failed to verify because Viper had no
`<Bounded_int>WellFoundedOrder` domain providing the
`decreasing`/`bounded` axioms instantiated for the kind's domain
type. Decreases-tuple type collection picks `decreases/all.vpr`
for any DomainType (other than predicate-instance), which gives the
abstract `WellFoundedOrder[T]` declaration; we now provide the
type-specific instantiation.
For each kind `k` whose domain is emitted, finalize() also emits
`Bounded_<k>WellFoundedOrder { axiom <k>$dec_ax; axiom <k>$bounded_ax }`:
forall x, y: Bounded_<k> :: { decreasing(x, y) }
from(x) < from(y) ==> decreasing(x, y)
forall x: Bounded_<k> :: { bounded(x) } bounded(x)
The `bounded` axiom is unconditional because the range axiom on
`from` already guarantees `lower <= from(x)` for every domain
value, and the Int order on `[lower, upper]` is well-founded.
Smoke-tested with a recursive function decreasing on `int` and
`int8`; both verify. `regressions/features/integers` 22/22 still
pass; `GobraPackageTests` improves from 10 to 8 failures (the
`fib` and `byte` packages, both of which had termination errors,
now pass).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Previously, the explicit ghost type `integer` and the "untyped integer constant" used to type literals before context inference shared the *same* internal representation: `IntT(UnboundedInteger)`. The `assignableTo` rules treat `UNTYPED_INT_CONST` (= `IntT(UntypedConst)` = `IntT(UnboundedInteger)`) as freely assignable to any `IntT`: case (UNTYPED_INT_CONST, r) if underlyingType(r).isInstanceOf[IntT] => … case (l, UNTYPED_INT_CONST) if underlyingType(l).isInstanceOf[IntT] => … That rule is correct for *literals*, but because `i: integer` had the same type tag as a literal, expressions like forall i integer :: … byteCache[i].value == i silently type-checked, even though `byteCache[i].value` is a `byte` and `i` is an `integer` — a mismatch that should be a type error. Fix: introduce a new `IntegerKind`, `UntypedConstInteger`, used exclusively for untyped constants. `TypeBounds.UntypedConst` now defaults to `UntypedConstInteger` (so `UNTYPED_INT_CONST` becomes `IntT(UntypedConstInteger)`), while the explicit `integer` ghost type continues to use `UnboundedInteger`. The two kinds are encoded identically in Viper (both as `vpr.Int`), so `TypePatterns.UnboundedInt` matches both — the encoding is unaffected. `merge` is updated symmetrically: untyped const adapts to its sibling, but `UnboundedInteger` does NOT auto-merge with bounded kinds (would otherwise hide errors like `int + integer`). Also widened a stale `IntT(UnboundedInteger)` match in the shift bound calculation in `ExprTyping`, and the bitwise-not / shift constant evaluation cases in `ConstantEvaluation`, to additionally accept `UntypedConstInteger` (literals in those positions are still mathematical). Verified `regressions/features/integers` 22/22 still pass. The `same_package/pkg_init/byte/` package now reports the expected type errors on `byteCache[j].value == j` after the user's `forall j byte → forall j integer` rewrite. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
`int8$add`, `int8$sub`, …, `int8$div`, `int8$mod`, the four bitwise
binary functions, and the two shift functions all returned `Int`,
forcing every call site to wrap the result with `int8$wrap` to lift it
back into the domain. The wrap step was lossy in spec context (the
post `inRange(x) ==> from(result) == x` is conditional, so out-of-range
values became unconstrained even when the producing arithmetic could
have been precise) and added a redundant Viper round-trip on every
arithmetic expression.
Change the signatures to `(domTyp, …): domTyp` and express the contract
directly on `from(result)`:
function int8$add(x: int8, y: int8): int8
[requires inRange(from(x) + from(y))] // when --overflow
ensures [inRange(from(x) + from(y)) ==>]
from(result) == from(x) + from(y)
The conditional post intentionally leaves the result unconstrained on
overflow without --overflow — same loss-of-information as before, just
not double-applied. The bitwise binary and shift functions now have an
empty postcondition (no need for `inRange(result)` since the result is
already an in-range domain value via the `from`/range axiom).
Removed the `wrap` call in `handleBoundedBinOp` and the shift handlers;
each just yields the bare `FuncApp`. The `wrap` function itself is
retained because `asDomain` still uses it to lift an Unbounded operand
into the domain (rare with the litD kind-propagation fix, but still
reachable for e.g. `Length`-typed operands in mixed expressions).
Also relaxed the `perm(num, den)` typing rule to additionally accept
`UntypedConstInteger` operands. After the previous commit split untyped
constants from the typed `integer` kind, literal arguments like
`perm(1, 2)` had type `IntT(UntypedConstInteger)` and the strict rule
rejected them.
`regressions/features/integers` 22/22 still pass; `errors.gobra` (which
uses `perm(1, 2)`) and the waitgroup stub's `perm(integer(-n), 1)` now
type-check.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The previous bounded-int encoding emitted two axioms that interact badly
with each other and with arithmetic-function postconditions:
- `from_injective`: `forall x, y :: { from(x), from(y) }
from(x) == from(y) ==> x == y`
The pair trigger `{from(x), from(y)}` is N²: every new `from(...)` term
in scope (and arithmetic posts manufacture one per call site) matches
against every existing from-term, scaling instantiations quadratically
in the number of bounded-int values present in the proof state.
- The `to` function had a precondition `inRange(x)` and a function
postcondition `from(result) == x`, requiring per-call-site precondition
discharge.
This commit:
* Promotes `to` to a total domain function (no precondition), making it
a pure rewrite at the SMT level. Its defining property is now a single
domain axiom triggered on `to(n)`:
forall n: Int :: { to(n) } inRange(n) ==> from(to(n)) == n
* Drops `from_injective` entirely. The encoder's `equal` override
already reduces equality on bounded ints to equality on the
`from`-images, so injectivity is never relied upon at the Viper level.
* Updates the two `to` call sites (default value `to(0)`, integer
literal `to(lit.v)`) to use `DomainFuncApp` instead of `FuncApp`.
I considered also emitting the inverse axiom
`forall x: Bounded_int :: { from(x) } to(from(x)) == x`,
but that creates a genuine matching loop with `from_to_inverse`: an
instantiation of `to(from(x))` matches the latter's `to(n)` trigger and
introduces `from(to(from(x)))`, which in turn matches the former's
`from(x)` trigger and introduces `to(from(to(from(x))))`, ad infinitum.
Z3's depth heuristics bound this in practice but the cascade is wasted
work; we keep only the one direction.
`regressions/features/integers` and `regressions/features/overflow_checks`
still complete (no hangs); the StatsCollectorTests bottleneck is in
Silicon's symbolic execution of `dynamic_pred_0` (interface-dispatch
predicate with deeply nested CondExp body) and is independent of these
axioms — see commit chain for follow-up work there.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…integer-type-semantics-RUVTQ'
…integer-type-semantics-RUVTQ'
The domain-typed encoding made the abstract arithmetic/bitwise/shift helper
functions take domain-typed parameters and refer to from(x)/from(y) of those
universally quantified parameters in their postconditions. Silicon turns each
function postcondition into a quantified axiom; because `from` appears on
essentially every bounded term, Z3's e-matching kept instantiating those
axioms against the `to`/`from` bridge axioms without termination — a matching
loop that manifested as Gobra hanging on the StatsCollector tests (which run
with the default --overflow off).
Keep the helpers over Int (exactly as the pre-domain-types encoding, which was
never prone to this loop) and apply from/to only at concrete, ground call
sites: a bounded binary op `l <op> r` of kind k is encoded as
k$to( k$op( k$from(l), k$from(r) ) )
where the Int-valued helper k$op carries the range contract (and the overflow
precondition when checking) and the domain function k$to lifts the in-range
result back into the domain.
After this change the only quantified axioms over a domain are `from`'s range
axiom (trigger { from(x) }) and `to`'s inverse axiom (trigger { to(n) }).
Neither produces a term matching the other's trigger, so e-matching
terminates.
Also:
- Remove the now-unused `wrap` function; asDomain converts via `to`.
- Replace the bounded->bounded conversion function with integerToBounded
composed with `from` (no domain-typed quantified `from` either).
- Drop the dead Names.boundedIntWrap / Names.boundedIntConv helpers.
https://claude.ai/code/session_01VLNTKs1NTzfhQjBz8u5y1U
The pipeline only logged "<phase> done" at debug level, so at the default INFO level a hang showed no indication of which phase was stuck. Add an INFO-level "Phase N/6: <name>" marker at the start of each phase (parsing, type-checking, desugaring, internal transformations, Viper encoding, backend verification). The last marker printed before a hang now identifies the phase — in particular it distinguishes a frontend loop (e.g. type-checking) from a Z3 e-matching loop (backend verification). Promotes the local `timeFormatter` to a field on the GoVerifier trait so the phase methods can reuse it. https://claude.ai/code/session_01VLNTKs1NTzfhQjBz8u5y1U
… roundtrips
Quantifiers over bounded-int values compile comparisons like 0 <= j to
int$from(j) >= 0, so Silver's trigger inference discovers { k$from(j) } as a
valid trigger set. Since from appears on essentially every bounded ground term
in a trace, such a trigger fires for every bounded term the prover ever
creates: each loop iteration mints fresh terms, each of which re-instantiates
every from-triggered quantifier — the instantiation explosion that made
Silicon time out on e.g. monotonicset/bounded.gobra (256-iteration loop over a
uint16-keyed map, previously "did not terminate", now 45s / 0 errors).
Add ViperUtil.dropBoundedFromOnlyTriggers, applied after every autoTrigger in
AssertionEncoding: trigger sets consisting solely of bounded-int from
applications are dropped whenever container- or heap-based sets (m[j],
j in domain(m), ...) exist. This restores exactly the trigger discipline of
the pre-domain encoding, where plain integer comparisons contributed no
trigger candidates at all. from-only sets are kept when they are the sole
candidates — an untriggered quantifier would be strictly worse.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…er side
Reinstate the injectivity of the from bridge function as a domain axiom with
the pair trigger { from(x), from(y) }: its body introduces no new function
terms (only an equality between already-existing quantified terms), so unlike
the to(from(x)) == x direction — which chains with from(to(n)) == n into an
ever-growing term matching loop — it cannot feed e-matching divergence; worst
case it costs O(n^2) instantiations over ground from-terms. Without it,
equality on bounded domain values does not reflect integer equality, which
breaks map-key and set-membership reasoning (dict[int], set[uint16], ...).
Comparisons and equalities now accept a bounded operand on EITHER side
(previously only the left operand was handled, and MemoryEncoding's guard
only checked the left operand): both operands are projected to Int, applying
from to the bounded one(s). Literals and default values fold to their plain
Int value instead of from(to(c)) — sound since the type checker guarantees
bounded literals are in range — keeping quantifier bodies free of to/from
chatter that both bloats terms and feeds trigger inference.
Also drop the unused Names.integer* and boundedIntNeg helpers.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
With bounded integers encoded as opaque Viper domain types, every place that mixes a bounded value with a Viper Int slot (or vice versa) must convert explicitly; this fixes the remaining sort-mismatch crashes surfaced by a full regression sweep: - Container indices (sequence/array/slice/string, incl. SeqDrop/SeqTake and ghost updates) project bounded — including defined-type (`type T uint8`) — indices to Int via IntKindAlignment.asUnboundedInt, resolving underlying types through the encoding context. - make([]T, n) / make(map[K]V, n) / make(chan T, n) size checks project their size argument before building raw Viper comparisons; the synthesized BufferSize() call now declares the configured Go int kind (plumbed into ChannelEncoding like BuiltInEncoding). - Range sequences follow the frontend-inferred element kind: the desugarer wraps seq[a..b] in a bounded-element context with a Conversion that SequenceEncoding encodes via a generated per-kind Seq[Int] -> Seq[Bounded_k] mapping function (seqToBounded). - ADT match patterns route literal comparisons through the equality dispatch instead of raw EqCmp; map literals align their value kinds; option types push kind alignment into the some/none constructor; conditionals fold constant untyped operands (e.g. -1) into the bounded sibling kind. - in.BinaryIntExpr.typ uses a lenient kind merge: the desugarer synthesizes arithmetic mixing user expressions with internally-created integer-kinded nodes (range-loop indices, len/cap results); the strict merge remains the frontend type-checking rule. - Fix in.MapValues.typ returning the map's key type instead of its value type (pre-existing copy-paste bug, exposed by `5 elem range(m)` kind alignment). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…nteger` Ghost values are not adaptable constants: `len` of a ghost collection, set/ multiset cardinalities, multiplicities, and option projections of untyped elements now have the mathematical `integer` type instead of the untyped- constant kind, matching the ghost `integer` design (and the typing unit tests). Range sequences follow their bounds: mathematical unless a bound has a concrete bounded kind (e.g. `seq[x..y]` with x, y int). To keep spec idioms like `len(s) == y - x + 1` (integer vs. bounded int) type-checking, typeMerge now merges `integer` with any integer kind — to `integer`, never to the bounded kind, so assignments still require explicit conversions; the encoding projects the bounded side via its total `from` bridge. Also add the Skolem-inverse name for bounded-int injectivity. The stats_collector Area specs get upper bounds so their multiplication obligations are provable (and fast) under the sound no-overflow-assumption semantics; unbounded `width * height > 0` is not provable and its unprovable nonlinear query made Z3 diverge in the chopper configuration (the sbt-test stall). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Introduce a --unboundedIntegers flag (also usable as an in-file `// ##(...)` option) that encodes every integer type — including bounded types like int, int8, uint16, ... — as Viper's mathematical (unbounded) Int, restoring Gobra's integer encoding prior to the sound bounded-integer semantics. The flag is a single switch at the two type-pattern matchers that drive integer-encoding routing: under the flag, `BoundedInt` matches nothing and `UnboundedInt` matches every integer kind. As a result BoundedIntEncoding never fires, the bounded-comparison guards in MemoryEncoding are inert, and all integers flow through IntEncoding exactly as before the bounded semantics were introduced — the arithmetic range contracts on bounded operations disappear because those abstract helper functions are no longer generated. Every other code path (type checking, desugaring, constant evaluation) is unchanged. The flag is plumbed through Config like int32bit and threaded into the translator Context so the pattern matchers can consult it. Because unbounded integers have no bounds to overflow, --unboundedIntegers is rejected in combination with --overflow. Adds a regression test exercising the flag via the in-file option. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019XmXB7YEeszsGbsE14pVUU
`len` on ghost collections (sequences, sets, ...) now has the mathematical `integer` type rather than a bounded `int`. Type the helper functions' results as `integer` accordingly so `return len(s)` no longer produces a spurious type error. The intended type error — passing the `integer`-typed `len(xs)` where a `seq[int]` is expected — is preserved. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019XmXB7YEeszsGbsE14pVUU
Both tests rely on the previous unbounded-integer encoding: - issues/000659: the quantified permission `forall i int :: acc(s.nodes[i])` is no longer provably injective under the bounded-integer encoding, so the fold fails before the expected assertion error. - features/termination/termination-fail-01: `n+1` may overflow under bounded integers, so the loop invariant `i <= n+1` is not established and the expected termination error is masked. Pass `--unboundedIntegers` as an in-file option so these programs verify as originally intended. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019XmXB7YEeszsGbsE14pVUU
`positiveSumWithoutTrusted` relies on `x > 0 && y > 0 ==> x + y > 0`, which no longer holds under the sound bounded-integer encoding because `x + y` may overflow, producing an unexpected postcondition error. Pass `--unboundedIntegers` as an in-file option so the test verifies as originally intended. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019XmXB7YEeszsGbsE14pVUU
The parallel-sum, pair-insertion-sort and search-replace evaluation examples prove properties over sums of slice elements and over index arithmetic that are only valid for mathematical integers: once bounded integers may overflow, the sums become opaque and the specifications are no longer provable. Pass `--unboundedIntegers` as an in-file option so these examples verify under the integer encoding they were written against, mirroring the annotation into the impl_errors/spec_errors variants of the same examples. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019XmXB7YEeszsGbsE14pVUU
`len` on a ghost sequence has the mathematical `integer` type, which is not assignable to `int`. Passing `len(pseqs)` directly as the `int` id argument of `wg.TokenById` is therefore a type error. Convert it explicitly with `int(...)`. This is a type-checking fix, independent of the integer encoding: the `--unboundedIntegers` in-file option does not affect assignability, so these three examples failed to type-check even with it set. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019XmXB7YEeszsGbsE14pVUU
Add negative checks to the flag's regression test: with --unboundedIntegers the bounded kinds get no range axioms, so a uint8 is an arbitrary mathematical integer and neither its non-negativity nor an int8's upper bound is provable. Both assertions are expected to fail; if either ever starts verifying, the bounded range axioms are leaking into the unbounded encoding. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019XmXB7YEeszsGbsE14pVUU
A quantifier variable of a bounded integer kind ranges over exactly the values of that type: 'forall x uint8 :: x >= 0' holds, and the range needs no explicit statement in the quantifier. This replaces the previous mathematical-sort binding (193ddab), which read quantifiers over all integers. The desugarer binds the variable at its declared type again. To keep the performance that motivated the mathematical binding, the assertion encoding lowers each bounded bound variable to an Int-sorted Viper variable plus an explicit 'lower <= x <= upper' guard, rewriting 'k$from(x)' occurrences to the variable itself and remaining domain-sorted occurrences to 'k$to(x)'. By the bridge axioms (from is injective and from(to(n)) == n on the range), this is equivalent to quantifying over the domain, while quantified permissions keep linear injective receivers ('acc(&s[i])' uses 'i' directly). Triggers are rewritten alongside; a trigger that degenerates to a bare variable is dropped, falling back to auto-triggering. The lowering covers forall, exists, quantified permissions, and assign-such-that, and is a no-op under --unboundedIntegers. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Found running the bounded-int semantics on VerifiedSCION's pkg/addr: 'parsed |= AS(v)' (with 'type AS uint64') crashed the encoder with "cannot merge types AS_..._T and uint64". in.BinaryIntExpr.typ only accepted a defined type next to an unbounded or untyped-constant integer operand — the only kinds that existed before bounded semantics. A conversion like 'AS(v)' now yields the underlying bounded kind, and the type-checker may assign untyped constants a concrete kind, so a defined type merges with an operand of any integer kind (the result is the defined type, relying on the frontend having type-checked the program). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Found on VerifiedSCION pkg/addr ('h & ^SVCMcast' with 'type HostSVC
uint16'): in.BitNeg inherited IntOperation's unbounded-Int typ, but the
bounded encoding produces a domain-typed value for it. Enclosing operations
use the node's typ to decide whether the domain-to-Int projection is still
needed, so the mismatch passed a Bounded_uint16 value straight into the
Int-typed uint16$band helper — a Viper consistency error. '^x' now reports
its operand's type, matching how binary integer expressions merge theirs.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The Int-plus-range-guard lowering breaks witness finding for existentials: 'exists n int :: true' encodes to an existential whose body is a pure arithmetic guard, which gives Z3 no term to instantiate, and the regression suite lost every assign-such-that witness the same way. Universals keep the lowering (that is where quantified-permission receivers and stub unification matter); existentials and the assign-such-that witness check bind the variable at the domain sort instead — SMT sorts are non-empty, domain values are intrinsically in-range, and ground to/from terms anchor instantiation, so no guard is needed. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Go guarantees that len/cap of any array, slice, or string fits in int. Under bounded integer semantics this fact is needed for completeness: a user's quantified footprint over an int-typed index variable is implicitly range-guarded, and without an upper bound on the container's length it no longer entails internally generated footprints that quantify over the mathematical integers. Found on VerifiedSCION's pkg/addr, where 'string(text)' under the standard byte-slice footprint spec failed the generated conversion function's precondition. The ShArray, Slice, and String domains now carry 'len <= MaxInt' axioms (also cap for slices), with MaxInt taken from the configured int kind (64-bit by default, 32-bit under --int32). The axioms are omitted under --unboundedIntegers, preserving the old encoding there. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The bounded encoding turns spec arithmetic like 'i + j' into applications of abstract helper functions (int$add, ...). Silver's automatic trigger inference treated those like any function application and picked them as trigger terms, so a quantifier such as 'forall i, j :: a[i][j] == i + j' got triggers requiring a ground int$add(1, 2) term that never exists (constant arithmetic is folded) — the quantifier silently never instantiated (array-index-simple1/2 regressions). The helpers are now registered with silver's trigger generation as neither possible trigger terms nor allowed inside them, exactly like the interpreted '+' they replace. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
A package imported under two spellings (e.g. "encoding/binary" via an
include path and "verification/dependencies/encoding/binary" via the
project root) resolved to the same directory but produced two distinct
package ids ("./x/y" vs "x/y"), because Path.relativize falls back to
the unnormalized path for relative inputs. The package was then parsed,
type-checked, and encoded twice while the Viper member names (derived from
the absolutized source paths) coincided — yielding hundreds of duplicate-
identifier consistency errors on VerifiedSCION's pkg/slayers/path. Both
paths are now absolutized and normalized before the id is derived.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…axiom
Universally quantified bounded variables used at their domain sort (map
keys, set elements, function arguments) were rewritten to 'to(v)'. A
trigger like '{ m[to(v)] }' can never e-match a ground 'm[i]': the linking
equality 'to(from(i)) == i' is only derivable through a 'to(from(i))' term
that nothing creates, so such quantifiers silently failed to instantiate
(VerifiedSCION's monoset: every fact about a dict[int64] under a
quantifier). Domain occurrences are now rewritten to 'inv(v)' instead —
the injectivity axiom already creates 'inv(from(i)) == i' anchors for
every ground projected value, so lowered triggers match via congruence.
A fourth bridge axiom 'forall n :: { inv(n) } inRange(n) ==> from(inv(n))
== n' (surjectivity of from onto its range) lets proofs establish facts
about 'inv(v)' for an arbitrary in-range v, e.g. call preconditions inside
quantified postconditions. Triggered on 'inv(n)', it stays inert unless
lowered quantifier terms exist and creates no new term classes — no
matching loop.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The bounded-int adaptation of this test (1eb2f3c) introduced pure/ghost members without decreases clauses, which the termination checker rejects. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
'let x := len(b) in ...' crashed the backend under bounded semantics (consistency error "No matching local variable ... with type Bounded_int, instead found Int", or Silicon's "key not found"): the desugarer typed the binder from the right-hand side's internal type (unbounded for length expressions) while the body's references to the variable resolve at the frontend type (bounded int), so binder and uses encoded at different Viper sorts. Binders are now typed at the frontend type, and the Let encodings align the bound right-hand side with the binder's encoded sort (to/from wrap), mirroring the assignment normalization. Found on VerifiedSCION's pkg/slayers/path/scion. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The closure implements a spec that carries termination measures, so the implementation proof requires the closure to declare one as well. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
A pure function returning a bounded kind can have a body that encodes to
plain Int — e.g. a conditional whose branches are untyped-constant
arithmetic ('b ? MetadataLen : MetadataLen + 1') — producing an ill-sorted
vpr.Function ("Type of function body must match function type"). The pure
method/function encodings now wrap the body with the to/from bridge when
its encoded sort differs from the declared result sort, mirroring the let
and assignment normalizations. Found on VerifiedSCION's
pkg/slayers/path/epic.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
# Conflicts: # src/main/resources/stubs/sync/waitgroup.gobra # src/main/scala/viper/gobra/ast/internal/Program.scala # src/test/resources/regressions/examples/evaluation/impl_errors/parallel_search_replace.gobra # src/test/resources/regressions/examples/evaluation/impl_errors/parallel_sum.gobra # src/test/resources/regressions/examples/evaluation/parallel_search_replace.gobra # src/test/resources/regressions/examples/evaluation/parallel_sum.gobra # src/test/resources/regressions/examples/evaluation/spec_errors/parallel_search_replace.gobra # src/test/resources/regressions/examples/evaluation/spec_errors/parallel_sum.gobra # src/test/resources/regressions/examples/parallel_search_replace_shared.gobra # src/test/resources/regressions/examples/tutorial-examples/channels.gobra # src/test/resources/regressions/examples/tutorial-examples/multi-channel.gobra # src/test/resources/regressions/features/channels/channel-simple-buffered1.gobra # src/test/resources/regressions/features/channels/channel-simple-buffered2.gobra # src/test/resources/regressions/features/channels/channel-simple5.gobra # src/test/resources/regressions/features/channels/channel-simple6.gobra # src/test/resources/regressions/features/channels/channel-simple7.gobra # src/test/resources/regressions/features/channels/foo/foo.gobra # src/test/resources/regressions/features/channels/multi-channel-simple1.gobra # src/test/resources/regressions/features/defunc/waitgroup-fail1.gobra # src/test/resources/regressions/features/defunc/waitgroup-simple1.gobra # src/test/resources/regressions/issues/000695.gobra # src/test/resources/same_package/pkg_init/concfib/fib.go
'float64(i)' with a bounded i crashed the encoder with a Viper consistency error: the int<->float conversion functions (fromIntTo64, from64ToInt, ...) operate on Viper Ints, but a bounded-kind operand encodes to a domain value. The operand is now projected to its integer image on the way in (reusing IntKindAlignment.asUnboundedInt, which also resolves defined types whose underlying type is bounded), and an Int result is lifted back into the target's domain on the way out. Found on VerifiedSCION's router (dataplane.go) and verification/utils/floats. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The merge brought in master's restructuring of PFunctionSpec, which merges the pres/preserves/posts vectors into a single clauses vector. The bounded- integer typing tests still passed five vectors, so isPure was supplied both positionally and by name. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…e-UFkBe' into claude/integer-type-semantics-RUVTQ # Conflicts: # src/main/resources/stubs/sync/waitgroup.gobra # src/main/scala/viper/gobra/ast/internal/Program.scala # src/main/scala/viper/gobra/ast/internal/transform/OverflowChecksTransform.scala # src/main/scala/viper/gobra/translator/context/DfltTranslatorConfig.scala # src/test/resources/regressions/examples/tutorial-examples/channels.gobra # src/test/resources/regressions/features/defunc/waitgroup-simple1.gobra # src/test/resources/same_package/pkg_init/concfib/fib.go
…tfdry' into claude/integer-type-semantics-RUVTQ # Conflicts: # src/main/scala/viper/gobra/ast/internal/Program.scala
…o claude/integer-type-semantics-RUVTQ The base branch gained the type-checking port (#1083), which is a subset of this branch's work, so the two collided in 8 files. Resolutions: * Program.scala: keep this branch's generalized defined-type cases (`case (x: DefinedT, _: IntT)`), which the port narrowed to UnboundedInteger|UntypedConstInteger because it has no bounded conversions. Take the port's corrected mergeLenient comment: the original rationale here (desugarer-synthesized range-loop increments) is wrong -- i0 and the synthesized IntLit both default to UnboundedInteger and merge trivially. The real reason is that TypeMerging accepts `integer` mixed with a bounded kind, so `len(s) - i` reaches BinaryIntExpr.typ with two kinds. Drop the now-unused UntypedConstInteger import. * The 7 .gobra tests: keep this branch's versions. The port applied only the type-checking-driven subset of these same changes, so the conflicts are the explanatory comments it left out. Also picks up features/integers/integer-bounded-mix.gobra from the port, which pins the mergeLenient requirement. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
jcp19
changed the title
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
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.
Do not review yet
Summary
This PR replaces the AST-level overflow checking transformation with a new encoding-based approach for bounded integer types. Instead of instrumenting the AST with explicit overflow checks, bounded integer arithmetic operations are now translated to abstract Viper functions with range postconditions, enabling more efficient and precise overflow verification.
Key Changes
New BoundedIntEncoding class: Implements a
LeafTypeEncodingthat handles all bounded integer types (int8, uint8, int16, uint16, int32, uint32, int64, uint64, byte, rune, uintptr) by:vpr.Intat the Viper levelcheckOverflowsis enabledRemoved OverflowChecksTransform: Deleted the AST-level transformation that previously added explicit overflow check assertions throughout the program, reducing AST instrumentation overhead
Updated IntEncoding: Modified to only handle unbounded integers (the ghost
integertype) by:ctx.Int()toctx.UnboundedInt()Enhanced type checking: Added validation to prevent bitwise operations on the unbounded
integertype, which is mathematically undefined for bitwise operationsUpdated Names object: Added naming functions for bounded integer operations and conversion functions to support the new encoding
Updated TypePatterns: Added
BoundedIntandUnboundedIntpattern matchers to distinguish between bounded and unbounded integer typesUpdated translator configuration: Integrated
BoundedIntEncodinginto the type encoding pipelineImplementation Details
Bounded integer arithmetic functions use abstract Viper functions with:
Division and modulo operations implement Go's truncation-towards-zero semantics using conditional expressions
Shift operations require non-negative shift amounts via preconditions
Type conversions between bounded kinds and from unbounded to bounded are handled through dedicated conversion functions with appropriate range contracts
Error transformation maps Viper precondition failures to
OverflowErrorandShiftPreconditionErrorfor better error reportinghttps://claude.ai/code/session_01VLNTKs1NTzfhQjBz8u5y1U