Skip to content

Commit

Permalink
Fix typo - rename SSLseg to SLLseg
Browse files Browse the repository at this point in the history
  • Loading branch information
@NatKarmios
NatKarmios committed Nov 27, 2024
1 parent 54a6b00 commit 3460b07
Show file tree
Hide file tree
Showing 7 changed files with 57 additions and 57 deletions.
26 changes: 13 additions & 13 deletions debug-ui/examples/wisl/lab/sll/auto.wisl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -232,7 +232,7 @@ predicate SLLseg(+x, y, vs) {
//
// Lemma: appending a given value to a given SLLseg
//
lemma SSLseg_append {
lemma SLLseg_append {
statement:
forall x, vs, v, z.
SLLseg(x, #y, vs) * (#y -b> v, z) |- SLLseg(x, z, vs @ [ v ])
Expand All @@ -243,7 +243,7 @@ lemma SSLseg_append {
assert {bind: #nv, #nnext, #nvs}
(x -b> #nv, #nnext) * SLLseg(#nnext, #y, #nvs) *
(vs == #nv :: #nvs);
apply SSLseg_append(#nnext, #nvs, v, z);
apply SLLseg_append(#nnext, #nvs, v, z);
fold SLLseg(x, z, vs @ [ v ])
} else {
fold SLLseg(#y, z, [ v ])
Expand Down Expand Up @@ -299,11 +299,11 @@ function SLL_append_iter(x, k){
[[ assert {bind: #prev} prev == #prev ]];
prev := next;
next := [next + 1];
[[ apply SSLseg_append(head, #vs1, #v, prev) ]]
[[ apply SLLseg_append(head, #vs1, #v, prev) ]]
};
[prev + 1] := y;
[[ assert {bind: #svs, #sv} SLLseg(head, prev, #svs) * (prev -b> #sv, y) ]];
[[ apply SSLseg_append(head, #svs, #sv, y) ]];
[[ apply SLLseg_append(head, #svs, #sv, y) ]];
[[ assert (SLLseg(head, y, #vx)) ]];
[[ apply SLLseg_concat_SLL(head, y) ]]
};
Expand All @@ -327,11 +327,11 @@ function SLL_append_node_iter(x, y){
[[ assert {bind: #prev} prev == #prev ]];
prev := next;
next := [next + 1];
[[ apply SSLseg_append(head, #vs1, #v, prev) ]]
[[ apply SLLseg_append(head, #vs1, #v, prev) ]]
};
[prev + 1] := y;
[[ assert {bind: #svs, #sv} SLLseg(head, prev, #svs) * (prev -b> #sv, y) ]];
[[ apply SSLseg_append(head, #svs, #sv, y) ]];
[[ apply SLLseg_append(head, #svs, #sv, y) ]];
[[ assert (SLLseg(head, y, #vs)) ]]; // <-- add deliberate bug to #vx
[[ apply SLLseg_concat_SLL(head, y) ]]
};
Expand All @@ -355,11 +355,11 @@ function SLL_concat_iter(x, y){
[[ assert {bind: #prev} prev == #prev ]];
prev := next;
next := [next + 1];
[[ apply SSLseg_append(head, #vs1, #v, prev) ]]
[[ apply SLLseg_append(head, #vs1, #v, prev) ]]
};
[prev + 1] := y;
[[ assert {bind:#svs, #sv} SLLseg(head, prev, #svs) * (prev -b> #sv, y) ]];
[[ apply SSLseg_append(head, #svs, #sv, y) ]];
[[ apply SLLseg_append(head, #svs, #sv, y) ]];
[[ apply SLLseg_concat_SLL(head, y) ]]
};
return head
Expand Down Expand Up @@ -392,11 +392,11 @@ function SLL_copy_iter(x){
[p + 1] := c;
p := c;
t := [t + 1];
[[ apply SSLseg_append(x, #alpha1, v, t) ]];
[[ apply SSLseg_append(y, #alpha3, #a, p) ]]
[[ apply SLLseg_append(x, #alpha1, v, t) ]];
[[ apply SLLseg_append(y, #alpha3, #a, p) ]]
};
[[ assert {bind: #alpha3} SLLseg(y, p, #alpha3) ]];
[[ apply SSLseg_append(y, #alpha3, v, null) ]];
[[ apply SLLseg_append(y, #alpha3, v, null) ]];
[[ apply SLLseg_to_SLL(x) ]];
[[ apply SLLseg_to_SLL(y) ]]
};
Expand All @@ -417,7 +417,7 @@ function SLL_length_iter(x) {
[[ assert {bind: #v, #z} #y -b> #v, #z ]];
y := [y+1];
n := n+1;
[[ apply SSLseg_append(x, #nvx, #v, y) ]]
[[ apply SLLseg_append(x, #nvx, #v, y) ]]
};
[[ unfold SLL(null, #nvy)]];
[[ apply SLLseg_to_SLL(x) ]];
Expand Down Expand Up @@ -457,7 +457,7 @@ function SLL_member_iter(x, k) {
v := [next];
found := (v = k);
next := [next + 1];
[[ apply SSLseg_append(x, #beta, #v, next) ]];
[[ apply SLLseg_append(x, #beta, #v, next) ]];
[[ unfold list_member(#gamma, k, #rg) ]];
[[ apply list_member_append(#beta, k, false, #v) ]]
};
Expand Down
4 changes: 2 additions & 2 deletions debug-ui/examples/wisl/lab/sll/manual.wisl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -231,7 +231,7 @@ predicate SLLseg(+x, y, vs) {
//
// Lemma: appending a given value to a given SLLseg
//
lemma SSLseg_append {
lemma SLLseg_append {
statement:
forall x, vs, v, z.
SLLseg(x, #y, vs) * (#y -b> v, z) |- SLLseg(x, z, vs @ [ v ])
Expand All @@ -242,7 +242,7 @@ lemma SSLseg_append {
assert {bind: #nv, #nnext, #nvs}
(x -b> #nv, #nnext) * SLLseg(#nnext, #y, #nvs) *
(vs == #nv :: #nvs);
apply SSLseg_append(#nnext, #nvs, v, z);
apply SLLseg_append(#nnext, #nvs, v, z);
fold SLLseg(x, z, vs @ [ v ])
} else {
fold SLLseg(#y, z, [ v ])
Expand Down
26 changes: 13 additions & 13 deletions debug-ui/examples/wisl/lab/sll/manual_solutions.wisl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -263,7 +263,7 @@ predicate SLLseg(+x, y, vs) {
//
// Lemma: appending a given value to a given SLLseg
//
lemma SSLseg_append {
lemma SLLseg_append {
statement:
forall x, vs, v, z.
SLLseg(x, #y, vs) * (#y -b> v, z) |- SLLseg(x, z, vs @ [ v ])
Expand All @@ -274,7 +274,7 @@ lemma SSLseg_append {
assert {bind: #nv, #nnext, #nvs}
(x -b> #nv, #nnext) * SLLseg(#nnext, #y, #nvs) *
(vs == #nv :: #nvs);
apply SSLseg_append(#nnext, #nvs, v, z);
apply SLLseg_append(#nnext, #nvs, v, z);
fold SLLseg(x, z, vs @ [ v ])
} else {
fold SLLseg(#y, z, [ v ])
Expand Down Expand Up @@ -333,11 +333,11 @@ function SLL_append_iter(x, k){
[[ unfold SLL(next, #vs2) ]];
prev := next;
next := [next + 1];
[[ apply SSLseg_append(head, #vs1, #v, prev) ]]
[[ apply SLLseg_append(head, #vs1, #v, prev) ]]
};
[prev + 1] := y;
[[ assert {bind: #svs, #sv} SLLseg(head, prev, #svs) * (prev -b> #sv, y) ]];
[[ apply SSLseg_append(head, #svs, #sv, y) ]];
[[ apply SLLseg_append(head, #svs, #sv, y) ]];
[[ assert (SLLseg(head, y, #vx)) ]];
[[ apply SLLseg_concat_SLL(head, y) ]]
};
Expand All @@ -364,11 +364,11 @@ function SLL_append_node_iter(x, y){
[[ unfold SLL(next, #vs2) ]];
prev := next;
next := [next + 1];
[[ apply SSLseg_append(head, #vs1, #v, prev) ]]
[[ apply SLLseg_append(head, #vs1, #v, prev) ]]
};
[prev + 1] := y;
[[ assert {bind: #svs, #sv} SLLseg(head, prev, #svs) * (prev -b> #sv, y) ]];
[[ apply SSLseg_append(head, #svs, #sv, y) ]];
[[ apply SLLseg_append(head, #svs, #sv, y) ]];
[[ assert (SLLseg(head, y, #vs)) ]]; // <-- add deliberate bug to #vx
[[ apply SLLseg_concat_SLL(head, y) ]]
};
Expand All @@ -395,11 +395,11 @@ function SLL_concat_iter(x, y){
[[ unfold SLL(next, #vs2) ]];
prev := next;
next := [next + 1];
[[ apply SSLseg_append(head, #vs1, #v, prev) ]]
[[ apply SLLseg_append(head, #vs1, #v, prev) ]]
};
[prev + 1] := y;
[[ assert {bind:#svs, #sv} SLLseg(head, prev, #svs) * (prev -b> #sv, y) ]];
[[ apply SSLseg_append(head, #svs, #sv, y) ]];
[[ apply SLLseg_append(head, #svs, #sv, y) ]];
[[ apply SLLseg_concat_SLL(head, y) ]]
};
return head
Expand Down Expand Up @@ -436,11 +436,11 @@ function SLL_copy_iter(x){
[p + 1] := c;
p := c;
t := [t + 1];
[[ apply SSLseg_append(x, #alpha1, v, t) ]];
[[ apply SSLseg_append(y, #alpha3, #a, p) ]]
[[ apply SLLseg_append(x, #alpha1, v, t) ]];
[[ apply SLLseg_append(y, #alpha3, #a, p) ]]
};
[[ assert {bind: #alpha3} SLLseg(y, p, #alpha3) ]];
[[ apply SSLseg_append(y, #alpha3, v, null) ]];
[[ apply SLLseg_append(y, #alpha3, v, null) ]];
[[ apply SLLseg_to_SLL(x) ]];
[[ apply SLLseg_to_SLL(y) ]]
};
Expand All @@ -463,7 +463,7 @@ function SLL_length_iter(x) {
[[ assert {bind: #v, #z} #y -b> #v, #z ]];
y := [y+1];
n := n+1;
[[ apply SSLseg_append(x, #nvx, #v, y) ]]
[[ apply SLLseg_append(x, #nvx, #v, y) ]]
};
[[ fold SLL(null, [])]];
[[ unfold SLL(null, #nvy)]];
Expand Down Expand Up @@ -507,7 +507,7 @@ function SLL_member_iter(x, k) {
v := [next];
found := (v = k);
next := [next + 1];
[[ apply SSLseg_append(x, #beta, #v, next) ]];
[[ apply SLLseg_append(x, #beta, #v, next) ]];
[[ unfold list_member(#gamma, k, #rg) ]];
[[ apply list_member_append(#beta, k, false, #v) ]]
};
Expand Down
6 changes: 3 additions & 3 deletions debug-ui/examples/wisl/verify/gil/list_length_iter.gil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ lemma SLLseg_to_SLL(x)
#nv, #nnext]; apply SLLseg_to_SLL(#nnext)
} *]

lemma SSLseg_append(x, vs, v, z)
lemma SLLseg_append(x, vs, v, z)
[[ emp * (x == #x) * (vs == #vs) * (v == #v) * (z == #z) *
SLLseg(#x, #y, #vs) * <cell>(#wisl__1, 0i; #v) *
<bound>(#wisl__1; 2i) * <cell>(#wisl__1, 1i; #z) *
Expand All @@ -26,7 +26,7 @@ lemma SSLseg_append(x, vs, v, z)
<cell>(#wisl__0, 1i; #nnext) * types(#wisl__0 : Obj) *
(#x == {{ #wisl__0, 0i }}) * SLLseg(#nnext, #y, #nvs) *
(#vs == l+ ({{ #nv }}, #nvs))) [bind: #wisl__0,
#nv, #nnext, #nvs]; apply SSLseg_append(#nnext, #nvs, #v, #z) ;
#nv, #nnext, #nvs]; apply SLLseg_append(#nnext, #nvs, #v, #z) ;
fold SLLseg(#x, #z, l+ (#vs, {{ #v }}))
} else { fold SLLseg(#y, #z, {{ #v }}) } *]
pred SLL(+x, vs : List) : (x == null) * (vs == {{ }}),
Expand Down Expand Up @@ -70,7 +70,7 @@ proc SLL_length_iter_loop0(n, x, y) {
y := l-nth(gvar1, 2i);
gvar2 := "i__add"(n, 1i);
n := gvar2;
apply SSLseg_append(x, #nvx, #v, y) ;
apply SLLseg_append(x, #nvx, #v, y) ;
loopretvar__ := "SLL_length_iter_loop0"(n, x, y);
goto endif0;
else0: loopretvar__ := {{ n, x, y }};
Expand Down
6 changes: 3 additions & 3 deletions debug-ui/examples/wisl/verify/list_length_iter.wisl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ predicate SLLseg(+x, y, vs) {
//
// Lemma: appending a given value to a given SLLseg
//
lemma SSLseg_append {
lemma SLLseg_append {
statement:
forall x, vs, v, z.
SLLseg(x, #y, vs) * (#y -b> v, z) |- SLLseg(x, z, vs @ [ v ])
Expand All @@ -32,7 +32,7 @@ lemma SSLseg_append {
assert {bind: #nv, #nnext, #nvs}
(x -b> #nv, #nnext) * SLLseg(#nnext, #y, #nvs) *
(vs == #nv :: #nvs);
apply SSLseg_append(#nnext, #nvs, v, z);
apply SLLseg_append(#nnext, #nvs, v, z);
fold SLLseg(x, z, vs @ [ v ])
} else {
fold SLLseg(#y, z, [ v ])
Expand Down Expand Up @@ -68,7 +68,7 @@ function SLL_length_iter(x) {
[[ assert {bind: #v, #z} #y -b> #v, #z ]];
y := [y+1];
n := n+1;
[[ apply SSLseg_append(x, #nvx, #v, y) ]]
[[ apply SLLseg_append(x, #nvx, #v, y) ]]
};
[[ unfold SLL(null, #nvy)]];
[[ apply SLLseg_to_SLL(x) ]];
Expand Down
26 changes: 13 additions & 13 deletions wisl/examples/SLL_ex_complete.wisl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -232,7 +232,7 @@ predicate SLLseg(+x, y, vs) {
//
// Lemma: appending a given value to a given SLLseg
//
lemma SSLseg_append {
lemma SLLseg_append {
statement:
forall x, vs, v, z.
SLLseg(x, #y, vs) * (#y -b> v, z) |- SLLseg(x, z, vs @ [ v ])
Expand All @@ -243,7 +243,7 @@ lemma SSLseg_append {
assert {bind: #nv, #nnext, #nvs}
(x -b> #nv, #nnext) * SLLseg(#nnext, #y, #nvs) *
(vs == #nv :: #nvs);
apply SSLseg_append(#nnext, #nvs, v, z);
apply SLLseg_append(#nnext, #nvs, v, z);
fold SLLseg(x, z, vs @ [ v ])
} else {
fold SLLseg(#y, z, [ v ])
Expand Down Expand Up @@ -299,11 +299,11 @@ function SLL_append_iter(x, k){
[[ assert {bind: #prev} prev == #prev ]];
prev := next;
next := [next + 1];
[[ apply SSLseg_append(head, #vs1, #v, prev) ]]
[[ apply SLLseg_append(head, #vs1, #v, prev) ]]
};
[prev + 1] := y;
[[ assert {bind: #svs, #sv} SLLseg(head, prev, #svs) * (prev -b> #sv, y) ]];
[[ apply SSLseg_append(head, #svs, #sv, y) ]];
[[ apply SLLseg_append(head, #svs, #sv, y) ]];
[[ assert (SLLseg(head, y, #vx)) ]];
[[ apply SLLseg_concat_SLL(head, y) ]]
};
Expand All @@ -327,11 +327,11 @@ function SLL_append_node_iter(x, y){
[[ assert {bind: #prev} prev == #prev ]];
prev := next;
next := [next + 1];
[[ apply SSLseg_append(head, #vs1, #v, prev) ]]
[[ apply SLLseg_append(head, #vs1, #v, prev) ]]
};
[prev + 1] := y;
[[ assert {bind: #svs, #sv} SLLseg(head, prev, #svs) * (prev -b> #sv, y) ]];
[[ apply SSLseg_append(head, #svs, #sv, y) ]];
[[ apply SLLseg_append(head, #svs, #sv, y) ]];
[[ assert (SLLseg(head, y, #vs)) ]]; // <-- add deliberate bug to #vx
[[ apply SLLseg_concat_SLL(head, y) ]]
};
Expand All @@ -355,11 +355,11 @@ function SLL_concat_iter(x, y){
[[ assert {bind: #prev} prev == #prev ]];
prev := next;
next := [next + 1];
[[ apply SSLseg_append(head, #vs1, #v, prev) ]]
[[ apply SLLseg_append(head, #vs1, #v, prev) ]]
};
[prev + 1] := y;
[[ assert {bind:#svs, #sv} SLLseg(head, prev, #svs) * (prev -b> #sv, y) ]];
[[ apply SSLseg_append(head, #svs, #sv, y) ]];
[[ apply SLLseg_append(head, #svs, #sv, y) ]];
[[ apply SLLseg_concat_SLL(head, y) ]]
};
return head
Expand Down Expand Up @@ -392,11 +392,11 @@ function SLL_copy_iter(x){
[p + 1] := c;
p := c;
t := [t + 1];
[[ apply SSLseg_append(x, #alpha1, v, t) ]];
[[ apply SSLseg_append(y, #alpha3, #a, p) ]]
[[ apply SLLseg_append(x, #alpha1, v, t) ]];
[[ apply SLLseg_append(y, #alpha3, #a, p) ]]
};
[[ assert {bind: #alpha3} SLLseg(y, p, #alpha3) ]];
[[ apply SSLseg_append(y, #alpha3, v, null) ]];
[[ apply SLLseg_append(y, #alpha3, v, null) ]];
[[ apply SLLseg_to_SLL(x) ]];
[[ apply SLLseg_to_SLL(y) ]]
};
Expand All @@ -417,7 +417,7 @@ function SLL_length_iter(x) {
[[ assert {bind: #v, #z} #y -b> #v, #z ]];
y := [y+1];
n := n+1;
[[ apply SSLseg_append(x, #nvx, #v, y) ]]
[[ apply SLLseg_append(x, #nvx, #v, y) ]]
};
[[ unfold SLL(null, #nvy)]];
[[ apply SLLseg_to_SLL(x) ]];
Expand Down Expand Up @@ -457,7 +457,7 @@ function SLL_member_iter(x, k) {
v := [next];
found := (v = k);
next := [next + 1];
[[ apply SSLseg_append(x, #beta, #v, next) ]];
[[ apply SLLseg_append(x, #beta, #v, next) ]];
[[ unfold list_member(#gamma, k, #rg) ]];
[[ apply list_member_append(#beta, k, false, #v) ]]
};
Expand Down
Loading

0 comments on commit 3460b07

Please sign in to comment.