move-stackless-bytecode 0.1.5

============ initial translation from Move ================

[variant baseline]
fun Test::branching_result($t0|is_div: bool, $t1|a: u64, $t2|b: u64): u64 {
     var $t3|tmp#$3: u64
     var $t4: bool
     var $t5: u64
     var $t6: u64
     var $t7: u64
     var $t8: u64
     var $t9: u64
     var $t10: u64
     var $t11: u64
  0: $t4 := move($t0)
  1: if ($t4) goto 2 else goto 8
  2: label L0
  3: $t5 := move($t1)
  4: $t6 := move($t2)
  5: $t7 := /($t5, $t6)
  6: $t3 := $t7
  7: goto 14
  8: label L2
  9: $t8 := move($t1)
 10: $t9 := move($t2)
 11: $t10 := *($t8, $t9)
 12: $t3 := $t10
 13: goto 14
 14: label L3
 15: $t11 := move($t3)
 16: return $t11
}


[variant baseline]
fun Test::implicit_and_explicit_abort($t0|a: u64, $t1|b: u64): u64 {
     var $t2: u64
     var $t3: u64
     var $t4: bool
     var $t5: u64
     var $t6: u64
     var $t7: u64
     var $t8: u64
  0: $t2 := copy($t1)
  1: $t3 := 0
  2: $t4 := !=($t2, $t3)
  3: if ($t4) goto 4 else goto 7
  4: label L0
  5: $t5 := 22
  6: abort($t5)
  7: label L2
  8: $t6 := move($t0)
  9: $t7 := move($t1)
 10: $t8 := /($t6, $t7)
 11: return $t8
}


[variant baseline]
fun Test::multiple_results($t0|a: u64, $t1|b: u64): (u64, u64) {
     var $t2: u64
     var $t3: u64
     var $t4: u64
     var $t5: u64
     var $t6: u64
     var $t7: u64
  0: $t2 := copy($t0)
  1: $t3 := copy($t1)
  2: $t4 := /($t2, $t3)
  3: $t5 := move($t0)
  4: $t6 := move($t1)
  5: $t7 := %($t5, $t6)
  6: return ($t4, $t7)
}


[variant baseline]
fun Test::mut_ref_param($t0|r: &mut Test::R): u64 {
     var $t1|x: u64
     var $t2: &mut Test::R
     var $t3: &u64
     var $t4: u64
     var $t5: &mut Test::R
     var $t6: &u64
     var $t7: u64
     var $t8: u64
     var $t9: u64
     var $t10: &mut Test::R
     var $t11: &mut u64
     var $t12: u64
  0: $t2 := copy($t0)
  1: $t3 := borrow_field<Test::R>.v($t2)
  2: $t4 := read_ref($t3)
  3: $t1 := $t4
  4: $t5 := copy($t0)
  5: $t6 := borrow_field<Test::R>.v($t5)
  6: $t7 := read_ref($t6)
  7: $t8 := 1
  8: $t9 := -($t7, $t8)
  9: $t10 := move($t0)
 10: $t11 := borrow_field<Test::R>.v($t10)
 11: write_ref($t11, $t9)
 12: $t12 := move($t1)
 13: return $t12
}


[variant baseline]
fun Test::ref_param($t0|r: &Test::R): u64 {
     var $t1: &Test::R
     var $t2: &u64
     var $t3: u64
  0: $t1 := move($t0)
  1: $t2 := borrow_field<Test::R>.v($t1)
  2: $t3 := read_ref($t2)
  3: return $t3
}


[variant baseline]
fun Test::ref_param_return_ref($t0|r: &Test::R): &u64 {
     var $t1: &Test::R
     var $t2: &u64
  0: $t1 := move($t0)
  1: $t2 := borrow_field<Test::R>.v($t1)
  2: return $t2
}


[variant baseline]
fun Test::resource_with_old($t0|val: u64) {
     var $t1|r: &mut Test::R
     var $t2: address
     var $t3: bool
     var $t4: bool
     var $t5: u64
     var $t6: address
     var $t7: &mut Test::R
     var $t8: &mut Test::R
     var $t9: &u64
     var $t10: u64
     var $t11: u64
     var $t12: u64
     var $t13: &mut Test::R
     var $t14: &mut u64
  0: $t2 := 0x0
  1: $t3 := exists<Test::R>($t2)
  2: $t4 := !($t3)
  3: if ($t4) goto 4 else goto 7
  4: label L0
  5: $t5 := 33
  6: abort($t5)
  7: label L2
  8: $t6 := 0x0
  9: $t7 := borrow_global<Test::R>($t6)
 10: $t1 := $t7
 11: $t8 := copy($t1)
 12: $t9 := borrow_field<Test::R>.v($t8)
 13: $t10 := read_ref($t9)
 14: $t11 := move($t0)
 15: $t12 := +($t10, $t11)
 16: $t13 := move($t1)
 17: $t14 := borrow_field<Test::R>.v($t13)
 18: write_ref($t14, $t12)
 19: return ()
}

