Drop specific permission amounts in pure functions's preconditions (#387

)

* test

* Apply suggestions from code review

* Update pkg/slayers/path/epic/epic_spec.gobra

* Update pkg/slayers/path/epic/epic_spec.gobra

* drop unnecessary formalization of waitgroups

* tiny change

* drop access predicates

* stabilize verification conditions that now fail

* fix yet one more proof obligation; extract code into additional theorem

* yet another proof obligation fixed

* refactor widen lemma for HopField to reuse a previous proof

* fix bad triggers generated by Gobra

* Refactor parts of scion_spec.gobra for proof stability (#389)

* backup

* cleanup

* Update pkg/slayers/scion.go

* Update pkg/slayers/scion_spec.gobra

* backup

* backup

* backup

* backup

* fix proof obligation in CurrSegEquality

* drop Uncallable

* fix outstanding proof obligations

* drop unnecessary function

* backup

* restore old spec

* add gobra action cfg

* Update pkg/slayers/path/path_spec.gobra

* Fix `doXover` on the new semantics (#395)

* start

* identify problematic postconditions

* drop one assumption

* drop comments

* fix proof of new postconditions of XoverLemma

* small simplifications

* drop yet another assumption

* drop last assumption

.github/workflows/gobra.yml

@@ -27,6 +27,7 @@ env:
   disableNL: '0'
   unsafeWildcardOptimization: '1'
   overflow: '0'
+  respectFunctionPrePermAmounts: '0'
 
 jobs:
   verify-deps:
@@ -69,6 +70,7 @@ jobs:
           disableNL: ${{ env.disableNL }}
           viperBackend: ${{ env.viperBackend }}
           unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
+          respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }}
       - name: Verify package 'pkg/addr'
         uses: viperproject/gobra-action@main
         with:
@@ -89,6 +91,7 @@ jobs:
           disableNL: ${{ env.disableNL }}
           viperBackend: ${{ env.viperBackend }}
           unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
+          respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }}
       - name: Verify package 'pkg/experimental/epic'
         uses: viperproject/gobra-action@main
         with:
@@ -108,6 +111,7 @@ jobs:
           disableNL: ${{ env.disableNL }}
           viperBackend: ${{ env.viperBackend }}
           unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
+          respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }}
       - name: Verify package 'pkg/log'
         uses: viperproject/gobra-action@main
         with:
@@ -127,6 +131,7 @@ jobs:
           disableNL: ${{ env.disableNL }}
           viperBackend: ${{ env.viperBackend }}
           unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
+          respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }}
       - name: Verify package 'pkg/private/serrors'
         uses: viperproject/gobra-action@main
         with:
@@ -146,6 +151,7 @@ jobs:
           disableNL: ${{ env.disableNL }}
           viperBackend: ${{ env.viperBackend }}
           unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
+          respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }}
       - name: Verify package 'pkg/scrypto'
         uses: viperproject/gobra-action@main
         with:
@@ -165,6 +171,7 @@ jobs:
           disableNL: ${{ env.disableNL }}
           viperBackend: ${{ env.viperBackend }}
           unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
+          respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }}
       - name: Verify package 'pkg/slayers'
         uses: viperproject/gobra-action@main
         with:
@@ -184,6 +191,7 @@ jobs:
           disableNL: ${{ env.disableNL }}
           viperBackend: ${{ env.viperBackend }}
           unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
+          respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }}
       - name: Verify package 'pkg/slayers/path'
         uses: viperproject/gobra-action@main
         with:
@@ -203,6 +211,7 @@ jobs:
           disableNL: ${{ env.disableNL }}
           viperBackend: ${{ env.viperBackend }}
           unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
+          respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }}
       - name: Verify package 'pkg/slayers/path/empty'
         uses: viperproject/gobra-action@main
         with:
@@ -222,6 +231,7 @@ jobs:
           disableNL: ${{ env.disableNL }}
           viperBackend: ${{ env.viperBackend }}
           unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
+          respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }}
       - name: Verify package 'pkg/slayers/path/epic'
         uses: viperproject/gobra-action@main
         with:
@@ -242,6 +252,7 @@ jobs:
           disableNL: ${{ env.disableNL }}
           viperBackend: ${{ env.viperBackend }}
           unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
