Adapt according to upcomming syntax for perms - #426
Draft
jcp19 wants to merge 11 commits into
Draft
Conversation
- Use the new perm(p, q) syntax for fractional permission literals. - Turn integer-typed fields of ghost types (io.Ifs, io.AS, io.Ainfo, MsgTerm_Num, SegLens) into unbounded mathematical 'integer's, and lift the ghost functions operating on them accordingly. - Move strconv.Exp to the integer domain (Exp(2, 64) does not fit a bounded int) and give ParseUint a bound postcondition instead of relying on callers assuming ranges; add Exp2_16/Exp2_32 lemmas to concretize the bounds needed by pkg/addr. - Add bitwise.ShiftRight48Bits lemma (with Dafny proof) to justify the narrowing conversion in addr.IA.ISD(). - Fix ByteValue lemma bound (256 is not representable in a byte). - Add MIN_INT/MAX_INT constants to the definitions package. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MZR7Q1Yq9zBGZ65EoUHjqF
With the new Gobra integer semantics, unsigned types are known to be non-negative, so the 'assume 0 <= ...' workarounds in fmtAS and the 'isd >= 0' precondition are no longer needed. Narrowing conversions now carry proof obligations instead: - ParseISD/asParseBGP discharge them via the strconv.Exp2_16/Exp2_32 lemmas (replacing the previous inline assertion chains). - IA.ISD() uses the new bitwise.ShiftRight48Bits lemma. - PackWithPad gets a precondition bounding pad so the buffer size computation cannot overflow. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MZR7Q1Yq9zBGZ65EoUHjqF
…n CI - Drop the ConsIngress/ConsEgress non-negativity conjuncts from (*HopField).Mem(): they now follow from the uint16 type. - Drop tautological '0 <= t && t < maxPathType' bounds on path.Type (uint8 with maxPathType == 256), including inside PkgMem. - Adapt ghost conversions to the integer-typed IO-spec fields: IO_ifsToIfs requires the abstract interface ID to fit a uint16, and the now-pointless uint(...) wrappers around Ainfo values are gone. - Type the MaxPathType ghost const explicitly as int. - CI: enable overflow checking for pkg/addr and pkg/slayers/path. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MZR7Q1Yq9zBGZ65EoUHjqF
Under bounded integer semantics, i >= 0 holds by type for uint64. This precondition was the reason call sites needed 'assume 0 <= x' workarounds. pkg/addr verifies cleanly without it. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MZR7Q1Yq9zBGZ65EoUHjqF
Gobra's parser rejects a newline immediately after a quantifier trigger. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MZR7Q1Yq9zBGZ65EoUHjqF
Under overflow checking, spec expressions like 'middle + HopLen <= end'
or 'headerOffset + InfoLen * currINF' carry overflow obligations that
are not dischargeable for unconstrained ints. Move this ghost arithmetic
to unbounded integers: InfoFieldOffset now returns integer,
AssertSliceOverlap takes integer bounds (int arguments widen
implicitly), and the affected preconditions widen one operand.
Also import the encoding/binary stub under the same path as the code
files ('encoding/binary') to avoid the package being loaded twice under
two different identifiers.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01MZR7Q1Yq9zBGZ65EoUHjqF
Adopt the rule that ghost-layer byte offsets, indices and lengths live in the unbounded integer domain: the slices ghost API (Bytes predicate, GetByte, Split/Combine/Reslice/Unslice helpers) and the offset-taking ghost functions of pkg/slayers/path now take integer parameters. Code level callers are unaffected since bounded values widen implicitly. This removes the explicit integer(...) casts introduced previously and lets SegLens-derived integer values flow without conversions. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MZR7Q1Yq9zBGZ65EoUHjqF
- Drop the four 'assume 0 <= ...' uint-bounds workarounds (base.go, raw.go): non-negativity of unsigned values is now given by the types. - Fix SegLen sums in specs and invariants to accumulate in the int domain (int(a) + int(b)) to match the code, instead of summing in uint8 where the addition could wrap. - Drop sign conjuncts on uint8 values from ValidCurrInfSpec and ValidCurrHfSpec; expose the NumHops upper bound in GetNumHops. - Harmonize the encoding/binary spec imports (raw_spec, widen-lemma follow in the next commit) to avoid loading the stub under two package identities. - Drop casts in a serrors.New call that are no longer needed. Verification status: local runs pending; the ghost-layer integer lift of raw_spec/decoded_spec/lemma files lands in a follow-up commit. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MZR7Q1Yq9zBGZ65EoUHjqF
Move the byte-offset/index/length parameters and returns of the ghost functions in raw_spec.gobra, info_hop_setter_lemmas.gobra and widen-lemma.gobra to the unbounded integer type, so that values derived from io.SegLens flow without conversions and the ghost arithmetic is overflow-free by construction. Code-level int values widen implicitly at the boundary. The only remaining integer->int boundary is in RawBytesToBase, where ghost values initialize the code-level int fields of Base and an explicit int(...) conversion is required. Also harmonize the encoding/binary spec imports with the code imports (same fix as in pkg/slayers/path) to avoid loading the stub twice. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MZR7Q1Yq9zBGZ65EoUHjqF
The int(...) casts in serrors.New calls were workarounds for an old type-checker limitation; the 0 <= Timestamp/Counter postconditions on PktID.DecodeFromBytes are implied by the uint32 field types under the new bounded integer semantics. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MZR7Q1Yq9zBGZ65EoUHjqF
Same fix as in pkg/slayers/path and pkg/slayers/path/scion: importing the binary stub under two different paths makes Gobra load it as two packages and fail consistency checking with duplicate identifiers. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MZR7Q1Yq9zBGZ65EoUHjqF
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
2 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.
No description provided.