Prusti 2.2.1 Example

[EmilyOng]

Code example from Section 2.2.1 in Modular Specification and Verification of Closures in Rust:

let mut i = 1;
let mut j = 2; // j is captured by (mutable) reference below:
let mut cl = |x: &mut i32| -> i32 { j += *x; *x += 1; j + *x };
let r = cl(&mut i);
assert_eq!(i, 2); // the closure's side effect on its argument
assert_eq!(j, 3); // the closure's side effect on its captured state
assert_eq!(r, 5); // the closure's result

Direct translation

Currently, this form of let bindings are not expected. ```ocaml let closure_with_effect () (*@ ex i; ex j; ens i->2*j->3 /\ res=5 @*) = let i = ref 1 and j = ref 2 in let cl x = j := !j + !x; x := !x + 1; !j + !x in cl i ```

Using Heifer:

let closure_with_effect ()
(*@ ex i; ex j; ens i->2*j->3 /\ res=5 @*)
= let i = ref 1 in
  let j = ref 2 in
  let cl x =
    j := !j + !x;
    x := !x + 1;
    !j + !x in
  cl i

Staged Specification for cl(x, res)

``` cl(x,res) = req x->a * j->b // If x != j ens j->b+a * x->a+1 /\ res=b+a+a+1 req x->a /\ x=j // If x = j (sep. logic notation) ens j->2a+1 /\ res=2a+1+a+1 ```

[EmilyOng]

For this to work, we need to fix the missing bindings for j, as it was mentioned earlier. For example:

let let_with_and ()
= let i = ref 1 and j = ref 2 in
  ()

The parsed program is:

let i = ref 1 in                     
()

And, the normed specification is ex v2; Norm(v2->1/\res=()).

The tokens are:

LET LIDENT LPAREN RPAREN EQUAL LET LIDENT EQUAL LIDENT INT AND LIDENT EQUAL LIDENT INT IN LPAREN RPAREN EOF

[EmilyOng]

In parser.mly, a consideration for expr AND expr may be needed here, or there might be some other parts I'm still looking at.

[dariusf]

You can work around this for now like this, as the bindings aren't mutually recursive:

let let_with_and ()
= let i = ref 1 in
  let j = ref 2 in
  ()

The bug is in how we translate the OCaml AST to our core_lang - we're only using the first value binding.

If you would like to try fixing this, I think it's fine to translate it to the workaround for now, and leave mutual recursion for later.