+          respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }}
       - name: Verify package 'pkg/slayers/path/onehop'
         uses: viperproject/gobra-action@main
         with:
@@ -261,6 +272,7 @@ jobs:
           disableNL: ${{ env.disableNL }}
           viperBackend: ${{ env.viperBackend }}
           unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
+          respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }}
       - name: Verify package 'pkg/slayers/path/scion'
         uses: viperproject/gobra-action@main
         with:
@@ -280,6 +292,7 @@ jobs:
           disableNL: ${{ env.disableNL }}
           viperBackend: ${{ env.viperBackend }}
           unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
+          respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }}
       - name: Verify package 'private/topology'
         uses: viperproject/gobra-action@main
         with:
@@ -299,6 +312,7 @@ jobs:
           disableNL: ${{ env.disableNL }}
           viperBackend: ${{ env.viperBackend }}
           unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
+          respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }}
       - name: Verify package 'private/topology/underlay'
         uses: viperproject/gobra-action@main
         with:
@@ -318,6 +332,7 @@ jobs:
           disableNL: ${{ env.disableNL }}
           viperBackend: ${{ env.viperBackend }}
           unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
+          respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }}
       - name: Verify package 'private/underlay/conn'
         uses: viperproject/gobra-action@main
         with:
@@ -337,6 +352,7 @@ jobs:
           disableNL: ${{ env.disableNL }}
           viperBackend: ${{ env.viperBackend }}
           unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
+          respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }}
       - name: Verify package 'private/underlay/sockctrl'
         uses: viperproject/gobra-action@main
         with:
@@ -356,6 +372,7 @@ jobs:
           disableNL: ${{ env.disableNL }}
           viperBackend: ${{ env.viperBackend }}
           unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
+          respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }}
       - name: Verify package 'router/bfd'
         uses: viperproject/gobra-action@main
         with:
@@ -375,6 +392,7 @@ jobs:
           disableNL: ${{ env.disableNL }}
           viperBackend: ${{ env.viperBackend }}
           unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
+          respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }}
       - name: Verify package 'router/control'
         uses: viperproject/gobra-action@main
         with:
@@ -394,6 +412,7 @@ jobs:
           disableNL: ${{ env.disableNL }}
           viperBackend: ${{ env.viperBackend }}
           unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
+          respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }}
       - name: Upload the verification report
         uses: actions/upload-artifact@v4
         with:
@@ -426,3 +445,4 @@ jobs:
           disableNL: '0'
           viperBackend: ${{ env.viperBackend }}
           unsafeWildcardOptimization: '0'
+          respectFunctionPrePermAmounts: ${{ env.respectFunctionPrePermAmounts }}

pkg/addr/isdas.go

@@ -241,8 +241,8 @@ func (ia *IA) UnmarshalText(b []byte) error {
 	return nil
 }
 
-// @ pure
 // @ decreases
+// @ pure
 func (ia IA) IsZero() bool {
 	return ia == 0
 }

pkg/experimental/epic/epic.go