============ after pipeline `spec_instrumentation` ================

[variant verification]
fun Test::branching_result($t0|is_div: bool, $t1|a: u64, $t2|b: u64): u64 {
     var $t3|tmp#$3: u64
     var $t4: num
  0: if ($t0) goto 1 else goto 4
  1: label L0
  2: $t3 := /($t1, $t2) on_abort goto 12 with $t4
  3: goto 6
  4: label L2
  5: $t3 := *($t1, $t2) on_abort goto 12 with $t4
  6: label L3
  7: label L4
     # VC: function does not abort under this condition at tests/spec_instrumentation/fun_spec.move:27:6+50
  8: assert Not(And($t0, Eq<u64>($t2, 0)))
     # VC: post-condition does not hold at tests/spec_instrumentation/fun_spec.move:28:6+35
  9: assert Implies($t0, Eq<u64>($t3, Div($t1, $t2)))
     # VC: post-condition does not hold at tests/spec_instrumentation/fun_spec.move:29:6+36
 10: assert Implies(Not($t0), Eq<u64>($t3, Mul($t1, $t2)))
 11: return $t3
 12: label L5
     # VC: abort not covered by any of the `aborts_if` clauses at tests/spec_instrumentation/fun_spec.move:26:2+165
 13: assert And($t0, Eq<u64>($t2, 0))
     # VC: abort code not covered by any of the `aborts_if` or `aborts_with` clauses at tests/spec_instrumentation/fun_spec.move:26:2+165
 14: assert And(And($t0, Eq<u64>($t2, 0)), Eq(-1, $t4))
 15: abort($t4)
}


[variant verification]
fun Test::implicit_and_explicit_abort($t0|a: u64, $t1|b: u64): u64 {
     var $t2: u64
     var $t3: bool
     var $t4: u64
     var $t5: num
     var $t6: u64
  0: $t2 := 0
  1: $t3 := !=($t1, $t2)
  2: if ($t3) goto 3 else goto 7
  3: label L0
  4: $t4 := 22
  5: $t5 := move($t4)
  6: goto 14
  7: label L2
  8: $t6 := /($t0, $t1) on_abort goto 14 with $t5
  9: label L3
     # VC: function does not abort under this condition at tests/spec_instrumentation/fun_spec.move:9:6+25
 10: assert Not(Eq<u64>($t1, 0))
     # VC: function does not abort under this condition at tests/spec_instrumentation/fun_spec.move:10:6+17
 11: assert Not(Eq<u64>($t0, 0))
     # VC: post-condition does not hold at tests/spec_instrumentation/fun_spec.move:11:6+24
 12: assert Eq<u64>($t6, Div($t0, $t1))
 13: return $t6
 14: label L4
     # VC: abort not covered by any of the `aborts_if` clauses at tests/spec_instrumentation/fun_spec.move:8:2+121
 15: assert Or(Eq<u64>($t1, 0), Eq<u64>($t0, 0))
     # VC: abort code not covered by any of the `aborts_if` or `aborts_with` clauses at tests/spec_instrumentation/fun_spec.move:8:2+121
 16: assert Or(And(Eq<u64>($t1, 0), Eq(22, $t5)), Eq<u64>($t0, 0))
 17: abort($t5)
}


[variant verification]
fun Test::multiple_results($t0|a: u64, $t1|b: u64): (u64, u64) {
     var $t2: u64
     var $t3: num
     var $t4: u64
  0: $t2 := /($t0, $t1) on_abort goto 7 with $t3
  1: $t4 := %($t0, $t1) on_abort goto 7 with $t3
  2: label L1
     # VC: function does not abort under this condition at tests/spec_instrumentation/fun_spec.move:18:6+40
  3: assert Not(Eq<u64>($t1, 0))
     # VC: post-condition does not hold at tests/spec_instrumentation/fun_spec.move:19:6+26
  4: assert Eq<u64>($t2, Div($t0, $t1))
     # VC: post-condition does not hold at tests/spec_instrumentation/fun_spec.move:20:6+26
  5: assert Eq<u64>($t4, Mod($t0, $t1))
  6: return ($t2, $t4)
  7: label L2
     # VC: abort not covered by any of the `aborts_if` clauses at tests/spec_instrumentation/fun_spec.move:17:2+136
  8: assert Eq<u64>($t1, 0)
     # VC: abort code not covered by any of the `aborts_if` or `aborts_with` clauses at tests/spec_instrumentation/fun_spec.move:17:2+136
  9: assert And(Eq<u64>($t1, 0), Eq(-1, $t3))
 10: abort($t3)
}


