//# init
// Tests for parsing specifications

// TODO: (DD, 1/6/20) This file could be integrated with the prover test framework
// in language/move-prover/byte-code-to-boogie/tests
// so we could run these through boogie.

// Test parsing the conditions themselves relative to return values, acquires clauses
//# publish
module 0x1.TestConditions {

  struct T has key { i: u64 }

  public ensures_alone()
  ensures true
  {
      label b0: return;
  }

  public requires_alone()
  requires true
  {
      label b0: return;
  }

  public aborts_if_alone()
  aborts_if true   //! postcondition might not hold
  {
      label b0: return;
  }

  public succeeds_if_alone()
  succeeds_if true
  {
      label b0: return;
  }

  public ensures_with_return(): bool
  ensures true
  {
      label b0: return true;
  }

  public ensures_with_acquires()
  acquires T
  ensures true
  {
    label b0:
      _ = borrow_global<T>(0x0);
      return;
  }

  public ensures_with_return_acquires(): bool
  acquires T
  ensures true
  {
    label b0:
      _ = borrow_global<T>(0x0);
      return true;
  }

  public multiple_ensures()
  ensures true
  ensures false
  ensures true
  {
      label b0: return;
  }

  public all_together_now(): bool
  acquires T
  requires true
  requires false
  ensures true
  ensures false
  aborts_if true
  aborts_if false
  succeeds_if true
  succeeds_if false
  {
    label b0:
      _ = borrow_global<T>(0x0);
      return true;
  }

}

// check that we can parse the language of spec expressions without access paths
//# publish
module 0x1.TestSpecExp {

  struct T { b: bool }
  struct T1<Name> { b: Name }

  public ensures_ret()
  ensures RET
  {
      label b0: return;
  }

  public ensures_multiple_ret()
  ensures RET(0)
  ensures RET(1)
  {
      label b0: return;
  }


  public ensures_txn_sender()
  ensures txn_sender {
      label b0: return;
  }

  public ensures_addr()
  ensures 0x0
  {
      label b0: return;
  }

  public ensures_formal(b: bool)
  ensures b
  {
      label b0: return;
  }

  public ensures_global(a: address)
  ensures global<Self.T>(a)
  {
      label b0: return;
  }


  public ensures_generic_global(a: address)
  ensures global<Self.T1<bool>>(a)
  {
      label b0: return;
  }

  public ensures_exists(a: address)
  ensures global_exists<Self.T>(a)
  {
      label b0: return;
  }

  public ensures_exists_generic(a: address)
  ensures global_exists<Self.T1<bool>>(a)
  {
      label b0: return;
  }

  public ensures_old(b: bool)
  ensures old(b)
  {
      label b0: return;
  }

  public ensures_old_global(a: address)
  ensures old(global<Self.T>(a))
  {
      label b0: return;
  }

}

// check that we can handle the trickier case of access paths
//# publish
module 0x1.TestEnsuresAccessPath {

  struct T { b: bool, a: address }
  struct T1 { y: Self.T }
  struct T2 { x: Self.T1 }


  public ensures_access_path(t: Self.T): Self.T
  ensures t.b
  {
      label b0: return move(t);
  }

  public ensures_access_path2(t: Self.T1): Self.T1
  ensures t.y.b
  {
      label b0: return move(t);
  }

  public ensures_access_path3(t: Self.T2): Self.T2
  ensures t.x.y.b
  {
      label b0: return move(t);
  }

  public ensures_old_access_path(t: Self.T): Self.T
  ensures old(t.b)
  {
      label b0: return move(t);
  }

  public ensures_exists_access_path(t: Self.T): Self.T
  ensures global_exists<Self.T>(t.a)
  {
      label b0: return move(t);
  }

  public ensures_global_access_path(t: Self.T): Self.T
  ensures global<Self.T>(t.a)
  {
      label b0: return move(t);
  }

}

//# publish
module 0x1.TestBinaryOps {
  struct T { b: bool }
  struct Pair { x: u64, y: u64}

  public ret_eq_seven(): u64
  ensures RET == 7
  {
      label b0: return 7;
  }

  public ret_neq_seven(): u64
  ensures RET != 7
  {
      label b0: return 5;
  }

  public ret_add(x: u64): u64
  ensures RET == x + 1
  {
      label b0: return move(x) + 1;
  }

  public ret_sub(x: u64): u64
  ensures RET - 1 == x
  {
      label b0: return move(x) + 1;
  }

  public ret_unop(x: bool): bool
  ensures RET == !x
  {
      label b0: return !move(x);
  }

  public ret_access_path_exp(p: &Self.Pair): u64
  ensures RET == p.x + p.y
  {
      label b0: return *&copy(p).Pair::y;
  }

  public ret_implies(x: u64): u64
  ensures x >= 4 ==> RET == x % 4
  ensures x < 4  ==> RET == x
  {
      label b0: return move(x) % 4;
  }

  public ret_spec_function(x: u64): u64
  ensures some_function(x, x) > RET
  {
      label b0: return move(x);
  }
}