Merge branch 'master' into minit

viperproject · Jan 22, 2025 · 679a587 · 679a587
2 parents 6a33fab + 76a8578
commit 679a587
Show file tree

Hide file tree

Showing 9 changed files with 12 additions and 11 deletions.
diff --git a/.github/workflows/dafny.yml b/.github/workflows/dafny.yml
@@ -14,12 +14,13 @@ on:
 
 jobs:
   verify:
-    runs-on: ubuntu-latest
+    # Dafny fails for ubuntu-24.04 with error "no libssl found".
+    runs-on: ubuntu-22.04
     steps:
       - name: Checkout the current repository
         uses: actions/checkout@v3
       - name: "Install Dafny"
         uses: dafny-lang/setup-dafny-action@v1
       - name: "Verify bitwise operations."
         run: |
-          dafny verification/utils/bitwise/proofs.dfy
+          dafny verification/utils/bitwise/proofs.dfy
diff --git a/pkg/slayers/path/empty/empty_spec.gobra b/pkg/slayers/path/empty/empty_spec.gobra
@@ -37,7 +37,7 @@ func (e Path) DowngradePerm(buf []byte) {
 ghost
 pure
 decreases
-func (p Path) IsValidResultOfDecoding(b []byte, err error) (res bool) {
+func (p Path) IsValidResultOfDecoding(b []byte) bool {
 	return true
 }
 

diff --git a/pkg/slayers/path/epic/epic_spec.gobra b/pkg/slayers/path/epic/epic_spec.gobra
@@ -102,7 +102,7 @@ pure func (p *Path) GetUnderlyingScionPathBuf(buf []byte) []byte {
 ghost
 pure
 decreases
-func (p *Path) IsValidResultOfDecoding(b []byte, err error) (res bool) {
+func (p *Path) IsValidResultOfDecoding(b []byte) (res bool) {
 	return true
 }
 

diff --git a/pkg/slayers/path/onehop/onehop_spec.gobra b/pkg/slayers/path/onehop/onehop_spec.gobra
@@ -54,7 +54,7 @@ pure func (o *Path) InferSizeUb(ghost ub []byte) (b bool) {
 ghost
 pure
 decreases
-func (p *Path) IsValidResultOfDecoding(b []byte, err error) (res bool) {
+func (p *Path) IsValidResultOfDecoding(b []byte) (res bool) {
 	return true
 }
 

diff --git a/pkg/slayers/path/path.go b/pkg/slayers/path/path.go
@@ -85,17 +85,17 @@ type Path interface {
 	//@ requires  NonInitMem()
 	//@ preserves acc(sl.Bytes(b, 0, len(b)), R42)
 	//@ ensures   err == nil ==> Mem(b)
+	//@ ensures   err == nil ==> IsValidResultOfDecoding(b)
 	//@ ensures   err != nil ==> err.ErrorMem()
 	//@ ensures   err != nil ==> NonInitMem()
-	//@ ensures   err == nil ==> IsValidResultOfDecoding(b, err)
 	//@ decreases
 	DecodeFromBytes(b []byte) (err error)
 	//@ ghost
 	//@ pure
 	//@ requires Mem(b)
 	//@ requires acc(sl.Bytes(b, 0, len(b)), R42)
 	//@ decreases
-	//@ IsValidResultOfDecoding(b []byte, err error) (res bool)
+	//@ IsValidResultOfDecoding(b []byte) bool
 	// Reverse reverses a path such that it can be used in the reversed direction.
 	// XXX(shitz): This method should possibly be moved to a higher-level path manipulation package.
 	//@ requires  Mem(ub)

diff --git a/pkg/slayers/path/path_spec.gobra b/pkg/slayers/path/path_spec.gobra
@@ -43,7 +43,7 @@ func (p *rawPath) DowngradePerm(ghost buf []byte) {
 ghost
 pure
 decreases
-func (p *rawPath) IsValidResultOfDecoding(b []byte, err error) (res bool) {
+func (p *rawPath) IsValidResultOfDecoding(b []byte) bool {
 	return true
 }
 

diff --git a/pkg/slayers/path/scion/decoded_spec.gobra b/pkg/slayers/path/scion/decoded_spec.gobra
@@ -25,7 +25,7 @@ import (
 ghost
 pure
 decreases
-func (p *Decoded) IsValidResultOfDecoding(b []byte, err error) (res bool) {
+func (p *Decoded) IsValidResultOfDecoding(b []byte) (res bool) {
 	return true
 }
 

diff --git a/pkg/slayers/path/scion/raw_spec.gobra b/pkg/slayers/path/scion/raw_spec.gobra
@@ -46,7 +46,7 @@ pure
 requires  acc(s.Mem(buf), _)
 requires  acc(sl.Bytes(buf, 0, len(buf)), R42)
 decreases
-func (s *Raw) IsValidResultOfDecoding(buf []byte, err error) (res bool) {
+func (s *Raw) IsValidResultOfDecoding(buf []byte) (res bool) {
 	return let base := s.GetBase(buf) in
 		base.EqAbsHeader(buf) &&
 		base.WeaklyValid()

diff --git a/verification/dependencies/crypto/aes/cipher.gobra b/verification/dependencies/crypto/aes/cipher.gobra
@@ -25,7 +25,7 @@ ensures   err == nil ==>
 ensures   err == nil ==>
 	(result != nil &&
 	result.Mem()   &&
-	result.BlockSize() == len(key))
+	result.BlockSize() == BlockSize)
 ensures   err != nil ==> err.ErrorMem()
 decreases
 func NewCipher(key []byte) (result cipher.Block, err error)