[variant verification]
fun Test::mut_ref_param($t0|r: &mut Test::R): u64 {
     var $t1|x: u64
     var $t2: Test::R
     var $t3: u64
     var $t4: u64
     var $t5: u64
     var $t6: u64
     var $t7: num
     var $t8: &mut u64
  0: $t2 := read_ref($t0)
  1: $t3 := get_field<Test::R>.v($t0)
  2: $t4 := get_field<Test::R>.v($t0)
  3: $t5 := 1
  4: $t6 := -($t4, $t5) on_abort goto 15 with $t7
  5: $t8 := borrow_field<Test::R>.v($t0)
  6: write_ref($t8, $t6)
  7: write_back[Reference($t0).v (u64)]($t8)
  8: trace_local[r]($t0)
  9: trace_local[r]($t0)
 10: label L1
     # VC: function does not abort under this condition at tests/spec_instrumentation/fun_spec.move:67:6+42
 11: assert Not(Eq<u64>(select Test::R.v($t2), 0))
     # VC: post-condition does not hold at tests/spec_instrumentation/fun_spec.move:68:6+27
 12: assert Eq<u64>($t3, select Test::R.v($t2))
     # VC: post-condition does not hold at tests/spec_instrumentation/fun_spec.move:69:6+28
 13: assert Eq<u64>(select Test::R.v($t0), Add(select Test::R.v($t2), 1))
 14: return $t3
 15: label L2
     # VC: abort not covered by any of the `aborts_if` clauses at tests/spec_instrumentation/fun_spec.move:66:2+138
 16: assert Eq<u64>(select Test::R.v($t2), 0)
     # VC: abort code not covered by any of the `aborts_if` or `aborts_with` clauses at tests/spec_instrumentation/fun_spec.move:66:2+138
 17: assert And(Eq<u64>(select Test::R.v($t2), 0), Eq(-1, $t7))
 18: abort($t7)
}


[variant verification]
fun Test::ref_param($t0|r: Test::R): u64 {
     var $t1: u64
  0: $t1 := get_field<Test::R>.v($t0)
  1: label L1
     # VC: post-condition does not hold at tests/spec_instrumentation/fun_spec.move:51:6+22
  2: assert Eq<u64>($t1, select Test::R.v($t0))
  3: return $t1
}


[variant verification]
fun Test::ref_param_return_ref($t0|r: Test::R): u64 {
     var $t1: u64
  0: $t1 := get_field<Test::R>.v($t0)
  1: label L1
     # VC: post-condition does not hold at tests/spec_instrumentation/fun_spec.move:58:6+22
  2: assert Eq<u64>($t1, select Test::R.v($t0))
  3: return $t1
}


[variant verification]
fun Test::resource_with_old($t0|val: u64) {
     var $t1|r: &mut Test::R
     var $t2: address
     var $t3: bool
     var $t4: bool
     var $t5: u64
     var $t6: num
     var $t7: address
     var $t8: &mut Test::R
     var $t9: u64
     var $t10: u64
     var $t11: &mut u64
  0: assume Gt($t0, 0)
  1: assume CanModify<Test::R>(0)
  2: @0 := save_mem(Test::R)
  3: $t2 := 0x0
  4: $t3 := exists<Test::R>($t2)
  5: $t4 := !($t3)
  6: if ($t4) goto 7 else goto 11
  7: label L0
  8: $t5 := 33
  9: $t6 := move($t5)
 10: goto 26
 11: label L2
 12: $t7 := 0x0
     # VC: caller does not have permission to modify `Test::R` at given address at tests/spec_instrumentation/fun_spec.move:36:14+17
 13: assert CanModify<Test::R>($t7)
 14: $t8 := borrow_global<Test::R>($t7) on_abort goto 26 with $t6
 15: $t9 := get_field<Test::R>.v($t8)
 16: $t10 := +($t9, $t0) on_abort goto 26 with $t6
 17: $t11 := borrow_field<Test::R>.v($t8)
 18: write_ref($t11, $t10)
 19: write_back[Reference($t8).v (u64)]($t11)
 20: write_back[Test::R@]($t8)
 21: label L3
     # VC: function does not abort under this condition at tests/spec_instrumentation/fun_spec.move:41:6+35
 22: assert Not(Not(exists[@0]<Test::R>(0)))
     # VC: function does not abort under this condition at tests/spec_instrumentation/fun_spec.move:42:6+58
 23: assert Not(Ge(Add(select Test::R.v(global[@0]<Test::R>(0)), $t0), 18446744073709551615))
     # VC: post-condition does not hold at tests/spec_instrumentation/fun_spec.move:43:6+58
 24: assert Eq<u64>(select Test::R.v(global<Test::R>(0)), Add(select Test::R.v(global[@0]<Test::R>(0)), $t0))
 25: return ()
 26: label L4
     # VC: abort not covered by any of the `aborts_if` clauses at tests/spec_instrumentation/fun_spec.move:39:2+250
 27: assert Or(Not(exists[@0]<Test::R>(0)), Ge(Add(select Test::R.v(global[@0]<Test::R>(0)), $t0), 18446744073709551615))
     # VC: abort code not covered by any of the `aborts_if` or `aborts_with` clauses at tests/spec_instrumentation/fun_spec.move:39:2+250
 28: assert Or(And(Not(exists[@0]<Test::R>(0)), Eq(33, $t6)), Ge(Add(select Test::R.v(global[@0]<Test::R>(0)), $t0), 18446744073709551615))
 29: abort($t6)
}



