From 654a8292a0cb3680c3ddec8259d8aa8f6b4c3fd1 Mon Sep 17 00:00:00 2001 From: adjenny Date: Mon, 12 Dec 2022 17:02:22 +0100 Subject: [PATCH 01/20] start attempt at ring --- src/container/ring/ring.go | 2 + src/container/ring/ring.gobra | 251 ++++++++++++++++++++++++++++++++++ 2 files changed, 253 insertions(+) create mode 100644 src/container/ring/ring.gobra diff --git a/src/container/ring/ring.go b/src/container/ring/ring.go index 268670bc852..88c0f011121 100644 --- a/src/container/ring/ring.go +++ b/src/container/ring/ring.go @@ -3,6 +3,8 @@ // license that can be found in the LICENSE file. // Package ring implements operations on circular lists. + +// +gobra package ring // A Ring is an element of a circular list, or ring. diff --git a/src/container/ring/ring.gobra b/src/container/ring/ring.gobra new file mode 100644 index 00000000000..9b8e2095399 --- /dev/null +++ b/src/container/ring/ring.gobra @@ -0,0 +1,251 @@ +// Copyright 2009 The Go Authors. All rights reserved. +// Use of this source code is governed by a BSD-style +// license that can be found in the LICENSE file. + +// Package ring implements operations on circular lists. + +// +gobra +package ring + +// A Ring is an element of a circular list, or ring. +// Rings do not have a beginning or end; a pointer to any ring element +// serves as reference to the entire ring. Empty rings are represented +// as nil Ring pointers. The zero value for a Ring is a one-element +// ring with a nil Value. +type Ring struct { + next, prev *Ring + Value any // for use by client; untouched by this library +} + + +pred (r *Ring) Mem(ghost s set[*Ring], ghost isInit bool) { + r in s && + (forall i *Ring :: i in s ==> (acc(&i.next) && acc(&i.prev) && acc(&i.Value))) && + ((r.next == nil || r.prev == nil) ==> !isInit) && //# More correctly, it is !isInit if it cannot reach itself in both directions via the same Ring elements + (!isInit ==> ((s == set[*Ring]{r}) && (r.next == nil && r.prev == nil))) && + (isInit ==> ( + (len(s)==1 ==> (r.next==r && r.prev==r)) && + (forall i *Ring :: i in s ==> (i.next != nil && i.prev != nil)) && + (forall i, j *Ring :: ((i in s && i.next == j) ==> (j in s && j.prev == i && i.next.prev == i && j.prev.next == j))) && + (forall i, j *Ring :: ((i in s && i.prev == j) ==> (j in s && j.next == i && i.prev.next == i && j.next.prev == j))))) +} +//# enforce structure by: +//# forall elements, forall i in [0,len]: moveLeft(i) == moveRight(len-i) +//# problematic for Ring because we get Len() by the same logic + +requires r.Mem(elems, isInit) +ensures r.Mem(set[*Ring]{r}, true) +ensures r == res +decreases +func (r *Ring) init(ghost elems set[*Ring], ghost isInit bool) (res *Ring) { + unfold r.Mem(elems, isInit) + r.next = r + r.prev = r + fold r.Mem(set[*Ring]{r}, true) + return r +} + + +// Next returns the next ring element. r must not be empty. +requires r != nil +requires r in elems +requires owner.Mem(elems, isInit) +ensures !isInit ==> (owner.Mem(set[*Ring]{r}, true) && res == r) //# The comment does not explain that r is returned if the ring is not initialized but that's what the implementation does. +ensures isInit ==> owner.Mem(elems, true) +ensures isInit ==> (unfolding owner.Mem(elems, true) in (res == r.next)) +decreases +func (r *Ring) Next(ghost owner *Ring, ghost elems set[*Ring], ghost isInit bool) (res *Ring) { + unfold owner.Mem(elems, isInit) + if r.next == nil { + //# here we know !isInit + fold owner.Mem(elems, false) + return r.init(elems, false) + } + res = r.next + fold owner.Mem(elems, true) +} + + +// Prev returns the previous ring element. r must not be empty. +requires r != nil +requires r in elems +requires owner.Mem(elems, isInit) +ensures !isInit ==> (owner.Mem(set[*Ring]{r}, true) && res == r) //# The comment does not explain that r is returned if the ring is not initialized but that's what the implementation does. +ensures isInit ==> owner.Mem(elems, true) +ensures isInit ==> (unfolding owner.Mem(elems, true) in (res == r.prev)) +decreases +func (r *Ring) Prev(ghost owner *Ring, ghost elems set[*Ring], ghost isInit bool) (res *Ring) { + unfold owner.Mem(elems, isInit) + if r.next == nil { + //# here we know !isInit + fold owner.Mem(elems, false) + return r.init(elems, false) + } + res = r.prev + fold owner.Mem(elems, true) +} + + +ghost +requires owner.Mem(elems,true) +requires r in elems +requires n >= 0 +ensures (n==0) ==> res==r +ensures (n>0) ==> res==(unfolding owner.Mem(elems,true) in r.next.moveNext(n-1, owner, elems)) +pure func (r *Ring) moveNext(n int, ghost owner *Ring, ghost elems set[*Ring]) (res * Ring){ + return unfolding owner.Mem(elems,true) in ((n==0) ? r : r.next.moveNext(n-1, owner, elems)) +} + +/* +//# TEST NEXT +requires r.Mem(elems,true) +requires r in elems +ensures r.Mem(elems, true) +ensures (res == r.moveNext(3, r, elems)) +func (r *Ring) moveNextTest(ghost elems set[*Ring]) (res *Ring){ + unfold r.Mem(elems, true) + res = r.next.next.next + fold r.Mem(elems, true) +} +*/ + +ghost +requires owner.Mem(elems,true) +requires r in elems +requires n <= 0 +ensures (n==0) ==> res==r +ensures (n<0) ==> res==(unfolding owner.Mem(elems,true) in r.prev.movePrev(n+1, owner, elems)) +pure func (r *Ring) movePrev(n int, ghost owner *Ring, ghost elems set[*Ring]) (res * Ring){ + return unfolding owner.Mem(elems,true) in ((n==0) ? r : r.prev.movePrev(n+1, owner, elems)) +} + +/* +//# TEST PREV +requires r.Mem(elems,true) +requires r in elems +ensures r.Mem(elems, true) +ensures (res == r.movePrev(-3, r, elems)) +func (r *Ring) movePrevTest(ghost elems set[*Ring]) (res *Ring){ + unfold r.Mem(elems, true) + res = r.prev.prev.prev + fold r.Mem(elems, true) +} +*/ + + +// Move moves n % r.Len() elements backward (n < 0) or forward (n >= 0) +// in the ring and returns that ring element. r must not be empty. +requires owner.Mem(elems, isInit) //# make this PRESERVES +requires r != nil +requires r in elems +ensures !isInit ==> (r.Mem(set[*Ring]{r}, true) && res == r) //# The comment does not explain that r is returned if the ring is not initialized but that's what the implementation does. +ensures (isInit && n == 0) ==> (res == r) +//# how to reason that res is n steps away? +ensures (isInit && n>0) ==> (res == old(r.moveNext(n, owner, elems))) +ensures (isInit && n<0) ==> (res == old(r.movePrev(n, owner, elems))) +//# Why does the implementation not make the modulo calculation and save on potentially unnecessary iterations? --> We'd need to run Len() (Len() many iterations) but for n > 2*Len() it'd still always make sense to compute the modulus +func (r *Ring) Move(n int, ghost owner *Ring, ghost elems set[*Ring], ghost isInit bool) (res *Ring) { + if unfolding owner.Mem(elems, isInit) in r.next == nil { + return r.init(elems, isInit) + } + + startRing := r //# included for invariant + startN := n //# included for invariant + switch { + case n < 0: + invariant n <= 0 + invariant startRing.movePrev((startN - n), owner, elems) == r //# should we take old(r)? + for ; n < 0; n++ { + r = r.prev + } + case n > 0: + invariant n >= 0 + invariant startRing.moveNext((startN - n), owner, elems) == r + for ; n > 0; n-- { + r = r.next + } + } + return r +} + + +/* +// New creates a ring of n elements. +func New(n int) *Ring { + if n <= 0 { + return nil + } + r := new(Ring) + p := r + for i := 1; i < n; i++ { + p.next = &Ring{prev: p} + p = p.next + } + p.next = r + r.prev = p + return r +} + +// Link connects ring r with ring s such that r.Next() +// becomes s and returns the original value for r.Next(). +// r must not be empty. +// +// If r and s point to the same ring, linking +// them removes the elements between r and s from the ring. +// The removed elements form a subring and the result is a +// reference to that subring (if no elements were removed, +// the result is still the original value for r.Next(), +// and not nil). +// +// If r and s point to different rings, linking +// them creates a single ring with the elements of s inserted +// after r. The result points to the element following the +// last element of s after insertion. +func (r *Ring) Link(s *Ring) *Ring { + n := r.Next() + if s != nil { + p := s.Prev() + // Note: Cannot use multiple assignment because + // evaluation order of LHS is not specified. + r.next = s + s.prev = r + n.prev = p + p.next = n + } + return n +} + +// Unlink removes n % r.Len() elements from the ring r, starting +// at r.Next(). If n % r.Len() == 0, r remains unchanged. +// The result is the removed subring. r must not be empty. +func (r *Ring) Unlink(n int) *Ring { + if n <= 0 { + return nil + } + return r.Link(r.Move(n + 1)) +} + +// Len computes the number of elements in ring r. +// It executes in time proportional to the number of elements. +func (r *Ring) Len() int { + n := 0 + if r != nil { + n = 1 + for p := r.Next(); p != r; p = p.next { + n++ + } + } + return n +} + +// Do calls function f on each element of the ring, in forward order. +// The behavior of Do is undefined if f changes *r. +func (r *Ring) Do(f func(any)) { + if r != nil { + f(r.Value) + for p := r.Next(); p != r; p = p.next { + f(p.Value) + } + } +} +*/ From a11ba47582ae7fb22540b94314eb6e0abdd423e5 Mon Sep 17 00:00:00 2001 From: adjenny Date: Tue, 20 Dec 2022 23:32:00 +0100 Subject: [PATCH 02/20] prove memory safety for Move(n), changed implementation of New() --- src/container/ring/ring.gobra | 120 +++++++++++++++++++++++----------- 1 file changed, 81 insertions(+), 39 deletions(-) diff --git a/src/container/ring/ring.gobra b/src/container/ring/ring.gobra index 9b8e2095399..66be15d5864 100644 --- a/src/container/ring/ring.gobra +++ b/src/container/ring/ring.gobra @@ -20,7 +20,7 @@ type Ring struct { pred (r *Ring) Mem(ghost s set[*Ring], ghost isInit bool) { r in s && - (forall i *Ring :: i in s ==> (acc(&i.next) && acc(&i.prev) && acc(&i.Value))) && + (forall i *Ring :: i in s ==> (acc(&i.next) && acc(&i.prev) && acc(&i.Value))) && ((r.next == nil || r.prev == nil) ==> !isInit) && //# More correctly, it is !isInit if it cannot reach itself in both directions via the same Ring elements (!isInit ==> ((s == set[*Ring]{r}) && (r.next == nil && r.prev == nil))) && (isInit ==> ( @@ -49,40 +49,40 @@ func (r *Ring) init(ghost elems set[*Ring], ghost isInit bool) (res *Ring) { // Next returns the next ring element. r must not be empty. requires r != nil requires r in elems -requires owner.Mem(elems, isInit) -ensures !isInit ==> (owner.Mem(set[*Ring]{r}, true) && res == r) //# The comment does not explain that r is returned if the ring is not initialized but that's what the implementation does. -ensures isInit ==> owner.Mem(elems, true) -ensures isInit ==> (unfolding owner.Mem(elems, true) in (res == r.next)) +requires r.Mem(elems, isInit) +ensures !isInit ==> (r.Mem(set[*Ring]{r}, true) && res == r) //# The comment does not explain that r is returned if the ring is not initialized but that's what the implementation does. +ensures isInit ==> r.Mem(elems, true) +ensures isInit ==> (unfolding r.Mem(elems, true) in (res == r.next)) decreases -func (r *Ring) Next(ghost owner *Ring, ghost elems set[*Ring], ghost isInit bool) (res *Ring) { - unfold owner.Mem(elems, isInit) +func (r *Ring) Next(ghost elems set[*Ring], ghost isInit bool) (res *Ring) { + unfold r.Mem(elems, isInit) if r.next == nil { //# here we know !isInit - fold owner.Mem(elems, false) + fold r.Mem(elems, false) return r.init(elems, false) } res = r.next - fold owner.Mem(elems, true) + fold r.Mem(elems, true) } // Prev returns the previous ring element. r must not be empty. requires r != nil requires r in elems -requires owner.Mem(elems, isInit) -ensures !isInit ==> (owner.Mem(set[*Ring]{r}, true) && res == r) //# The comment does not explain that r is returned if the ring is not initialized but that's what the implementation does. -ensures isInit ==> owner.Mem(elems, true) -ensures isInit ==> (unfolding owner.Mem(elems, true) in (res == r.prev)) +requires r.Mem(elems, isInit) +ensures !isInit ==> (r.Mem(set[*Ring]{r}, true) && res == r) //# The comment does not explain that r is returned if the ring is not initialized but that's what the implementation does. +ensures isInit ==> r.Mem(elems, true) +ensures isInit ==> (unfolding r.Mem(elems, true) in (res == r.prev)) decreases -func (r *Ring) Prev(ghost owner *Ring, ghost elems set[*Ring], ghost isInit bool) (res *Ring) { - unfold owner.Mem(elems, isInit) +func (r *Ring) Prev(ghost elems set[*Ring], ghost isInit bool) (res *Ring) { + unfold r.Mem(elems, isInit) if r.next == nil { //# here we know !isInit - fold owner.Mem(elems, false) + fold r.Mem(elems, false) return r.init(elems, false) } res = r.prev - fold owner.Mem(elems, true) + fold r.Mem(elems, true) } @@ -133,59 +133,100 @@ func (r *Ring) movePrevTest(ghost elems set[*Ring]) (res *Ring){ */ + // Move moves n % r.Len() elements backward (n < 0) or forward (n >= 0) // in the ring and returns that ring element. r must not be empty. -requires owner.Mem(elems, isInit) //# make this PRESERVES +requires r.Mem(elems, isInit) //# make this PRESERVES requires r != nil requires r in elems -ensures !isInit ==> (r.Mem(set[*Ring]{r}, true) && res == r) //# The comment does not explain that r is returned if the ring is not initialized but that's what the implementation does. -ensures (isInit && n == 0) ==> (res == r) -//# how to reason that res is n steps away? -ensures (isInit && n>0) ==> (res == old(r.moveNext(n, owner, elems))) -ensures (isInit && n<0) ==> (res == old(r.movePrev(n, owner, elems))) +ensures !isInit ==> (r.Mem(set[*Ring]{r}, true) && res == old(r)) //# The comment does not explain that r is returned if the ring is not initialized but that's what the implementation does. +ensures (n == 0) ==> (res == r) +ensures isInit ==> r.Mem(elems, true) +//ensures (isInit && n>0) ==> (res == r.moveNext(n, r, elems)) +//ensures (isInit && n<0) ==> (res == r.movePrev(n, r, elems)) //# Why does the implementation not make the modulo calculation and save on potentially unnecessary iterations? --> We'd need to run Len() (Len() many iterations) but for n > 2*Len() it'd still always make sense to compute the modulus -func (r *Ring) Move(n int, ghost owner *Ring, ghost elems set[*Ring], ghost isInit bool) (res *Ring) { - if unfolding owner.Mem(elems, isInit) in r.next == nil { +func (r *Ring) Move(n int, ghost elems set[*Ring], ghost isInit bool) (res *Ring) { + if unfolding r.Mem(elems, isInit) in r.next == nil { return r.init(elems, isInit) + assert r.Mem(set[*Ring]{r}, true) } - + startRing := r //# included for invariant startN := n //# included for invariant switch { case n < 0: - invariant n <= 0 - invariant startRing.movePrev((startN - n), owner, elems) == r //# should we take old(r)? + invariant startRing.Mem(elems, true) + invariant r in elems + invariant startN <= n && n <= 0 + //invariant startRing.movePrev((startN - n), startRing, elems) == r + decreases 0 - n for ; n < 0; n++ { + unfold startRing.Mem(elems, true) r = r.prev + fold startRing.Mem(elems, true) } case n > 0: - invariant n >= 0 - invariant startRing.moveNext((startN - n), owner, elems) == r + invariant startRing.Mem(elems, true) + invariant r in elems + invariant startN >= n && n >= 0 + //invariant startRing.moveNext((startN - n), owner, elems) == r + decreases n for ; n > 0; n-- { + unfold startRing.Mem(elems, true) r = r.next + fold startRing.Mem(elems, true) } } return r } -/* + // New creates a ring of n elements. -func New(n int) *Ring { +ensures n <= 0 ==> res == nil +ensures n > 0 ==> (len(elems) == n && res.Mem(elems, true)) +func New(n int) (res *Ring, ghost elems set[*Ring]) { if n <= 0 { - return nil + res = nil + elems = set[*Ring]{} + return } r := new(Ring) p := r + + //# Changed the implementation to already form a cycle here so that we can use + //# the memory predicate in the invariant and have an easier time establishing it in the end. + r.next = r + r.prev = r + elems = set[*Ring]{r} + fold r.Mem(elems, true) + + invariant r.Mem(elems, true) + invariant len(elems) == i + invariant p in elems + invariant 1 <= i && i <= n + decreases n - i for i := 1; i < n; i++ { - p.next = &Ring{prev: p} - p = p.next + //# Implementation was changed. Every iteration we take a consistent ring and return a consistent ring with a new element. + unfold r.Mem(elems, true) + q := &Ring{} + q.prev = p + q.next = p.next + q.prev.next = q + q.next.prev = q + p = q + elems = elems union set[*Ring]{p} + fold r.Mem(elems, true) } - p.next = r - r.prev = p - return r + + //p.next = r //# removed + //r.prev = p //# removed + + res = r } +/* + // Link connects ring r with ring s such that r.Next() // becomes s and returns the original value for r.Next(). // r must not be empty. @@ -201,7 +242,7 @@ func New(n int) *Ring { // them creates a single ring with the elements of s inserted // after r. The result points to the element following the // last element of s after insertion. -func (r *Ring) Link(s *Ring) *Ring { +func (r *Ring) Link(s *Ring) (res *Ring) { n := r.Next() if s != nil { p := s.Prev() @@ -215,6 +256,7 @@ func (r *Ring) Link(s *Ring) *Ring { return n } + // Unlink removes n % r.Len() elements from the ring r, starting // at r.Next(). If n % r.Len() == 0, r remains unchanged. // The result is the removed subring. r must not be empty. From 4bf7dfbf528c163a72836e97d9f0b5d61d27184c Mon Sep 17 00:00:00 2001 From: adjenny Date: Tue, 27 Dec 2022 19:57:26 +0100 Subject: [PATCH 03/20] start on Link --- src/container/ring/ring.gobra | 76 ++++++++++++++++++++++++----------- 1 file changed, 52 insertions(+), 24 deletions(-) diff --git a/src/container/ring/ring.gobra b/src/container/ring/ring.gobra index 66be15d5864..7ea345e0c35 100644 --- a/src/container/ring/ring.gobra +++ b/src/container/ring/ring.gobra @@ -26,6 +26,7 @@ pred (r *Ring) Mem(ghost s set[*Ring], ghost isInit bool) { (isInit ==> ( (len(s)==1 ==> (r.next==r && r.prev==r)) && (forall i *Ring :: i in s ==> (i.next != nil && i.prev != nil)) && + //((len(s) > 1) ==> (forall i *Ring :: i in s ==> (i.next != i && i.prev != i))) && (forall i, j *Ring :: ((i in s && i.next == j) ==> (j in s && j.prev == i && i.next.prev == i && j.prev.next == j))) && (forall i, j *Ring :: ((i in s && i.prev == j) ==> (j in s && j.next == i && i.prev.next == i && j.next.prev == j))))) } @@ -47,42 +48,44 @@ func (r *Ring) init(ghost elems set[*Ring], ghost isInit bool) (res *Ring) { // Next returns the next ring element. r must not be empty. +//# We use 'owner' here to make calls from different receivers in the same ring structure work (see e.g. Link) requires r != nil requires r in elems -requires r.Mem(elems, isInit) -ensures !isInit ==> (r.Mem(set[*Ring]{r}, true) && res == r) //# The comment does not explain that r is returned if the ring is not initialized but that's what the implementation does. -ensures isInit ==> r.Mem(elems, true) -ensures isInit ==> (unfolding r.Mem(elems, true) in (res == r.next)) +requires owner.Mem(elems, isInit) +ensures !isInit ==> (owner.Mem(set[*Ring]{r}, true) && res == r) //# The comment does not explain that r is returned if the ring is not initialized but that's what the implementation does. +ensures isInit ==> (owner.Mem(elems, true) && res in elems) +ensures isInit ==> (unfolding owner.Mem(elems, true) in (res == r.next)) decreases -func (r *Ring) Next(ghost elems set[*Ring], ghost isInit bool) (res *Ring) { - unfold r.Mem(elems, isInit) +func (r *Ring) Next(ghost elems set[*Ring], ghost owner *Ring, ghost isInit bool) (res *Ring) { + unfold owner.Mem(elems, isInit) if r.next == nil { //# here we know !isInit - fold r.Mem(elems, false) + fold owner.Mem(elems, false) return r.init(elems, false) } res = r.next - fold r.Mem(elems, true) + fold owner.Mem(elems, true) } // Prev returns the previous ring element. r must not be empty. +//# We use 'owner' here to make calls from different receivers in the same ring structure work (see e.g. Link) requires r != nil requires r in elems -requires r.Mem(elems, isInit) -ensures !isInit ==> (r.Mem(set[*Ring]{r}, true) && res == r) //# The comment does not explain that r is returned if the ring is not initialized but that's what the implementation does. -ensures isInit ==> r.Mem(elems, true) -ensures isInit ==> (unfolding r.Mem(elems, true) in (res == r.prev)) +requires owner.Mem(elems, isInit) +ensures !isInit ==> (owner.Mem(set[*Ring]{r}, true) && res == r) //# The comment does not explain that r is returned if the ring is not initialized but that's what the implementation does. +ensures isInit ==> (owner.Mem(elems, true) && res in elems) +ensures isInit ==> (unfolding owner.Mem(elems, true) in (res == r.prev)) decreases -func (r *Ring) Prev(ghost elems set[*Ring], ghost isInit bool) (res *Ring) { - unfold r.Mem(elems, isInit) +func (r *Ring) Prev(ghost elems set[*Ring], ghost owner *Ring, ghost isInit bool) (res *Ring) { + unfold owner.Mem(elems, isInit) if r.next == nil { //# here we know !isInit - fold r.Mem(elems, false) + fold owner.Mem(elems, false) return r.init(elems, false) } res = r.prev - fold r.Mem(elems, true) + fold owner.Mem(elems, true) } @@ -210,12 +213,15 @@ func New(n int) (res *Ring, ghost elems set[*Ring]) { //# Implementation was changed. Every iteration we take a consistent ring and return a consistent ring with a new element. unfold r.Mem(elems, true) q := &Ring{} + //assume q != p q.prev = p q.next = p.next q.prev.next = q q.next.prev = q p = q elems = elems union set[*Ring]{p} + //assert p.next != p + //assert p.prev != p fold r.Mem(elems, true) } @@ -225,38 +231,60 @@ func New(n int) (res *Ring, ghost elems set[*Ring]) { res = r } -/* + // Link connects ring r with ring s such that r.Next() // becomes s and returns the original value for r.Next(). // r must not be empty. // -// If r and s point to the same ring, linking +// If r and s point to the same ring, linking // them removes the elements between r and s from the ring. // The removed elements form a subring and the result is a // reference to that subring (if no elements were removed, // the result is still the original value for r.Next(), // and not nil). +//#"Pointing to the same ring" here means to elements of the same ring structure // // If r and s point to different rings, linking // them creates a single ring with the elements of s inserted // after r. The result points to the element following the // last element of s after insertion. -func (r *Ring) Link(s *Ring) (res *Ring) { - n := r.Next() +//#This means likewise the result points to the original r.Next() +requires r != nil +requires r in elemsR +requires r.Mem(elemsR, true) +requires (s != nil && !(s in elemsR)) ==> (s.Mem(elemsS, true) && s in elemsS) +//ensures (!(s in elemsR)) ==> (res == old(unfolding r.Mem(elemsR, true) in r.next && res.Mem((elemsR union elemsS), true))) +func (r *Ring) Link(s *Ring, ghost elemsR set[*Ring], ghost elemsS set[*Ring]) (res *Ring) { + n := r.Next(elemsR, r, true) if s != nil { - p := s.Prev() + ghost elemsX := (s in elemsR)?(elemsR):(elemsS) + ghost owner := (s in elemsR)?(r):(s) + p := s.Prev(elemsX, owner, true) // Note: Cannot use multiple assignment because // evaluation order of LHS is not specified. + unfold r.Mem(elemsR, true) + ghost if !(s in elemsR){ + unfold s.Mem(elemsS, true) + } r.next = s s.prev = r - n.prev = p - p.next = n + n.prev = p //# This only works due to the postcondition 'res in elems' in Next() + p.next = n //# This only works due to the postcondition 'res in elems' in Prev() + ghost if !(s in elemsR){ + fold n.Mem((elemsR union elemsS), true) + } + /*ghost if (s in elemsR){ + ghost if r==s && len(elemsR)>1{ + fold n.Mem((elemsR setminus (set[*Ring]{r})), true) + } + //fold n.Mem((?????), true) //# elems needs to be all elements strictly between r and s, BUT WHAT IF r==s?? + }*/ } return n } - +/* // Unlink removes n % r.Len() elements from the ring r, starting // at r.Next(). If n % r.Len() == 0, r remains unchanged. // The result is the removed subring. r must not be empty. From 9465f4e8f99a33af6036ee783e7867fa27bd1931 Mon Sep 17 00:00:00 2001 From: adjenny Date: Mon, 2 Jan 2023 22:25:19 +0100 Subject: [PATCH 04/20] partial file: specified sort.Interface, sort.IntSlice implementation, sort.IsSorted, memory safety for insertionSort --- src/sort/sort_partial.gobra | 221 ++++++++++++++++++++++++++++++++++++ 1 file changed, 221 insertions(+) create mode 100644 src/sort/sort_partial.gobra diff --git a/src/sort/sort_partial.gobra b/src/sort/sort_partial.gobra new file mode 100644 index 00000000000..5eefe59d8c7 --- /dev/null +++ b/src/sort/sort_partial.gobra @@ -0,0 +1,221 @@ +// Copyright 2009 The Go Authors. All rights reserved. +// Use of this source code is governed by a BSD-style +// license that can be found in the LICENSE file. + +//go:generate go run gen_sort_variants.go + +// Package sort provides primitives for sorting slices and user-defined collections. +// +gobra +package sort + +//import "math/bits" //# Had to comment this out, otherwise verification progress does not go above 3% + +// An implementation of Interface can be sorted by the routines in this package. +// The methods refer to elements of the underlying collection by integer index. +type Interface interface { + pred Mem(ghost s seq[any]) + + // Len is the number of elements in the collection. + requires acc(Mem(elems), 1/2) + ensures acc(Mem(elems), 1/2) + ensures res == len(elems) + ensures res >= 0 + Len(ghost elems seq[any]) (res int) + + // Less reports whether the element with index i + // must sort before the element with index j. + // + // If both Less(i, j) and Less(j, i) are false, + // then the elements at index i and j are considered equal. //# What does "considered equal mean"? We cannot use == in the spec since equality is relative to the defined order + // Sort may place equal elements in any order in the final result, + // while Stable preserves the original input order of equal elements. + // + // Less must describe a transitive ordering: + // - if both Less(i, j) and Less(j, k) are true, then Less(i, k) must be true as well. + // - if both Less(i, j) and Less(j, k) are false, then Less(i, k) must be false as well. + requires Mem(elems) + requires 0 <= i && i < len(elems) + requires 0 <= j && j < len(elems) + ensures forall a, b, c int :: (0 <= a && a < len(elems) && 0 <= b && b < len(elems) && 0 <= c && c < len(elems) && less_spec(a,b,elems) && less_spec(b,c,elems)) ==> less_spec(a,c,elems) + pure less_spec(i, j int, ghost elems seq[any]) (res bool) + // + // Note that floating-point comparison (the < operator on float32 or float64 values) + // is not a transitive ordering when not-a-number (NaN) values are involved. + // See Float64Slice.Less for a correct implementation for floating-point values. + requires acc(Mem(elems), 1/2) + requires 0 <= i && i < len(elems) + requires 0 <= j && j < len(elems) + ensures acc(Mem(elems), 1/2) + ensures res == less_spec(i, j, elems) + Less(i, j int, ghost elems seq[any]) (res bool) + + // Swap swaps the elements with indexes i and j. + requires Mem(elems) + requires 0 <= i && i < len(elems) //# possibly make Len() pure and use that + requires 0 <= j && j < len(elems) //# possibly make Len() pure and use that + ensures Mem(swapped_elems) + ensures len(elems) == len(swapped_elems) //# somehow this does not suffice to infer i and j are in range [0, len(swapped_elems)-1] + ensures 0 <= i && i < len(elems) && i < len(swapped_elems) //# possibly make Len() pure and use that + ensures 0 <= j && j < len(elems) && j < len(swapped_elems) //# possibly make Len() pure and use that + ensures elems[i] === swapped_elems[j] + ensures elems[j] === swapped_elems[i] + ensures forall x int :: (0 <= x && x < len(elems) && x != i && x != j) ==> (elems[x] === swapped_elems[x]) + Swap(i, j int, ghost elems seq[any]) (ghost swapped_elems seq[any]) +} + + +//# LOTS IN BETWEEN..... + +ghost +requires data != nil +requires data.Mem(elems) +requires 0 <= start && start < len(elems) +requires start <= end && end < len(elems) +ensures (end - start <= 1) ==> res +ensures (end - start > 1 && !data.less_spec(end, end-1, elems)) ==> (res == isPartiallySorted(data, start, end-1, elems)) +ensures (end - start > 1 && data.less_spec(end, end-1, elems)) ==> !res +//ensures res ==> (forall idx int :: ((start < idx && idx < end+1) ==> (!data.less_spec(idx, idx-1, elems)))) //# Would like to be able to infer that +pure +func isPartiallySorted(data Interface, start, end int, ghost elems seq[any]) (res bool) { + return (end - start <= 1) ? true : (!data.less_spec(end, end-1, elems) ? isPartiallySorted(data, start, end-1, elems) : false) +} + +// IsSorted reports whether data is sorted. +preserves data.Mem(elems) +requires data != nil +ensures res ==> (forall idx int :: ((0 < idx && idx < len(elems)) ==> (!data.less_spec(idx, idx-1, elems)))) +func IsSorted(data Interface, ghost elems seq[any]) (res bool) { + n := data.Len(elems) + + res = true //# moved this up for use in the invariant + + invariant i < n + invariant (len(elems) > 0) ==> (0 <= i) //# if n==0 then i==-1 after initialization + invariant data.Mem(elems) + invariant (res && len(elems) != 0) ==> (forall idx int :: ((i < idx && idx < len(elems)) ==> (!data.less_spec(idx, idx-1, elems)))) + //invariant (res && len(elems) != 0) ==> isPartiallySorted(data, i, n-1, elems) //# Would like for this to hold here + decreases i + for i := n - 1; i > 0; i-- { + if data.Less(i, i-1, elems) { + res = false + return + } + } + return +} + +// Convenience types for common cases + +// IntSlice attaches the methods of Interface to []int, sorting in increasing order. +type IntSlice []int + +//# Adapted from Gobra tutorial +ghost +requires forall j int :: 0 <= j && j < len(s) ==> acc(&s[j],_) +ensures len(res) == len(s) +ensures forall j int :: {s[j]} {res[j]} 0 <= j && j < len(s) ==> s[j] == res[j] +pure func toSeq(s []int) (res seq[any]) { + return (len(s) == 0 ? seq[any]{} : + toSeq(s[:len(s)-1]) ++ seq[any]{s[len(s) - 1]}) +} + +pred (x IntSlice) Mem(ghost s seq[any]){ + len(x) == len(s) && //# If this is not the first line in the predicate, then we cannot verify e.g. the last postcondition in Len() + forall j int :: 0 <= j && j < len(x) ==> acc(&x[j]) && + s == toSeq(x) && + forall j int :: {x[j]} {s[j]} 0 <= j && j < len(s) ==> x[j] == s[j] +} + +requires acc(x.Mem(elems), 1/2) +ensures acc(x.Mem(elems), 1/2) +ensures unfolding acc(x.Mem(elems), 1/2) in res == len(elems) +ensures res >= 0 +func (x IntSlice) Len(ghost elems seq[any]) (res int) { + return len(x) +} + +requires x.Mem(elems) +requires 0 <= i && i < len(elems) +requires 0 <= j && j < len(elems) +ensures forall a, b, c int :: (0 <= a && a < len(elems) && 0 <= b && b < len(elems) && 0 <= c && c < len(elems) && x.less_spec(a,b,elems) && x.less_spec(b,c,elems)) ==> x.less_spec(a,c,elems) +pure func (x IntSlice) less_spec(i, j int, ghost elems seq[any]) (res bool){ + return unfolding x.Mem(elems) in x[i] < x[j] +} + + +requires acc(x.Mem(elems), 1/2) +requires 0 <= i && i < len(elems) +requires 0 <= j && j < len(elems) +ensures acc(x.Mem(elems), 1/2) +ensures res == x.less_spec(i, j, elems) +func (x IntSlice) Less(i, j int, ghost elems seq[any]) (res bool) { + return unfolding acc(x.Mem(elems), 1/2) in x[i] < x[j] +} + +requires x.Mem(elems) +requires 0 <= i && i < len(elems) +requires 0 <= j && j < len(elems) +ensures x.Mem(swapped_elems) +ensures len(elems) == len(swapped_elems) //# somehow this does not suffice to infer i and j are in range [0, len(swapped_elems)-1] +ensures 0 <= i && i < len(elems) && i < len(swapped_elems) //# possibly make Len() pure and use that +ensures 0 <= j && j < len(elems) && j < len(swapped_elems) //# possibly make Len() pure and use that +//# These 3 lines are required.. +ensures old(unfolding x.Mem(elems) in x[i]) === (unfolding x.Mem(swapped_elems) in x[j]) +ensures old(unfolding x.Mem(elems) in x[j]) === (unfolding x.Mem(swapped_elems) in x[i]) +ensures forall idx int :: (0 <= idx && idx < len(elems) && idx != i && idx != j) ==> (old(unfolding x.Mem(elems) in x[idx]) === (unfolding x.Mem(swapped_elems) in x[idx])) +//# ..for these 3 corresponding lines to work. Why? +ensures elems[i] === swapped_elems[j] +ensures elems[j] === swapped_elems[i] +ensures forall idx int :: (0 <= idx && idx < len(elems) && idx != i && idx != j) ==> (elems[idx] === swapped_elems[idx]) +func (x IntSlice) Swap(i, j int, ghost elems seq[any]) (ghost swapped_elems seq[any]) { + unfold x.Mem(elems) + x[i], x[j] = x[j], x[i] + swapped_elems = toSeq(x) + fold x.Mem(swapped_elems) +} + +//# implementation proof +(IntSlice) implements Interface{ } + + + +// ######### BEGIN FROM zsortinterface ############## +// insertionSort sorts data[a:b] using insertion sort. +requires data.Mem(elems) +requires data != nil +requires 0 <= a && a < len(elems) +requires a+1 < b && b <= len(elems) //# the element at position b does not get sorted +ensures data.Mem(sorted_elems) +//ensures isPartiallySorted(data, a, b-1, sorted_elems) +func insertionSort(data Interface, a, b int, ghost elems seq[any]) (ghost sorted_elems seq[any]) { + sorted_elems = elems + assert data.Mem(sorted_elems) + + invariant a < i && i <= b + invariant b <= len(sorted_elems) + invariant (a < b) ==> (i <= b) + invariant data.Mem(sorted_elems) + //invariant isPartiallySorted(data, a, i-1, sorted_elems) + decreases b-i + for i := a + 1; i < b; i++ { //# for any kind of sorting to happen b has to be at least a+2, does this mean if called with b=a+1 that this will not be sorted? Answer: YES, should we enforce that in the precondition? + invariant i < b + invariant b <= len(sorted_elems) + invariant a <= j && j <= i + invariant (a < j) ==> (0 <= j-1) + invariant data.Mem(sorted_elems) + //invariant isPartiallySorted(data, a, XXX, sorted_elems) + //invariant isPartiallySorted(data, YYY, i, sorted_elems) + decreases j-a + for j := i; j > a /*&& data.Less(j, j-1, elems)*/; j-- { //# Here it complains it could be j-1<0. But we know 0 Date: Sun, 8 Jan 2023 03:40:55 +0100 Subject: [PATCH 05/20] restore ring directory to master --- src/container/ring/ring.go | 2 - src/container/ring/ring.gobra | 321 ---------------------------------- 2 files changed, 323 deletions(-) delete mode 100644 src/container/ring/ring.gobra diff --git a/src/container/ring/ring.go b/src/container/ring/ring.go index 88c0f011121..268670bc852 100644 --- a/src/container/ring/ring.go +++ b/src/container/ring/ring.go @@ -3,8 +3,6 @@ // license that can be found in the LICENSE file. // Package ring implements operations on circular lists. - -// +gobra package ring // A Ring is an element of a circular list, or ring. diff --git a/src/container/ring/ring.gobra b/src/container/ring/ring.gobra deleted file mode 100644 index 7ea345e0c35..00000000000 --- a/src/container/ring/ring.gobra +++ /dev/null @@ -1,321 +0,0 @@ -// Copyright 2009 The Go Authors. All rights reserved. -// Use of this source code is governed by a BSD-style -// license that can be found in the LICENSE file. - -// Package ring implements operations on circular lists. - -// +gobra -package ring - -// A Ring is an element of a circular list, or ring. -// Rings do not have a beginning or end; a pointer to any ring element -// serves as reference to the entire ring. Empty rings are represented -// as nil Ring pointers. The zero value for a Ring is a one-element -// ring with a nil Value. -type Ring struct { - next, prev *Ring - Value any // for use by client; untouched by this library -} - - -pred (r *Ring) Mem(ghost s set[*Ring], ghost isInit bool) { - r in s && - (forall i *Ring :: i in s ==> (acc(&i.next) && acc(&i.prev) && acc(&i.Value))) && - ((r.next == nil || r.prev == nil) ==> !isInit) && //# More correctly, it is !isInit if it cannot reach itself in both directions via the same Ring elements - (!isInit ==> ((s == set[*Ring]{r}) && (r.next == nil && r.prev == nil))) && - (isInit ==> ( - (len(s)==1 ==> (r.next==r && r.prev==r)) && - (forall i *Ring :: i in s ==> (i.next != nil && i.prev != nil)) && - //((len(s) > 1) ==> (forall i *Ring :: i in s ==> (i.next != i && i.prev != i))) && - (forall i, j *Ring :: ((i in s && i.next == j) ==> (j in s && j.prev == i && i.next.prev == i && j.prev.next == j))) && - (forall i, j *Ring :: ((i in s && i.prev == j) ==> (j in s && j.next == i && i.prev.next == i && j.next.prev == j))))) -} -//# enforce structure by: -//# forall elements, forall i in [0,len]: moveLeft(i) == moveRight(len-i) -//# problematic for Ring because we get Len() by the same logic - -requires r.Mem(elems, isInit) -ensures r.Mem(set[*Ring]{r}, true) -ensures r == res -decreases -func (r *Ring) init(ghost elems set[*Ring], ghost isInit bool) (res *Ring) { - unfold r.Mem(elems, isInit) - r.next = r - r.prev = r - fold r.Mem(set[*Ring]{r}, true) - return r -} - - -// Next returns the next ring element. r must not be empty. -//# We use 'owner' here to make calls from different receivers in the same ring structure work (see e.g. Link) -requires r != nil -requires r in elems -requires owner.Mem(elems, isInit) -ensures !isInit ==> (owner.Mem(set[*Ring]{r}, true) && res == r) //# The comment does not explain that r is returned if the ring is not initialized but that's what the implementation does. -ensures isInit ==> (owner.Mem(elems, true) && res in elems) -ensures isInit ==> (unfolding owner.Mem(elems, true) in (res == r.next)) -decreases -func (r *Ring) Next(ghost elems set[*Ring], ghost owner *Ring, ghost isInit bool) (res *Ring) { - unfold owner.Mem(elems, isInit) - if r.next == nil { - //# here we know !isInit - fold owner.Mem(elems, false) - return r.init(elems, false) - } - res = r.next - fold owner.Mem(elems, true) -} - - -// Prev returns the previous ring element. r must not be empty. -//# We use 'owner' here to make calls from different receivers in the same ring structure work (see e.g. Link) -requires r != nil -requires r in elems -requires owner.Mem(elems, isInit) -ensures !isInit ==> (owner.Mem(set[*Ring]{r}, true) && res == r) //# The comment does not explain that r is returned if the ring is not initialized but that's what the implementation does. -ensures isInit ==> (owner.Mem(elems, true) && res in elems) -ensures isInit ==> (unfolding owner.Mem(elems, true) in (res == r.prev)) -decreases -func (r *Ring) Prev(ghost elems set[*Ring], ghost owner *Ring, ghost isInit bool) (res *Ring) { - unfold owner.Mem(elems, isInit) - if r.next == nil { - //# here we know !isInit - fold owner.Mem(elems, false) - return r.init(elems, false) - } - res = r.prev - fold owner.Mem(elems, true) -} - - -ghost -requires owner.Mem(elems,true) -requires r in elems -requires n >= 0 -ensures (n==0) ==> res==r -ensures (n>0) ==> res==(unfolding owner.Mem(elems,true) in r.next.moveNext(n-1, owner, elems)) -pure func (r *Ring) moveNext(n int, ghost owner *Ring, ghost elems set[*Ring]) (res * Ring){ - return unfolding owner.Mem(elems,true) in ((n==0) ? r : r.next.moveNext(n-1, owner, elems)) -} - -/* -//# TEST NEXT -requires r.Mem(elems,true) -requires r in elems -ensures r.Mem(elems, true) -ensures (res == r.moveNext(3, r, elems)) -func (r *Ring) moveNextTest(ghost elems set[*Ring]) (res *Ring){ - unfold r.Mem(elems, true) - res = r.next.next.next - fold r.Mem(elems, true) -} -*/ - -ghost -requires owner.Mem(elems,true) -requires r in elems -requires n <= 0 -ensures (n==0) ==> res==r -ensures (n<0) ==> res==(unfolding owner.Mem(elems,true) in r.prev.movePrev(n+1, owner, elems)) -pure func (r *Ring) movePrev(n int, ghost owner *Ring, ghost elems set[*Ring]) (res * Ring){ - return unfolding owner.Mem(elems,true) in ((n==0) ? r : r.prev.movePrev(n+1, owner, elems)) -} - -/* -//# TEST PREV -requires r.Mem(elems,true) -requires r in elems -ensures r.Mem(elems, true) -ensures (res == r.movePrev(-3, r, elems)) -func (r *Ring) movePrevTest(ghost elems set[*Ring]) (res *Ring){ - unfold r.Mem(elems, true) - res = r.prev.prev.prev - fold r.Mem(elems, true) -} -*/ - - - -// Move moves n % r.Len() elements backward (n < 0) or forward (n >= 0) -// in the ring and returns that ring element. r must not be empty. -requires r.Mem(elems, isInit) //# make this PRESERVES -requires r != nil -requires r in elems -ensures !isInit ==> (r.Mem(set[*Ring]{r}, true) && res == old(r)) //# The comment does not explain that r is returned if the ring is not initialized but that's what the implementation does. -ensures (n == 0) ==> (res == r) -ensures isInit ==> r.Mem(elems, true) -//ensures (isInit && n>0) ==> (res == r.moveNext(n, r, elems)) -//ensures (isInit && n<0) ==> (res == r.movePrev(n, r, elems)) -//# Why does the implementation not make the modulo calculation and save on potentially unnecessary iterations? --> We'd need to run Len() (Len() many iterations) but for n > 2*Len() it'd still always make sense to compute the modulus -func (r *Ring) Move(n int, ghost elems set[*Ring], ghost isInit bool) (res *Ring) { - if unfolding r.Mem(elems, isInit) in r.next == nil { - return r.init(elems, isInit) - assert r.Mem(set[*Ring]{r}, true) - } - - startRing := r //# included for invariant - startN := n //# included for invariant - switch { - case n < 0: - invariant startRing.Mem(elems, true) - invariant r in elems - invariant startN <= n && n <= 0 - //invariant startRing.movePrev((startN - n), startRing, elems) == r - decreases 0 - n - for ; n < 0; n++ { - unfold startRing.Mem(elems, true) - r = r.prev - fold startRing.Mem(elems, true) - } - case n > 0: - invariant startRing.Mem(elems, true) - invariant r in elems - invariant startN >= n && n >= 0 - //invariant startRing.moveNext((startN - n), owner, elems) == r - decreases n - for ; n > 0; n-- { - unfold startRing.Mem(elems, true) - r = r.next - fold startRing.Mem(elems, true) - } - } - return r -} - - - -// New creates a ring of n elements. -ensures n <= 0 ==> res == nil -ensures n > 0 ==> (len(elems) == n && res.Mem(elems, true)) -func New(n int) (res *Ring, ghost elems set[*Ring]) { - if n <= 0 { - res = nil - elems = set[*Ring]{} - return - } - r := new(Ring) - p := r - - //# Changed the implementation to already form a cycle here so that we can use - //# the memory predicate in the invariant and have an easier time establishing it in the end. - r.next = r - r.prev = r - elems = set[*Ring]{r} - fold r.Mem(elems, true) - - invariant r.Mem(elems, true) - invariant len(elems) == i - invariant p in elems - invariant 1 <= i && i <= n - decreases n - i - for i := 1; i < n; i++ { - //# Implementation was changed. Every iteration we take a consistent ring and return a consistent ring with a new element. - unfold r.Mem(elems, true) - q := &Ring{} - //assume q != p - q.prev = p - q.next = p.next - q.prev.next = q - q.next.prev = q - p = q - elems = elems union set[*Ring]{p} - //assert p.next != p - //assert p.prev != p - fold r.Mem(elems, true) - } - - //p.next = r //# removed - //r.prev = p //# removed - - res = r -} - - - -// Link connects ring r with ring s such that r.Next() -// becomes s and returns the original value for r.Next(). -// r must not be empty. -// -// If r and s point to the same ring, linking -// them removes the elements between r and s from the ring. -// The removed elements form a subring and the result is a -// reference to that subring (if no elements were removed, -// the result is still the original value for r.Next(), -// and not nil). -//#"Pointing to the same ring" here means to elements of the same ring structure -// -// If r and s point to different rings, linking -// them creates a single ring with the elements of s inserted -// after r. The result points to the element following the -// last element of s after insertion. -//#This means likewise the result points to the original r.Next() -requires r != nil -requires r in elemsR -requires r.Mem(elemsR, true) -requires (s != nil && !(s in elemsR)) ==> (s.Mem(elemsS, true) && s in elemsS) -//ensures (!(s in elemsR)) ==> (res == old(unfolding r.Mem(elemsR, true) in r.next && res.Mem((elemsR union elemsS), true))) -func (r *Ring) Link(s *Ring, ghost elemsR set[*Ring], ghost elemsS set[*Ring]) (res *Ring) { - n := r.Next(elemsR, r, true) - if s != nil { - ghost elemsX := (s in elemsR)?(elemsR):(elemsS) - ghost owner := (s in elemsR)?(r):(s) - p := s.Prev(elemsX, owner, true) - // Note: Cannot use multiple assignment because - // evaluation order of LHS is not specified. - unfold r.Mem(elemsR, true) - ghost if !(s in elemsR){ - unfold s.Mem(elemsS, true) - } - r.next = s - s.prev = r - n.prev = p //# This only works due to the postcondition 'res in elems' in Next() - p.next = n //# This only works due to the postcondition 'res in elems' in Prev() - ghost if !(s in elemsR){ - fold n.Mem((elemsR union elemsS), true) - } - /*ghost if (s in elemsR){ - ghost if r==s && len(elemsR)>1{ - fold n.Mem((elemsR setminus (set[*Ring]{r})), true) - } - //fold n.Mem((?????), true) //# elems needs to be all elements strictly between r and s, BUT WHAT IF r==s?? - }*/ - } - return n -} - -/* -// Unlink removes n % r.Len() elements from the ring r, starting -// at r.Next(). If n % r.Len() == 0, r remains unchanged. -// The result is the removed subring. r must not be empty. -func (r *Ring) Unlink(n int) *Ring { - if n <= 0 { - return nil - } - return r.Link(r.Move(n + 1)) -} - -// Len computes the number of elements in ring r. -// It executes in time proportional to the number of elements. -func (r *Ring) Len() int { - n := 0 - if r != nil { - n = 1 - for p := r.Next(); p != r; p = p.next { - n++ - } - } - return n -} - -// Do calls function f on each element of the ring, in forward order. -// The behavior of Do is undefined if f changes *r. -func (r *Ring) Do(f func(any)) { - if r != nil { - f(r.Value) - for p := r.Next(); p != r; p = p.next { - f(p.Value) - } - } -} -*/ From a7d8388fbd063a0f9281bde935a3cd817b629591 Mon Sep 17 00:00:00 2001 From: adjenny Date: Sun, 8 Jan 2023 04:06:48 +0100 Subject: [PATCH 06/20] allowed same indices a, b in 'insertionSort' --- src/sort/sort_partial.gobra | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) diff --git a/src/sort/sort_partial.gobra b/src/sort/sort_partial.gobra index 5eefe59d8c7..d7e5f198d19 100644 --- a/src/sort/sort_partial.gobra +++ b/src/sort/sort_partial.gobra @@ -184,38 +184,44 @@ func (x IntSlice) Swap(i, j int, ghost elems seq[any]) (ghost swapped_elems seq[ requires data.Mem(elems) requires data != nil requires 0 <= a && a < len(elems) -requires a+1 < b && b <= len(elems) //# the element at position b does not get sorted +requires a <= b && b <= len(elems) //# the element at position b does not get sorted ensures data.Mem(sorted_elems) +ensures len(sorted_elems) == len(elems) +ensures a == b ==> isPartiallySorted(data, a, a, sorted_elems) //ensures isPartiallySorted(data, a, b-1, sorted_elems) func insertionSort(data Interface, a, b int, ghost elems seq[any]) (ghost sorted_elems seq[any]) { sorted_elems = elems + assert len(sorted_elems) == len(elems) assert data.Mem(sorted_elems) - invariant a < i && i <= b + invariant len(sorted_elems) == len(elems) + invariant a < i invariant b <= len(sorted_elems) - invariant (a < b) ==> (i <= b) + invariant a < b ==> i <= b invariant data.Mem(sorted_elems) //invariant isPartiallySorted(data, a, i-1, sorted_elems) decreases b-i for i := a + 1; i < b; i++ { //# for any kind of sorting to happen b has to be at least a+2, does this mean if called with b=a+1 that this will not be sorted? Answer: YES, should we enforce that in the precondition? + invariant len(sorted_elems) == len(elems) invariant i < b invariant b <= len(sorted_elems) invariant a <= j && j <= i - invariant (a < j) ==> (0 <= j-1) + invariant a < j ==> 0 <= j-1 invariant data.Mem(sorted_elems) //invariant isPartiallySorted(data, a, XXX, sorted_elems) //invariant isPartiallySorted(data, YYY, i, sorted_elems) decreases j-a - for j := i; j > a /*&& data.Less(j, j-1, elems)*/; j-- { //# Here it complains it could be j-1<0. But we know 0 a /*&& data.Less(j, j-1, elems)*/; j-- { assert 0 <= j-1 assert i < b assert i < len(sorted_elems) - if data.Less(j, j-1, sorted_elems) { + if data.Less(j, j-1, sorted_elems) { //# The second conjunct in the loop condition was commented out and introduced here as an IF block. This is due to a bug in Gobra where short circuiting is not detected. See https://github.com/viperproject/gobra/issues/511 sorted_elems = data.Swap(j, j-1, sorted_elems) } else { break } } } + } // ######### END FROM zsortinterface ############## From a86707b6be4378835a3c7228a9d44a1309073a9b Mon Sep 17 00:00:00 2001 From: adjenny Date: Mon, 9 Jan 2023 02:30:54 +0100 Subject: [PATCH 07/20] simplified, attempt at 'isPartiallySorted', attempt at sequence equality check --- src/sort/sort_partial.gobra | 90 +++++++++++++++++++++++++------------ 1 file changed, 61 insertions(+), 29 deletions(-) diff --git a/src/sort/sort_partial.gobra b/src/sort/sort_partial.gobra index d7e5f198d19..1b783b84976 100644 --- a/src/sort/sort_partial.gobra +++ b/src/sort/sort_partial.gobra @@ -60,6 +60,7 @@ type Interface interface { ensures elems[i] === swapped_elems[j] ensures elems[j] === swapped_elems[i] ensures forall x int :: (0 <= x && x < len(elems) && x != i && x != j) ==> (elems[x] === swapped_elems[x]) + ensures old(less_spec(i, j, elems)) ==> !less_spec(i, j, swapped_elems) //# We make the effect of the Swap operation on the Less relation explicit. Swap(i, j int, ghost elems seq[any]) (ghost swapped_elems seq[any]) } @@ -71,36 +72,40 @@ requires data != nil requires data.Mem(elems) requires 0 <= start && start < len(elems) requires start <= end && end < len(elems) -ensures (end - start <= 1) ==> res -ensures (end - start > 1 && !data.less_spec(end, end-1, elems)) ==> (res == isPartiallySorted(data, start, end-1, elems)) -ensures (end - start > 1 && data.less_spec(end, end-1, elems)) ==> !res -//ensures res ==> (forall idx int :: ((start < idx && idx < end+1) ==> (!data.less_spec(idx, idx-1, elems)))) //# Would like to be able to infer that +ensures end - start == 0 ==> res == true +ensures (end - start > 0 && !data.less_spec(end, end - 1, elems)) ==> res == isPartiallySorted(data, start, end - 1, elems) +ensures (end - start > 0 && data.less_spec(end, end - 1, elems)) ==> !res +//ensures res ==> (forall idx int :: ((start < idx && idx <= end) ==> !data.less_spec(idx, idx - 1, elems))) //# Would like to be able to infer that +//ensures (res && start+2 < end) ==> !data.less_spec(end, end - 1, elems) && !data.less_spec(end-1, end - 2, elems) && !data.less_spec(end-2, end-3, elems) pure func isPartiallySorted(data Interface, start, end int, ghost elems seq[any]) (res bool) { - return (end - start <= 1) ? true : (!data.less_spec(end, end-1, elems) ? isPartiallySorted(data, start, end-1, elems) : false) + return (end - start == 0) ? true : (!data.less_spec(end, end - 1, elems) ? isPartiallySorted(data, start, end - 1, elems) : false) } // IsSorted reports whether data is sorted. preserves data.Mem(elems) requires data != nil -ensures res ==> (forall idx int :: ((0 < idx && idx < len(elems)) ==> (!data.less_spec(idx, idx-1, elems)))) +ensures res ==> forall idx int :: ((0 < idx && idx < len(elems)) ==> (!data.less_spec(idx, idx - 1, elems))) +ensures !res ==> !(forall idx int :: ((0 < idx && idx < len(elems)) ==> (!data.less_spec(idx, idx - 1, elems)))) func IsSorted(data Interface, ghost elems seq[any]) (res bool) { n := data.Len(elems) res = true //# moved this up for use in the invariant + invariant res invariant i < n - invariant (len(elems) > 0) ==> (0 <= i) //# if n==0 then i==-1 after initialization + invariant len(elems) > 0 ==> 0 <= i //# if n==0 then i==-1 after initialization invariant data.Mem(elems) - invariant (res && len(elems) != 0) ==> (forall idx int :: ((i < idx && idx < len(elems)) ==> (!data.less_spec(idx, idx-1, elems)))) - //invariant (res && len(elems) != 0) ==> isPartiallySorted(data, i, n-1, elems) //# Would like for this to hold here + invariant len(elems) != 0 ==> (forall idx int :: ((i < idx && idx < len(elems)) ==> !data.less_spec(idx, idx - 1, elems))) + //invariant len(elems) != 0 ==> isPartiallySorted(data, i, n - 1, elems) //# Would like for this to hold here decreases i for i := n - 1; i > 0; i-- { - if data.Less(i, i-1, elems) { - res = false - return + if data.Less(i, i - 1, elems) { + return false } + //assert isPartiallySorted(data, i, n - 1, elems) } + assert res return } @@ -111,12 +116,12 @@ type IntSlice []int //# Adapted from Gobra tutorial ghost -requires forall j int :: 0 <= j && j < len(s) ==> acc(&s[j],_) +requires forall j int :: 0 <= j && j < len(s) ==> acc(&s[j], _) ensures len(res) == len(s) ensures forall j int :: {s[j]} {res[j]} 0 <= j && j < len(s) ==> s[j] == res[j] pure func toSeq(s []int) (res seq[any]) { return (len(s) == 0 ? seq[any]{} : - toSeq(s[:len(s)-1]) ++ seq[any]{s[len(s) - 1]}) + toSeq(s[:len(s) - 1]) ++ seq[any]{s[len(s) - 1]}) } pred (x IntSlice) Mem(ghost s seq[any]){ @@ -159,14 +164,15 @@ ensures x.Mem(swapped_elems) ensures len(elems) == len(swapped_elems) //# somehow this does not suffice to infer i and j are in range [0, len(swapped_elems)-1] ensures 0 <= i && i < len(elems) && i < len(swapped_elems) //# possibly make Len() pure and use that ensures 0 <= j && j < len(elems) && j < len(swapped_elems) //# possibly make Len() pure and use that -//# These 3 lines are required.. -ensures old(unfolding x.Mem(elems) in x[i]) === (unfolding x.Mem(swapped_elems) in x[j]) -ensures old(unfolding x.Mem(elems) in x[j]) === (unfolding x.Mem(swapped_elems) in x[i]) -ensures forall idx int :: (0 <= idx && idx < len(elems) && idx != i && idx != j) ==> (old(unfolding x.Mem(elems) in x[idx]) === (unfolding x.Mem(swapped_elems) in x[idx])) -//# ..for these 3 corresponding lines to work. Why? +//# This line is required.. +//ensures old(unfolding x.Mem(elems) in x[i]) == (unfolding x.Mem(swapped_elems) in x[j]) +//ensures old(unfolding x.Mem(elems) in x[j]) == (unfolding x.Mem(swapped_elems) in x[i]) +ensures forall idx int :: (0 <= idx && idx < len(elems) && idx != i && idx != j) ==> (old(unfolding x.Mem(elems) in x[idx]) == (unfolding x.Mem(swapped_elems) in x[idx])) +//# ..for these 3 corresponding lines to work. ensures elems[i] === swapped_elems[j] ensures elems[j] === swapped_elems[i] ensures forall idx int :: (0 <= idx && idx < len(elems) && idx != i && idx != j) ==> (elems[idx] === swapped_elems[idx]) +ensures old(x.less_spec(i, j, elems)) ==> !x.less_spec(i, j, swapped_elems) func (x IntSlice) Swap(i, j int, ghost elems seq[any]) (ghost swapped_elems seq[any]) { unfold x.Mem(elems) x[i], x[j] = x[j], x[i] @@ -188,35 +194,37 @@ requires a <= b && b <= len(elems) //# the element at position b does not get so ensures data.Mem(sorted_elems) ensures len(sorted_elems) == len(elems) ensures a == b ==> isPartiallySorted(data, a, a, sorted_elems) -//ensures isPartiallySorted(data, a, b-1, sorted_elems) +//ensures isPartiallySorted(data, a, b - 1, sorted_elems) func insertionSort(data Interface, a, b int, ghost elems seq[any]) (ghost sorted_elems seq[any]) { sorted_elems = elems - assert len(sorted_elems) == len(elems) assert data.Mem(sorted_elems) invariant len(sorted_elems) == len(elems) invariant a < i - invariant b <= len(sorted_elems) invariant a < b ==> i <= b invariant data.Mem(sorted_elems) - //invariant isPartiallySorted(data, a, i-1, sorted_elems) + //# invariant prefix [a:i] is always sorted + //invariant forall idx int :: (a < idx && idx < i && i < b) ==> !data.less_spec(idx, idx - 1, sorted_elems) + //invariant isPartiallySorted(data, a, i - 1, sorted_elems) decreases b-i for i := a + 1; i < b; i++ { //# for any kind of sorting to happen b has to be at least a+2, does this mean if called with b=a+1 that this will not be sorted? Answer: YES, should we enforce that in the precondition? invariant len(sorted_elems) == len(elems) invariant i < b - invariant b <= len(sorted_elems) invariant a <= j && j <= i - invariant a < j ==> 0 <= j-1 + invariant a < j ==> 0 <= j - 1 invariant data.Mem(sorted_elems) + //# invariant prefix [a:j-2] is always sorted and [j:i] is always sorted + //invariant forall idx int :: (j < idx && idx < i) ==> !data.less_spec(idx, idx - 1, sorted_elems) //invariant isPartiallySorted(data, a, XXX, sorted_elems) //invariant isPartiallySorted(data, YYY, i, sorted_elems) decreases j-a - for j := i; j > a /*&& data.Less(j, j-1, elems)*/; j-- { - assert 0 <= j-1 + for j := i; j > a /*&& data.Less(j, j - 1, elems)*/; j-- { + assert 0 <= j - 1 assert i < b assert i < len(sorted_elems) - if data.Less(j, j-1, sorted_elems) { //# The second conjunct in the loop condition was commented out and introduced here as an IF block. This is due to a bug in Gobra where short circuiting is not detected. See https://github.com/viperproject/gobra/issues/511 - sorted_elems = data.Swap(j, j-1, sorted_elems) + if data.Less(j, j - 1, sorted_elems) { //# The second conjunct in the loop condition was commented out and introduced here as an IF block. This is due to a bug in Gobra where short circuiting is not detected. See https://github.com/viperproject/gobra/issues/511 + sorted_elems = data.Swap(j, j - 1, sorted_elems) + assert !data.less_spec(j, j - 1, sorted_elems) } else { break } @@ -225,3 +233,27 @@ func insertionSort(data Interface, a, b int, ghost elems seq[any]) (ghost sorted } // ######### END FROM zsortinterface ############## + + +//# helper + +ghost +ensures forall e any :: e in elemsSeq ==> e in elemsSet +pure func toSet(ghost elemsSeq seq[any]) (ghost elemsSet seq[any]) + +/* +ghost +ensures toSet(seq1) === toSet(seq2) ==> res +ensures toSet(seq1) !== toSet(seq2) ==> !res +pure func haveSameElements(ghost seq1 seq[any], ghost seq2 seq[any]) (res bool){ + return toSet(seq1) === toSet(seq2) +} +*/ + +ghost +requires x.Mem(elemsSeq) +ensures forall e any :: e in elemsSeq ==> e in elemsSet +pure func (x IntSlice) toSet(ghost elemsSeq seq[any]) (ghost elemsSet seq[any]) + + + From f07353fd77f128c1dbb20d0fb34532d981e81f28 Mon Sep 17 00:00:00 2001 From: adjenny Date: Tue, 10 Jan 2023 01:44:22 +0100 Subject: [PATCH 08/20] introduced 'haveSameElements(..)' with assumption on implementation level in IntSlice.Swap --- src/sort/sort_partial.gobra | 43 ++++++++++++++++++++++++++----------- 1 file changed, 30 insertions(+), 13 deletions(-) diff --git a/src/sort/sort_partial.gobra b/src/sort/sort_partial.gobra index 1b783b84976..649a582e659 100644 --- a/src/sort/sort_partial.gobra +++ b/src/sort/sort_partial.gobra @@ -60,6 +60,7 @@ type Interface interface { ensures elems[i] === swapped_elems[j] ensures elems[j] === swapped_elems[i] ensures forall x int :: (0 <= x && x < len(elems) && x != i && x != j) ==> (elems[x] === swapped_elems[x]) + ensures haveSameElements(elems, swapped_elems) ensures old(less_spec(i, j, elems)) ==> !less_spec(i, j, swapped_elems) //# We make the effect of the Swap operation on the Less relation explicit. Swap(i, j int, ghost elems seq[any]) (ghost swapped_elems seq[any]) } @@ -172,12 +173,14 @@ ensures forall idx int :: (0 <= idx && idx < len(elems) && idx != i && idx != j ensures elems[i] === swapped_elems[j] ensures elems[j] === swapped_elems[i] ensures forall idx int :: (0 <= idx && idx < len(elems) && idx != i && idx != j) ==> (elems[idx] === swapped_elems[idx]) +ensures haveSameElements(elems, swapped_elems) ensures old(x.less_spec(i, j, elems)) ==> !x.less_spec(i, j, swapped_elems) func (x IntSlice) Swap(i, j int, ghost elems seq[any]) (ghost swapped_elems seq[any]) { unfold x.Mem(elems) x[i], x[j] = x[j], x[i] swapped_elems = toSeq(x) fold x.Mem(swapped_elems) + assume haveSameElements(elems, swapped_elems) //# We believe this to be true. I was not able to establish this as a fact and I was not able to map directly from IntSlice to mset[any]. } //# implementation proof @@ -192,14 +195,14 @@ requires data != nil requires 0 <= a && a < len(elems) requires a <= b && b <= len(elems) //# the element at position b does not get sorted ensures data.Mem(sorted_elems) -ensures len(sorted_elems) == len(elems) +ensures haveSameElements(elems, sorted_elems) ensures a == b ==> isPartiallySorted(data, a, a, sorted_elems) //ensures isPartiallySorted(data, a, b - 1, sorted_elems) func insertionSort(data Interface, a, b int, ghost elems seq[any]) (ghost sorted_elems seq[any]) { sorted_elems = elems assert data.Mem(sorted_elems) - invariant len(sorted_elems) == len(elems) + invariant haveSameElements(elems, sorted_elems) invariant a < i invariant a < b ==> i <= b invariant data.Mem(sorted_elems) @@ -208,7 +211,7 @@ func insertionSort(data Interface, a, b int, ghost elems seq[any]) (ghost sorted //invariant isPartiallySorted(data, a, i - 1, sorted_elems) decreases b-i for i := a + 1; i < b; i++ { //# for any kind of sorting to happen b has to be at least a+2, does this mean if called with b=a+1 that this will not be sorted? Answer: YES, should we enforce that in the precondition? - invariant len(sorted_elems) == len(elems) + invariant haveSameElements(elems, sorted_elems) invariant i < b invariant a <= j && j <= i invariant a < j ==> 0 <= j - 1 @@ -230,7 +233,6 @@ func insertionSort(data Interface, a, b int, ghost elems seq[any]) (ghost sorted } } } - } // ######### END FROM zsortinterface ############## @@ -238,22 +240,37 @@ func insertionSort(data Interface, a, b int, ghost elems seq[any]) (ghost sorted //# helper ghost -ensures forall e any :: e in elemsSeq ==> e in elemsSet -pure func toSet(ghost elemsSeq seq[any]) (ghost elemsSet seq[any]) +ensures forall e any :: e in elemsSeq ==> e in elemsMultiSet +ensures len(elemsSeq) == len(elemsMultiSet) +pure func toMultiSet(ghost elemsSeq seq[any]) (ghost elemsMultiSet mset[any]) + + -/* ghost -ensures toSet(seq1) === toSet(seq2) ==> res -ensures toSet(seq1) !== toSet(seq2) ==> !res +ensures toMultiSet(seq1) === toMultiSet(seq2) ==> res +ensures toMultiSet(seq1) !== toMultiSet(seq2) ==> !res +ensures res ==> len(seq1) == len(seq2) pure func haveSameElements(ghost seq1 seq[any], ghost seq2 seq[any]) (res bool){ - return toSet(seq1) === toSet(seq2) + return toMultiSet(seq1) === toMultiSet(seq2) } + + + +/* +ensures forall e int :: e in s1 ==> e in s2 //# this causes gobra to crash, it works with mset[int] as the return type +pure func test(ghost s1 mset[int]) (ghost s2 mset[any]) */ + +/* ghost -requires x.Mem(elemsSeq) -ensures forall e any :: e in elemsSeq ==> e in elemsSet -pure func (x IntSlice) toSet(ghost elemsSeq seq[any]) (ghost elemsSet seq[any]) +requires forall j int :: 0 <= j && j < len(s) ==> acc(&s[j], _) +ensures len(res) == len(s) +ensures forall j int :: 0 <= j && j < len(s) ==> s[j] in res +pure func toMultiSet(s []int) (res mset[any]) { + return (len(s) == 0 ? mset[any]{} : + toSeqX(s[:len(s) - 1]) union mset[any]{s[len(s) - 1]}) +}*/ From 54446dca2176b4b1e191f3b8887cb17ab2181506 Mon Sep 17 00:00:00 2001 From: adjenny Date: Thu, 12 Jan 2023 03:58:07 +0100 Subject: [PATCH 09/20] updated comments --- src/sort/sort_partial.gobra | 46 +++++++++++++++++++------------------ 1 file changed, 24 insertions(+), 22 deletions(-) diff --git a/src/sort/sort_partial.gobra b/src/sort/sort_partial.gobra index 649a582e659..6dc3a6e98af 100644 --- a/src/sort/sort_partial.gobra +++ b/src/sort/sort_partial.gobra @@ -10,14 +10,16 @@ package sort //import "math/bits" //# Had to comment this out, otherwise verification progress does not go above 3% +ghost const ReadPerm perm = 1/2 + // An implementation of Interface can be sorted by the routines in this package. // The methods refer to elements of the underlying collection by integer index. type Interface interface { pred Mem(ghost s seq[any]) // Len is the number of elements in the collection. - requires acc(Mem(elems), 1/2) - ensures acc(Mem(elems), 1/2) + requires acc(Mem(elems), ReadPerm) + ensures acc(Mem(elems), ReadPerm) ensures res == len(elems) ensures res >= 0 Len(ghost elems seq[any]) (res int) @@ -42,10 +44,10 @@ type Interface interface { // Note that floating-point comparison (the < operator on float32 or float64 values) // is not a transitive ordering when not-a-number (NaN) values are involved. // See Float64Slice.Less for a correct implementation for floating-point values. - requires acc(Mem(elems), 1/2) + requires acc(Mem(elems), ReadPerm) requires 0 <= i && i < len(elems) requires 0 <= j && j < len(elems) - ensures acc(Mem(elems), 1/2) + ensures acc(Mem(elems), ReadPerm) ensures res == less_spec(i, j, elems) Less(i, j int, ghost elems seq[any]) (res bool) @@ -66,7 +68,7 @@ type Interface interface { } -//# LOTS IN BETWEEN..... +//# PLACEHOLDER: Here would be more code from the original sort.go file. ghost requires data != nil @@ -76,7 +78,8 @@ requires start <= end && end < len(elems) ensures end - start == 0 ==> res == true ensures (end - start > 0 && !data.less_spec(end, end - 1, elems)) ==> res == isPartiallySorted(data, start, end - 1, elems) ensures (end - start > 0 && data.less_spec(end, end - 1, elems)) ==> !res -//ensures res ==> (forall idx int :: ((start < idx && idx <= end) ==> !data.less_spec(idx, idx - 1, elems))) //# Would like to be able to infer that +//ensures res ==> (forall idx int :: ((start < idx && idx <= end) ==> !data.less_spec(idx, idx - 1, elems))) +//# The below line verifies and should just be an unrolled version of the above line in cases were start+2 < end. However, the above line does not verify. //ensures (res && start+2 < end) ==> !data.less_spec(end, end - 1, elems) && !data.less_spec(end-1, end - 2, elems) && !data.less_spec(end-2, end-3, elems) pure func isPartiallySorted(data Interface, start, end int, ghost elems seq[any]) (res bool) { @@ -132,9 +135,9 @@ pred (x IntSlice) Mem(ghost s seq[any]){ forall j int :: {x[j]} {s[j]} 0 <= j && j < len(s) ==> x[j] == s[j] } -requires acc(x.Mem(elems), 1/2) -ensures acc(x.Mem(elems), 1/2) -ensures unfolding acc(x.Mem(elems), 1/2) in res == len(elems) +requires acc(x.Mem(elems), ReadPerm) +ensures acc(x.Mem(elems), ReadPerm) +ensures unfolding acc(x.Mem(elems), ReadPerm) in res == len(elems) ensures res >= 0 func (x IntSlice) Len(ghost elems seq[any]) (res int) { return len(x) @@ -149,25 +152,23 @@ pure func (x IntSlice) less_spec(i, j int, ghost elems seq[any]) (res bool){ } -requires acc(x.Mem(elems), 1/2) +requires acc(x.Mem(elems), ReadPerm) requires 0 <= i && i < len(elems) requires 0 <= j && j < len(elems) -ensures acc(x.Mem(elems), 1/2) +ensures acc(x.Mem(elems), ReadPerm) ensures res == x.less_spec(i, j, elems) func (x IntSlice) Less(i, j int, ghost elems seq[any]) (res bool) { - return unfolding acc(x.Mem(elems), 1/2) in x[i] < x[j] + return unfolding acc(x.Mem(elems), ReadPerm) in x[i] < x[j] } requires x.Mem(elems) requires 0 <= i && i < len(elems) requires 0 <= j && j < len(elems) ensures x.Mem(swapped_elems) -ensures len(elems) == len(swapped_elems) //# somehow this does not suffice to infer i and j are in range [0, len(swapped_elems)-1] -ensures 0 <= i && i < len(elems) && i < len(swapped_elems) //# possibly make Len() pure and use that -ensures 0 <= j && j < len(elems) && j < len(swapped_elems) //# possibly make Len() pure and use that +ensures len(elems) == len(swapped_elems) //# Somehow this does not suffice to infer i and j are in range [0, len(swapped_elems)-1] and it needs to be stated explicitly below. +ensures 0 <= i && i < len(elems) && i < len(swapped_elems) +ensures 0 <= j && j < len(elems) && j < len(swapped_elems) //# This line is required.. -//ensures old(unfolding x.Mem(elems) in x[i]) == (unfolding x.Mem(swapped_elems) in x[j]) -//ensures old(unfolding x.Mem(elems) in x[j]) == (unfolding x.Mem(swapped_elems) in x[i]) ensures forall idx int :: (0 <= idx && idx < len(elems) && idx != i && idx != j) ==> (old(unfolding x.Mem(elems) in x[idx]) == (unfolding x.Mem(swapped_elems) in x[idx])) //# ..for these 3 corresponding lines to work. ensures elems[i] === swapped_elems[j] @@ -188,7 +189,7 @@ func (x IntSlice) Swap(i, j int, ghost elems seq[any]) (ghost swapped_elems seq[ -// ######### BEGIN FROM zsortinterface ############## +// ######### BEGIN FROM zsortinterface.go ############## // insertionSort sorts data[a:b] using insertion sort. requires data.Mem(elems) requires data != nil @@ -221,7 +222,7 @@ func insertionSort(data Interface, a, b int, ghost elems seq[any]) (ghost sorted //invariant isPartiallySorted(data, a, XXX, sorted_elems) //invariant isPartiallySorted(data, YYY, i, sorted_elems) decreases j-a - for j := i; j > a /*&& data.Less(j, j - 1, elems)*/; j-- { + for j := i; j > a /*&& data.Less(j, j - 1, elems)*/; j-- { //# The second conjunct in the loop condition was commented out. See comment below. assert 0 <= j - 1 assert i < b assert i < len(sorted_elems) @@ -234,10 +235,10 @@ func insertionSort(data Interface, a, b int, ghost elems seq[any]) (ghost sorted } } } -// ######### END FROM zsortinterface ############## +// ######### END FROM zsortinterface.go ############## -//# helper +//# helper: ghost ensures forall e any :: e in elemsSeq ==> e in elemsMultiSet @@ -270,7 +271,8 @@ ensures forall j int :: 0 <= j && j < len(s) ==> s[j] in res pure func toMultiSet(s []int) (res mset[any]) { return (len(s) == 0 ? mset[any]{} : toSeqX(s[:len(s) - 1]) union mset[any]{s[len(s) - 1]}) -}*/ +} +*/ From 5b4b59cf3ab051ee4bfa635220a677334878cfea Mon Sep 17 00:00:00 2001 From: adjenny Date: Sat, 21 Jan 2023 01:55:41 +0100 Subject: [PATCH 10/20] inserted more triggers --- src/sort/sort_partial.gobra | 41 ++++++++++++++++++++++--------------- 1 file changed, 24 insertions(+), 17 deletions(-) diff --git a/src/sort/sort_partial.gobra b/src/sort/sort_partial.gobra index 6dc3a6e98af..b7e3b1918cf 100644 --- a/src/sort/sort_partial.gobra +++ b/src/sort/sort_partial.gobra @@ -8,7 +8,7 @@ // +gobra package sort -//import "math/bits" //# Had to comment this out, otherwise verification progress does not go above 3% +//# import "math/bits" //# Had to comment this out for verification to work. ghost const ReadPerm perm = 1/2 @@ -28,7 +28,7 @@ type Interface interface { // must sort before the element with index j. // // If both Less(i, j) and Less(j, i) are false, - // then the elements at index i and j are considered equal. //# What does "considered equal mean"? We cannot use == in the spec since equality is relative to the defined order + // then the elements at index i and j are considered equal. // Sort may place equal elements in any order in the final result, // while Stable preserves the original input order of equal elements. // @@ -38,7 +38,7 @@ type Interface interface { requires Mem(elems) requires 0 <= i && i < len(elems) requires 0 <= j && j < len(elems) - ensures forall a, b, c int :: (0 <= a && a < len(elems) && 0 <= b && b < len(elems) && 0 <= c && c < len(elems) && less_spec(a,b,elems) && less_spec(b,c,elems)) ==> less_spec(a,c,elems) + ensures forall a, b, c int :: {less_spec(a, b, elems), less_spec(b, c, elems)} (0 <= a && a < len(elems) && 0 <= b && b < len(elems) && 0 <= c && c < len(elems) && less_spec(a, b, elems) && less_spec(b, c, elems)) ==> less_spec(a, c, elems) pure less_spec(i, j int, ghost elems seq[any]) (res bool) // // Note that floating-point comparison (the < operator on float32 or float64 values) @@ -61,7 +61,7 @@ type Interface interface { ensures 0 <= j && j < len(elems) && j < len(swapped_elems) //# possibly make Len() pure and use that ensures elems[i] === swapped_elems[j] ensures elems[j] === swapped_elems[i] - ensures forall x int :: (0 <= x && x < len(elems) && x != i && x != j) ==> (elems[x] === swapped_elems[x]) + ensures forall x int :: (0 <= x && x < len(elems) && x != i && x != j) ==> (elems[x] === swapped_elems[x]) //# find triggers ensures haveSameElements(elems, swapped_elems) ensures old(less_spec(i, j, elems)) ==> !less_spec(i, j, swapped_elems) //# We make the effect of the Swap operation on the Less relation explicit. Swap(i, j int, ghost elems seq[any]) (ghost swapped_elems seq[any]) @@ -78,7 +78,7 @@ requires start <= end && end < len(elems) ensures end - start == 0 ==> res == true ensures (end - start > 0 && !data.less_spec(end, end - 1, elems)) ==> res == isPartiallySorted(data, start, end - 1, elems) ensures (end - start > 0 && data.less_spec(end, end - 1, elems)) ==> !res -//ensures res ==> (forall idx int :: ((start < idx && idx <= end) ==> !data.less_spec(idx, idx - 1, elems))) +//ensures res ==> (forall idx int :: ((start < idx && idx <= end) ==> !data.less_spec(idx, idx - 1, elems))) //# find triggers //# The below line verifies and should just be an unrolled version of the above line in cases were start+2 < end. However, the above line does not verify. //ensures (res && start+2 < end) ==> !data.less_spec(end, end - 1, elems) && !data.less_spec(end-1, end - 2, elems) && !data.less_spec(end-2, end-3, elems) pure @@ -89,8 +89,8 @@ func isPartiallySorted(data Interface, start, end int, ghost elems seq[any]) (re // IsSorted reports whether data is sorted. preserves data.Mem(elems) requires data != nil -ensures res ==> forall idx int :: ((0 < idx && idx < len(elems)) ==> (!data.less_spec(idx, idx - 1, elems))) -ensures !res ==> !(forall idx int :: ((0 < idx && idx < len(elems)) ==> (!data.less_spec(idx, idx - 1, elems)))) +ensures res ==> forall idx int :: {data.less_spec(idx, idx - 1, elems)} ((0 < idx && idx < len(elems)) ==> (!data.less_spec(idx, idx - 1, elems))) +ensures !res ==> !(forall idx int :: {data.less_spec(idx, idx - 1, elems)} ((0 < idx && idx < len(elems)) ==> (!data.less_spec(idx, idx - 1, elems)))) func IsSorted(data Interface, ghost elems seq[any]) (res bool) { n := data.Len(elems) @@ -100,7 +100,7 @@ func IsSorted(data Interface, ghost elems seq[any]) (res bool) { invariant i < n invariant len(elems) > 0 ==> 0 <= i //# if n==0 then i==-1 after initialization invariant data.Mem(elems) - invariant len(elems) != 0 ==> (forall idx int :: ((i < idx && idx < len(elems)) ==> !data.less_spec(idx, idx - 1, elems))) + invariant len(elems) != 0 ==> (forall idx int :: {data.less_spec(idx, idx - 1, elems)} ((i < idx && idx < len(elems)) ==> !data.less_spec(idx, idx - 1, elems))) //invariant len(elems) != 0 ==> isPartiallySorted(data, i, n - 1, elems) //# Would like for this to hold here decreases i for i := n - 1; i > 0; i-- { @@ -120,7 +120,7 @@ type IntSlice []int //# Adapted from Gobra tutorial ghost -requires forall j int :: 0 <= j && j < len(s) ==> acc(&s[j], _) +requires forall j int :: 0 <= j && j < len(s) ==> acc(&s[j], _) //# find triggers ensures len(res) == len(s) ensures forall j int :: {s[j]} {res[j]} 0 <= j && j < len(s) ==> s[j] == res[j] pure func toSeq(s []int) (res seq[any]) { @@ -130,7 +130,7 @@ pure func toSeq(s []int) (res seq[any]) { pred (x IntSlice) Mem(ghost s seq[any]){ len(x) == len(s) && //# If this is not the first line in the predicate, then we cannot verify e.g. the last postcondition in Len() - forall j int :: 0 <= j && j < len(x) ==> acc(&x[j]) && + forall j int :: 0 <= j && j < len(x) ==> acc(&x[j]) && //# find triggers s == toSeq(x) && forall j int :: {x[j]} {s[j]} 0 <= j && j < len(s) ==> x[j] == s[j] } @@ -146,7 +146,7 @@ func (x IntSlice) Len(ghost elems seq[any]) (res int) { requires x.Mem(elems) requires 0 <= i && i < len(elems) requires 0 <= j && j < len(elems) -ensures forall a, b, c int :: (0 <= a && a < len(elems) && 0 <= b && b < len(elems) && 0 <= c && c < len(elems) && x.less_spec(a,b,elems) && x.less_spec(b,c,elems)) ==> x.less_spec(a,c,elems) +ensures forall a, b, c int :: {x.less_spec(a, b, elems), x.less_spec(b, c, elems)} (0 <= a && a < len(elems) && 0 <= b && b < len(elems) && 0 <= c && c < len(elems) && x.less_spec(a, b, elems) && x.less_spec(b, c, elems)) ==> x.less_spec(a, c, elems) pure func (x IntSlice) less_spec(i, j int, ghost elems seq[any]) (res bool){ return unfolding x.Mem(elems) in x[i] < x[j] } @@ -161,6 +161,7 @@ func (x IntSlice) Less(i, j int, ghost elems seq[any]) (res bool) { return unfolding acc(x.Mem(elems), ReadPerm) in x[i] < x[j] } + requires x.Mem(elems) requires 0 <= i && i < len(elems) requires 0 <= j && j < len(elems) @@ -169,11 +170,11 @@ ensures len(elems) == len(swapped_elems) //# Somehow this does not suffice to i ensures 0 <= i && i < len(elems) && i < len(swapped_elems) ensures 0 <= j && j < len(elems) && j < len(swapped_elems) //# This line is required.. -ensures forall idx int :: (0 <= idx && idx < len(elems) && idx != i && idx != j) ==> (old(unfolding x.Mem(elems) in x[idx]) == (unfolding x.Mem(swapped_elems) in x[idx])) +ensures forall idx int :: (0 <= idx && idx < len(elems) && idx != i && idx != j) ==> (old(unfolding x.Mem(elems) in x[idx]) == (unfolding x.Mem(swapped_elems) in x[idx])) //# find triggers //# ..for these 3 corresponding lines to work. ensures elems[i] === swapped_elems[j] ensures elems[j] === swapped_elems[i] -ensures forall idx int :: (0 <= idx && idx < len(elems) && idx != i && idx != j) ==> (elems[idx] === swapped_elems[idx]) +ensures forall idx int :: (0 <= idx && idx < len(elems) && idx != i && idx != j) ==> (elems[idx] === swapped_elems[idx]) //# find triggers ensures haveSameElements(elems, swapped_elems) ensures old(x.less_spec(i, j, elems)) ==> !x.less_spec(i, j, swapped_elems) func (x IntSlice) Swap(i, j int, ghost elems seq[any]) (ghost swapped_elems seq[any]) { @@ -182,10 +183,16 @@ func (x IntSlice) Swap(i, j int, ghost elems seq[any]) (ghost swapped_elems seq[ swapped_elems = toSeq(x) fold x.Mem(swapped_elems) assume haveSameElements(elems, swapped_elems) //# We believe this to be true. I was not able to establish this as a fact and I was not able to map directly from IntSlice to mset[any]. + + //# These four following assumptions should not be required, it works without them in GobraIDE stable version as of Jan. 20th 2023. + assume forall idx int :: (0 <= idx && idx < len(elems) && idx != i && idx != j) ==> (old(unfolding x.Mem(elems) in x[idx]) == (unfolding x.Mem(swapped_elems) in x[idx])) + assume elems[i] === swapped_elems[j] + assume elems[j] === swapped_elems[i] + assume forall idx int :: (0 <= idx && idx < len(elems) && idx != i && idx != j) ==> (elems[idx] === swapped_elems[idx]) } //# implementation proof -(IntSlice) implements Interface{ } +//(IntSlice) implements Interface{ } @@ -208,7 +215,7 @@ func insertionSort(data Interface, a, b int, ghost elems seq[any]) (ghost sorted invariant a < b ==> i <= b invariant data.Mem(sorted_elems) //# invariant prefix [a:i] is always sorted - //invariant forall idx int :: (a < idx && idx < i && i < b) ==> !data.less_spec(idx, idx - 1, sorted_elems) + //invariant forall idx int :: (a < idx && idx < i && i < b) ==> !data.less_spec(idx, idx - 1, sorted_elems) //# find triggers //invariant isPartiallySorted(data, a, i - 1, sorted_elems) decreases b-i for i := a + 1; i < b; i++ { //# for any kind of sorting to happen b has to be at least a+2, does this mean if called with b=a+1 that this will not be sorted? Answer: YES, should we enforce that in the precondition? @@ -218,7 +225,7 @@ func insertionSort(data Interface, a, b int, ghost elems seq[any]) (ghost sorted invariant a < j ==> 0 <= j - 1 invariant data.Mem(sorted_elems) //# invariant prefix [a:j-2] is always sorted and [j:i] is always sorted - //invariant forall idx int :: (j < idx && idx < i) ==> !data.less_spec(idx, idx - 1, sorted_elems) + //invariant forall idx int :: (j < idx && idx < i) ==> !data.less_spec(idx, idx - 1, sorted_elems) //# find triggers //invariant isPartiallySorted(data, a, XXX, sorted_elems) //invariant isPartiallySorted(data, YYY, i, sorted_elems) decreases j-a @@ -241,7 +248,7 @@ func insertionSort(data Interface, a, b int, ghost elems seq[any]) (ghost sorted //# helper: ghost -ensures forall e any :: e in elemsSeq ==> e in elemsMultiSet +ensures forall e any :: e in elemsSeq ==> e in elemsMultiSet //# find triggers ensures len(elemsSeq) == len(elemsMultiSet) pure func toMultiSet(ghost elemsSeq seq[any]) (ghost elemsMultiSet mset[any]) From fb95db704c15c82a866baad1e0271aa37d54d9f4 Mon Sep 17 00:00:00 2001 From: adjenny Date: Sat, 21 Jan 2023 02:25:53 +0100 Subject: [PATCH 11/20] added 'decreases' clause where possible --- src/sort/sort_partial.gobra | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/src/sort/sort_partial.gobra b/src/sort/sort_partial.gobra index b7e3b1918cf..54c8575c260 100644 --- a/src/sort/sort_partial.gobra +++ b/src/sort/sort_partial.gobra @@ -22,6 +22,7 @@ type Interface interface { ensures acc(Mem(elems), ReadPerm) ensures res == len(elems) ensures res >= 0 + decreases Len(ghost elems seq[any]) (res int) // Less reports whether the element with index i @@ -49,6 +50,7 @@ type Interface interface { requires 0 <= j && j < len(elems) ensures acc(Mem(elems), ReadPerm) ensures res == less_spec(i, j, elems) + decreases Less(i, j int, ghost elems seq[any]) (res bool) // Swap swaps the elements with indexes i and j. @@ -64,6 +66,7 @@ type Interface interface { ensures forall x int :: (0 <= x && x < len(elems) && x != i && x != j) ==> (elems[x] === swapped_elems[x]) //# find triggers ensures haveSameElements(elems, swapped_elems) ensures old(less_spec(i, j, elems)) ==> !less_spec(i, j, swapped_elems) //# We make the effect of the Swap operation on the Less relation explicit. + decreases Swap(i, j int, ghost elems seq[any]) (ghost swapped_elems seq[any]) } @@ -91,6 +94,7 @@ preserves data.Mem(elems) requires data != nil ensures res ==> forall idx int :: {data.less_spec(idx, idx - 1, elems)} ((0 < idx && idx < len(elems)) ==> (!data.less_spec(idx, idx - 1, elems))) ensures !res ==> !(forall idx int :: {data.less_spec(idx, idx - 1, elems)} ((0 < idx && idx < len(elems)) ==> (!data.less_spec(idx, idx - 1, elems)))) +decreases func IsSorted(data Interface, ghost elems seq[any]) (res bool) { n := data.Len(elems) @@ -123,6 +127,7 @@ ghost requires forall j int :: 0 <= j && j < len(s) ==> acc(&s[j], _) //# find triggers ensures len(res) == len(s) ensures forall j int :: {s[j]} {res[j]} 0 <= j && j < len(s) ==> s[j] == res[j] +decreases len(s) pure func toSeq(s []int) (res seq[any]) { return (len(s) == 0 ? seq[any]{} : toSeq(s[:len(s) - 1]) ++ seq[any]{s[len(s) - 1]}) @@ -139,6 +144,7 @@ requires acc(x.Mem(elems), ReadPerm) ensures acc(x.Mem(elems), ReadPerm) ensures unfolding acc(x.Mem(elems), ReadPerm) in res == len(elems) ensures res >= 0 +decreases func (x IntSlice) Len(ghost elems seq[any]) (res int) { return len(x) } @@ -157,6 +163,7 @@ requires 0 <= i && i < len(elems) requires 0 <= j && j < len(elems) ensures acc(x.Mem(elems), ReadPerm) ensures res == x.less_spec(i, j, elems) +decreases func (x IntSlice) Less(i, j int, ghost elems seq[any]) (res bool) { return unfolding acc(x.Mem(elems), ReadPerm) in x[i] < x[j] } @@ -177,6 +184,7 @@ ensures elems[j] === swapped_elems[i] ensures forall idx int :: (0 <= idx && idx < len(elems) && idx != i && idx != j) ==> (elems[idx] === swapped_elems[idx]) //# find triggers ensures haveSameElements(elems, swapped_elems) ensures old(x.less_spec(i, j, elems)) ==> !x.less_spec(i, j, swapped_elems) +decreases func (x IntSlice) Swap(i, j int, ghost elems seq[any]) (ghost swapped_elems seq[any]) { unfold x.Mem(elems) x[i], x[j] = x[j], x[i] @@ -192,7 +200,7 @@ func (x IntSlice) Swap(i, j int, ghost elems seq[any]) (ghost swapped_elems seq[ } //# implementation proof -//(IntSlice) implements Interface{ } +(IntSlice) implements Interface{ } @@ -206,6 +214,7 @@ ensures data.Mem(sorted_elems) ensures haveSameElements(elems, sorted_elems) ensures a == b ==> isPartiallySorted(data, a, a, sorted_elems) //ensures isPartiallySorted(data, a, b - 1, sorted_elems) +decreases func insertionSort(data Interface, a, b int, ghost elems seq[any]) (ghost sorted_elems seq[any]) { sorted_elems = elems assert data.Mem(sorted_elems) From 0ba6b672ee6d6205d630b5bfb914a1f3152b5556 Mon Sep 17 00:00:00 2001 From: adjenny Date: Mon, 23 Jan 2023 18:47:43 +0100 Subject: [PATCH 12/20] changes of meeting jan 23rd --- src/sort/sort_partial.gobra | 26 ++++++++++---------------- 1 file changed, 10 insertions(+), 16 deletions(-) diff --git a/src/sort/sort_partial.gobra b/src/sort/sort_partial.gobra index 54c8575c260..8a4d7f637d6 100644 --- a/src/sort/sort_partial.gobra +++ b/src/sort/sort_partial.gobra @@ -126,7 +126,7 @@ type IntSlice []int ghost requires forall j int :: 0 <= j && j < len(s) ==> acc(&s[j], _) //# find triggers ensures len(res) == len(s) -ensures forall j int :: {s[j]} {res[j]} 0 <= j && j < len(s) ==> s[j] == res[j] +ensures forall j int :: {&s[j]} {res[j]} 0 <= j && j < len(s) ==> s[j] == res[j] decreases len(s) pure func toSeq(s []int) (res seq[any]) { return (len(s) == 0 ? seq[any]{} : @@ -137,7 +137,7 @@ pred (x IntSlice) Mem(ghost s seq[any]){ len(x) == len(s) && //# If this is not the first line in the predicate, then we cannot verify e.g. the last postcondition in Len() forall j int :: 0 <= j && j < len(x) ==> acc(&x[j]) && //# find triggers s == toSeq(x) && - forall j int :: {x[j]} {s[j]} 0 <= j && j < len(s) ==> x[j] == s[j] + forall j int :: {&x[j]} {s[j]} 0 <= j && j < len(s) ==> x[j] == s[j] } requires acc(x.Mem(elems), ReadPerm) @@ -176,9 +176,6 @@ ensures x.Mem(swapped_elems) ensures len(elems) == len(swapped_elems) //# Somehow this does not suffice to infer i and j are in range [0, len(swapped_elems)-1] and it needs to be stated explicitly below. ensures 0 <= i && i < len(elems) && i < len(swapped_elems) ensures 0 <= j && j < len(elems) && j < len(swapped_elems) -//# This line is required.. -ensures forall idx int :: (0 <= idx && idx < len(elems) && idx != i && idx != j) ==> (old(unfolding x.Mem(elems) in x[idx]) == (unfolding x.Mem(swapped_elems) in x[idx])) //# find triggers -//# ..for these 3 corresponding lines to work. ensures elems[i] === swapped_elems[j] ensures elems[j] === swapped_elems[i] ensures forall idx int :: (0 <= idx && idx < len(elems) && idx != i && idx != j) ==> (elems[idx] === swapped_elems[idx]) //# find triggers @@ -190,13 +187,9 @@ func (x IntSlice) Swap(i, j int, ghost elems seq[any]) (ghost swapped_elems seq[ x[i], x[j] = x[j], x[i] swapped_elems = toSeq(x) fold x.Mem(swapped_elems) - assume haveSameElements(elems, swapped_elems) //# We believe this to be true. I was not able to establish this as a fact and I was not able to map directly from IntSlice to mset[any]. - - //# These four following assumptions should not be required, it works without them in GobraIDE stable version as of Jan. 20th 2023. - assume forall idx int :: (0 <= idx && idx < len(elems) && idx != i && idx != j) ==> (old(unfolding x.Mem(elems) in x[idx]) == (unfolding x.Mem(swapped_elems) in x[idx])) - assume elems[i] === swapped_elems[j] - assume elems[j] === swapped_elems[i] - assume forall idx int :: (0 <= idx && idx < len(elems) && idx != i && idx != j) ==> (elems[idx] === swapped_elems[idx]) + assume forall idx int :: (0 <= idx && idx < len(elems)) ==> elems[idx] == old(unfolding x.Mem(elems) in x[idx]) //# Cannot be asserted in GobraCLI but works in GobraIDE as of Jan 23rd 2023 + assert forall idx int :: (0 <= idx && idx < len(swapped_elems)) ==> swapped_elems[idx] == unfolding x.Mem(swapped_elems) in x[idx] + assume haveSameElements(elems, swapped_elems) //# We believe this to be true. } //# implementation proof @@ -212,7 +205,7 @@ requires 0 <= a && a < len(elems) requires a <= b && b <= len(elems) //# the element at position b does not get sorted ensures data.Mem(sorted_elems) ensures haveSameElements(elems, sorted_elems) -ensures a == b ==> isPartiallySorted(data, a, a, sorted_elems) +//ensures a == b ==> isPartiallySorted(data, a, a, sorted_elems) //ensures isPartiallySorted(data, a, b - 1, sorted_elems) decreases func insertionSort(data Interface, a, b int, ghost elems seq[any]) (ghost sorted_elems seq[any]) { @@ -224,7 +217,7 @@ func insertionSort(data Interface, a, b int, ghost elems seq[any]) (ghost sorted invariant a < b ==> i <= b invariant data.Mem(sorted_elems) //# invariant prefix [a:i] is always sorted - //invariant forall idx int :: (a < idx && idx < i && i < b) ==> !data.less_spec(idx, idx - 1, sorted_elems) //# find triggers + //invariant forall idx int :: (a < idx && idx < i) ==> !data.less_spec(idx, idx - 1, sorted_elems) //# find triggers //invariant isPartiallySorted(data, a, i - 1, sorted_elems) decreases b-i for i := a + 1; i < b; i++ { //# for any kind of sorting to happen b has to be at least a+2, does this mean if called with b=a+1 that this will not be sorted? Answer: YES, should we enforce that in the precondition? @@ -233,8 +226,9 @@ func insertionSort(data Interface, a, b int, ghost elems seq[any]) (ghost sorted invariant a <= j && j <= i invariant a < j ==> 0 <= j - 1 invariant data.Mem(sorted_elems) - //# invariant prefix [a:j-2] is always sorted and [j:i] is always sorted - //invariant forall idx int :: (j < idx && idx < i) ==> !data.less_spec(idx, idx - 1, sorted_elems) //# find triggers + //# invariant prefix [a:j-1] is always sorted and [j:i] is always sorted + //invariant (j <= a || !data.less_spec(j, j - 1, sorted_elems)) ==> (forall idx int :: (a < idx && idx < i) ==> !data.less_spec(idx, idx - 1, sorted_elems)) + //invariant (j > a && data.less_spec(j, j - 1, sorted_elems)) ==> (forall idx int :: (a < idx && idx < i && idx != j) ==> !data.less_spec(idx, idx - 1, sorted_elems)) //# find triggers //invariant isPartiallySorted(data, a, XXX, sorted_elems) //invariant isPartiallySorted(data, YYY, i, sorted_elems) decreases j-a From a8bd81120692415d191f7dae923ffe2898087741 Mon Sep 17 00:00:00 2001 From: adjenny Date: Mon, 23 Jan 2023 18:53:31 +0100 Subject: [PATCH 13/20] updated 'Swap' spec --- src/sort/sort_partial.gobra | 18 ++++++++---------- 1 file changed, 8 insertions(+), 10 deletions(-) diff --git a/src/sort/sort_partial.gobra b/src/sort/sort_partial.gobra index 8a4d7f637d6..c0deb6934be 100644 --- a/src/sort/sort_partial.gobra +++ b/src/sort/sort_partial.gobra @@ -55,16 +55,15 @@ type Interface interface { // Swap swaps the elements with indexes i and j. requires Mem(elems) - requires 0 <= i && i < len(elems) //# possibly make Len() pure and use that - requires 0 <= j && j < len(elems) //# possibly make Len() pure and use that + requires 0 <= i && i < len(elems) + requires 0 <= j && j < len(elems) ensures Mem(swapped_elems) - ensures len(elems) == len(swapped_elems) //# somehow this does not suffice to infer i and j are in range [0, len(swapped_elems)-1] - ensures 0 <= i && i < len(elems) && i < len(swapped_elems) //# possibly make Len() pure and use that - ensures 0 <= j && j < len(elems) && j < len(swapped_elems) //# possibly make Len() pure and use that + ensures haveSameElements(elems, swapped_elems) + ensures 0 <= i && i < len(elems) + ensures 0 <= j && j < len(elems) ensures elems[i] === swapped_elems[j] ensures elems[j] === swapped_elems[i] ensures forall x int :: (0 <= x && x < len(elems) && x != i && x != j) ==> (elems[x] === swapped_elems[x]) //# find triggers - ensures haveSameElements(elems, swapped_elems) ensures old(less_spec(i, j, elems)) ==> !less_spec(i, j, swapped_elems) //# We make the effect of the Swap operation on the Less relation explicit. decreases Swap(i, j int, ghost elems seq[any]) (ghost swapped_elems seq[any]) @@ -173,13 +172,12 @@ requires x.Mem(elems) requires 0 <= i && i < len(elems) requires 0 <= j && j < len(elems) ensures x.Mem(swapped_elems) -ensures len(elems) == len(swapped_elems) //# Somehow this does not suffice to infer i and j are in range [0, len(swapped_elems)-1] and it needs to be stated explicitly below. -ensures 0 <= i && i < len(elems) && i < len(swapped_elems) -ensures 0 <= j && j < len(elems) && j < len(swapped_elems) +ensures haveSameElements(elems, swapped_elems) +ensures 0 <= i && i < len(elems) +ensures 0 <= j && j < len(elems) ensures elems[i] === swapped_elems[j] ensures elems[j] === swapped_elems[i] ensures forall idx int :: (0 <= idx && idx < len(elems) && idx != i && idx != j) ==> (elems[idx] === swapped_elems[idx]) //# find triggers -ensures haveSameElements(elems, swapped_elems) ensures old(x.less_spec(i, j, elems)) ==> !x.less_spec(i, j, swapped_elems) decreases func (x IntSlice) Swap(i, j int, ghost elems seq[any]) (ghost swapped_elems seq[any]) { From 5064b302164578a21c54dc0e948b783eafc480f3 Mon Sep 17 00:00:00 2001 From: adjenny Date: Mon, 23 Jan 2023 23:55:58 +0100 Subject: [PATCH 14/20] transitive proof and decreases clause --- src/sort/sort_partial.gobra | 49 +++++++++++++++++++++++-------------- 1 file changed, 30 insertions(+), 19 deletions(-) diff --git a/src/sort/sort_partial.gobra b/src/sort/sort_partial.gobra index c0deb6934be..450225b45ef 100644 --- a/src/sort/sort_partial.gobra +++ b/src/sort/sort_partial.gobra @@ -36,10 +36,16 @@ type Interface interface { // Less must describe a transitive ordering: // - if both Less(i, j) and Less(j, k) are true, then Less(i, k) must be true as well. // - if both Less(i, j) and Less(j, k) are false, then Less(i, k) must be false as well. - requires Mem(elems) + ghost + preserves acc(Mem(elems), _) + ensures forall a, b, c int :: {less_spec(a, b, elems), less_spec(b, c, elems)} (0 <= a && a < len(elems) && 0 <= b && b < len(elems) && 0 <= c && c < len(elems) && less_spec(a, b, elems) && less_spec(b, c, elems)) ==> less_spec(a, c, elems) + decreases + LemmaLessIsTransitive(ghost elems seq[any]) + + requires acc(Mem(elems), ReadPerm) requires 0 <= i && i < len(elems) requires 0 <= j && j < len(elems) - ensures forall a, b, c int :: {less_spec(a, b, elems), less_spec(b, c, elems)} (0 <= a && a < len(elems) && 0 <= b && b < len(elems) && 0 <= c && c < len(elems) && less_spec(a, b, elems) && less_spec(b, c, elems)) ==> less_spec(a, c, elems) + decreases pure less_spec(i, j int, ghost elems seq[any]) (res bool) // // Note that floating-point comparison (the < operator on float32 or float64 values) @@ -71,21 +77,20 @@ type Interface interface { //# PLACEHOLDER: Here would be more code from the original sort.go file. - +//# isPartiallySorted is intended to be used in specifications. +//# It reports whether the elemented from indicies 'start' to 'end' (inclusive) are sorted in non-decreasing order according to 'less_spec' ghost requires data != nil requires data.Mem(elems) requires 0 <= start && start < len(elems) requires start <= end && end < len(elems) -ensures end - start == 0 ==> res == true -ensures (end - start > 0 && !data.less_spec(end, end - 1, elems)) ==> res == isPartiallySorted(data, start, end - 1, elems) -ensures (end - start > 0 && data.less_spec(end, end - 1, elems)) ==> !res -//ensures res ==> (forall idx int :: ((start < idx && idx <= end) ==> !data.less_spec(idx, idx - 1, elems))) //# find triggers -//# The below line verifies and should just be an unrolled version of the above line in cases were start+2 < end. However, the above line does not verify. -//ensures (res && start+2 < end) ==> !data.less_spec(end, end - 1, elems) && !data.less_spec(end-1, end - 2, elems) && !data.less_spec(end-2, end-3, elems) +ensures end == start ==> sorted +ensures (end > start && !data.less_spec(end, end - 1, elems)) ==> sorted == isPartiallySorted(data, start, end - 1, elems) +ensures (end > start && data.less_spec(end, end - 1, elems)) ==> !sorted +decreases end - start pure -func isPartiallySorted(data Interface, start, end int, ghost elems seq[any]) (res bool) { - return (end - start == 0) ? true : (!data.less_spec(end, end - 1, elems) ? isPartiallySorted(data, start, end - 1, elems) : false) +func isPartiallySorted(data Interface, start, end int, ghost elems seq[any]) (sorted bool) { + return (end == start) ? true : (!data.less_spec(end, end - 1, elems) ? isPartiallySorted(data, start, end - 1, elems) : false) } // IsSorted reports whether data is sorted. @@ -103,14 +108,13 @@ func IsSorted(data Interface, ghost elems seq[any]) (res bool) { invariant i < n invariant len(elems) > 0 ==> 0 <= i //# if n==0 then i==-1 after initialization invariant data.Mem(elems) - invariant len(elems) != 0 ==> (forall idx int :: {data.less_spec(idx, idx - 1, elems)} ((i < idx && idx < len(elems)) ==> !data.less_spec(idx, idx - 1, elems))) - //invariant len(elems) != 0 ==> isPartiallySorted(data, i, n - 1, elems) //# Would like for this to hold here + invariant len(elems) > 0 ==> (forall idx int :: {data.less_spec(idx, idx - 1, elems)} ((i < idx && idx < len(elems)) ==> !data.less_spec(idx, idx - 1, elems))) decreases i for i := n - 1; i > 0; i-- { if data.Less(i, i - 1, elems) { return false } - //assert isPartiallySorted(data, i, n - 1, elems) + assert !data.less_spec(i, i - 1, elems) } assert res return @@ -148,15 +152,22 @@ func (x IntSlice) Len(ghost elems seq[any]) (res int) { return len(x) } -requires x.Mem(elems) +ghost +preserves acc(x.Mem(elems), _) +ensures forall a, b, c int :: {x.less_spec(a, b, elems), x.less_spec(b, c, elems)} (0 <= a && a < len(elems) && 0 <= b && b < len(elems) && 0 <= c && c < len(elems) && x.less_spec(a, b, elems) && x.less_spec(b, c, elems)) ==> x.less_spec(a, c, elems) +decreases +func (x IntSlice) LemmaLessIsTransitive(ghost elems seq[any]){ + unfold acc(x.Mem(elems), _) +} + +requires acc(x.Mem(elems), ReadPerm) requires 0 <= i && i < len(elems) requires 0 <= j && j < len(elems) -ensures forall a, b, c int :: {x.less_spec(a, b, elems), x.less_spec(b, c, elems)} (0 <= a && a < len(elems) && 0 <= b && b < len(elems) && 0 <= c && c < len(elems) && x.less_spec(a, b, elems) && x.less_spec(b, c, elems)) ==> x.less_spec(a, c, elems) +decreases pure func (x IntSlice) less_spec(i, j int, ghost elems seq[any]) (res bool){ - return unfolding x.Mem(elems) in x[i] < x[j] + return unfolding acc(x.Mem(elems), ReadPerm) in x[i] < x[j] } - requires acc(x.Mem(elems), ReadPerm) requires 0 <= i && i < len(elems) requires 0 <= j && j < len(elems) @@ -177,7 +188,7 @@ ensures 0 <= i && i < len(elems) ensures 0 <= j && j < len(elems) ensures elems[i] === swapped_elems[j] ensures elems[j] === swapped_elems[i] -ensures forall idx int :: (0 <= idx && idx < len(elems) && idx != i && idx != j) ==> (elems[idx] === swapped_elems[idx]) //# find triggers +ensures forall idx int :: {elems[idx]} {swapped_elems[idx]} (0 <= idx && idx < len(elems) && idx != i && idx != j) ==> (elems[idx] === swapped_elems[idx]) ensures old(x.less_spec(i, j, elems)) ==> !x.less_spec(i, j, swapped_elems) decreases func (x IntSlice) Swap(i, j int, ghost elems seq[any]) (ghost swapped_elems seq[any]) { From f2cefeb6ab344d8b510cceca1eee94a390897d7b Mon Sep 17 00:00:00 2001 From: adjenny Date: Tue, 24 Jan 2023 01:30:51 +0100 Subject: [PATCH 15/20] updated less_spec --- src/sort/sort_partial.gobra | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/src/sort/sort_partial.gobra b/src/sort/sort_partial.gobra index 450225b45ef..064132bc647 100644 --- a/src/sort/sort_partial.gobra +++ b/src/sort/sort_partial.gobra @@ -45,6 +45,7 @@ type Interface interface { requires acc(Mem(elems), ReadPerm) requires 0 <= i && i < len(elems) requires 0 <= j && j < len(elems) + ensures i == j ==> !res decreases pure less_spec(i, j int, ghost elems seq[any]) (res bool) // @@ -163,6 +164,7 @@ func (x IntSlice) LemmaLessIsTransitive(ghost elems seq[any]){ requires acc(x.Mem(elems), ReadPerm) requires 0 <= i && i < len(elems) requires 0 <= j && j < len(elems) +ensures i == j ==> !res decreases pure func (x IntSlice) less_spec(i, j int, ghost elems seq[any]) (res bool){ return unfolding acc(x.Mem(elems), ReadPerm) in x[i] < x[j] @@ -214,8 +216,6 @@ requires 0 <= a && a < len(elems) requires a <= b && b <= len(elems) //# the element at position b does not get sorted ensures data.Mem(sorted_elems) ensures haveSameElements(elems, sorted_elems) -//ensures a == b ==> isPartiallySorted(data, a, a, sorted_elems) -//ensures isPartiallySorted(data, a, b - 1, sorted_elems) decreases func insertionSort(data Interface, a, b int, ghost elems seq[any]) (ghost sorted_elems seq[any]) { sorted_elems = elems @@ -226,10 +226,10 @@ func insertionSort(data Interface, a, b int, ghost elems seq[any]) (ghost sorted invariant a < b ==> i <= b invariant data.Mem(sorted_elems) //# invariant prefix [a:i] is always sorted - //invariant forall idx int :: (a < idx && idx < i) ==> !data.less_spec(idx, idx - 1, sorted_elems) //# find triggers - //invariant isPartiallySorted(data, a, i - 1, sorted_elems) + //invariant i < b ==> (forall idx int :: (a < idx && idx < i) ==> !data.less_spec(idx, idx - 1, sorted_elems)) //# find triggers + invariant i < b ==> (forall idx1, idx2 int :: (0 <= idx1 && idx1 <= idx2 && idx2 < i) ==> !data.less_spec(idx2, idx1, sorted_elems)) decreases b-i - for i := a + 1; i < b; i++ { //# for any kind of sorting to happen b has to be at least a+2, does this mean if called with b=a+1 that this will not be sorted? Answer: YES, should we enforce that in the precondition? + for i := a + 1; i < b; i++ { invariant haveSameElements(elems, sorted_elems) invariant i < b invariant a <= j && j <= i @@ -237,9 +237,9 @@ func insertionSort(data Interface, a, b int, ghost elems seq[any]) (ghost sorted invariant data.Mem(sorted_elems) //# invariant prefix [a:j-1] is always sorted and [j:i] is always sorted //invariant (j <= a || !data.less_spec(j, j - 1, sorted_elems)) ==> (forall idx int :: (a < idx && idx < i) ==> !data.less_spec(idx, idx - 1, sorted_elems)) - //invariant (j > a && data.less_spec(j, j - 1, sorted_elems)) ==> (forall idx int :: (a < idx && idx < i && idx != j) ==> !data.less_spec(idx, idx - 1, sorted_elems)) //# find triggers - //invariant isPartiallySorted(data, a, XXX, sorted_elems) - //invariant isPartiallySorted(data, YYY, i, sorted_elems) + //invariant i < b ==> ((j > a && data.less_spec(j, j - 1, sorted_elems)) ==> (forall idx int :: (a < idx && idx < i && idx != j) ==> !data.less_spec(idx, idx - 1, sorted_elems)) ) //# find triggers + //invariant i < b ==> (forall idx1, idx2 int :: (0 <= idx1 && idx1 <= idx2 && idx2 < j) ==> !data.less_spec(idx2, idx1, sorted_elems)) + //invariant i < b ==> (forall idx1, idx2 int :: (j < idx1 && idx1 <= idx2 && idx2 < i) ==> !data.less_spec(idx2, idx1, sorted_elems)) decreases j-a for j := i; j > a /*&& data.Less(j, j - 1, elems)*/; j-- { //# The second conjunct in the loop condition was commented out. See comment below. assert 0 <= j - 1 @@ -249,6 +249,7 @@ func insertionSort(data Interface, a, b int, ghost elems seq[any]) (ghost sorted sorted_elems = data.Swap(j, j - 1, sorted_elems) assert !data.less_spec(j, j - 1, sorted_elems) } else { + assert !data.less_spec(j, j - 1, sorted_elems) break } } From bcd006260d07baee453d9631c74cd303f6c5e6b9 Mon Sep 17 00:00:00 2001 From: adjenny Date: Tue, 24 Jan 2023 04:03:20 +0100 Subject: [PATCH 16/20] updated 'toMultiset' --- src/sort/sort_partial.gobra | 42 ++++++++++++++++++------------------- 1 file changed, 20 insertions(+), 22 deletions(-) diff --git a/src/sort/sort_partial.gobra b/src/sort/sort_partial.gobra index 064132bc647..8661e4f7e12 100644 --- a/src/sort/sort_partial.gobra +++ b/src/sort/sort_partial.gobra @@ -18,10 +18,8 @@ type Interface interface { pred Mem(ghost s seq[any]) // Len is the number of elements in the collection. - requires acc(Mem(elems), ReadPerm) - ensures acc(Mem(elems), ReadPerm) + preserves acc(Mem(elems), ReadPerm) ensures res == len(elems) - ensures res >= 0 decreases Len(ghost elems seq[any]) (res int) @@ -38,7 +36,7 @@ type Interface interface { // - if both Less(i, j) and Less(j, k) are false, then Less(i, k) must be false as well. ghost preserves acc(Mem(elems), _) - ensures forall a, b, c int :: {less_spec(a, b, elems), less_spec(b, c, elems)} (0 <= a && a < len(elems) && 0 <= b && b < len(elems) && 0 <= c && c < len(elems) && less_spec(a, b, elems) && less_spec(b, c, elems)) ==> less_spec(a, c, elems) + ensures forall a, b, c int :: {less_spec(a, b, elems), less_spec(b, c, elems)} (0 <= a && a < len(elems) && 0 <= b && b < len(elems) && 0 <= c && c < len(elems) && less_spec(a, b, elems) && less_spec(b, c, elems)) ==> less_spec(a, c, elems) decreases LemmaLessIsTransitive(ghost elems seq[any]) @@ -52,11 +50,10 @@ type Interface interface { // Note that floating-point comparison (the < operator on float32 or float64 values) // is not a transitive ordering when not-a-number (NaN) values are involved. // See Float64Slice.Less for a correct implementation for floating-point values. - requires acc(Mem(elems), ReadPerm) - requires 0 <= i && i < len(elems) - requires 0 <= j && j < len(elems) - ensures acc(Mem(elems), ReadPerm) - ensures res == less_spec(i, j, elems) + preserves acc(Mem(elems), ReadPerm) + requires 0 <= i && i < len(elems) + requires 0 <= j && j < len(elems) + ensures res == less_spec(i, j, elems) decreases Less(i, j int, ghost elems seq[any]) (res bool) @@ -144,10 +141,8 @@ pred (x IntSlice) Mem(ghost s seq[any]){ forall j int :: {&x[j]} {s[j]} 0 <= j && j < len(s) ==> x[j] == s[j] } -requires acc(x.Mem(elems), ReadPerm) -ensures acc(x.Mem(elems), ReadPerm) -ensures unfolding acc(x.Mem(elems), ReadPerm) in res == len(elems) -ensures res >= 0 +preserves acc(x.Mem(elems), ReadPerm) +ensures unfolding acc(x.Mem(elems), ReadPerm) in res == len(elems) decreases func (x IntSlice) Len(ghost elems seq[any]) (res int) { return len(x) @@ -155,7 +150,7 @@ func (x IntSlice) Len(ghost elems seq[any]) (res int) { ghost preserves acc(x.Mem(elems), _) -ensures forall a, b, c int :: {x.less_spec(a, b, elems), x.less_spec(b, c, elems)} (0 <= a && a < len(elems) && 0 <= b && b < len(elems) && 0 <= c && c < len(elems) && x.less_spec(a, b, elems) && x.less_spec(b, c, elems)) ==> x.less_spec(a, c, elems) +ensures forall a, b, c int :: {x.less_spec(a, b, elems), x.less_spec(b, c, elems)} (0 <= a && a < len(elems) && 0 <= b && b < len(elems) && 0 <= c && c < len(elems) && x.less_spec(a, b, elems) && x.less_spec(b, c, elems)) ==> x.less_spec(a, c, elems) decreases func (x IntSlice) LemmaLessIsTransitive(ghost elems seq[any]){ unfold acc(x.Mem(elems), _) @@ -170,11 +165,10 @@ pure func (x IntSlice) less_spec(i, j int, ghost elems seq[any]) (res bool){ return unfolding acc(x.Mem(elems), ReadPerm) in x[i] < x[j] } -requires acc(x.Mem(elems), ReadPerm) -requires 0 <= i && i < len(elems) -requires 0 <= j && j < len(elems) -ensures acc(x.Mem(elems), ReadPerm) -ensures res == x.less_spec(i, j, elems) +preserves acc(x.Mem(elems), ReadPerm) +requires 0 <= i && i < len(elems) +requires 0 <= j && j < len(elems) +ensures res == x.less_spec(i, j, elems) decreases func (x IntSlice) Less(i, j int, ghost elems seq[any]) (res bool) { return unfolding acc(x.Mem(elems), ReadPerm) in x[i] < x[j] @@ -226,8 +220,8 @@ func insertionSort(data Interface, a, b int, ghost elems seq[any]) (ghost sorted invariant a < b ==> i <= b invariant data.Mem(sorted_elems) //# invariant prefix [a:i] is always sorted - //invariant i < b ==> (forall idx int :: (a < idx && idx < i) ==> !data.less_spec(idx, idx - 1, sorted_elems)) //# find triggers - invariant i < b ==> (forall idx1, idx2 int :: (0 <= idx1 && idx1 <= idx2 && idx2 < i) ==> !data.less_spec(idx2, idx1, sorted_elems)) + //invariant i < b ==> (forall idx int :: (a < idx && idx < i) ==> !data.less_spec(idx, idx - 1, sorted_elems)) //# neighbors are ordered + //invariant i < b ==> (forall idx1, idx2 int :: (0 <= idx1 && idx1 <= idx2 && idx2 < i) ==> !data.less_spec(idx2, idx1, sorted_elems)) decreases b-i for i := a + 1; i < b; i++ { invariant haveSameElements(elems, sorted_elems) @@ -263,7 +257,11 @@ func insertionSort(data Interface, a, b int, ghost elems seq[any]) (ghost sorted ghost ensures forall e any :: e in elemsSeq ==> e in elemsMultiSet //# find triggers ensures len(elemsSeq) == len(elemsMultiSet) -pure func toMultiSet(ghost elemsSeq seq[any]) (ghost elemsMultiSet mset[any]) +pure func toMultiSet(ghost elemsSeq seq[any]) (ghost elemsMultiSet mset[any]){ + return (len(elemsSeq) == 0 ? mset[any]{} : + mset[any]{elemsSeq[len(elemsSeq) - 1]} union toMultiSet(elemsSeq[:len(elemsSeq) - 1])) +} + From c3ddd55ddd0e9ed9970e4ca8bd0027c746dacf10 Mon Sep 17 00:00:00 2001 From: adjenny Date: Tue, 24 Jan 2023 04:51:14 +0100 Subject: [PATCH 17/20] changed IntSlice.Mem predicate --- src/sort/sort_partial.gobra | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/sort/sort_partial.gobra b/src/sort/sort_partial.gobra index 8661e4f7e12..afd4db17560 100644 --- a/src/sort/sort_partial.gobra +++ b/src/sort/sort_partial.gobra @@ -137,8 +137,7 @@ pure func toSeq(s []int) (res seq[any]) { pred (x IntSlice) Mem(ghost s seq[any]){ len(x) == len(s) && //# If this is not the first line in the predicate, then we cannot verify e.g. the last postcondition in Len() forall j int :: 0 <= j && j < len(x) ==> acc(&x[j]) && //# find triggers - s == toSeq(x) && - forall j int :: {&x[j]} {s[j]} 0 <= j && j < len(s) ==> x[j] == s[j] + s == toSeq(x) } preserves acc(x.Mem(elems), ReadPerm) From e7497edbbfcbf8ff240baa2c98f5ade645ec50b8 Mon Sep 17 00:00:00 2001 From: adjenny Date: Wed, 25 Jan 2023 04:58:01 +0100 Subject: [PATCH 18/20] updated postcondition of 'Swap', removed attempts from 'insertionSort' --- src/sort/sort_partial.gobra | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/src/sort/sort_partial.gobra b/src/sort/sort_partial.gobra index afd4db17560..57cec46776b 100644 --- a/src/sort/sort_partial.gobra +++ b/src/sort/sort_partial.gobra @@ -69,6 +69,7 @@ type Interface interface { ensures elems[j] === swapped_elems[i] ensures forall x int :: (0 <= x && x < len(elems) && x != i && x != j) ==> (elems[x] === swapped_elems[x]) //# find triggers ensures old(less_spec(i, j, elems)) ==> !less_spec(i, j, swapped_elems) //# We make the effect of the Swap operation on the Less relation explicit. + ensures old(less_spec(j, i, elems)) ==> !less_spec(j, i, swapped_elems) decreases Swap(i, j int, ghost elems seq[any]) (ghost swapped_elems seq[any]) } @@ -185,6 +186,7 @@ ensures elems[i] === swapped_elems[j] ensures elems[j] === swapped_elems[i] ensures forall idx int :: {elems[idx]} {swapped_elems[idx]} (0 <= idx && idx < len(elems) && idx != i && idx != j) ==> (elems[idx] === swapped_elems[idx]) ensures old(x.less_spec(i, j, elems)) ==> !x.less_spec(i, j, swapped_elems) +ensures old(x.less_spec(j, i, elems)) ==> !x.less_spec(j, i, swapped_elems) decreases func (x IntSlice) Swap(i, j int, ghost elems seq[any]) (ghost swapped_elems seq[any]) { unfold x.Mem(elems) @@ -219,8 +221,6 @@ func insertionSort(data Interface, a, b int, ghost elems seq[any]) (ghost sorted invariant a < b ==> i <= b invariant data.Mem(sorted_elems) //# invariant prefix [a:i] is always sorted - //invariant i < b ==> (forall idx int :: (a < idx && idx < i) ==> !data.less_spec(idx, idx - 1, sorted_elems)) //# neighbors are ordered - //invariant i < b ==> (forall idx1, idx2 int :: (0 <= idx1 && idx1 <= idx2 && idx2 < i) ==> !data.less_spec(idx2, idx1, sorted_elems)) decreases b-i for i := a + 1; i < b; i++ { invariant haveSameElements(elems, sorted_elems) @@ -229,10 +229,6 @@ func insertionSort(data Interface, a, b int, ghost elems seq[any]) (ghost sorted invariant a < j ==> 0 <= j - 1 invariant data.Mem(sorted_elems) //# invariant prefix [a:j-1] is always sorted and [j:i] is always sorted - //invariant (j <= a || !data.less_spec(j, j - 1, sorted_elems)) ==> (forall idx int :: (a < idx && idx < i) ==> !data.less_spec(idx, idx - 1, sorted_elems)) - //invariant i < b ==> ((j > a && data.less_spec(j, j - 1, sorted_elems)) ==> (forall idx int :: (a < idx && idx < i && idx != j) ==> !data.less_spec(idx, idx - 1, sorted_elems)) ) //# find triggers - //invariant i < b ==> (forall idx1, idx2 int :: (0 <= idx1 && idx1 <= idx2 && idx2 < j) ==> !data.less_spec(idx2, idx1, sorted_elems)) - //invariant i < b ==> (forall idx1, idx2 int :: (j < idx1 && idx1 <= idx2 && idx2 < i) ==> !data.less_spec(idx2, idx1, sorted_elems)) decreases j-a for j := i; j > a /*&& data.Less(j, j - 1, elems)*/; j-- { //# The second conjunct in the loop condition was commented out. See comment below. assert 0 <= j - 1 From 5b3bb69263335006a560396c2110c0713d0823d0 Mon Sep 17 00:00:00 2001 From: adjenny Date: Wed, 25 Jan 2023 05:09:59 +0100 Subject: [PATCH 19/20] fixed triggers, now also works on Gobra CLI --- src/sort/sort_partial.gobra | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/sort/sort_partial.gobra b/src/sort/sort_partial.gobra index 57cec46776b..ba4187e6dda 100644 --- a/src/sort/sort_partial.gobra +++ b/src/sort/sort_partial.gobra @@ -67,7 +67,7 @@ type Interface interface { ensures 0 <= j && j < len(elems) ensures elems[i] === swapped_elems[j] ensures elems[j] === swapped_elems[i] - ensures forall x int :: (0 <= x && x < len(elems) && x != i && x != j) ==> (elems[x] === swapped_elems[x]) //# find triggers + ensures forall x int :: {elems[x]} {swapped_elems[x]} (0 <= x && x < len(elems) && x != i && x != j) ==> (elems[x] === swapped_elems[x]) ensures old(less_spec(i, j, elems)) ==> !less_spec(i, j, swapped_elems) //# We make the effect of the Swap operation on the Less relation explicit. ensures old(less_spec(j, i, elems)) ==> !less_spec(j, i, swapped_elems) decreases @@ -126,7 +126,7 @@ type IntSlice []int //# Adapted from Gobra tutorial ghost -requires forall j int :: 0 <= j && j < len(s) ==> acc(&s[j], _) //# find triggers +requires forall j int :: {&s[j]} 0 <= j && j < len(s) ==> acc(&s[j], _) ensures len(res) == len(s) ensures forall j int :: {&s[j]} {res[j]} 0 <= j && j < len(s) ==> s[j] == res[j] decreases len(s) @@ -137,7 +137,7 @@ pure func toSeq(s []int) (res seq[any]) { pred (x IntSlice) Mem(ghost s seq[any]){ len(x) == len(s) && //# If this is not the first line in the predicate, then we cannot verify e.g. the last postcondition in Len() - forall j int :: 0 <= j && j < len(x) ==> acc(&x[j]) && //# find triggers + forall j int :: {&x[j]} 0 <= j && j < len(x) ==> acc(&x[j]) && s == toSeq(x) } From 26a9d3722e770581574acbca86edabf169de342c Mon Sep 17 00:00:00 2001 From: adjenny Date: Fri, 27 Jan 2023 23:58:06 +0100 Subject: [PATCH 20/20] included transitivity for !Less --- src/sort/sort_partial.gobra | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/src/sort/sort_partial.gobra b/src/sort/sort_partial.gobra index ba4187e6dda..740547f5c8a 100644 --- a/src/sort/sort_partial.gobra +++ b/src/sort/sort_partial.gobra @@ -35,8 +35,9 @@ type Interface interface { // - if both Less(i, j) and Less(j, k) are true, then Less(i, k) must be true as well. // - if both Less(i, j) and Less(j, k) are false, then Less(i, k) must be false as well. ghost - preserves acc(Mem(elems), _) + preserves acc(Mem(elems), ReadPerm) ensures forall a, b, c int :: {less_spec(a, b, elems), less_spec(b, c, elems)} (0 <= a && a < len(elems) && 0 <= b && b < len(elems) && 0 <= c && c < len(elems) && less_spec(a, b, elems) && less_spec(b, c, elems)) ==> less_spec(a, c, elems) + ensures forall a, b, c int :: {less_spec(a, b, elems), less_spec(b, c, elems)} (0 <= a && a < len(elems) && 0 <= b && b < len(elems) && 0 <= c && c < len(elems) && !less_spec(a, b, elems) && !less_spec(b, c, elems)) ==> !less_spec(a, c, elems) decreases LemmaLessIsTransitive(ghost elems seq[any]) @@ -149,11 +150,13 @@ func (x IntSlice) Len(ghost elems seq[any]) (res int) { } ghost -preserves acc(x.Mem(elems), _) +preserves acc(x.Mem(elems), ReadPerm) ensures forall a, b, c int :: {x.less_spec(a, b, elems), x.less_spec(b, c, elems)} (0 <= a && a < len(elems) && 0 <= b && b < len(elems) && 0 <= c && c < len(elems) && x.less_spec(a, b, elems) && x.less_spec(b, c, elems)) ==> x.less_spec(a, c, elems) +ensures forall a, b, c int :: {x.less_spec(a, b, elems), x.less_spec(b, c, elems)} (0 <= a && a < len(elems) && 0 <= b && b < len(elems) && 0 <= c && c < len(elems) && !x.less_spec(a, b, elems) && !x.less_spec(b, c, elems)) ==> !x.less_spec(a, c, elems) decreases func (x IntSlice) LemmaLessIsTransitive(ghost elems seq[any]){ - unfold acc(x.Mem(elems), _) + unfold acc(x.Mem(elems), ReadPerm) + fold acc(x.Mem(elems), ReadPerm) } requires acc(x.Mem(elems), ReadPerm)