fixes a weird incompleteness in Gobra where a 1/16 seems smaller than wildcard permission amount

Author: ArquintL

dh/implementation/initiator/initiator.go

@@ -370,13 +370,11 @@ func (i *Initiator) ProduceHsMsg3() (signedMsg3 []byte, success bool) {
 	}
 
 	//@ requires acc(i, 1/2) && acc(i.l.Mem(), 1/2)
-	//@ requires acc(Mem(signedMsg3), 1/2) && Abs(signedMsg3) == by.signB(ay.tuple5B(ay.integer32B(Msg3Tag), ay.integer32B(i.idA), ay.integer32B(i.idB), by.gamma(i.YT), by.expB(ay.generatorB(), by.gamma(i.xT))), by.gamma(i.skAT))
+	//@ requires Mem(signedMsg3) && signedMsg3 != nil && Abs(signedMsg3) == by.signB(ay.tuple5B(ay.integer32B(Msg3Tag), ay.integer32B(i.idA), ay.integer32B(i.idB), by.gamma(i.YT), by.expB(ay.generatorB(), by.gamma(i.xT))), by.gamma(i.skAT))
 	//@ requires pl.token(t0) && io.P_Alice(t0, ridT, s0)
 	//@ requires HasHsMsg3OutFact(ridT, i.idA, i.idB, i.YT, i.xT, i.skAT, s0)
 	//@ requires ProcessedHsMsg2Pred(ridT, i.idA, i.idB, i.skAT, i.skBT, i.xT, i.YT, s0)
 	//@ ensures  acc(i, 1/2) && acc(i.l.Mem(), 1/2)
-	// due to the workaround for sanitization, we obtain a different slice to which `signedMsg3` points:
-	// ensures  acc(Mem(signedMsg3), 1/2) && signedMsg3 != nil
 	//@ ensures  Mem(signedMsg3) && signedMsg3 != nil && Abs(signedMsg3) == before(Abs(signedMsg3))
 	//@ ensures  pl.token(t1) && io.P_Alice(t1, ridT, s1)
 	//@ ensures  ProcessedHsMsg2Pred(ridT, i.idA, i.idB, i.skAT, i.skBT, i.xT, i.YT, s1)
@@ -408,8 +406,7 @@ func (i *Initiator) ProduceHsMsg3() (signedMsg3 []byte, success bool) {
 	sharedSecret, err /*@, sharedSecretB @*/ = i.l.DhSharedSecret(i.x, i.Y)
 	if err == nil { //argot:ignore diodon-dh-io-independence
 		i.irKey, i.riKey = NewBytes(32), NewBytes(32)
-		//@ ghost var t0Abs, t1Abs by.Bytes
-		err /*@, t0Abs, t1Abs @*/ = KDF2Slice(i.irKey, i.riKey, sharedSecret /*@, sharedSecretB @*/)
+		err = KDF2Slice(i.irKey, i.riKey, sharedSecret)
 		if err == nil {
 			i.l.PrintKeys(i.irKey, i.riKey)
 			//@ fold HandshakeCompletedPred(i.irKey, i.riKey, i.xT, i.YT)

dh/implementation/library/crypto.go

@@ -221,12 +221,10 @@ func Equals(s1, s2 []byte) (res bool) {
 // which is a bug.
 // @ trusted
 // @ decreases
-// @ requires  Mem(t0) && Mem(t1)
-// @ requires  acc(Mem(key), 1/16) && keyAbs == Abs(key)
-// @ ensures   Mem(t0) && t0Abs == Abs(t0) && Mem(t1) && t1Abs == Abs(t1)
-// @ ensures   err == nil ==> kdf1B(keyAbs) == t0Abs
-// @ ensures   err == nil ==> kdf2B(keyAbs) == t1Abs
-func KDF2Slice(t0, t1 []byte, key []byte /*@, ghost keyAbs Bytes @*/) (err error /*@, ghost t0Abs Bytes, ghost t1Abs Bytes @*/) {
+// @ preserves Mem(t0) && Mem(t1) && acc(Mem(key), 1/16)
+// @ ensures   err == nil ==> kdf1B(Abs(key)) == Abs(t0)
+// @ ensures   err == nil ==> kdf2B(Abs(key)) == Abs(t1)
+func KDF2Slice(t0, t1 []byte, key []byte) (err error) {
 	if len(t0) != 32 || len(t1) != 32 {
 		err = errors.New("invalid argument length")
 		return
@@ -240,7 +238,7 @@ func KDF2Slice(t0, t1 []byte, key []byte /*@, ghost keyAbs Bytes @*/) (err error
 }
 
 // @ trusted
-// @ preserves Mem(sum) && Mem(key) && Mem(in0)
+// @ preserves Mem(sum) && acc(Mem(key), 1/32) && acc(Mem(in0), 1/32)
 func HMAC1Slice(sum []byte, key, in0 []byte) {
 	mac := hmac.New(func() hash.Hash {
 		h, _ := blake2s.New256(nil)

dh/implementation/library/io.go

@@ -10,12 +10,14 @@ import fmt "fmt"
 // calling this function results in a proof obligations that the necessary I/O permission
 // for performing an output operation are present. Thus, we can treat this function as
 // sanitizing `data`
+// technically, fractional permissions for `data` is sufficient. However, we express the specification
+// in a way that it does not matter for callers whether this function copies the slice of bytes or returns
+// the same one.
 // @ trusted
-// @ requires acc(Mem(data), 1/16)
+// @ requires Mem(data) && data != nil
 // @ requires token(t) && e_OutFact(t, rid, m) && gamma(m) == Abs(data)
-// @ ensures  acc(Mem(data), 1/16)
 // @ ensures  token(t1) && t1 == old(get_e_OutFact_placeDst(t, rid, m))
-// @ ensures  Mem(res) && Abs(data) == Abs(res) && res != nil // added due to the workaround for the data flow analysis' imprecision
+// @ ensures  Mem(res) && Abs(res) == old(Abs(data)) && res != nil
 func PerformVirtualOutputOperation(data []byte /*@, ghost t Place, ghost rid tm.Term, ghost m tm.Term @*/) (res []byte /*@, ghost t1 Place @*/) {
 	// due to an imprecision in the data flow analysis, we have to copy the slice instead of directly returning `data`
 	// otherwise, the data flow analysis considers the result tainted despite configuring this function as a sanitizer

dh/implementation/library/state.go

@@ -17,7 +17,7 @@ pred Mem(data []byte)
 
 ghost
 decreases
-requires acc(Mem(b), _)
+requires acc(Mem(b), 1/32)
 pure func Abs(b []byte) (res by.Bytes)
 @*/