Skip to content

Commit

Permalink
[motoko-san] enhance todo showcase
Browse files Browse the repository at this point in the history 
* Strengthen actor invariant on `nextId`
* Strengthen `getTodo` specifiction
  • Loading branch information
@GoPavel
GoPavel committed Jun 30, 2024
1 parent 1b68d0d commit 4a9668c
Show file tree
Hide file tree
Showing 2 changed files with 61 additions and 9 deletions.
48 changes: 43 additions & 5 deletions test/viper/ok/todo_record.vpr.ok
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(
define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
define $array_init(a, t, x) forall i : Int :: {$loc(a, i).t} 0 <= i && i < $size(a) ==> $loc(a, i).t == x
/* Tuple encoding */
adt Tuple$2 [T0, T1] { Tup$2(tup$2$0 : T0, tup$2$1 : T1) }
/* Option encoding */
adt Option[T] {
None()
Expand All @@ -27,7 +28,7 @@ define $Perm($Self) ((((true && (acc(($Self).todos,write) && $array_acc(
($Self).todos,
$c_ToDo, write))) &&
acc(($Self).num,write)) && acc(($Self).nextId,write)))
define $Inv($Self) (invariant_14($Self))
define $Inv($Self) ((invariant_14($Self) && invariant_15($Self)))
method __init__($Self: Ref)

requires $Perm($Self)
Expand All @@ -50,12 +51,19 @@ field num: Int
field nextId: Int
define invariant_14($Self) (((0 <= ($Self).num) && (($Self).num <= $size(
($Self).todos))))
define invariant_15($Self) ((forall i : Int :: (((0 <= i) && (i < ($Self).num)) ==> (
(($loc(($Self).todos, i)).$c_ToDo).$ToDo$id <
($Self).nextId))))
method resize($Self: Ref, n: Int)

requires $Perm($Self)
requires ((0 <= ($Self).num) && (($Self).num <= $size(($Self).todos)))
requires (forall i : Int :: (((0 <= i) && (i < ($Self).num)) ==> (
(($loc(($Self).todos, i)).$c_ToDo).$ToDo$id < ($Self).nextId)))
ensures $Perm($Self)
ensures ((0 <= ($Self).num) && (($Self).num <= $size(($Self).todos)))
ensures (forall i : Int :: (((0 <= i) && (i < ($Self).num)) ==> (
(($loc(($Self).todos, i)).$c_ToDo).$ToDo$id < ($Self).nextId)))
ensures ((($Self).num == old(($Self).num)) && (($Self).nextId ==
old(($Self).nextId)))
ensures ($size(($Self).todos) >= n)
Expand All @@ -77,6 +85,8 @@ method resize($Self: Ref, n: Int)
invariant $Perm($Self)
invariant $array_acc(new_array, $c_ToDo, write)
invariant ((0 <= ($Self).num) && (($Self).num <= $size(($Self).todos)))
invariant (forall ii : Int :: (((0 <= ii) && (ii < ($Self).num)) ==> (
(($loc(($Self).todos, ii)).$c_ToDo).$ToDo$id < ($Self).nextId)))
invariant ((($Self).num == old(($Self).num)) && (($Self).nextId ==
old(($Self).nextId)))
invariant ((0 <= i) && (i <= $size(($Self).todos)))
Expand Down Expand Up @@ -118,7 +128,7 @@ method getTodos($Self: Ref)
label $Ret;
}
method getTodo($Self: Ref, id: Int)
returns ($Res: Option[ToDo])
returns ($Res: Tuple$2[Option[ToDo], Int])
requires $Perm($Self)
requires $Inv($Self)
ensures $Perm($Self)
Expand All @@ -131,7 +141,18 @@ method getTodo($Self: Ref, id: Int)
(($loc(($Self).todos, i)).$c_ToDo).$ToDo$id == id))) ==>
(exists i : Int :: (((0 <= i) && (i < ($Self).num)) && (Some(($loc(
($Self).todos,
i)).$c_ToDo) == $Res))))
i)).$c_ToDo) ==
($Res).tup$2$0))))
ensures ((($Res).tup$2$0 == None()) == (forall i : Int :: (((0 <= i) && (i <
($Self).num)) ==> ((($loc(
($Self).todos,
i)).$c_ToDo).$ToDo$id != id))))
ensures ((($Res).tup$2$0 != None()) ==> ((0 <= ($Res).tup$2$1) && (
($Res).tup$2$1 < $size(($Self).todos))))
ensures ((($Res).tup$2$0 != None()) ==> (($Res).tup$2$0 == Some((
$loc(
($Self).todos,
($Res).tup$2$1)).$c_ToDo)))
ensures $Inv($Self)
{ var i: Int
var res: Option[ToDo]
Expand All @@ -140,6 +161,8 @@ method getTodo($Self: Ref, id: Int)
while ((i < ($Self).num))
invariant $Perm($Self)
invariant ((0 <= ($Self).num) && (($Self).num <= $size(($Self).todos)))
invariant (forall ii : Int :: (((0 <= ii) && (ii < ($Self).num)) ==> (
(($loc(($Self).todos, ii)).$c_ToDo).$ToDo$id < ($Self).nextId)))
invariant ((($Self).num == old(($Self).num)) && (($Self).nextId ==
old(($Self).nextId)))
invariant ($size(($Self).todos) == old($size(($Self).todos)))
Expand All @@ -148,6 +171,13 @@ method getTodo($Self: Ref, id: Int)
($loc(($Self).todos, ii)).$c_ToDo == old(($loc(($Self).todos,
ii)).$c_ToDo))))
invariant ((0 <= i) && (i <= ($Self).num))
invariant ((forall j : Int :: (((0 <= j) && (j < i)) ==> ((
(
$loc(
($Self).todos,
j)).$c_ToDo).$ToDo$id != id))) == (res ==
None()))
invariant ((res != None()) ==> (res == Some(($loc(($Self).todos, i)).$c_ToDo)))
{
label $lbl$continue$l;
if (((($loc(($Self).todos, i)).$c_ToDo).$ToDo$id == id))
Expand All @@ -157,7 +187,7 @@ method getTodo($Self: Ref, id: Int)
};
};
label $lbl$l;
$Res := res;
$Res := Tup$2(res, i);
goto $Ret;
label $Ret;
}
Expand All @@ -174,7 +204,7 @@ method addTodo($Self: Ref, description: Int)
TODO(),
description,
$Res))
ensures (forall i : Int :: (((0 <= i) && ((i + 1) < ($Self).num)) ==> (
ensures (forall i : Int :: (((0 <= i) && (i < (($Self).num - 1))) ==> (
($loc(($Self).todos, i)).$c_ToDo == old(($loc(($Self).todos, i)).$c_ToDo))))
ensures $Inv($Self)
{ var id: Int
Expand Down Expand Up @@ -211,6 +241,8 @@ method completeTodo($Self: Ref, id: Int)
while ((i < ($Self).num))
invariant $Perm($Self)
invariant ((0 <= ($Self).num) && (($Self).num <= $size(($Self).todos)))
invariant (forall ii : Int :: (((0 <= ii) && (ii < ($Self).num)) ==> (
(($loc(($Self).todos, ii)).$c_ToDo).$ToDo$id < ($Self).nextId)))
invariant ((0 <= i) && (i <= $size(($Self).todos)))
invariant ((($Self).num == old(($Self).num)) && (($Self).nextId ==
old(($Self).nextId)))
Expand Down Expand Up @@ -263,6 +295,8 @@ method showTodos($Self: Ref)
while ((i < ($Self).num))
invariant $Perm($Self)
invariant ((0 <= ($Self).num) && (($Self).num <= $size(($Self).todos)))
invariant (forall ii : Int :: (((0 <= ii) && (ii < ($Self).num)) ==> (
(($loc(($Self).todos, ii)).$c_ToDo).$ToDo$id < ($Self).nextId)))
invariant ((($Self).num == old(($Self).num)) && (($Self).nextId ==
old(($Self).nextId)))
invariant ($size(($Self).todos) == old($size(($Self).todos)))
Expand Down Expand Up @@ -318,6 +352,8 @@ method clearCompleted($Self: Ref)
invariant $Perm($Self)
invariant $array_acc(new_array, $c_ToDo, write)
invariant ((0 <= ($Self).num) && (($Self).num <= $size(($Self).todos)))
invariant (forall ii : Int :: (((0 <= ii) && (ii < ($Self).num)) ==> (
(($loc(($Self).todos, ii)).$c_ToDo).$ToDo$id < ($Self).nextId)))
invariant ((($Self).num == old(($Self).num)) && (($Self).nextId ==
old(($Self).nextId)))
invariant ($size(($Self).todos) == old($size(($Self).todos)))
Expand All @@ -338,6 +374,8 @@ method clearCompleted($Self: Ref)
invariant (forall ii : Int :: (((0 <= ii) && (ii < j)) ==> (
(($loc(new_array, ii)).$c_ToDo).$ToDo$completed ==
TODO())))
invariant (forall ii : Int :: (((0 <= ii) && (ii < j)) ==> (
(($loc(new_array, ii)).$c_ToDo).$ToDo$id < ($Self).nextId)))
{
if (((($loc(($Self).todos, i)).$c_ToDo).$ToDo$completed ==
TODO()))
Expand Down
22 changes: 18 additions & 4 deletions test/viper/todo_record.mo
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,11 +12,14 @@ actor Assistant {
var nextId : Nat = 1;

assert:invariant 0 <= num and num <= todos.size();
assert:invariant Prim.forall<Nat>(func i = (0 <= i and i < num) implies todos[i].id < nextId);

private func resize(n: Nat) {
// Actor's invariant is preserved:
assert:func 0 <= num and num <= todos.size();
assert:return 0 <= num and num <= todos.size();
assert:func Prim.forall<Nat>(func i = (0 <= i and i < num) implies todos[i].id < nextId);
assert:return Prim.forall<Nat>(func i = (0 <= i and i < num) implies todos[i].id < nextId);
// unchanged fields:
assert:return num == (old(num)) and nextId == (old(nextId));
// functional specification:
Expand All @@ -31,6 +34,7 @@ actor Assistant {
while (i < todos.size()) {
// actor invariant:
assert:loop:invariant 0 <= num and num <= todos.size();
assert:loop:invariant Prim.forall<Nat>(func ii = (0 <= ii and ii < num) implies todos[ii].id < nextId);
// unchanged fields:
assert:loop:invariant num == (old(num)) and nextId == (old(nextId));
assert:loop:invariant 0 <= i and i <= todos.size();
Expand Down Expand Up @@ -60,32 +64,38 @@ actor Assistant {
return new_array;
};

public query func getTodo(id : Nat): async ?ToDo {
public query func getTodo(id : Nat): async (?ToDo, Nat) {
assert:return num == (old(num)) and nextId == (old(nextId));
assert:return todos.size() == (old(todos.size()));
assert:return Prim.forall<Nat>(func i =
(0 <= i and i < (old(todos.size())) implies todos[i] == (old(todos[i]))));
assert:return (Prim.exists<Nat>(func i = (0 <= i and i < num and todos[i].id == id))
implies
Prim.exists<Nat>(func i = (0 <= i and i < num and ?todos[i] == Prim.Ret<?ToDo>())));
Prim.exists<Nat>(func i = (0 <= i and i < num and ?todos[i] == Prim.Ret<(?ToDo, Nat)>().0)));
assert:return (Prim.Ret<(?ToDo, Nat)>().0 == null) == (Prim.forall<Nat>(func i = (0 <= i and i < num implies todos[i].id != id)));
assert:return (Prim.Ret<(?ToDo, Nat)>().0 != null) implies 0 <= Prim.Ret<(?ToDo, Nat)>().1 and Prim.Ret<(?ToDo, Nat)>().1 < todos.size();
assert:return (Prim.Ret<(?ToDo, Nat)>().0 != null) implies (Prim.Ret<(?ToDo, Nat)>().0 == ?(todos[Prim.Ret<(?ToDo, Nat)>().1]));
var i : Nat = 0;
var res : ?ToDo = null;
label l while (i < num) {
// actor invariant:
assert:loop:invariant 0 <= num and num <= todos.size();
assert:loop:invariant Prim.forall<Nat>(func ii = (0 <= ii and ii < num) implies todos[ii].id < nextId);
// fields unchanged:
assert:loop:invariant num == (old(num)) and nextId == (old(nextId));
// functional specification:
assert:loop:invariant todos.size() == (old(todos.size()));
assert:loop:invariant Prim.forall<Nat>(func ii =
(0 <= ii and ii < (old(todos.size())) implies todos[ii] == (old(todos[ii]))));
assert:loop:invariant 0 <= i and i <= num;
assert:loop:invariant (Prim.forall<Nat>(func j = (0 <= j and j < i implies todos[j].id != id))) == (res == null);
assert:loop:invariant (res != null) implies (res == ?(todos[i]));
if (todos[i].id == id) {
res := ?todos[i];
break l;
};
};
return res;
return (res, i);
};

// Returns the ID that was given to the ToDo item
Expand All @@ -96,7 +106,7 @@ actor Assistant {
assert:return Prim.Ret<Nat>() == (old(nextId));
assert:return todos[num-1] == ({ id = Prim.Ret<Nat>(); desc = description; completed = #TODO });
assert:return Prim.forall<Nat>(func i =
(0 <= i and i+1 < num implies todos[i] == (old(todos[i]))));
(0 <= i and i < num-1 implies todos[i] == (old(todos[i]))));
let id = nextId;
if (num >= todos.size()) {
resize(num * 2+1);
Expand All @@ -118,6 +128,7 @@ actor Assistant {
while (i < num) {
// actor invariant
assert:loop:invariant 0 <= num and num <= todos.size();
assert:loop:invariant Prim.forall<Nat>(func ii = (0 <= ii and ii < num) implies todos[ii].id < nextId);
// functional specifications:
assert:loop:invariant 0 <= i and i <= todos.size();
assert:loop:invariant num == (old(num)) and nextId == (old(nextId));
Expand Down Expand Up @@ -151,6 +162,7 @@ actor Assistant {
while (i < num) {
// actor invariant
assert:loop:invariant 0 <= num and num <= todos.size();
assert:loop:invariant Prim.forall<Nat>(func ii = (0 <= ii and ii < num) implies todos[ii].id < nextId);
// unchanged fields:
assert:loop:invariant num == (old(num)) and nextId == (old(nextId));
assert:loop:invariant todos.size() == (old(todos.size()));
Expand Down Expand Up @@ -183,6 +195,7 @@ actor Assistant {
while (i < num) {
// actor invariant
assert:loop:invariant 0 <= num and num <= todos.size();
assert:loop:invariant Prim.forall<Nat>(func ii = (0 <= ii and ii < num) implies todos[ii].id < nextId);
// unchanged fields:
assert:loop:invariant num == (old(num)) and nextId == (old(nextId));
assert:loop:invariant todos.size() == (old(todos.size()));
Expand All @@ -199,6 +212,7 @@ actor Assistant {
(0 <= k and k < j and new_array[k] == todos[ii] ))));
assert:loop:invariant Prim.forall<Nat>(func ii =
(0 <= ii and ii < j implies new_array[ii].completed == #TODO ));
assert:loop:invariant Prim.forall<Nat>(func ii = (0 <= ii and ii < j) implies new_array[ii].id < nextId);
if (todos[i].completed == #TODO) {
new_array[j] := todos[i];
j += 1;
Expand Down

0 comments on commit 4a9668c

Please sign in to comment.