sort PR #6

witemap · 2023-01-12T03:00:01Z

No description provided.

… sort.IsSorted, memory safety for insertionSort

…ity check

…evel in IntSlice.Swap

src/sort/sort_partial.gobra

witemap · 2023-01-12T03:08:00Z

src/sort/sort_partial.gobra

+	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)


We talked in the meeting how this transitivity requirement should be replaced via the introduction of a method like lessTransitiveProof to improve performance.
While I understood the simple examples you presented in the meeting. I don't know how to go about this in this context. How would lessTransitiveProof have to look like on the implementation level, i.e. what would be its body if it even has a body?

There is no general answer to what the body would look like. Nonetheless, the body must always exist, otherwise this is not verified, it is just an assumption. In order to write the body of lessTransitiveProof, you will need to know the body of less_spec. Most often, if these implementations are trivial, the smt solver will be able to prove the postcondition of lessTransitiveProof. In some other cases you may need to introduce some additional lemmas or to do a proof by induction, which can be encoded as a recursive (ghost) method in Gobra. We can take a look at examples in our next meeting

witemap · 2023-01-12T03:17:34Z

src/sort/sort_partial.gobra

+
+
+/*
+ensures forall e int :: e in s1 ==> e in s2 //# this causes gobra to crash, it works with mset[int] as the return type


This postcondition causes Gobra to crash with the message:

An exception occurred during execution of Gobra: java.util.concurrent.ExecutionException: java.lang.AssertionError: assertion failed: Expected second operand e_V1@119@00 to be of sort Tuple2[Ref, Types], but found Int.

This does not happen if s2 is also of type mset[int].
It is very possible that this is not even a legal operation I'm trying to do here but I still think Gobra should not crash outright.
Moreover, looking at the postcondition in toSeq it is possible to compare elements in the collections of type []int and seq[any]. It is just the contains operator in that leads to the crash.

yes, ideally Gobra should insert a type conversion automatically here or should return a type error. The reason here is that ints and values of interface types are encoded differently (with different types at the viper level), but we are treating them at the viper level as if they were encoded as the same type.

As for now, as soon as PR viperproject/gobra#600 is merged, we can side-step this issue by replacing e in s2 with (interface{})(e) in s2. Can you please open an issue on the issue tracker about this?

opened issue https://github.com/viperproject/gobra/issues/601

viperproject/gobra#600 was merged. The approach with a cast should work now

witemap · 2023-01-12T03:22:44Z

src/sort/sort_partial.gobra

+	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].


I was not able to make haveSameElements work on the implementation level.
It cannot automatically be established after the elements in x have been swapped. I tried to implement a mapping of x to a multiset in an effort to try and prove this on the implementation level, however, this approach failed due to the error described in https://github.com/jcp19/verified_go_stdlib/pull/6/files#r1067661530.

Nonetheless, this assumption should still be safe. Swap is the only method described in the interface that actively changes the order of the elements and it is safe to assume here that really haveSameElements(elems, swapped_elems) holds.

witemap · 2023-01-12T03:40:47Z

src/sort/sort_partial.gobra

+//# 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) {


The functionIsSorted below naturally yields the postcondition [1]:

forall idx int :: ((0 < idx && idx < len(elems)) ==> (!data.less_spec(idx, idx - 1, elems)))

if the elements are sorted.

This definition of "sortedness" makes sense but does not easily lend itself to checking for sortedness of data of any length (i.e. it cannot be directly applied when Len()<=1). I thought it would be nice to have a ghost pure helper function isPartiallySorted that can then also be used to easily check for sortedness of "subslices" of data as is required in insertionSort and even more useful in the invariants of insertionSort.

This implementation of isPartiallySorted follows the typical pattern of a recursive sortedness check. However, it does not manage to establish the same postcondition mentioned above in [1].
Conversely, I tried to use my implementation of isPartiallySorted in the loop invariant of IsSorted but it could not be preserved.

To be clear, I don't even need the postcondition [1] in line 81 here. It was just included as a sanity check to see why I could not use isPartiallySorted in IsSorted.
Nonetheless, I think it should still hold and cannot spot the issue.

This definition of "sortedness" makes sense but does not easily lend itself to checking for sortedness of data of any length (i.e. it cannot be directly applied when Len()<=1)

Why not? here, if len(elems) <= 1, then the property trivially holds - every sequence with 0 or 1 elements is sorted

witemap · 2023-01-12T03:42:42Z

src/sort/sort_partial.gobra

+		if data.Less(i, i - 1, elems) {
+			return false
+		}
+		//assert isPartiallySorted(data, i, n - 1, elems)


as commented above, this assertion does not hold

witemap · 2023-01-16T17:21:30Z

src/sort/sort_partial.gobra

+//# 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]))
+//# ..for these 3 corresponding lines to work.
+ensures  elems[i] === swapped_elems[j]


This postcondition (and presumably the next one too) cannot get verified by the GobraCLI.
I run the most current versions of the GobraIDE and GobraCLI.
This postcondition only verifies for the GobraIDE stable build version but fails for the GobraIDE nightly build version and the GobraCLI.
Postcondition might not hold: Assertion elems[i] === swapped_elems[j] might not hold.

I can verify that old(unfolding x.Mem(elems) in x[i]) === (unfolding x.Mem(swapped_elems) in x[j]). Further, it should know from the predicate x.Mem(elems) from the precondition that in the old context we had a 1:1 mapping between the elements of x and elems. The same is given in the new context by x.Mem(swapped_elems) for a mapping between x and swapped_elems.

jcp19

I will continue later

jcp19 · 2023-01-20T16:12:35Z

src/sort/sort_partial.gobra

+	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)


There is no general answer to what the body would look like. Nonetheless, the body must always exist, otherwise this is not verified, it is just an assumption. In order to write the body of lessTransitiveProof, you will need to know the body of less_spec. Most often, if these implementations are trivial, the smt solver will be able to prove the postcondition of lessTransitiveProof. In some other cases you may need to introduce some additional lemmas or to do a proof by induction, which can be encoded as a recursive (ghost) method in Gobra. We can take a look at examples in our next meeting

jcp19 · 2023-01-20T16:17:34Z

src/sort/sort_partial.gobra

+	requires acc(Mem(elems), ReadPerm)
+	ensures  acc(Mem(elems), ReadPerm)
+	ensures  res == len(elems)
+	ensures  res >= 0


functions should also be annotated as terminating. Note that termination measures in interface methods' contracts have a special meaning - they define an upper bound on the termination measures of the implementations. If you are curious, I can explain why in the next meeting

you are absolutely right of course. the lack of these annotations might also be the reason why i can't use isPartiallySorted in the spec of other methods. an appropriate termination measure for isPartiallySorted would be end - start.

however, simply adding decreases to less_spec causes the error

Pure function might not terminate. Required tuple condition might not hold.

since i need less_spec to be terminating for isPartiallySorted to be terminating i also cannot add the decreases end - start clause to isPartiallySorted as of now.

i'd be glad to have a look at this in the meeting as you suggested

for which line is this error message reported?

1: If i put decreases for both the interface version of less_spec and on the implementation of (x IntSlice) less_spec i get the above error pointing at the first line of the precondition of less_spec in the interface.

Additionally, I get Pure function might not terminate. Termination condition might not decrease 3 times.
2: Once pointing at the line right above the new decreases clause in (x IntSlice) less_spec.
3,4: And TWICE pointing at the line right above the new decreases clause.
5: Additionally i get

Error at: <.:0:0> Fold might fail. Assertion 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] might not hold.

which is just the last 3 lines of the x.Mem predicate.

It reports 5 errors, one of them twice but mentions Gobra has found 4 errors.

Putting decreases only on the implementation (x IntSlice) less_spec reports errors 2 and 5.
Putting decreases only on the interface version of less_spec reports errors 1, 3, 4 and 5 but says it found only 3 errors.

GobraIDE is a different story again. It verifies fine if we have decreases only on the implementation (x IntSlice) less_spec which is not very useful alone even if it were true. In any other scenario it reports error 1 and additionally Postcondition might not hold. Assertion "entire spec and declaration of less_spec" might not hold at the same line as error 1.

src/sort/sort_partial.gobra

jcp19 · 2023-01-20T16:22:29Z

src/sort/sort_partial.gobra

+	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)


no triggers have been specified here. I guess that { less_spec(a, b, elems), less_spec(b,c,elems) } would be a good fit

you are right. your proposed triggers also work fine, thank you!

i still struggle with some of the others as a result of the inconsistency between GobraIDE and the CLI version

adjenny added 9 commits December 12, 2022 17:02

start attempt at ring

654a829

prove memory safety for Move(n), changed implementation of New()

a11ba47

start on Link

4bf7dfb

partial file: specified sort.Interface, sort.IntSlice implementation,…

9465f4e

… sort.IsSorted, memory safety for insertionSort

restore ring directory to master

189783b

allowed same indices a, b in 'insertionSort'

a7d8388

simplified, attempt at 'isPartiallySorted', attempt at sequence equal…

a86707b

…ity check

introduced 'haveSameElements(..)' with assumption on implementation l…

f07353f

…evel in IntSlice.Swap

updated comments

54446dc

witemap commented Jan 12, 2023

View reviewed changes

src/sort/sort_partial.gobra Outdated Show resolved Hide resolved

witemap commented Jan 12, 2023

View reviewed changes

witemap commented Jan 16, 2023

View reviewed changes

jcp19 reviewed Jan 20, 2023

View reviewed changes

adjenny and others added 12 commits January 21, 2023 01:55

inserted more triggers

5b4b59c

added 'decreases' clause where possible

fb95db7

Merge branch 'master' into adrian-sort

735c8a3

changes of meeting jan 23rd

0ba6b67

updated 'Swap' spec

a8bd811

transitive proof and decreases clause

5064b30

updated less_spec

f2cefeb

updated 'toMultiset'

bcd0062

changed IntSlice.Mem predicate

c3ddd55

updated postcondition of 'Swap', removed attempts from 'insertionSort'

e7497ed

fixed triggers, now also works on Gobra CLI

5b3bb69

included transitivity for !Less

26a9d37

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

sort PR #6

sort PR #6

witemap commented Jan 12, 2023

witemap Jan 12, 2023

jcp19 Jan 20, 2023

witemap Jan 12, 2023

jcp19 Jan 22, 2023

witemap Jan 22, 2023

jcp19 Jan 23, 2023

witemap Jan 12, 2023

witemap Jan 12, 2023

jcp19 Jan 20, 2023

witemap Jan 12, 2023

witemap Jan 16, 2023

jcp19 left a comment

jcp19 Jan 20, 2023

jcp19 Jan 20, 2023

witemap Jan 21, 2023

jcp19 Jan 22, 2023

witemap Jan 22, 2023

jcp19 Jan 20, 2023

witemap Jan 21, 2023



		/*
		ensures forall e int :: e in s1 ==> e in s2 //# this causes gobra to crash, it works with mset[int] as the return type

sort PR #6

Are you sure you want to change the base?

sort PR #6

Conversation

witemap commented Jan 12, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jcp19 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment