Adapt according to upcomming syntax for perms - #426

Draft

jcp19 wants to merge 11 commits into

claude/verifiedscion-integer-types-2x4rsj

Commits on Jul 23, 2026

Migrate shared verification deps to new Gobra integer semantics
claude
committed
3babb2c
pkg/addr: drop range assumptions, adapt to bounded integer semantics
claude
committed
c05cd0f
pkg/slayers/path: adapt to bounded integers, enable overflow checks in CI
claude
committed
1712f21
strconv stub: drop tautological sign precondition on FormatUint
claude
committed
e4fc309
Fix quantifier layout in PkgMem: no line break after trigger set
claude
committed
e9375cb
Lift ghost offset arithmetic into the integer domain
claude
committed
633c785
Move ghost offset parameters of path/slices specs to integer
claude
committed
d435d72
pkg/slayers/path/scion: begin bounded-integer migration (base, raw)
claude
committed
d6557a0
pkg/slayers/path/scion: lift ghost offset layer to integer
claude
committed
3688375
onehop, epic: drop workaround casts and tautological postconditions
claude
committed
0d6c3ef
epic: harmonize encoding/binary spec import with code import
claude
committed
f3ca81f