Add functional spec to InfoField.SerializeTo (#300)

* absPkt opaque and other improvements * tests for local enter guard * new approach for absPkt * tests with GetIngressIDNotZero() * fix verification error * progress io-skeleton in process * progress Xover * progress io-spec skeleton in process * removed dulicate of lemma * fix verification error * removed old concurrency test * refactored absPkt * continue refactoring of absPkt * fixed postcondition in process * progress lemmas for io-spec * addressed feedback * progress in updateNonConsDirIngressSegID * fix verification errors * Prove IO lemmas in `path/scion` (#290) * try to prove lemma * backup * fix incompletness via additional lemma * fix verification error * fix verification errors and clean up * fix verification errors introduced in the latest changes to the PR * fix consistency error * add lemmas for updateNonConsDirIngressSegID() * backup * Change to EQAbsHeader (#293) * changed EQAbsHeader * readbility improvements * backup * backup * simplify Decoded.Reverse * progress in handleRouterAlerts methods * clean-up * add section header * drop comment * Fix verification errors in dependencies (#291) * backup * backup * backup * simplify Decoded.Reverse * clean-up * add section header * drop comment * backup * backup * fix verification errors in processEgress and DoXover addressing feedback clean up * backup * drop one assume * readability improvements * backup * backup * simplify proof * adapt lemmas * verify spec for SerializeTo of infofield
viperproject · Apr 4, 2024 · 5ae6bfd · 5ae6bfd
1 parent 1349d7a
commit 5ae6bfd
Show file tree

Hide file tree

Showing 5 changed files with 125 additions and 2 deletions.
diff --git a/pkg/slayers/path/infofield.go b/pkg/slayers/path/infofield.go
@@ -22,6 +22,7 @@ import (
 
  "github.com/scionproto/scion/pkg/private/serrors"
  "github.com/scionproto/scion/pkg/private/util"
+ //@ bits "github.com/scionproto/scion/verification/utils/bitwise"
  //@ . "github.com/scionproto/scion/verification/utils/definitions"
  //@ "github.com/scionproto/scion/verification/utils/slices"
  //@ "verification/io"
@@ -86,26 +87,43 @@ func (inf *InfoField) DecodeFromBytes(raw []byte) (err error) {
 // @ preserves acc(inf, R10)
 // @ preserves slices.AbsSlice_Bytes(b, 0, InfoLen)
 // @ ensures err == nil
+// @ ensures inf.ToIntermediateAbsInfoField() ==
+// @ BytesToIntermediateAbsInfoField(b, 0, 0, InfoLen)
 // @ decreases
 func (inf *InfoField) SerializeTo(b []byte) (err error) {
  if len(b) < InfoLen {
  return serrors.New("buffer for InfoField too short", "expected", InfoLen,
  "actual", len(b))
  }
+ //@ ghost targetAbsInfo := inf.ToIntermediateAbsInfoField()
  //@ unfold slices.AbsSlice_Bytes(b, 0, InfoLen)
  b[0] = 0
  if inf.ConsDir {
  b[0] |= 0x1
  }
+ //@ ghost tmpInfo1 := BytesToIntermediateAbsInfoFieldHelper(b, 0, InfoLen)
+ //@ bits.InfoFieldFirstByteSerializationLemmas()
+ //@ assert tmpInfo1.ConsDir == targetAbsInfo.ConsDir
+ //@ ghost firstByte := b[0]
  if inf.Peer {
  b[0] |= 0x2
  }
+ //@ tmpInfo2 := BytesToIntermediateAbsInfoFieldHelper(b, 0, InfoLen)
+ //@ assert tmpInfo2.Peer == (b[0] & 0x2 == 0x2)
+ //@ assert tmpInfo2.ConsDir == (b[0] & 0x1 == 0x1)
+ //@ assert tmpInfo2.Peer == targetAbsInfo.Peer
+ //@ assert tmpInfo2.ConsDir == tmpInfo1.ConsDir
+ //@ assert tmpInfo2.ConsDir == targetAbsInfo.ConsDir
  b[1] = 0 // reserved
  //@ assert &b[2:4][0] == &b[2] && &b[2:4][1] == &b[3]
  binary.BigEndian.PutUint16(b[2:4], inf.SegID)
+ //@ ghost tmpInfo3 := BytesToIntermediateAbsInfoFieldHelper(b, 0, InfoLen)
+ //@ assert tmpInfo3.UInfo == targetAbsInfo.UInfo
  //@ assert &b[4:8][0] == &b[4] && &b[4:8][1] == &b[5]
  //@ assert &b[4:8][2] == &b[6] && &b[4:8][3] == &b[7]
  binary.BigEndian.PutUint32(b[4:8], inf.Timestamp)
+ //@ ghost tmpInfo4 := BytesToIntermediateAbsInfoFieldHelper(b, 0, InfoLen)
+ //@ assert tmpInfo4.AInfo == targetAbsInfo.AInfo
  //@ fold slices.AbsSlice_Bytes(b, 0, InfoLen)
  return nil
 }

diff --git a/pkg/slayers/path/infofield_spec.gobra b/pkg/slayers/path/infofield_spec.gobra
@@ -99,7 +99,17 @@ requires acc(sl.AbsSlice_Bytes(raw, start, end), _)
 decreases
 pure func BytesToIntermediateAbsInfoField(raw [] byte, start int, middle int, end int) (IntermediateAbsInfoField) {
  return unfolding acc(sl.AbsSlice_Bytes(raw, start, end), _) in
- let _ := Asserting(forall k int :: {&raw[middle+2:middle+4][k]} 0 <= k && k < 2 ==> &raw[middle+2:middle+4][k] == &raw[middle+2 + k]) in
+ BytesToIntermediateAbsInfoFieldHelper(raw, middle, end)
+}
+
+ghost
+requires 0 <= middle
+requires middle+InfoLen <= end && end <= len(raw)
+requires forall i int :: { &raw[i] } middle <= i && i < end ==>
+ acc(&raw[i], _)
+decreases
+pure func BytesToIntermediateAbsInfoFieldHelper(raw [] byte, middle int, end int) (IntermediateAbsInfoField) {
+ return let _ := Asserting(forall k int :: {&raw[middle+2:middle+4][k]} 0 <= k && k < 2 ==> &raw[middle+2:middle+4][k] == &raw[middle+2 + k]) in
  let _ := Asserting(forall k int :: {&raw[middle+4:middle+8][k]} 0 <= k && k < 4 ==> &raw[middle+4:middle+8][k] == &raw[middle+4 + k]) in
  IntermediateAbsInfoField(IntermediateAbsInfoField_{
  AInfo : io.IO_ainfo(binary.BigEndian.Uint32(raw[middle+4:middle+8])),

diff --git a/verification/dependencies/encoding/binary/binary.gobra b/verification/dependencies/encoding/binary/binary.gobra
@@ -126,21 +126,41 @@ ensures res == "binary.LittleEndian"
 decreases
 pure func (l littleEndian) GoString() (res string) { return "binary.LittleEndian" }
 
+// The specs here could be simpler now that we have FUint16Spec and FPutUint16Spec.
+
+decreases
+pure func (e bigEndian) Uint16Spec(b0, b1 byte) (res uint16) {
+ return uint16(b1) | uint16(b0)<<8
+}
+
 trusted // related to https:/viperproject/gobra/issues/192
 requires acc(&b[0], _) && acc(&b[1], _)
 ensures res >= 0
+ensures res == BigEndian.Uint16Spec(b[0], b[1])
 decreases
 pure func (e bigEndian) Uint16(b []byte) (res uint16) {
  return uint16(b[1]) | uint16(b[0])<<8
 }
 
+decreases
+pure func (e bigEndian) PutUint16Spec(b0, b1 byte, v uint16) bool {
+ return b0 == byte(v >> 8) &&
+ b1 == byte(v)
+}
+
+// Proven in verification/utils/bitwise/proofs.dfy
+trusted
 preserves acc(&b[0]) && acc(&b[1])
+ensures BigEndian.PutUint16Spec(b[0], b[1], v)
+ensures BigEndian.Uint16Spec(b[0], b[1]) == v
 decreases
 func (e bigEndian) PutUint16(b []byte, v uint16) {
  b[0] = byte(v >> 8)
  b[1] = byte(v)
 }
 
+// The specs here could be simpler now that we have FUint32Spec and FPutUint32Spec.
+
 decreases
 pure func (e bigEndian) Uint32Spec(b0, b1, b2, b3 byte) (res uint32) {
  return uint32(b3) | uint32(b2)<<8 | uint32(b1)<<16 | uint32(b0)<<24
@@ -163,8 +183,11 @@ pure func (e bigEndian) PutUint32Spec(b0, b1, b2, b3 byte, v uint32) bool {
  b3 == byte(v)
 }
 
+// Proven in verification/utils/bitwise/proofs.dfy
+trusted
 preserves acc(&b[0]) && acc(&b[1]) && acc(&b[2]) && acc(&b[3])
 ensures BigEndian.PutUint32Spec(b[0], b[1], b[2], b[3], v)
+ensures BigEndian.Uint32Spec(b[0], b[1], b[2], b[3]) == v
 decreases
 func (e bigEndian) PutUint32(b []byte, v uint32) {
  b[0] = byte(v >> 24)

diff --git a/verification/utils/bitwise/bitwise-eqs.gobra b/verification/utils/bitwise/bitwise-eqs.gobra
@@ -52,4 +52,19 @@ ghost
 ensures res == b & 0x3F
 ensures 0 <= res && res < 64
 decreases
-pure func And3fAtMost64(b uint8) (res uint8)
+pure func And3fAtMost64(b uint8) (res uint8)
+
+ghost
+ensures 0 | 1 == 1
+ensures 0 | 2 == 2
+ensures 1 | 2 == 3
+ensures 0 & 1 == 0
+ensures 0 & 2 == 0
+ensures 1 & 1 == 1
+ensures 1 & 2 == 0
+ensures 2 & 1 == 0
+ensures 2 & 2 == 2
+ensures 3 & 1 == 1
+ensures 3 & 2 == 2
+decreases
+pure func InfoFieldFirstByteSerializationLemmas() bool
diff --git a/verification/utils/bitwise/proofs.dfy b/verification/utils/bitwise/proofs.dfy
@@ -105,4 +105,61 @@ lemma SerializeAndDeserializeLemma(m: MetaHdr, b0: bv8, b1: bv8, b2: bv8, b3: bv
 lemma SerializeAndDeserializeMetaHdrLemma(m: MetaHdr)
  requires InBounds(m)
  ensures DecodedFrom(SerializedToLine(m)) == m
+{}
+
+lemma InfoFieldFirstByteSerializationLemmas()
+ // or
+ ensures 0 as bv8 | 1 == 1
+ ensures 0 as bv8 | 2 == 2
+ ensures 1 as bv8 | 2 == 3
+ // and
+ ensures 0 as bv8 & 1 == 0
+ ensures 0 as bv8 & 2 == 0
+ ensures 1 as bv8 & 1 == 1
+ ensures 1 as bv8 & 2 == 0
+ ensures 2 as bv8 & 1 == 0
+ ensures 2 as bv8 & 2 == 2
+ ensures 3 as bv8 & 1 == 1
+ ensures 3 as bv8 & 2 == 2
+{}
+
+
+// Functional specs for encoding/binary (BigEndian)
+function FUint16Spec(b0: bv8, b1: bv8): bv16 {
+ (b1 as bv16) | ((b0 as bv16) << 8)
+}
+
+function FPutUint16Spec(v: bv16): (bv8, bv8) {
+ ((v >> 8) as bv8, (v & 0xFF) as bv8)
+}
+
+lemma FUint16AfterFPutUint16(v: bv16)
+ ensures var (b0, b1) := FPutUint16Spec(v);
+ FUint16Spec(b0, b1) == v
+{}
+
+lemma FPutUint16AfterFUint16(b0: bv8, b1: bv8)
+ ensures var v := FUint16Spec(b0, b1);
+ FPutUint16Spec(v) == (b0, b1)
+{}
+
+function FUint32Spec(b0: bv8, b1: bv8, b2: bv8, b3: bv8): bv32 {
+ (b3 as bv32) | ((b2 as bv32) << 8) | ((b1 as bv32) << 16) | ((b0 as bv32) << 24)
+}
+
+function FPutUint32Spec(v: bv32): (bv8, bv8, bv8, bv8) {
+ (((v >> 24) & 0xFF) as bv8,
+ ((v >> 16) & 0xFF) as bv8,
+ ((v >> 8) & 0xFF) as bv8,
+ (v & 0xFF) as bv8)
+}
+
+lemma FUint32AfterFPutUint32(v: bv32)
+ ensures var (b0, b1, b2, b3) := FPutUint32Spec(v);
+ FUint32Spec(b0, b1, b2, b3) == v
+{}
+
+lemma FPutUint32AfterFUint32(b0: bv8, b1: bv8, b2: bv8, b3: bv8)
+ ensures var v := FUint32Spec(b0, b1, b2, b3);
+ FPutUint32Spec(v) == (b0, b1, b2, b3)
 {}