From 7cca7f989ee03300cae48f16924cbb69c9af2187 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Sun, 13 Oct 2024 12:52:05 +0200 Subject: [PATCH 1/4] backup --- pkg/slayers/path/path.go | 1 + verification/utils/monoset/monoset.gobra | 240 +++++++++++++++++++++++ 2 files changed, 241 insertions(+) create mode 100644 verification/utils/monoset/monoset.gobra diff --git a/pkg/slayers/path/path.go b/pkg/slayers/path/path.go index 951af3ab6..7301ae0b4 100644 --- a/pkg/slayers/path/path.go +++ b/pkg/slayers/path/path.go @@ -26,6 +26,7 @@ import ( "github.com/scionproto/scion/pkg/private/serrors" //@ . "github.com/scionproto/scion/verification/utils/definitions" + //@ "github.com/scionproto/scion/verification/utils/monoset" //@ sl "github.com/scionproto/scion/verification/utils/slices" ) diff --git a/verification/utils/monoset/monoset.gobra b/verification/utils/monoset/monoset.gobra new file mode 100644 index 000000000..a28b9fb21 --- /dev/null +++ b/verification/utils/monoset/monoset.gobra @@ -0,0 +1,240 @@ +package monotonicset + +type BoundedMonotonicSet struct { + ghost valuesMap dict[uint16](gpointer[bool]) +} + +pred (b BoundedMonotonicSet) Inv() { + forall i uint16 :: 0 <= i && i < 256 ==> + (i in domain(b.valuesMap) && acc(b.valuesMap[i], 1/2)) +} + +ghost +requires acc(b.Inv(), _) +requires 0 <= i && i < 256 +decreases +pure func (b BoundedMonotonicSet) FContains(i uint16) bool { + // extra indirection avoids a type-checking bug of Gobra. + return unfolding acc(b.Inv(), _) in + b.fcontainshelper(i) +} + +ghost +requires forall i uint16 :: 0 <= i && i < 256 ==> + (i in domain(b.valuesMap) && acc(b.valuesMap[i], _)) +requires 0 <= i && i < 256 +decreases +pure func (b BoundedMonotonicSet) fcontainshelper(i uint16) bool { + return *b.valuesMap[i] +} + + +pred (b BoundedMonotonicSet) Contains(i uint16) { + 0 <= i && i < 256 && + i in domain(b.valuesMap) && + acc(b.valuesMap[i], _) && + *b.valuesMap[i] +} + +ghost +requires b.Contains(i) +ensures b.Contains(i) && b.Contains(i) +decreases +func (b BoundedMonotonicSet) ContainsIsDup(i uint16) { + unfold b.Contains(i) + fold b.Contains(i) + fold b.Contains(i) +} + +pred (b BoundedMonotonicSet) DoesNotContain(i uint16) { + 0 <= i && i < 256 && + i in domain(b.valuesMap) && + acc(b.valuesMap[i], 1/2) && + !(*b.valuesMap[i]) +} + +ghost +preserves acc(b.Inv(), 1/4) +preserves acc(b.DoesNotContain(i), 1/4) +ensures 0 <= i && i < 256 +ensures !b.FContains(i) +decreases +func (b BoundedMonotonicSet) DoesNotContainImpliesNotFContains(i uint16) { + assert unfolding acc(b.Inv(), _) in + unfolding acc(b.DoesNotContain(i), _) in + !b.fcontainshelper(i) +} + +ghost +preserves acc(b.Inv(), 1/4) +preserves b.Contains(i) +ensures 0 <= i && i < 256 +ensures b.FContains(i) +decreases +func (b BoundedMonotonicSet) ContainsImpliesFContains(i uint16) { + assert unfolding acc(b.Inv(), _) in + unfolding acc(b.Contains(i), _) in + b.fcontainshelper(i) +} + +ghost +ensures res.Inv() +ensures forall i uint16 :: 0 <= i && i < 256 ==> + res.DoesNotContain(i) +// The following is technically redundant, but very useful. +ensures forall i uint16 :: 0 <= i && i < 256 ==> + !res.FContains(i) +decreases +func Alloc() (res BoundedMonotonicSet) { + b := BoundedMonotonicSet{} + var i uint16 + invariant 0 <= i && i <= 256 + invariant forall j uint16 :: 0 <= j && j < i ==> + j in domain(b.valuesMap) + // injectivity requirement + invariant forall j1, j2 uint16 :: 0 <= j1 && j1 < j2 && j2 < i ==> + b.valuesMap[j1] != b.valuesMap[j2] + invariant forall j uint16 :: 0 <= j && j < i ==> + acc(b.valuesMap[j]) + invariant forall j uint16 :: 0 <= j && j < i ==> + !(*b.valuesMap[j]) + decreases 256 - i + for i = 0; i < 256; i +=1 { + b.valuesMap[i] = new(bool) + } + + invariant 0 <= i && i <= 256 + invariant forall j uint16 :: 0 <= j && j < i ==> + j in domain(b.valuesMap) + // injectivity requirement + invariant forall j1, j2 uint16 :: 0 <= j1 && j1 < j2 && j2 < i ==> + b.valuesMap[j1] != b.valuesMap[j2] + invariant forall j uint16 :: i <= j && j < 256 ==> + acc(b.valuesMap[j]) && !(*b.valuesMap[j]) + invariant forall j uint16 :: 0 <= j && j < i ==> + acc(b.valuesMap[j], 1/2) + invariant forall j uint16 :: 0 <= j && j < i ==> + b.DoesNotContain(j) + invariant forall j uint16 :: 0 <= j && j < i ==> + !b.fcontainshelper(j) + decreases 256 - i + for i = 0; i < 256; i +=1 { + fold b.DoesNotContain(i) + } + fold b.Inv() + return b +} + +ghost +opaque // make this closed when that is supported +requires acc(b.Inv(), _) +decreases +pure func (b BoundedMonotonicSet) ToSet() set[uint16] { + return b.toSetAux(0) +} + +ghost +requires acc(b.Inv(), _) +requires 0 <= start && start < 256 +decreases 256 - start +pure func (b BoundedMonotonicSet) toSetAux(start uint16) set[uint16] { + return unfolding acc(b.Inv(), _) in ((*b.valuesMap[start] ? set[uint16]{start} : set[uint16]{}) union (start < 255 ? b.toSetAux(start+1) : set[uint16]{})) +} + +ghost +requires 0 < p +requires acc(b.Inv(), p) +requires b.Contains(v) +ensures acc(b.Inv(), p) +ensures v in b.ToSet() +decreases +func (b BoundedMonotonicSet) ContainsImpliesAbstractContains(v uint16, p perm) { + found := false + i := uint16(0) + part1 := set[uint16]{} + part2 := reveal b.ToSet() + + assert unfolding b.Contains(v) in 0 <= v && v < 256 + + invariant acc(b.Inv(), p/2) + invariant b.Contains(v) + invariant 0 <= i && i <= 256 + invariant v < i ==> found + invariant found ==> v in b.ToSet() + invariant part1 union part2 == b.ToSet() + invariant i < 256 ==> + part2 == unfolding acc(b.Inv(), _) in ((*b.valuesMap[i] ? set[uint16]{i} : set[uint16]{}) union (i < 255 ? b.toSetAux(i+1) : set[uint16]{})) + decreases 256 - i + for i = 0; i < 256; i += 1 { + newpart1 := part1 union unfolding acc(b.Inv(), _) in (*b.valuesMap[i] ? set[uint16]{i} : set[uint16]{}) + newpart2 := i < 255 ? b.toSetAux(i+1) : set[uint16]{} + if i == v { + unfold b.Contains(v) + found = true + assert *b.valuesMap[i] + assert newpart1 union newpart2 == b.ToSet() + assert v in (unfolding acc(b.Inv(), _) in (*b.valuesMap[i] ? set[uint16]{i} : set[uint16]{})) + assert v in newpart1 + fold b.Contains(v) + } + part1 = newpart1 + part2 = newpart2 + } +} + +ghost +requires 0 < p +preserves acc(b.Inv(), p) +preserves b.DoesNotContain(v) +ensures !(v in b.ToSet()) +decreases +func (b BoundedMonotonicSet) DoesNotContainsImpliesAbstractDoesNotContain(v uint16, p perm) { + found := false + i := uint16(0) + part1 := set[uint16]{} + part2 := reveal b.ToSet() + + assert unfolding b.DoesNotContain(v) in 0 <= v && v < 256 + + invariant acc(b.Inv(), p/2) + invariant b.DoesNotContain(v) + invariant 0 <= i && i <= 256 + invariant !found + invariant found == v in part1 + invariant part1 union part2 == b.ToSet() + invariant i < 256 ==> + part2 == unfolding acc(b.Inv(), _) in ((*b.valuesMap[i] ? set[uint16]{i} : set[uint16]{}) union (i < 255 ? b.toSetAux(i+1) : set[uint16]{})) + invariant i == 256 ==> + part2 == set[uint16]{} + decreases 256 - i + for i = 0; i < 256; i += 1 { + newpart1 := part1 union unfolding acc(b.Inv(), _) in (*b.valuesMap[i] ? set[uint16]{i} : set[uint16]{}) + newpart2 := i < 255 ? b.toSetAux(i+1) : set[uint16]{} + if i == v { + unfold b.DoesNotContain(v) + assert !(*b.valuesMap[i]) + assert newpart1 union newpart2 == b.ToSet() + assert !(v in (unfolding acc(b.Inv(), _) in (*b.valuesMap[i] ? set[uint16]{i} : set[uint16]{}))) + assert !(v in newpart1) + fold b.DoesNotContain(v) + } + part1 = newpart1 + part2 = newpart2 + } +} + +ghost +requires b.DoesNotContain(v) +preserves b.Inv() +ensures b.Contains(v) +ensures forall i uint16 :: 0 <= i && i < 256 && i != v ==> + b.FContains(i) == old(b.FContains(i)) +decreases +func (b BoundedMonotonicSet) Add(v uint16) { + unfold b.Inv() + unfold b.DoesNotContain(v) + ghost var ptr gpointer[bool] = b.valuesMap[v] + *ptr = true + fold b.Inv() + fold b.Contains(v) +} \ No newline at end of file From c7190e3586637d0358335872cac463c83bea0cf1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Sun, 13 Oct 2024 12:58:41 +0200 Subject: [PATCH 2/4] fix package clause --- verification/utils/monoset/monoset.gobra | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/verification/utils/monoset/monoset.gobra b/verification/utils/monoset/monoset.gobra index a28b9fb21..fadced530 100644 --- a/verification/utils/monoset/monoset.gobra +++ b/verification/utils/monoset/monoset.gobra @@ -1,4 +1,4 @@ -package monotonicset +package monoset type BoundedMonotonicSet struct { ghost valuesMap dict[uint16](gpointer[bool]) From ffebf55fe0137f7b3df3d12b9c62dbd8cd52418d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Sun, 13 Oct 2024 13:04:04 +0200 Subject: [PATCH 3/4] add //+gobra --- verification/utils/monoset/monoset.gobra | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/verification/utils/monoset/monoset.gobra b/verification/utils/monoset/monoset.gobra index fadced530..7b4e79638 100644 --- a/verification/utils/monoset/monoset.gobra +++ b/verification/utils/monoset/monoset.gobra @@ -1,3 +1,19 @@ +// Copyright 2024 ETH Zurich +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +// +gobra + package monoset type BoundedMonotonicSet struct { From c935b452a9a29e34400618c7fba010f37fdf12a5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Sun, 13 Oct 2024 13:32:08 +0200 Subject: [PATCH 4/4] backup --- pkg/slayers/path/path.go | 16 +++++++++++++--- pkg/slayers/path/path_spec.gobra | 21 ++++++++++++++++++++- verification/utils/monoset/monoset.gobra | 2 ++ 3 files changed, 35 insertions(+), 4 deletions(-) diff --git a/pkg/slayers/path/path.go b/pkg/slayers/path/path.go index 7301ae0b4..c10700d4f 100644 --- a/pkg/slayers/path/path.go +++ b/pkg/slayers/path/path.go @@ -15,12 +15,20 @@ // +gobra // @ initEnsures PathPackageMem() -// Skipped the following post-condition due to performance reasons -// initEnsures forall t Type :: 0 <= t && t < maxPathType ==> !Registered(t) -// Instead, we have: + // @ initEnsures !Registered(0) && !Registered(1) && !Registered(2) && !Registered(3) package path +// @ friendPkg "github.com/scionproto/scion/pkg/slayers" PkgInv() +// We have a simpler version than the following friend-package clause due to performance reasons: +// friendPkg "github.com/scionproto/scion/pkg/slayers" forall t Type :: { RegisteredTypes().DoesNotContain(t) } 0 <= t && t < 256 ==> +// RegisteredTypes().DoesNotContain(t) +// Instead, we have: +// @ friendPkg "github.com/scionproto/scion/pkg/slayers" RegisteredTypes().DoesNotContain(0) && +// @ RegisteredTypes().DoesNotContain(1) +// @ RegisteredTypes().DoesNotContain(2) +// @ RegisteredTypes().DoesNotContain(3) + import ( "fmt" @@ -38,6 +46,8 @@ var ( strictDecoding/*@@@*/ bool = true ) +// @ ghost var registeredKeys = monoset.Alloc() + func init() { // (VerifiedSCION) ghost initialization code to establish the PathPackageMem predicate. // @ assert acc(®isteredPaths) diff --git a/pkg/slayers/path/path_spec.gobra b/pkg/slayers/path/path_spec.gobra index 0963b1cd0..870a307b6 100644 --- a/pkg/slayers/path/path_spec.gobra +++ b/pkg/slayers/path/path_spec.gobra @@ -16,7 +16,10 @@ package path -import "github.com/scionproto/scion/verification/utils/slices" +import ( + "github.com/scionproto/scion/verification/utils/monoset" + "github.com/scionproto/scion/verification/utils/slices" +) /** rawPath spec **/ pred (r *rawPath) Mem(underlyingBuf []byte) { @@ -60,6 +63,21 @@ func (p *rawPath) LenSpec(ghost ub []byte) (l int) { /** Global state of the package **/ ghost const MaxPathType = maxPathType +pred PkgInv() { + acc(®isteredPaths) && + registeredKeys.Inv() && + (forall i uint16 :: 0 <= i && i < maxPathType ==> + registeredPaths[i].inUse == registeredKeys.FContains(i)) +} + +ghost +decreases +pure func RegisteredTypes() monotonicset.BoundedMonotonicSet { + return registeredKeys +} + + +// TODO: Drop what I can pred PathPackageMem() { acc(®isteredPaths) && acc(&strictDecoding) && @@ -91,6 +109,7 @@ pure func IsStrictDecoding() (b bool) { return unfolding acc(PathPackageMem(), _) in strictDecoding } +// Tge following is a closure spec, not an assumed impl. // without passing `writePerm` explicitely below, we run into // exceptions when verifying method RegisterPath in package 'empty' ensures acc(p.NonInitMem(), writePerm) diff --git a/verification/utils/monoset/monoset.gobra b/verification/utils/monoset/monoset.gobra index 7b4e79638..328f4d537 100644 --- a/verification/utils/monoset/monoset.gobra +++ b/verification/utils/monoset/monoset.gobra @@ -16,6 +16,8 @@ package monoset +// BoundedMonotonicSet represents sets of uint8 to which we may add new elements, but +// never remove old ones. type BoundedMonotonicSet struct { ghost valuesMap dict[uint16](gpointer[bool]) }