Minor fix in the spec hash.gobra (#408)

Author: jcp19

verification/dependencies/hash/hash.gobra

@@ -47,7 +47,7 @@ type Hash interface {
 	// It does not change the underlying hash state.
 	preserves acc(Mem(), 1/1000)
 	requires acc(b)
-	ensures  acc(res) && len(res) == Size()
+	ensures  acc(res) && len(res) == len(b) + Size()
 	decreases
 	Sum(b []byte) (res []byte)
 
@@ -70,4 +70,4 @@ type Hash interface {
 	ensures  res >= 0
 	decreases
 	BlockSize() (res int)
-}
+}