==== spec-instrumenter input specs ====

fun Test::branching_result[baseline]
spec {
  aborts_if And($t0, Eq<u64>($t2, 0));
  ensures Implies($t0, Eq<u64>(result0(), Div($t1, $t2)));
  ensures Implies(Not($t0), Eq<u64>(result0(), Mul($t1, $t2)));
}

fun Test::branching_result[verification]
spec {
  aborts_if And($t0, Eq<u64>($t2, 0));
  ensures Implies($t0, Eq<u64>(result0(), Div($t1, $t2)));
  ensures Implies(Not($t0), Eq<u64>(result0(), Mul($t1, $t2)));
}

fun Test::implicit_and_explicit_abort[baseline]
spec {
  aborts_if Eq<u64>($t1, 0);
  aborts_if Eq<u64>($t0, 0);
  ensures Eq<u64>(result0(), Div($t0, $t1));
}

fun Test::implicit_and_explicit_abort[verification]
spec {
  aborts_if Eq<u64>($t1, 0);
  aborts_if Eq<u64>($t0, 0);
  ensures Eq<u64>(result0(), Div($t0, $t1));
}

fun Test::multiple_results[baseline]
spec {
  aborts_if Eq<u64>($t1, 0);
  ensures Eq<u64>(result0(), Div($t0, $t1));
  ensures Eq<u64>(result1(), Mod($t0, $t1));
}

fun Test::multiple_results[verification]
spec {
  aborts_if Eq<u64>($t1, 0);
  ensures Eq<u64>(result0(), Div($t0, $t1));
  ensures Eq<u64>(result1(), Mod($t0, $t1));
}

fun Test::mut_ref_param[baseline]
spec {
  aborts_if Eq<u64>(select Test::R.v($t0), 0);
  ensures Eq<u64>(result0(), Old<u64>(select Test::R.v($t0)));
  ensures Eq<u64>(select Test::R.v($t0), Add(Old<u64>(select Test::R.v($t0)), 1));
}

fun Test::mut_ref_param[verification]
spec {
  aborts_if Eq<u64>(select Test::R.v($t0), 0);
  ensures Eq<u64>(result0(), Old<u64>(select Test::R.v($t0)));
  ensures Eq<u64>(select Test::R.v($t0), Add(Old<u64>(select Test::R.v($t0)), 1));
}

fun Test::ref_param[baseline]
spec {
  ensures Eq<u64>(result0(), select Test::R.v($t0));
}

fun Test::ref_param[verification]
spec {
  ensures Eq<u64>(result0(), select Test::R.v($t0));
}

fun Test::ref_param_return_ref[baseline]
spec {
  ensures Eq<u64>(result0(), select Test::R.v($t0));
}

fun Test::ref_param_return_ref[verification]
spec {
  ensures Eq<u64>(result0(), select Test::R.v($t0));
}

fun Test::resource_with_old[baseline]
spec {
  requires Gt($t0, 0);
  aborts_if Not(exists<Test::R>(0));
  aborts_if Ge(Add(select Test::R.v(global<Test::R>(0)), $t0), 18446744073709551615);
  ensures Eq<u64>(select Test::R.v(global<Test::R>(0)), Add(select Test::R.v(Old<Test::R>(global<Test::R>(0))), $t0));
  modifies global<Test::R>(0);
}

fun Test::resource_with_old[verification]
spec {
  requires Gt($t0, 0);
  aborts_if Not(exists<Test::R>(0));
  aborts_if Ge(Add(select Test::R.v(global<Test::R>(0)), $t0), 18446744073709551615);
  ensures Eq<u64>(select Test::R.v(global<Test::R>(0)), Add(select Test::R.v(Old<Test::R>(global<Test::R>(0))), $t0));
  modifies global<Test::R>(0);
}