ring PR #5
ring PR #5
Conversation
src/container/ring/ring.gobra
Outdated
| invariant forall e *Ring :: e in elems ==> ((e != r && e != p) ==> (e.next != nil && e.prev != nil)) | ||
| invariant forall e1, e2 *Ring :: (e1 in elems && e1.next == e2 && e1 != p && e2 != r) ==> (e2 in elems && e2.prev == e1 && e1.next.prev == e1 && e2.prev.next == e2) | ||
| //invariant forall e1, e2 *Ring :: (e1 in elems && e1.prev == e2 && e1 != r && e2 != p) ==> (e2 in elems && e2.next == e1 && e1.prev.next == e1 && e2.next.prev == e2) | ||
| //invariant forall e1, e2 *Ring :: (e1 in elems && e1.prev == e2 && e1 != r && e2 != p) ==> (e2 in elems && e2.next == e1) //# Why does this not work? |
There was a problem hiding this comment.
With these invariants I try to build up the required facts to fold the predicate r.Mem(elems, true) in the end. This line (239) does not verify. It is a shortened version of the line above which of course also does not work. It complains the loop invariant cannot be preserved. Interestingly, it verifies successfully with the invariant in line 237. This quantified expression is a modified version of a similar expression stated in the predicate. It aims to establish how neighboring ring elements are connected. Because the end-points of the ring (r at the beginning and p at the end) are not already connected in this original implementation I exclude them in the LHS of the implication. The idea is if we have e1.prev == e2 and e2 != p (i.e. e2 is not the "last" element in the chain) then we should have e2.next == e1. The implication is successful if we only had e2 in elems on the RHS. The code suggests the whole implication should hold true and the vice-versa case holds on line 237.
Even if this invariant were to hold, I am very unsure whether I could successfully fold the predicate at the very end.
There was a problem hiding this comment.
I spent some time debug but I did not find any obvious mistake. Maybe one way to move forward is to generate the viper file for this specific method (using --printVpr and the @ notation). With this file, you can then try to run silicon with the options --moreCompleteExhale --counterexample variables which produces a counterexample for the failing assertion at the viper level. With this, you can try to infer a counterexample at the Gobra level for the invariant
| } | ||
|
|
||
| //# Functional properties of this method have NOT yet been verified. |
There was a problem hiding this comment.
Functional properties (e.g. r.Move(3) produces r.next.next.next) could not be verified.
The idea would be to use something like moveNext from the ring_spec.gobra file in the invariant and postcondition. However, this did not terminate even after a day when used in the invariant. Testing moveNext by itself works just fine.
The same applies of course to cases where n<0 and movePrev.
| 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] @*/) { |
There was a problem hiding this comment.
I did not find the time to continue the investigation as to why the invariants for the original implementation of New did not verify. (see https://github.com/jcp19/verified_go_stdlib/pull/5#discussion_r1065748315)
Therefore, for this version I included my adapted implementation with an explanation and will point this out in the report.
| //# ensures (s != nil && s in elemsR && r == s && len(elemsR) > 1) ==> res.Mem((elemsR setminus (set[*Ring]{r})), true) CANNOT FOLD | ||
| //# ensures (s != nil && s in elemsR && r != s && len(elemsR) == 1) ==> UNIMPLEMENTED | ||
| //@ decreases | ||
| func (r *Ring) Link(s *Ring /*@, ghost elemsR set[*Ring], ghost elemsS set[*Ring] @*/) (res *Ring) { |
There was a problem hiding this comment.
Only a subset of the behaviours are dealt with here. Corresponding comments have been included.
Sometimes it is necessary to assume forall i *Ring :: i in (elemsR union elemsS) ==> (i.next != i && i.prev != i) since Gobra cannot establish that by itself. The problem is likely that the predicate by itself does not guarantee that all the elements form a single ring structure. If multiple smaller ring structures were possible then this implication could be false. However, the behaviour of the methods effectively preserves that it will always be a single ring structure once initialized. I will point this out in the report.
| //@ requires r != nil | ||
| //@ requires r.Mem(elems, isInit) | ||
| //@ ensures n <= 0 ==> res == nil | ||
| func (r *Ring) Unlink(n int /*@, ghost elems set[*Ring], ghost owner *Ring, ghost isInit bool @*/) (res *Ring) { |
There was a problem hiding this comment.
Unlink could not be specified even for the subset of cases we handled in Link. The reasons are:
- We don't get any information from
Moveabout at what position the element pointed to byris in the end Movechangesritself and we loose the reference to theMempredicate for the call toLink. This could possibly be fixed by carrying theownerthrough all calls everywhere.- We only call
Linkifn>0, thus even if we would get the information about the new position ofrfromMovewe would always enter a case inLinkthat we could not handle unlessn==len(elems
| //@ ensures r == nil ==> res == 0 | ||
| //@ ensures (r != nil && !isInit) ==> (r.Mem(set[*Ring]{r}, true) && res == 1) | ||
| //@ ensures (r != nil && isInit) ==> (r.Mem(elems, true) && res == len(elems)) | ||
| func (r *Ring) Len(/*@ ghost elems set[*Ring], ghost isInit bool @*/) (res int) { |
There was a problem hiding this comment.
The loop could not be verified since we could not establish that after len(elems) many iterations (i.e. p=p.next len(elems) many times) we get r==p.
| //@ requires false //# UNIMPLEMENTED | ||
| //@ requires r != nil ==> r.Mem(elems, isInit) | ||
| //@ trusted //# required because of error with 'f' | ||
| func (r *Ring) Do(f func(any) /*@, ghost elems set[*Ring], ghost isInit bool @*/) { |
There was a problem hiding this comment.
We made no attempt at Do
No description provided.