From 08b48c8d56bbec5a2cf1ad158c81902ee7f4beab Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Sat, 21 Oct 2023 20:02:38 +0200 Subject: [PATCH] Empty ( // @ e == nil && // @ o.Mem() && @@ -66,38 +67,38 @@ type Path struct{} // @ e.ErrorMem() && // @ o.NonInitMem()) // @ decreases -func (o Path) DecodeFromBytes(r []byte) (e error) { +func (o *Path) DecodeFromBytes(r []byte) (e error) { if len(r) != 0 { - //@ fold o.NonInitMem() return serrors.New("decoding an empty path", "len", len(r)) } + //@ unfold o.NonInitMem() //@ fold o.Mem() return nil } // @ ensures e == nil // @ decreases -func (o Path) SerializeTo(b []byte /*@, ghost ub []byte @*/) (e error) { +func (o *Path) SerializeTo(b []byte /*@, ghost ub []byte @*/) (e error) { return nil } // @ ensures p == o // @ ensures e == nil // @ decreases -func (o Path) Reverse( /*@ ghost ub []byte @*/ ) (p path.Path, e error) { +func (o *Path) Reverse( /*@ ghost ub []byte @*/ ) (p path.Path, e error) { return o, nil } // @ pure // @ ensures 0 <= r // @ decreases -func (o Path) Len( /*@ ghost ub []byte @*/ ) (r int) { +func (o *Path) Len( /*@ ghost ub []byte @*/ ) (r int) { return PathLen } // @ pure // @ ensures r == PathType // @ decreases -func (o Path) Type( /*@ ghost ub []byte @*/ ) (r path.Type) { +func (o *Path) Type( /*@ ghost ub []byte @*/ ) (r path.Type) { return PathType } diff --git a/pkg/slayers/path/empty/empty_spec.gobra b/pkg/slayers/path/empty/empty_spec.gobra index 0bd49a6b2..c068d47fd 100644 --- a/pkg/slayers/path/empty/empty_spec.gobra +++ b/pkg/slayers/path/empty/empty_spec.gobra @@ -21,25 +21,6 @@ import ( "github.com/scionproto/scion/verification/utils/slices" ) -Path implements path.Path - -pred (e Path) Mem() { true } -pred (e Path) NonInitMem() { true } - -ghost -decreases -pure func (e Path) Valid(ghost ub []byte) bool { - return len(ub) == 0 -} - -ghost -ensures e.NonInitMem() -decreases -func (e Path) DowngradePerm(buf []byte) { - unfold e.Mem() - fold e.NonInitMem() -} - // Definitions to allow *Path to be treated as a path.Path (*Path) implements path.Path diff --git a/pkg/slayers/path/empty/empty_spec_test.gobra b/pkg/slayers/path/empty/empty_spec_test.gobra index 6e5898d80..826cec1f9 100644 --- a/pkg/slayers/path/empty/empty_spec_test.gobra +++ b/pkg/slayers/path/empty/empty_spec_test.gobra @@ -17,11 +17,11 @@ package empty func FoldNonInitMem_test() { - e := Path{} + e@ := Path{} fold e.NonInitMem() } func FoldMem_test() { - e := Path{} + e@ := Path{} fold e.Mem() } diff --git a/pkg/slayers/path/hopfield.go b/pkg/slayers/path/hopfield.go index b4141cc85..6cb8a4c7b 100644 --- a/pkg/slayers/path/hopfield.go +++ b/pkg/slayers/path/hopfield.go @@ -77,6 +77,7 @@ type HopField struct { // @ requires len(raw) >= HopLen // @ preserves acc(h) // @ preserves acc(slices.AbsSlice_Bytes(raw, 0, HopLen), R45) +// @ ensures h.Valid() // @ ensures err == nil // @ decreases func (h *HopField) DecodeFromBytes(raw []byte) (err error) { diff --git a/pkg/slayers/path/scion/base_spec.gobra b/pkg/slayers/path/scion/base_spec.gobra index 04c3031ab..78e9296ae 100644 --- a/pkg/slayers/path/scion/base_spec.gobra +++ b/pkg/slayers/path/scion/base_spec.gobra @@ -21,6 +21,7 @@ import ( sl "github.com/scionproto/scion/verification/utils/slices" ) +// TODO: drop pred (b *Base) NonInitMem() { acc(b) } diff --git a/pkg/slayers/path/scion/decoded.go b/pkg/slayers/path/scion/decoded.go index 7e9c9012f..13c72fdff 100644 --- a/pkg/slayers/path/scion/decoded.go +++ b/pkg/slayers/path/scion/decoded.go @@ -56,8 +56,8 @@ type Decoded struct { // @ let b3 := sl.GetByte(data, 0, lenD, 3) in // @ let line := binary.BigEndian.Uint32Spec(b0, b1, b2, b3) in // @ let metaHdr := DecodedFrom(line) in -// @ metaHdr == s.GetMetaHdr(data) && -// @ s.InfsMatchHfs(data)) +// @ metaHdr == s.GetMetaHdr() && +// @ s.InfsMatchHfs()) // @ ensures r != nil ==> (r.ErrorMem() && s.NonInitMem()) // @ decreases func (s *Decoded) DecodeFromBytes(data []byte) (r error) { @@ -106,8 +106,8 @@ func (s *Decoded) DecodeFromBytes(data []byte) (r error) { //@ invariant acc(s.Base.Mem(), R1) //@ invariant len(s.HopFields) == s.Base.GetNumHops() //@ invariant 0 <= i && i <= s.Base.GetNumHops() - //@ invariant forall j int :: { &s.HopFields[j] } i <= j && j < s.Base.GetNumHops() ==> acc(&s.HopFields[j]) - //@ invariant forall j int :: { &s.HopFields[j] } 0 <= j && j < i ==> s.HopFields[j].Mem() + //@ invariant forall j int :: { &s.HopFields[j] } 0 <= j && j < s.Base.GetNumHops() ==> acc(&s.HopFields[j]) + //@ invariant forall j int :: { &s.HopFields[j] } 0 <= j && j < i ==> s.HopFields[j].Valid() //@ invariant len(data) >= MetaLen + s.Base.GetNumINF() * path.InfoLen + s.Base.GetNumHops() * path.HopLen //@ invariant offset == MetaLen + s.Base.GetNumINF() * path.InfoLen + i * path.HopLen //@ invariant acc(sl.AbsSlice_Bytes(data, 0, offset), R41) @@ -155,7 +155,7 @@ func (s *Decoded) SerializeTo(b []byte /*@, ghost ubuf []byte @*/) (r error) { //@ fold acc(s.Base.Mem(), R1) //@ sl.Unslice_Bytes(b, 0, MetaLen, writePerm) //@ sl.CombineAtIndex_Bytes(b, 0, len(b), MetaLen, writePerm) - //@ fold acc(s.Mem(ubuf), R1) + //@ fold acc(s.Mem(), R1) offset := MetaLen //@ invariant acc(s.Mem(), R1) && s.Valid(ubuf) @@ -182,10 +182,10 @@ func (s *Decoded) SerializeTo(b []byte /*@, ghost ubuf []byte @*/) (r error) { //@ sl.Unslice_Bytes(b, offset, offset + path.InfoLen, writePerm) //@ sl.CombineAtIndex_Bytes(b, offset, len(b), offset + path.InfoLen, writePerm) //@ sl.CombineAtIndex_Bytes(b, 0, len(b), offset, writePerm) - //@ fold acc(s.Mem(ubuf), R1) + //@ fold acc(s.Mem(), R1) offset += path.InfoLen } - //@ invariant acc(s.Mem(ubuf), R1) + //@ invariant acc(s.Mem(), R1) && s.Valid(ubuf) //@ invariant sl.AbsSlice_Bytes(ubuf, 0, len(ubuf)) //@ invariant b !== ubuf ==> sl.AbsSlice_Bytes(b, 0, len(b)) //@ invariant s.Len(ubuf) <= len(b) @@ -215,18 +215,19 @@ func (s *Decoded) SerializeTo(b []byte /*@, ghost ubuf []byte @*/) (r error) { } // Reverse reverses a SCION path. -// @ requires s.Mem(ubuf) +// @ requires s.Mem() && s.Valid(ubuf) // @ ensures r == nil ==> ( // @ p != nil && -// @ p.Mem(ubuf) && +// @ p.Mem() && +// @ p.Valid(ubuf) && // @ p == s && // @ typeOf(p) == type[*Decoded] && -// @ (old(s.ValidCurrIdxs(ubuf)) ==> s.ValidCurrIdxs(ubuf))) -// @ ensures r != nil ==> r.ErrorMem() && s.Mem(ubuf) +// @ (old(s.ValidCurrIdxs()) ==> s.ValidCurrIdxs())) +// @ ensures r != nil ==> r.ErrorMem() && s.Mem() // @ decreases func (s *Decoded) Reverse( /*@ ghost ubuf []byte @*/ ) (p path.Path, r error) { - //@ ghost isValid := s.ValidCurrIdxs(ubuf) - //@ unfold s.Mem(ubuf) + //@ ghost isValid := s.ValidCurrIdxs() + //@ unfold s.Mem() //@ unfold s.Base.Mem() if s.NumINF == 0 { //@ fold s.Base.Mem() @@ -234,14 +235,14 @@ func (s *Decoded) Reverse( /*@ ghost ubuf []byte @*/ ) (p path.Path, r error) { return nil, serrors.New("empty decoded path is invalid and cannot be reversed") } //@ fold s.Base.Mem() - //@ fold s.Mem(ubuf) - //@ ghost base := s.GetBase(ubuf) + //@ fold s.Mem() + //@ ghost base := s.GetBase() // Reverse order of InfoFields and SegLens - //@ invariant s.Mem(ubuf) - //@ invariant isValid ==> s.ValidCurrIdxs(ubuf) - //@ invariant 0 <= i && i < s.GetNumINF(ubuf) - //@ invariant 0 <= j && j < s.GetNumINF(ubuf) + //@ invariant s.Mem() && s.Valid(ubuf) + //@ invariant isValid ==> s.ValidCurrIdxs() + //@ invariant 0 <= i && i < s.GetNumINF() + //@ invariant 0 <= j && j < s.GetNumINF() //@ decreases j-i for i, j := 0, ( /*@ unfolding s.Mem() in (unfolding s.Base.Mem() in @*/ s.NumINF - 1 /*@) @*/); i < j; i, j = i+1, j-1 { //@ unfold s.Mem() @@ -249,10 +250,10 @@ func (s *Decoded) Reverse( /*@ ghost ubuf []byte @*/ ) (p path.Path, r error) { //@ unfold s.Base.Mem() s.PathMeta.SegLen[i], s.PathMeta.SegLen[j] = s.PathMeta.SegLen[j], s.PathMeta.SegLen[i] //@ fold s.Base.Mem() - //@ fold s.Mem(ubuf) + //@ fold s.Mem() } - //@ preserves s.Mem(ubuf) - //@ preserves isValid ==> s.ValidCurrIdxs(ubuf) + //@ preserves s.Mem() && s.Valid(ubuf) + //@ preserves isValid ==> s.ValidCurrIdxs() //@ decreases //@ outline( //@ unfold s.Mem() @@ -273,25 +274,21 @@ func (s *Decoded) Reverse( /*@ ghost ubuf []byte @*/ ) (p path.Path, r error) { // Reverse order of hop fields //@ invariant s.Mem() && s.Valid(ubuf) - //@ invariant 0 <= i && i <= s.GetNumHops(ubuf) - //@ invariant -1 <= j && j < s.GetNumHops(ubuf) - //@ invariant isValid ==> s.ValidCurrIdxs(ubuf) + //@ invariant 0 <= i && i <= s.GetNumHops() + //@ invariant -1 <= j && j < s.GetNumHops() + //@ invariant isValid ==> s.ValidCurrIdxs() //@ decreases j-i for i, j := 0, ( /*@ unfolding s.Mem() in (unfolding s.Base.Mem() in @*/ s.NumHops - 1 /*@ ) @*/); i < j; i, j = i+1, j-1 { //@ unfold s.Mem() //@ assert &s.HopFields[i] != &s.HopFields[j] - //@ unfold s.HopFields[i].Mem() - //@ unfold s.HopFields[j].Mem() //@ assert acc(&s.HopFields[i]) && acc(&s.HopFields[j]) s.HopFields[i], s.HopFields[j] = s.HopFields[j], s.HopFields[i] //@ assert acc(&s.HopFields[i]) && acc(&s.HopFields[j]) - //@ fold s.HopFields[i].Mem() - //@ fold s.HopFields[j].Mem() //@ fold s.Mem() } // Update CurrINF and CurrHF and SegLens - //@ preserves s.Mem(ubuf) - //@ preserves isValid ==> s.ValidCurrIdxs(ubuf) + //@ preserves s.Mem() && s.Valid(ubuf) + //@ preserves isValid ==> s.ValidCurrIdxs() //@ decreases //@ outline( //@ unfold s.Mem() diff --git a/pkg/slayers/path/scion/decoded_spec.gobra b/pkg/slayers/path/scion/decoded_spec.gobra index 86e2cb1ec..de6ee95d0 100644 --- a/pkg/slayers/path/scion/decoded_spec.gobra +++ b/pkg/slayers/path/scion/decoded_spec.gobra @@ -26,6 +26,7 @@ import ( /**** Predicates ****/ +// TODO: drop? pred (d *Decoded) NonInitMem() { acc(&d.InfoFields) && acc(&d.HopFields) && @@ -40,7 +41,7 @@ pred (d *Decoded) Mem() { (forall i int :: { &d.InfoFields[i] } 0 <= i && i < len(d.InfoFields) ==> acc(&d.InfoFields[i])) && acc(&d.HopFields) && len(d.HopFields) == d.Base.GetNumHops() && - (forall i int :: { &d.HopFields[i] } 0 <= i && i < len(d.HopFields) ==> d.HopFields[i].Mem()) + (forall i int :: { &d.HopFields[i] } 0 <= i && i < len(d.HopFields) ==> acc(&d.HopFields[i])) } ghost @@ -48,9 +49,9 @@ requires acc(d.Mem(), _) decreases pure func (d *Decoded) Valid(ghost ub []byte) bool { return unfolding acc(d.Mem(), _) in ( - d.Base.getNumINF() <= MaxINFs && - len(d.InfoFields) == d.Base.getNumINF() && - len(d.HopFields) == d.Base.getNumHops() && + d.Base.GetNumINF() <= MaxINFs && + len(d.InfoFields) == d.Base.GetNumINF() && + len(d.HopFields) == d.Base.GetNumHops() && (forall i int :: { &d.HopFields[i] } 0 <= i && i < len(d.HopFields) ==> d.HopFields[i].Valid())) } @@ -92,11 +93,11 @@ func (d *Decoded) Type(ghost ubuf []byte) (t path.Type) { * Unfortunately, Gobra does not fully support them yet, so we * introduced this method which acts as a wrapper. */ -preserves acc(d.Mem(ubuf), R19) +preserves acc(d.Mem(), R19) decreases func (d *Decoded) IsXover(ghost ubuf []byte) bool { - unfold acc(d.Mem(ubuf), R19) - defer fold acc(d.Mem(ubuf), R19) + unfold acc(d.Mem(), R19) + defer fold acc(d.Mem(), R19) return d.Base.IsXover() } @@ -109,10 +110,10 @@ func (d *Decoded) IsXover(ghost ubuf []byte) bool { */ requires d.Mem() && d.Valid(ubuf) ensures e == nil ==> ( - d.Mem(ubuf) && - d.Valid(ubuf) && + d.Mem() && + d.Valid(ubuf) && d.Len(ubuf) == old(d.Len(ubuf)) && - (old(d.ValidCurrIdxs(ubuf)) ==> d.ValidCurrIdxs(ubuf))) + (old(d.ValidCurrIdxs()) ==> d.ValidCurrIdxs())) ensures e != nil ==> d.NonInitMem() && e.ErrorMem() decreases func (d *Decoded) IncPath(ghost ubuf []byte) (e error) { @@ -127,52 +128,52 @@ func (d *Decoded) IncPath(ghost ubuf []byte) (e error) { } ghost -requires acc(d.Mem(ub), _) +requires acc(d.Mem(), _) decreases -pure func (d *Decoded) ValidCurrINF(ub []byte) bool { - return unfolding acc(d.Mem(ub), _) in d.Base.ValidCurrINF() +pure func (d *Decoded) ValidCurrINF() bool { + return unfolding acc(d.Mem(), _) in d.Base.ValidCurrINF() } ghost -requires acc(d.Mem(ub), _) +requires acc(d.Mem(), _) decreases -pure func (d *Decoded) ValidCurrHF(ub []byte) bool { - return unfolding acc(d.Mem(ub), _) in d.Base.ValidCurrHF() +pure func (d *Decoded) ValidCurrHF() bool { + return unfolding acc(d.Mem(), _) in d.Base.ValidCurrHF() } ghost -requires acc(d.Mem(ub), _) +requires acc(d.Mem(), _) decreases -pure func (d *Decoded) ValidCurrIdxs(ub []byte) bool { - return unfolding acc(d.Mem(ub), _) in d.Base.ValidCurrIdxs() +pure func (d *Decoded) ValidCurrIdxs() bool { + return unfolding acc(d.Mem(), _) in d.Base.ValidCurrIdxs() } ghost -requires acc(d.Mem(ub), _) +requires acc(d.Mem(), _) decreases -pure func (d *Decoded) GetNumINF(ub []byte) (res int) { - return unfolding acc(d.Mem(ub), _) in d.Base.GetNumINF() +pure func (d *Decoded) GetNumINF() (res int) { + return unfolding acc(d.Mem(), _) in d.Base.GetNumINF() } ghost -requires acc(d.Mem(ub), _) +requires acc(d.Mem(), _) decreases -pure func (d *Decoded) GetNumHops(ub []byte) (res int) { - return unfolding acc(d.Mem(ub), _) in d.Base.GetNumHops() +pure func (d *Decoded) GetNumHops() (res int) { + return unfolding acc(d.Mem(), _) in d.Base.GetNumHops() } ghost -requires acc(s.Mem(ub), _) +requires acc(s.Mem(), _) decreases -pure func (s *Decoded) GetMetaHdr(ub []byte) MetaHdr { - return unfolding acc(s.Mem(ub), _) in s.Base.GetMetaHdr() +pure func (s *Decoded) GetMetaHdr() MetaHdr { + return unfolding acc(s.Mem(), _) in s.Base.GetMetaHdr() } ghost -requires acc(d.Mem(ub), _) +requires acc(d.Mem(), _) decreases -pure func (d *Decoded) InfsMatchHfs(ub []byte) bool { - return unfolding acc(d.Mem(ub), _) in d.Base.InfsMatchHfs() +pure func (d *Decoded) InfsMatchHfs() bool { + return unfolding acc(d.Mem(), _) in d.Base.InfsMatchHfs() } /**** End of Stubs ****/ @@ -192,10 +193,10 @@ pure func (d *Decoded) getLenHopFields() int { } ghost -requires acc(d.Mem(ubuf), _) +requires acc(d.Mem(), _) decreases -pure func (d *Decoded) GetBase(ubuf []byte) Base { - return unfolding acc(d.Mem(ubuf), _) in +pure func (d *Decoded) GetBase() Base { + return unfolding acc(d.Mem(), _) in (unfolding acc(d.Base.Mem(), _) in d.Base) } diff --git a/pkg/slayers/path/scion/raw.go b/pkg/slayers/path/scion/raw.go index 57f42de6e..d40f49d10 100644 --- a/pkg/slayers/path/scion/raw.go +++ b/pkg/slayers/path/scion/raw.go @@ -133,18 +133,18 @@ func (s *Raw) Reverse( /*@ ghost ubuf []byte @*/ ) (p path.Path, err error) { // @ preserves acc(s.Mem(), R5) && s.Valid(ubuf) // @ preserves sl.AbsSlice_Bytes(ubuf, 0, len(ubuf)) // @ ensures err == nil ==> ( -// @ let newUb := s.RawBufferMem(ubuf) in +// @ let newUb := s.RawBufferMem() in // @ d.Mem() && // @ d.Valid(newUb) && -// @ (old(s.ValidCurrIdxs(ubuf)) ==> d.ValidCurrIdxs(newUb))) +// @ (old(s.ValidCurrIdxs()) ==> d.ValidCurrIdxs())) // @ ensures err != nil ==> err.ErrorMem() // @ decreases func (s *Raw) ToDecoded( /*@ ghost ubuf []byte @*/ ) (d *Decoded, err error) { - //@ unfold acc(s.Mem(ubuf), R6) + //@ unfold acc(s.Mem(), R6) //@ unfold acc(s.Base.Mem(), R6) //@ ghost var base Base = s.Base //@ ghost var pathMeta MetaHdr = s.Base.PathMeta - //@ ghost validIdxs := s.ValidCurrIdxs(ubuf) + //@ ghost validIdxs := s.ValidCurrIdxs() //@ assert validIdxs ==> s.Base.PathMeta.InBounds() //@ assert validIdxs ==> base.ValidCurrIdxsSpec() //@ assert s.Raw[:MetaLen] === ubuf[:MetaLen] @@ -203,9 +203,9 @@ func (s *Raw) ToDecoded( /*@ ghost ubuf []byte @*/ ) (d *Decoded, err error) { //@ ghost lenR := len(s.Raw) // TODO: move to the top and rewrite body //@ ghost if validIdxs { //@ s.PathMeta.SerializeAndDeserializeLemma(b0, b1, b2, b3) - //@ assert pathMeta == decoded.GetMetaHdr(s.Raw) - //@ assert decoded.GetBase(s.Raw).ValidCurrIdxsSpec() - //@ assert decoded.ValidCurrIdxs(s.Raw) + //@ assert pathMeta == decoded.GetMetaHdr() + //@ assert decoded.GetBase().ValidCurrIdxsSpec() + //@ assert decoded.ValidCurrIdxs() //@ } //@ sl.Unslice_Bytes(ubuf, 0, len(s.Raw), HalfPerm) //@ sl.Unslice_Bytes(ubuf, 0, len(s.Raw), HalfPerm) @@ -343,7 +343,6 @@ func (s *Raw) GetHopField(idx int /*@, ghost ubuf []byte @*/) (res path.HopField return path.HopField{}, err } //@ s.UndoRawRangePerm(ubuf, hopOffset, hopOffset+path.HopLen, R10) - //@ unfold hop.Mem() return hop, nil } @@ -369,7 +368,7 @@ func (s *Raw) GetCurrentHopField( /*@ ghost ubuf []byte @*/ ) (res path.HopField // SetHopField updates the HopField at a given index. // @ requires 0 <= idx // @ preserves acc(s.Mem(), R20) && s.Valid(ubuf) -// @ preserves slices.AbsSlice_Bytes(ubuf, 0, len(ubuf)) +// @ preserves sl.AbsSlice_Bytes(ubuf, 0, len(ubuf)) // @ ensures r != nil ==> r.ErrorMem() // @ decreases func (s *Raw) SetHopField(hop path.HopField, idx int /*@, ghost ubuf []byte @*/) (r error) { @@ -377,7 +376,6 @@ func (s *Raw) SetHopField(hop path.HopField, idx int /*@, ghost ubuf []byte @*/) // (VerifiedSCION) Cannot assert bounds of uint: // https://github.com/viperproject/gobra/issues/192 //@ assume 0 <= hop.ConsIngress && 0 <= hop.ConsEgress - //@ fold hop.Mem() //@ unfold acc(s.Mem(), R20) //@ unfold acc(s.Base.Mem(), R20) if idx >= s.NumHops { diff --git a/pkg/slayers/path/scion/raw_spec.gobra b/pkg/slayers/path/scion/raw_spec.gobra index bde51c80f..196af33b3 100644 --- a/pkg/slayers/path/scion/raw_spec.gobra +++ b/pkg/slayers/path/scion/raw_spec.gobra @@ -96,35 +96,35 @@ func (s *Raw) IsFirstHopAfterXover(ghost ub []byte) (res bool) { * Unfortunately, Gobra does not fully support them yet, so we * introduced this wrapper method which acts as a wrapper. */ -preserves acc(s.Mem(), R9) && s.Valid(ub) +preserves acc(s.Mem(), R9) decreases -func (s *Raw) IsXover(ghost ub []byte) bool { +func (s *Raw) IsXover() bool { unfold acc(s.Mem(), R9) defer fold acc(s.Mem(), R9) return s.Base.IsXover() } ghost -requires acc(s.Mem(ub), _) +requires acc(s.Mem(), _) decreases -pure func (s *Raw) ValidCurrINF(ghost ub []byte) bool { - return unfolding acc(s.Mem(ub), _) in +pure func (s *Raw) ValidCurrINF() bool { + return unfolding acc(s.Mem(), _) in s.Base.ValidCurrINF() } ghost -requires acc(s.Mem(ub), _) +requires acc(s.Mem(), _) decreases -pure func (s *Raw) ValidCurrHF(ghost ub []byte) bool { - return unfolding acc(s.Mem(ub), _) in +pure func (s *Raw) ValidCurrHF() bool { + return unfolding acc(s.Mem(), _) in s.Base.ValidCurrHF() } ghost -requires acc(s.Mem(ub), _) +requires acc(s.Mem(), _) decreases -pure func (s *Raw) ValidCurrIdxs(ghost ub []byte) bool { - return unfolding acc(s.Mem(ub), _) in +pure func (s *Raw) ValidCurrIdxs() bool { + return unfolding acc(s.Mem(), _) in s.Base.ValidCurrIdxs() } @@ -133,11 +133,11 @@ pure func (s *Raw) ValidCurrIdxs(ghost ub []byte) bool { /**** Lemmas ****/ ghost -requires s.Mem() && s.Valid(buf) +requires s.Mem() ensures s.NonInitMem() ensures old(s.RawBufferMem()) === s.RawBufferNonInitMem() decreases -func (s *Raw) DowngradePerm(buf []byte) { +func (s *Raw) DowngradePerm(ghost ub []byte) { unfold s.Mem() unfold s.Base.Mem() fold s.Base.NonInitMem()