Merge branch 'master' into temp

pkg/slayers/path/scion/raw.go

@@ -443,7 +443,7 @@ func (s *Raw) SetHopField(hop path.HopField, idx int /*@, ghost ubuf []byte @*/)
  //@ unfold acc(s.Mem(ubuf), R20)
  //@ unfold acc(s.Base.Mem(), R20)
  if idx >= s.NumHops {
- // (gavin) introduced `err`
+ // (VerifiedSCION) introduced `err`
  err := serrors.New("HopField index out of bounds", "max", s.NumHops-1, "actual", idx)
  //@ fold acc(s.Base.Mem(), R20)
  //@ fold acc(s.Mem(ubuf), R20)

verification/dependencies/context/context.gobra

@@ -59,27 +59,3 @@ ensures child.Mem()
 ensures child.Mem() --* parent.Mem()
 decreases _
 func WithValue(parent Context, key, val interface{ pred Mem() }) (child Context)
-
-/* Below functions are closure-dependent and currently unsupported.
-
-type CancelFunc func()
-
-requires parent.Mem()
-ensures child.Mem()
-ensures child.Mem() --* parent.Mem()
-decreases _
-func WithCancel(parent Context) (child Context, cancel CancelFunc)
-
-requires parent.Mem()
-ensures child.Mem()
-ensures child.Mem() --* parent.Mem()
-decreases _
-func WithDeadline(parent Context, d time.Time) (child Context, cancel CancelFunc)
-
-requires parent.Mem()
-ensures child.Mem()
-ensures child.Mem() --* parent.Mem()
-decreases _
-func WithTimeout(parent Context, timeout time.Duration) (child Context, cancel CancelFunc)
-
-*/

verification/dependencies/crypto/aes/cipher.gobra

@@ -19,7 +19,6 @@ const BlockSize = 16
 // The key argument should be the AES key,
 // either 16, 24, or 32 bytes to select
 // AES-128, AES-192, or AES-256.
-trusted
 preserves acc(slices.AbsSlice_Bytes(key, 0, len(key)), R50)
 ensures err == nil ==>
  len(key) == 16 || len(key) == 24 || len(key) == 32
@@ -29,16 +28,4 @@ ensures err == nil ==>
  result.BlockSize() == len(key))
 ensures err != nil ==> err.ErrorMem()
 decreases
-func NewCipher(key []byte) (result cipher.Block, err error) {
- k := len(key)
- switch k {
- default:
- return nil, KeySizeError(k)
- case 16, 24, 32:
- break
- }
- if boring.Enabled {
- return boring.NewAESCipher(key)
- }
- return newCipher(key)
-}
+func NewCipher(key []byte) (result cipher.Block, err error)

verification/dependencies/crypto/cipher/cbc.gobra

@@ -20,19 +20,10 @@ import "github.com/scionproto/scion/verification/utils/slices"
 // NewCBCEncrypter returns a BlockMode which encrypts in cipher block chaining
 // mode, using the given Block. The length of iv must be the same as the
 // Block's block size.
-trusted
 requires b != nil && b.Mem()
 requires len(iv) == b.BlockSize()
 preserves acc(slices.AbsSlice_Bytes(iv, 0, len(iv)), _)
 ensures result != nil && result.Mem()
 ensures result.BlockSize() == old(b.BlockSize())
 decreases _
-func NewCBCEncrypter(b Block, iv []byte) (result BlockMode) {
- if len(iv) != b.BlockSize() {
- panic("cipher.NewCBCEncrypter: IV length must equal block size")
- }
- if cbc, ok := b.(cbcEncAble); ok {
- return cbc.NewCBCEncrypter(iv)
- }
- return (*cbcEncrypter)(newCBC(b, iv))
-}
+func NewCBCEncrypter(b Block, iv []byte) (result BlockMode)

verification/dependencies/github.com/google/gopacket/layerclass.gobra

@@ -45,80 +45,6 @@ func (l LayerType) LayerTypes() (res []LayerType) {
  return []LayerType{l}
 }
 
-/*
-// (verifiedSCION) The following commented methods could be easily verified
-// after we introduce support for range:
-
-// LayerClassSlice implements a LayerClass with a slice.
-type LayerClassSlice []bool
-
-// Contains returns true if the given layer type should be considered part
-// of this layer class.
-func (s LayerClassSlice) Contains(t LayerType) bool {
- return int(t) < len(s) && s[t]
-}
-
-// LayerTypes returns all layer types in this LayerClassSlice.
-// Because of LayerClassSlice's implementation, this could be quite slow.
-func (s LayerClassSlice) LayerTypes() (all []LayerType) {
- for i := 0; i < len(s); i++ {
- if s[i] {
- all = append(all, LayerType(i))
- }
- }
- return
-}
-
-// NewLayerClassSlice creates a new LayerClassSlice by creating a slice of
-// size max(types) and setting slice[t] to true for each type t. Note, if
-// you implement your own LayerType and give it a high value, this WILL create
-// a very large slice.
-func NewLayerClassSlice(types []LayerType) LayerClassSlice {
- var max LayerType
- for _, typ := range types {
- if typ > max {
- max = typ
- }
- }
- t := make([]bool, int(max+1))
- for _, typ := range types {
- t[typ] = true
- }
- return t
-}
-
-// LayerClassMap implements a LayerClass with a map.
-type LayerClassMap map[LayerType]bool
-
-// Contains returns true if the given layer type should be considered part
-// of this layer class.
-func (m LayerClassMap) Contains(t LayerType) bool {
- return m[t]
-}
-
-// LayerTypes returns all layer types in this LayerClassMap.
-func (m LayerClassMap) LayerTypes() (all []LayerType) {
- for t := range m {
- all = append(all, t)
- }
- return
-}
-
-// NewLayerClassMap creates a LayerClassMap and sets map[t] to true for each
-// type in types.
-func NewLayerClassMap(types []LayerType) LayerClassMap {
- m := LayerClassMap{}
- for _, typ := range types {
- m[typ] = true
- }
- return m
-}
-*/
-
-// TODO: add explicit implementation proofs
-
-// TODO: verify after verifying the remainder of the file
-trusted
 preserves acc(types, R20)
 // NewLayerClass creates a LayerClass, attempting to be smart about which type
 // it creates based on which types are passed in.
@@ -127,13 +53,4 @@ ensures res.Mem()
 // ensures forall i LayerType :: i in types ==> res.Contains(i)
 // ensures forall i LayerType :: !i in types ==> !res.Contains(i)
 decreases
-func NewLayerClass(types []LayerType) (res LayerClass) {
- for _, typ := range types {
- if typ > maxLayerType {
- // NewLayerClassSlice could create a very large object, so instead create
- // a map.
- return NewLayerClassMap(types)
- }
- }
- return NewLayerClassSlice(types)
-}
+func NewLayerClass(types []LayerType) (res LayerClass)