@@ -205,7 +205,8 @@ func CoreFromPktCounter(counter uint32) (uint8, uint32) {
 
 // @ requires  len(key) == 16
 // @ preserves acc(sl.Bytes(key, 0, len(key)), R50)
-// @ ensures   reserr == nil ==> res != nil && res.Mem() && res.BlockSize() == 16
+// @ ensures   reserr == nil ==>
+// @ 	res != nil && res.Mem() && res.BlockSize() == 16
 // @ ensures   reserr != nil ==> reserr.ErrorMem()
 // @ decreases
 func initEpicMac(key []byte) (res cipher.BlockMode, reserr error) {

pkg/experimental/epic/epic_spec.gobra

@@ -19,13 +19,14 @@ package epic
 import sl "github.com/scionproto/scion/verification/utils/slices"
 
 pred postInitInvariant() {
-	acc(&zeroInitVector, _) &&
+	acc(&zeroInitVector) &&
 	len(zeroInitVector[:]) == 16 &&
-	acc(sl.Bytes(zeroInitVector[:], 0, len(zeroInitVector[:])), _)
+	acc(sl.Bytes(zeroInitVector[:], 0, len(zeroInitVector[:])))
 }
 
 // learn the invariant established by init
 ghost
+trusted // TODO: drop after init invs are added
 ensures acc(postInitInvariant(), _)
 decreases _
 func establishPostInitInvariant()

pkg/scrypto/scrypto_spec.gobra

@@ -27,7 +27,7 @@ import sl "github.com/scionproto/scion/verification/utils/slices"
 // calls to it will also succeed. This behaviour is abstracted using this
 // ghost function.
 ghost
-requires  acc(sl.Bytes(key, 0, len(key)), _)
+requires  sl.Bytes(key, 0, len(key))
 decreases _
 pure func ValidKeyForHash(key []byte) bool
 

pkg/slayers/extn.go

@@ -158,7 +158,7 @@ func serializeTLVOptionPadding(data []byte, padLength int) {
 // serializeTLVOptions serializes options to buf and returns the length of the serialized options.
 // Passing in a nil-buffer will treat the serialization as a dryrun that can be used to calculate
 // the length needed for the buffer.
-// @ requires Uncallable()
+// @ requires false
 func serializeTLVOptions(buf []byte, options []*tlvOption, fixLengths bool) (res int) {
 	dryrun := buf == nil
 	// length start at 2 since the padding needs to be calculated taking the first 2 bytes of the
@@ -326,7 +326,7 @@ func (h *HopByHopExtn) LayerPayload( /*@ ghost ub []byte @*/ ) (res []byte /*@ ,
 }
 
 // SerializeTo implementation according to gopacket.SerializableLayer.
-// @ requires Uncallable()
+// @ requires false
 func (h *HopByHopExtn) SerializeTo(b gopacket.SerializeBuffer,
 	opts gopacket.SerializeOptions) error {
 
@@ -561,7 +561,7 @@ func checkEndToEndExtnNextHdr(t L4ProtocolType) (err error) {
 }
 
 // SerializeTo implementation according to gopacket.SerializableLayer
-// @ requires Uncallable()
+// @ requires false
 func (e *EndToEndExtn) SerializeTo(b gopacket.SerializeBuffer,
 	opts gopacket.SerializeOptions) error {
 
@@ -579,7 +579,7 @@ func (e *EndToEndExtn) SerializeTo(b gopacket.SerializeBuffer,
 
 // FindOption returns the first option entry of the given type if any exists,
 // or ErrOptionNotFound otherwise.
-// @ requires Uncallable()
+// @ requires false
 func (e *EndToEndExtn) FindOption(typ OptionType) (*EndToEndOption, error) {
 	for _, o := range e.Options {
 		if o.OptType == typ {

pkg/slayers/extn_spec.gobra

@@ -52,7 +52,7 @@ pred (h *HopByHopExtn) Mem(ubuf []byte) {
 
 // Gobra is not able to infer that HopByHopExtn is "inheriting"
 // the implementation of LayerContents from extnBase.
-requires Uncallable()
+requires false
 func (h *HopByHopExtn) LayerContents() (res []byte) {
 	res = h.BaseLayer.LayerContents()
 	return res
@@ -85,7 +85,7 @@ pred (h *HopByHopExtnSkipper) Mem(ubuf []byte) {
 
 // Gobra is not able to infer that HopByHopExtnSkipper is "inheriting"
 // the implementation of LayerContents from extnBase.
-requires Uncallable()
+requires false
 func (h *HopByHopExtnSkipper) LayerContents() (res []byte) {
 	res = h.BaseLayer.LayerContents()
 	return res
@@ -140,7 +140,7 @@ pred (e *EndToEndExtn) Mem(ubuf []byte) {
 
 // Gobra is not able to infer that EndToEndExtn is "inheriting"
 // the implementation of LayerContents from extnBase.
-requires Uncallable()
+requires false
 func (e *EndToEndExtn) LayerContents() (res []byte) {
 	res = e.BaseLayer.LayerContents()
 	return res
@@ -175,7 +175,7 @@ pred (e *EndToEndExtnSkipper) Mem(ubuf []byte)  {
 
 // Gobra is not able to infer that EndToEndExtnSkipper is "inheriting"
 // the implementation of LayerContents from extnBase.
-requires Uncallable()
+requires false
 func (e *EndToEndExtnSkipper) LayerContents() (res []byte) {
 	res = e.BaseLayer.LayerContents()
 	return res

pkg/slayers/path/empty/empty_spec.gobra

@@ -35,16 +35,14 @@ func (e Path) DowngradePerm(buf []byte) {
 }
 
 ghost
-pure
 decreases
-func (p Path) IsValidResultOfDecoding(b []byte) bool {
+pure func (p Path) IsValidResultOfDecoding(b []byte) bool {
 	return true
 }
 
 ghost
-pure
 decreases
-func (p Path) LenSpec(ghost ub []byte) (l int) {
+pure func (p Path) LenSpec(ghost ub []byte) (l int) {
 	return PathLen
 }
 

pkg/slayers/path/epic/epic.go

@@ -225,7 +225,6 @@ func (p *Path) Len( /*@ ghost ubuf []byte @*/ ) (l int) {
 
 // Type returns the EPIC path type identifier.
 // @ pure
-// @ requires acc(p.Mem(ubuf), _)
 // @ ensures  t == PathType
 // @ decreases
 func (p *Path) Type( /*@ ghost ubuf []byte @*/ ) (t path.Type) {

pkg/slayers/path/epic/epic_spec.gobra

@@ -38,11 +38,10 @@ pred (p *Path) Mem(ubuf []byte) {
 }
 
 ghost
-pure
-requires acc(p.Mem(ub), _)
+requires p.Mem(ub)
 decreases
-func (p *Path) LenSpec(ghost ub []byte) (l int) {
-	return unfolding acc(p.Mem(ub), _) in
+pure func (p *Path) LenSpec(ghost ub []byte) (l int) {
+	return unfolding p.Mem(ub) in
 		(p.ScionPath == nil ?
 			MetadataLen :
 			MetadataLen + p.ScionPath.LenSpec(ub[MetadataLen:]))
@@ -58,51 +57,48 @@ func (p *Path) DowngradePerm(buf []byte) {
 }
 
 ghost
-requires acc(r.Mem(ub), _)
+requires r.Mem(ub)
 decreases
 pure func (r *Path) GetBase(ub []byte) scion.Base {
-	return unfolding acc(r.Mem(ub), _) in
+	return unfolding r.Mem(ub) in
 		r.ScionPath.GetBase(ub[MetadataLen:])
 }
 
 ghost
-pure
-requires acc(p.Mem(buf), _)
-ensures l == (unfolding acc(p.Mem(buf), _) in len(p.PHVF))
+requires p.Mem(buf)
 decreases
-func (p *Path) getPHVFLen(buf []byte) (l int) {
-	return unfolding acc(p.Mem(buf), _) in len(p.PHVF)
+pure func (p *Path) getPHVFLen(buf []byte) (l int) {
+	return unfolding p.Mem(buf) in
+		len(p.PHVF)
 }
 
 ghost
-pure
-requires acc(p.Mem(buf), _)
-ensures l == (unfolding acc(p.Mem(buf), _) in len(p.LHVF))
+requires p.Mem(buf)
 decreases
-func (p *Path) getLHVFLen(buf []byte) (l int) {
-	return unfolding acc(p.Mem(buf), _) in len(p.LHVF)
+pure func (p *Path) getLHVFLen(buf []byte) (l int) {
+	return unfolding p.Mem(buf) in
+		len(p.LHVF)
 }
 
 ghost
-pure
-requires acc(p.Mem(buf), _)
-ensures  r == (unfolding acc(p.Mem(buf), _) in p.ScionPath != nil)
+requires p.Mem(buf)
 decreases
-func (p *Path) hasScionPath(buf []byte) (r bool) {
-	return unfolding acc(p.Mem(buf), _) in p.ScionPath != nil
+pure func (p *Path) hasScionPath(buf []byte) (r bool) {
+	return unfolding p.Mem(buf) in
+		p.ScionPath != nil
 }
 
 ghost
-requires acc(p.Mem(buf), _)
+requires p.Mem(buf)
 decreases
 pure func (p *Path) GetUnderlyingScionPathBuf(buf []byte) []byte {
-	return unfolding acc(p.Mem(buf), _) in buf[MetadataLen:]
+	return unfolding p.Mem(buf) in
+		buf[MetadataLen:]
 }
 
 ghost
-pure
 decreases
-func (p *Path) IsValidResultOfDecoding(b []byte) (res bool) {
+pure func (p *Path) IsValidResultOfDecoding(b []byte) (res bool) {
 	return true
 }