Provably Correct Smart Contracts using DeepSEA

Daniel Britten

Ethereum Engineering Group Meetup 2023

Overall Goal: Demonstate a technique for showing the correctness of smart contracts

Overview:

• Theorem-proving example in the proof assistant Coq
• DeepSEA example: compilation
• DeepSEA example: proof
• Correctness property of a Crowdfunding contract
• Paper overviews

Introduction to theorem-proving in Coq

Example: Even and odd numbers

Definition Even (n : nat) := exists k, n = 2 * k.
Definition Odd  (m : nat) := exists l, m = 2 * l + 1.

Lemma EvenToOdd : forall (n : nat), Even n -> Odd (n + 1).
forall n : nat, Even n -> Odd (n + 1)
Proof.
forall n : nat, Even n -> Odd (n + 1)
  intros.
n: nat
H: Even n
Odd (n + 1)
  unfold Even in H.
n: nat
H: exists k : nat, n = 2 * k
Odd (n + 1)
  destruct H as [k].
n, k: nat
H: n = 2 * k
Odd (n + 1)
  unfold Odd.
n, k: nat
H: n = 2 * k
exists l : nat, n + 1 = 2 * l + 1
  exists k.
n, k: nat
H: n = 2 * k
n + 1 = 2 * k + 1
  rewrite <- H.
n, k: nat
H: n = 2 * k
n + 1 = n + 1
  reflexivity.
Qed.

DeepSEA

Introduction to creating a DeepSEA smart contract

Example: Trivial contract converting bool to int

object signature trivial = {
    const boolToInt : bool -> int
}

object Trivial : trivial {
    let boolToInt b =
      if b then 1 else 0
}

layer CONTRACT = { o = Trivial }

object signature trivial = {
    const boolToInt : bool -> int;
    boolToIntTracker : bool -> int
}

object Trivial : trivial {
    let seenTrueYet : bool := false

    let boolToInt b =
      if b then 1 else 0

    let boolToIntTracker b =
      if b then
        begin
            seenTrueYet := true;
            1
        end
      else 0
}

layer CONTRACT = { o = Trivial }

$ dsc trivial.ds bytecode
5b60005b60206109205101610920525b61022660006020610920510301525b60006020
610920510301516101005260206101002060006020610920510301525b600060006020
61092051030151555b60206109205103610920525b60005b9050386300000073600039
386000f35b60006000fd5b610940610920527c01000000000000000000000000000000
000000000000000000000000006000350480635192f3c01463000000495780631e01e7
071463000000965760006000fd5b6004355b60006109205101610920525b8063000000
67576300000085565b600190505b60006109205103610920525b805b90506000526020
6000f35b60009050630000006c565b60006000fd5b6004355b60206109205101610920
525b8063000000b4576300000111565b61022660006020610920510301525b60006020
610920510301516101005260206101002060006020610920510301525b600160006020
61092051030151555b600190505b60206109205103610920525b805b90506000526020
6000f35b6000905063000000f8565b60006000fd

$ dsc trivial.ds abi

[ {"type":"constructor",
  "name":"constructor",
  "inputs":[], "outputs":[], "payable":false,
  "constant":false, "stateMutability":"nonpayable"},
{"type":"function",
  "name":"boolToInt",
  "inputs":[{"name":"b", "type":"bool"}],
  "outputs":[{"name":"", "type":"uint256"}],
  "payable":false,
  "constant":true,
  "stateMutability":"view"},
{"type":"function",
  "name":"boolToIntTracker",
  "inputs":[{"name":"b", "type":"bool"}],
  "outputs":[{"name":"", "type":"uint256"}],
  "payable":true,
  "constant":false,
  "stateMutability":"payable"}]

object signature trivial = {
    const boolToInt : bool -> int;
    boolToIntTracker : bool -> int
}

object Trivial : trivial {
    let seenTrueYet : bool := false

    let boolToInt b =
      if b then 1 else 0

    let boolToIntTracker b =
      if b then
        begin
            seenTrueYet := true;
            1
        end
      else 0
}

layer CONTRACT = { o = Trivial }

$ dsc trivial.ds coq ...

if f then ret 1 else ret 0

Print Trivial_boolToInt_opt.
Trivial_boolToInt_opt = 
fun (memModelOps : MemoryModelOps mem) (f : bool)
  (_ : machine_env GetHighData) => if f then ret 1 else ret 0
     : forall memModelOps : MemoryModelOps mem,
       bool -> machine_env GetHighData -> DS Z32

Arguments Trivial_boolToInt_opt {memModelOps} _%bool_scope _
Print Trivial_boolToInt.
Trivial_boolToInt = 
fun memModelOps : MemoryModelOps mem =>
{|
  FC_ident_start := 10%positive;
  FC_params := [int_bool_pair];
  FC_returns := int_Z32_pair;
  FC_body :=
    CCifthenelse (ECtempvar tint_bool 11%positive)
      (CCyield (ECconst_int256 tint_Z32 1 (Int256.repr 1)))
      (CCyield (ECconst_int256 tint_Z32 0 (Int256.repr 0)))
|}
     : forall memModelOps : MemoryModelOps mem, function_constr

Arguments Trivial_boolToInt {memModelOps}

$ dsc trivial.ds coq ...

if f then
  MonadState.modify (update_Trivial_seenTrueYet true) ;;
  ret 1
else
  ret 0

Print Trivial_boolToIntTracker_opt.
Trivial_boolToIntTracker_opt = 
fun (memModelOps : MemoryModelOps mem) (f : bool)
  (_ : machine_env GetHighData) =>
if f
then MonadState.modify (update_Trivial_seenTrueYet true);; ret 1
else ret 0
     : forall memModelOps : MemoryModelOps mem,
       bool -> machine_env GetHighData -> DS Z32

Arguments Trivial_boolToIntTracker_opt {memModelOps} _%bool_scope _
Print Trivial_boolToIntTracker.
Trivial_boolToIntTracker = 
fun memModelOps : MemoryModelOps mem =>
{|
  FC_ident_start := 10%positive;
  FC_params := [int_bool_pair];
  FC_returns := int_Z32_pair;
  FC_body :=
    CCifthenelse (ECtempvar tint_bool 11%positive)
      (CCsequence
         (CCstore (LCvar Trivial_seenTrueYet_var)
            (ECconst_int256 tint_bool true Int256.one))
         (CCyield (ECconst_int256 tint_Z32 1 (Int256.repr 1))))
      (CCyield (ECconst_int256 tint_Z32 0 (Int256.repr 0)))
|}
     : forall memModelOps : MemoryModelOps mem, function_constr

Arguments Trivial_boolToIntTracker {memModelOps}

A proof about our Trivial contract

Lemma boolToInt_proof : forall input context before result after,
  let machine_environment :=
    (make_machine_env contract_address before context (fun _ _ _ _ => true)) in

  runStateT (Trivial_boolToInt_opt input machine_environment) (contract_state before)
    = Some (result, after)

  ->

  result = 1 <-> input = true.
contract_address: addr
memModelOps: MemoryModelOps mem
forall (input : bool) (context : CallContext)
  (before : BlockchainState) (result : Z32) (after : GetHighData),
let machine_environment :=
  make_machine_env contract_address before context
    (fun (_ : option global_abstract_data_type) (_ _ : addr)
       (_ : wei) => true) in
runStateT (Trivial_boolToInt_opt input machine_environment)
  (contract_state before) = Some (result, after) ->
result = 1 <-> input = true

Main goal:

result = 1 <-> input = true

Proof.
contract_address: addr
forall (input : bool) (context : CallContext)
  (before : BlockchainState) (result : Z32) (after : GetHighData),
let machine_environment :=
  make_machine_env contract_address before context
    (fun (_ : option global_abstract_data_type) (_ _ : addr)
       (_ : wei) => true) in
runStateT (Trivial_boolToInt_opt input machine_environment)
  (contract_state before) = Some (result, after) ->
result = 1 <-> input = true
  intros.
contract_address: addr
input: bool
context: CallContext
before: BlockchainState
result: Z32
after: GetHighData
H: runStateT (Trivial_boolToInt_opt input machine_environment)
  (contract_state before) = 
Some (result, after)
result = 1 <-> input = true
  Transparent Trivial_boolToInt_opt.
H: runStateT (Trivial_boolToInt_opt input machine_environment)
  (contract_state before) = 
Some (result, after)
result = 1 <-> input = true
  unfold Trivial_boolToInt_opt in H.
H: runStateT (if input then ret 1 else ret 0)
  (contract_state before) = 
Some (result, after)
result = 1 <-> input = true
  split; intros.
input = true
result = 1
    - (* "->" result is 1 ∴ input is true. *)
H: runStateT (if input then ret 1 else ret 0)
  (contract_state before) = 
Some (result, after)
H0: result = 1
input = true
      inv_runStateT_branching.
Heqb: input = true
H0: result = 1
H1: 1 = result
H2: contract_state before = after
true = true
Heqb: input = false
H0: result = 1
H1: 0 = result
H2: contract_state before = after
false = true
      + (* Go down true branch of if statement. *)
Heqb: input = true
H0: result = 1
H1: 1 = result
H2: contract_state before = after
true = true
        reflexivity.
      + (* Go down false branch of if statement, gives a contradiction. *)
Heqb: input = false
H0: result = 1
H1: 0 = result
H2: contract_state before = after
false = true
        subst.
H1: 0 = 1
false = true discriminate.
    - (* "<-" input is true ∴ result is 1. *)
H: runStateT (if input then ret 1 else ret 0)
  (contract_state before) = 
Some (result, after)
H0: input = true
result = 1
      inv_runStateT_branching.
Heqb: input = true
H0: true = true
H1: 1 = result
H2: contract_state before = after
result = 1
Heqb: input = false
H0: false = true
H1: 0 = result
H2: contract_state before = after
result = 1
      + (* Go down true branch of if statement *)
Heqb: input = true
H0: true = true
H1: 1 = result
H2: contract_state before = after
result = 1
        subst.
H0: true = true
1 = 1  reflexivity.
      + (* Go down false branch of if statement, gives a contradiction. *)
Heqb: input = false
H0: false = true
H1: 0 = result
H2: contract_state before = after
result = 1
        discriminate.
Qed.

object signature trivial = {
    const boolToInt : bool -> int;
    boolToIntTracker : bool -> int
}

object Trivial : trivial {
    let seenTrueYet : bool := false

    let boolToInt b =
      if b then 1 else 0

    let boolToIntTracker b =
      if b then
        begin
            seenTrueYet := true;
            1
        end
      else 0
}

layer CONTRACT = { o = Trivial }

Lemma boolToIntTracker_proof : forall input context before result after,
  let machine_environment :=
    (make_machine_env contract_address before context (fun _ _ _ _ => true)) in
  runStateT (Trivial_boolToIntTracker_opt input machine_environment) (contract_state before)
    = Some (result, after)
  -> result = 1 <-> input = true.
contract_address: addr
forall (input : bool) (context : CallContext)
  (before : BlockchainState) (result : Z32) (after : GetHighData),
let machine_environment :=
  make_machine_env contract_address before context
    (fun (_ : option global_abstract_data_type) (_ _ : addr)
       (_ : wei) => true) in
runStateT (Trivial_boolToIntTracker_opt input machine_environment)
  (contract_state before) = Some (result, after) ->
result = 1 <-> input = true
Proof.
contract_address: addr
forall (input : bool) (context : CallContext)
  (before : BlockchainState) (result : Z32) (after : GetHighData),
let machine_environment :=
  make_machine_env contract_address before context
    (fun (_ : option global_abstract_data_type) (_ _ : addr)
       (_ : wei) => true) in
runStateT (Trivial_boolToIntTracker_opt input machine_environment)
  (contract_state before) = Some (result, after) ->
result = 1 <-> input = true
  intros.
contract_address: addr
input: bool
context: CallContext
before: BlockchainState
result: Z32
after: GetHighData
H: runStateT
  (Trivial_boolToIntTracker_opt input machine_environment)
  (contract_state before) = 
Some (result, after)
result = 1 <-> input = true
  Transparent Trivial_boolToIntTracker_opt.
H: runStateT
  (Trivial_boolToIntTracker_opt input machine_environment)
  (contract_state before) = 
Some (result, after)
result = 1 <-> input = true
  unfold Trivial_boolToIntTracker_opt in H.
H: runStateT
  (if input
   then
    MonadState.modify (update_Trivial_seenTrueYet true);; ret 1
   else ret 0) (contract_state before) = 
Some (result, after)
result = 1 <-> input = true
  split; intros.
input = true
result = 1
    - (* "->" result is 1 ∴ input is true. *)
H: runStateT
  (if input
   then
    MonadState.modify (update_Trivial_seenTrueYet true);; ret 1
   else ret 0) (contract_state before) = 
Some (result, after)
H0: result = 1
input = true
      inv_runStateT_branching.
Heqb: input = true
H0: result = 1
H3: update_Trivial_seenTrueYet true (contract_state before) = m
H1: 1 = result
H4: m = after
true = true
Heqb: input = false
H0: result = 1
H1: 0 = result
false = true
      + (* Go down true branch of if statement. *)
Heqb: input = true
H0: result = 1
H3: update_Trivial_seenTrueYet true (contract_state before) = m
H1: 1 = result
H4: m = after
true = true
        reflexivity.
      + (* Go down false branch of if statement, gives a contradiction. *)
Heqb: input = false
H0: result = 1
H1: 0 = result
H2: contract_state before = after
false = true
        subst.
H1: 0 = 1
false = true discriminate.
    - (* "<-" input is true ∴ result is 1. *)
H: runStateT
  (if input
   then
    MonadState.modify (update_Trivial_seenTrueYet true);; ret 1
   else ret 0) (contract_state before) = 
Some (result, after)
H0: input = true
result = 1
      inv_runStateT_branching.
Heqb: input = true
H0: true = true
H3: update_Trivial_seenTrueYet true (contract_state before) = m
H1: 1 = result
H4: m = after
result = 1
Heqb: input = false
H0: false = true
H1: 0 = result
result = 1
      + (* Go down true branch of if statement *)
Heqb: input = true
H0: true = true
H3: update_Trivial_seenTrueYet true (contract_state before) = m
H1: 1 = result
H4: m = after
result = 1
        subst.
H0: true = true
1 = 1  reflexivity.
      + (* Go down false branch of if statement, gives a contradiction. *)
Heqb: input = false
H0: false = true
H1: 0 = result
H2: contract_state before = after
result = 1
        discriminate.
Qed.

A Crowdfunding Correctness Property

Definition since_as_long (Property1 : BlockchainState -> Prop)
    (Property2 : BlockchainState -> Prop) (PropertyAboutAction : Step -> Prop) :=
  forall actions start finish helper,
    ReachableVia start finish helper actions ->
    Property1 start
    -> (forall act, List.In act actions -> PropertyAboutAction act)
    -> Property2 finish.

Notation "Property2 `since` Property1 `as-long-as` PropertyAboutAction" :=
  (since_as_long Property1 Property2 PropertyAboutAction) (at level 1).

Theorem donation_preserved :
  forall (user : addr) (amount : Z),
                 (donation_recorded user amount)
    `since`      (donation_recorded user amount)
    `as-long-as` (no_claims_from user).
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
forall (user : addr) (amount : Z),
(donation_recorded user amount) `since` donation_recorded user amount
`as-long-as` (no_claims_from user)

Proof.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
forall (user : addr) (amount : Z),
(donation_recorded user amount) `since` donation_recorded user amount
`as-long-as` (no_claims_from user)
unfold since_as_long.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
forall (user : addr) (amount : Z) (actions : list Step)
  (start finish : BlockchainState) (helper : Step),
ReachableVia start finish helper actions ->
donation_recorded user amount start ->
(forall act : Step, In act actions -> no_claims_from user act) ->
donation_recorded user amount finish
intros.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
actions: list Step
start, finish: BlockchainState
helper: Step
H: ReachableVia start finish helper actions
H0: donation_recorded user amount start
H1: forall act : Step, In act actions -> no_claims_from user act
donation_recorded user amount finish

induction H; [assumption|].
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
prev: Step
prevList: list Step
H: ReachableVia start prevSt prev prevList
next_action: Action (stepOnce prev)
H0: donation_recorded user amount start
H1: forall act : Step,
In act (stepOnceAndWrap prev next_action :: prevList) ->
no_claims_from user act
IHReachableVia: (forall act : Step,
 In act prevList -> no_claims_from user act) ->
donation_recorded user amount prevSt
donation_recorded user amount (stepOnce prev)

assert(donation_recorded user amount prevSt).
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
prev: Step
prevList: list Step
H: ReachableVia start prevSt prev prevList
next_action: Action (stepOnce prev)
H0: donation_recorded user amount start
H1: forall act : Step,
In act (stepOnceAndWrap prev next_action :: prevList) ->
no_claims_from user act
IHReachableVia: (forall act : Step,
 In act prevList -> no_claims_from user act) ->
donation_recorded user amount prevSt
donation_recorded user amount prevSt
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
prev: Step
prevList: list Step
H: ReachableVia start prevSt prev prevList
next_action: Action (stepOnce prev)
H0: donation_recorded user amount start
H1: forall act : Step,
In act (stepOnceAndWrap prev next_action :: prevList) ->
no_claims_from user act
IHReachableVia: (forall act : Step,
 In act prevList -> no_claims_from user act) ->
donation_recorded user amount prevSt
H2: donation_recorded user amount prevSt
donation_recorded user amount (stepOnce prev)
apply IHReachableVia.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
prev: Step
prevList: list Step
H: ReachableVia start prevSt prev prevList
next_action: Action (stepOnce prev)
H0: donation_recorded user amount start
H1: forall act : Step,
In act (stepOnceAndWrap prev next_action :: prevList) ->
no_claims_from user act
IHReachableVia: (forall act : Step,
 In act prevList -> no_claims_from user act) ->
donation_recorded user amount prevSt
forall act : Step, In act prevList -> no_claims_from user act
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
prev: Step
prevList: list Step
H: ReachableVia start prevSt prev prevList
next_action: Action (stepOnce prev)
H0: donation_recorded user amount start
H1: forall act : Step,
In act (stepOnceAndWrap prev next_action :: prevList) ->
no_claims_from user act
IHReachableVia: (forall act : Step,
 In act prevList -> no_claims_from user act) ->
donation_recorded user amount prevSt
H2: donation_recorded user amount prevSt
donation_recorded user amount (stepOnce prev)
intros.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
prev: Step
prevList: list Step
H: ReachableVia start prevSt prev prevList
next_action: Action (stepOnce prev)
H0: donation_recorded user amount start
H1: forall act : Step,
In act (stepOnceAndWrap prev next_action :: prevList) ->
no_claims_from user act
IHReachableVia: (forall act : Step,
 In act prevList -> no_claims_from user act) ->
donation_recorded user amount prevSt
act: Step
H2: In act prevList
no_claims_from user act
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
prev: Step
prevList: list Step
H: ReachableVia start prevSt prev prevList
next_action: Action (stepOnce prev)
H0: donation_recorded user amount start
H1: forall act : Step,
In act (stepOnceAndWrap prev next_action :: prevList) ->
no_claims_from user act
IHReachableVia: (forall act : Step,
 In act prevList -> no_claims_from user act) ->
donation_recorded user amount prevSt
H2: donation_recorded user amount prevSt
donation_recorded user amount (stepOnce prev)
apply H1.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
prev: Step
prevList: list Step
H: ReachableVia start prevSt prev prevList
next_action: Action (stepOnce prev)
H0: donation_recorded user amount start
H1: forall act : Step,
In act (stepOnceAndWrap prev next_action :: prevList) ->
no_claims_from user act
IHReachableVia: (forall act : Step,
 In act prevList -> no_claims_from user act) ->
donation_recorded user amount prevSt
act: Step
H2: In act prevList
In act (stepOnceAndWrap prev next_action :: prevList)
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
prev: Step
prevList: list Step
H: ReachableVia start prevSt prev prevList
next_action: Action (stepOnce prev)
H0: donation_recorded user amount start
H1: forall act : Step,
In act (stepOnceAndWrap prev next_action :: prevList) ->
no_claims_from user act
IHReachableVia: (forall act : Step,
 In act prevList -> no_claims_from user act) ->
donation_recorded user amount prevSt
H2: donation_recorded user amount prevSt
donation_recorded user amount (stepOnce prev)
apply in_cons; assumption.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
prev: Step
prevList: list Step
H: ReachableVia start prevSt prev prevList
next_action: Action (stepOnce prev)
H0: donation_recorded user amount start
H1: forall act : Step,
In act (stepOnceAndWrap prev next_action :: prevList) ->
no_claims_from user act
IHReachableVia: (forall act : Step,
 In act prevList -> no_claims_from user act) ->
donation_recorded user amount prevSt
H2: donation_recorded user amount prevSt
donation_recorded user amount (stepOnce prev)

clear H0.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
prev: Step
prevList: list Step
H: ReachableVia start prevSt prev prevList
next_action: Action (stepOnce prev)
H1: forall act : Step,
In act (stepOnceAndWrap prev next_action :: prevList) ->
no_claims_from user act
IHReachableVia: (forall act : Step,
 In act prevList -> no_claims_from user act) ->
donation_recorded user amount prevSt
H2: donation_recorded user amount prevSt
donation_recorded user amount (stepOnce prev)
clear IHReachableVia.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
prev: Step
prevList: list Step
H: ReachableVia start prevSt prev prevList
next_action: Action (stepOnce prev)
H1: forall act : Step,
In act (stepOnceAndWrap prev next_action :: prevList) ->
no_claims_from user act
H2: donation_recorded user amount prevSt
donation_recorded user amount (stepOnce prev)
unfold donation_recorded in *.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
prev: Step
prevList: list Step
H: ReachableVia start prevSt prev prevList
next_action: Action (stepOnce prev)
H1: forall act : Step,
In act (stepOnceAndWrap prev next_action :: prevList) ->
no_claims_from user act
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
get_default 0 user
  (Crowdfunding_backers (contract_state (stepOnce prev))) > 0

reachableFromByLinks.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
prev: Step
prevList: list Step
H: ReachableVia start prevSt prev prevList
next_action: Action (stepOnce prev)
H1: forall act : Step,
In act (stepOnceAndWrap prev next_action :: prevList) ->
no_claims_from user act
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
HReachableViaLinkStateToStep: prevSt = Step_state prev
HReachableViaLinkStepToList: exists tl : list Step,
  prev :: tl = prevList
get_default 0 user
  (Crowdfunding_backers (contract_state (stepOnce prev))) > 0

assert (no_claims_from user prev).
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
prev: Step
prevList: list Step
H: ReachableVia start prevSt prev prevList
next_action: Action (stepOnce prev)
H1: forall act : Step,
In act (stepOnceAndWrap prev next_action :: prevList) ->
no_claims_from user act
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
HReachableViaLinkStateToStep: prevSt = Step_state prev
HReachableViaLinkStepToList: exists tl : list Step,
  prev :: tl = prevList
no_claims_from user prev
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
prev: Step
prevList: list Step
H: ReachableVia start prevSt prev prevList
next_action: Action (stepOnce prev)
H1: forall act : Step,
In act (stepOnceAndWrap prev next_action :: prevList) ->
no_claims_from user act
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
HReachableViaLinkStateToStep: prevSt = Step_state prev
HReachableViaLinkStepToList: exists tl : list Step,
  prev :: tl = prevList
H0: no_claims_from user prev
get_default 0 user
  (Crowdfunding_backers (contract_state (stepOnce prev))) > 0
apply H1.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
prev: Step
prevList: list Step
H: ReachableVia start prevSt prev prevList
next_action: Action (stepOnce prev)
H1: forall act : Step,
In act (stepOnceAndWrap prev next_action :: prevList) ->
no_claims_from user act
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
HReachableViaLinkStateToStep: prevSt = Step_state prev
HReachableViaLinkStepToList: exists tl : list Step,
  prev :: tl = prevList
In prev (stepOnceAndWrap prev next_action :: prevList)
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
prev: Step
prevList: list Step
H: ReachableVia start prevSt prev prevList
next_action: Action (stepOnce prev)
H1: forall act : Step,
In act (stepOnceAndWrap prev next_action :: prevList) ->
no_claims_from user act
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
HReachableViaLinkStateToStep: prevSt = Step_state prev
HReachableViaLinkStepToList: exists tl : list Step,
  prev :: tl = prevList
H0: no_claims_from user prev
get_default 0 user
  (Crowdfunding_backers (contract_state (stepOnce prev))) > 0
destruct HReachableViaLinkStepToList.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
prev: Step
prevList: list Step
H: ReachableVia start prevSt prev prevList
next_action: Action (stepOnce prev)
H1: forall act : Step,
In act (stepOnceAndWrap prev next_action :: prevList) ->
no_claims_from user act
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
HReachableViaLinkStateToStep: prevSt = Step_state prev
x: list Step
H0: prev :: x = prevList
In prev (stepOnceAndWrap prev next_action :: prevList)
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
prev: Step
prevList: list Step
H: ReachableVia start prevSt prev prevList
next_action: Action (stepOnce prev)
H1: forall act : Step,
In act (stepOnceAndWrap prev next_action :: prevList) ->
no_claims_from user act
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
HReachableViaLinkStateToStep: prevSt = Step_state prev
HReachableViaLinkStepToList: exists tl : list Step,
  prev :: tl = prevList
H0: no_claims_from user prev
get_default 0 user
  (Crowdfunding_backers (contract_state (stepOnce prev))) > 0
subst.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start: BlockchainState
prev: Step
x: list Step
H: ReachableVia start (Step_state prev) prev (prev :: x)
next_action: Action (stepOnce prev)
H1: forall act : Step,
In act (stepOnceAndWrap prev next_action :: prev :: x) ->
no_claims_from user act
H2: get_default 0 user
  (Crowdfunding_backers (contract_state (Step_state prev))) > 0
In prev (stepOnceAndWrap prev next_action :: prev :: x)
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
prev: Step
prevList: list Step
H: ReachableVia start prevSt prev prevList
next_action: Action (stepOnce prev)
H1: forall act : Step,
In act (stepOnceAndWrap prev next_action :: prevList) ->
no_claims_from user act
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
HReachableViaLinkStateToStep: prevSt = Step_state prev
HReachableViaLinkStepToList: exists tl : list Step,
  prev :: tl = prevList
H0: no_claims_from user prev
get_default 0 user
  (Crowdfunding_backers (contract_state (stepOnce prev))) > 0
right.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start: BlockchainState
prev: Step
x: list Step
H: ReachableVia start (Step_state prev) prev (prev :: x)
next_action: Action (stepOnce prev)
H1: forall act : Step,
In act (stepOnceAndWrap prev next_action :: prev :: x) ->
no_claims_from user act
H2: get_default 0 user
  (Crowdfunding_backers (contract_state (Step_state prev))) > 0
In prev (prev :: x)
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
prev: Step
prevList: list Step
H: ReachableVia start prevSt prev prevList
next_action: Action (stepOnce prev)
H1: forall act : Step,
In act (stepOnceAndWrap prev next_action :: prevList) ->
no_claims_from user act
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
HReachableViaLinkStateToStep: prevSt = Step_state prev
HReachableViaLinkStepToList: exists tl : list Step,
  prev :: tl = prevList
H0: no_claims_from user prev
get_default 0 user
  (Crowdfunding_backers (contract_state (stepOnce prev))) > 0 left.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start: BlockchainState
prev: Step
x: list Step
H: ReachableVia start (Step_state prev) prev (prev :: x)
next_action: Action (stepOnce prev)
H1: forall act : Step,
In act (stepOnceAndWrap prev next_action :: prev :: x) ->
no_claims_from user act
H2: get_default 0 user
  (Crowdfunding_backers (contract_state (Step_state prev))) > 0
prev = prev
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
prev: Step
prevList: list Step
H: ReachableVia start prevSt prev prevList
next_action: Action (stepOnce prev)
H1: forall act : Step,
In act (stepOnceAndWrap prev next_action :: prevList) ->
no_claims_from user act
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
HReachableViaLinkStateToStep: prevSt = Step_state prev
HReachableViaLinkStepToList: exists tl : list Step,
  prev :: tl = prevList
H0: no_claims_from user prev
get_default 0 user
  (Crowdfunding_backers (contract_state (stepOnce prev))) > 0 reflexivity.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
prev: Step
prevList: list Step
H: ReachableVia start prevSt prev prevList
next_action: Action (stepOnce prev)
H1: forall act : Step,
In act (stepOnceAndWrap prev next_action :: prevList) ->
no_claims_from user act
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
HReachableViaLinkStateToStep: prevSt = Step_state prev
HReachableViaLinkStepToList: exists tl : list Step,
  prev :: tl = prevList
H0: no_claims_from user prev
get_default 0 user
  (Crowdfunding_backers (contract_state (stepOnce prev))) > 0

destruct prev; simpl in *; unfold stepOnceAndWrap, step in *; simpl in *.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt, Step_state0: BlockchainState
Step_action0: Action Step_state0
prevList: list Step
H: ReachableVia start prevSt
  {| Step_state := Step_state0; Step_action := Step_action0 |}
  prevList
next_action: Action
  (stepOnce
     {|
       Step_state := Step_state0;
       Step_action := Step_action0
     |})
H1: forall act : Step,
{|
  Step_state :=
    stepOnce
      {|
        Step_state := Step_state0; Step_action := Step_action0
      |};
  Step_action := next_action
|} = act \/ In act prevList -> 
no_claims_from user act
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
HReachableViaLinkStateToStep: prevSt = Step_state0
HReachableViaLinkStepToList: exists tl : list Step,
  {|
    Step_state := Step_state0;
    Step_action := Step_action0
  |} :: tl = prevList
H0: no_claims_from user
  {| Step_state := Step_state0; Step_action := Step_action0 |}
get_default 0 user
  (Crowdfunding_backers
     (contract_state
        (stepOnce
           {|
             Step_state := Step_state0; Step_action := Step_action0
           |}))) > 0
clear H1. (* no_claims_one, not needed this time? *)
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt, Step_state0: BlockchainState
Step_action0: Action Step_state0
prevList: list Step
H: ReachableVia start prevSt
  {| Step_state := Step_state0; Step_action := Step_action0 |}
  prevList
next_action: Action
  (stepOnce
     {|
       Step_state := Step_state0;
       Step_action := Step_action0
     |})
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
HReachableViaLinkStateToStep: prevSt = Step_state0
HReachableViaLinkStepToList: exists tl : list Step,
  {|
    Step_state := Step_state0;
    Step_action := Step_action0
  |} :: tl = prevList
H0: no_claims_from user
  {| Step_state := Step_state0; Step_action := Step_action0 |}
get_default 0 user
  (Crowdfunding_backers
     (contract_state
        (stepOnce
           {|
             Step_state := Step_state0; Step_action := Step_action0
           |}))) > 0
clear next_action.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt, Step_state0: BlockchainState
Step_action0: Action Step_state0
prevList: list Step
H: ReachableVia start prevSt
  {| Step_state := Step_state0; Step_action := Step_action0 |}
  prevList
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
HReachableViaLinkStateToStep: prevSt = Step_state0
HReachableViaLinkStepToList: exists tl : list Step,
  {|
    Step_state := Step_state0;
    Step_action := Step_action0
  |} :: tl = prevList
H0: no_claims_from user
  {| Step_state := Step_state0; Step_action := Step_action0 |}
get_default 0 user
  (Crowdfunding_backers
     (contract_state
        (stepOnce
           {|
             Step_state := Step_state0; Step_action := Step_action0
           |}))) > 0
clear H. (* ReachableVia, no longer needed? *)
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt, Step_state0: BlockchainState
Step_action0: Action Step_state0
prevList: list Step
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
HReachableViaLinkStateToStep: prevSt = Step_state0
HReachableViaLinkStepToList: exists tl : list Step,
  {|
    Step_state := Step_state0;
    Step_action := Step_action0
  |} :: tl = prevList
H0: no_claims_from user
  {| Step_state := Step_state0; Step_action := Step_action0 |}
get_default 0 user
  (Crowdfunding_backers
     (contract_state
        (stepOnce
           {|
             Step_state := Step_state0; Step_action := Step_action0
           |}))) > 0
clear HReachableViaLinkStepToList.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt, Step_state0: BlockchainState
Step_action0: Action Step_state0
prevList: list Step
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
HReachableViaLinkStateToStep: prevSt = Step_state0
H0: no_claims_from user
  {| Step_state := Step_state0; Step_action := Step_action0 |}
get_default 0 user
  (Crowdfunding_backers
     (contract_state
        (stepOnce
           {|
             Step_state := Step_state0; Step_action := Step_action0
           |}))) > 0
unfold no_claims_from in H0.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt, Step_state0: BlockchainState
Step_action0: Action Step_state0
prevList: list Step
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
HReachableViaLinkStateToStep: prevSt = Step_state0
H0: match
  Step_action
    {| Step_state := Step_state0; Step_action := Step_action0 |}
with
| @call_Crowdfunding_claim _ _ _ _ _ _ => False
| _ => True
end
get_default 0 user
  (Crowdfunding_backers
     (contract_state
        (stepOnce
           {|
             Step_state := Step_state0; Step_action := Step_action0
           |}))) > 0
unfold stepOnce.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt, Step_state0: BlockchainState
Step_action0: Action Step_state0
prevList: list Step
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
HReachableViaLinkStateToStep: prevSt = Step_state0
H0: match
  Step_action
    {| Step_state := Step_state0; Step_action := Step_action0 |}
with
| @call_Crowdfunding_claim _ _ _ _ _ _ => False
| _ => True
end
get_default 0 user
  (Crowdfunding_backers
     (contract_state
        (step
           (Step_state
              {|
                Step_state := Step_state0;
                Step_action := Step_action0
              |})
           (Step_action
              {|
                Step_state := Step_state0;
                Step_action := Step_action0
              |})))) > 0 simpl.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt, Step_state0: BlockchainState
Step_action0: Action Step_state0
prevList: list Step
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
HReachableViaLinkStateToStep: prevSt = Step_state0
H0: match
  Step_action
    {| Step_state := Step_state0; Step_action := Step_action0 |}
with
| @call_Crowdfunding_claim _ _ _ _ _ _ => False
| _ => True
end
get_default 0 user
  (Crowdfunding_backers
     (contract_state (step Step_state0 Step_action0))) > 0
unfold donation_recorded in *.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt, Step_state0: BlockchainState
Step_action0: Action Step_state0
prevList: list Step
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
HReachableViaLinkStateToStep: prevSt = Step_state0
H0: match
  Step_action
    {| Step_state := Step_state0; Step_action := Step_action0 |}
with
| @call_Crowdfunding_claim _ _ _ _ _ _ => False
| _ => True
end
get_default 0 user
  (Crowdfunding_backers
     (contract_state (step Step_state0 Step_action0))) > 0
destruct Step_action0; simpl in *;
  rewrite <- HReachableViaLinkStateToStep in *;
  clear HReachableViaLinkStateToStep Step_state0.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
context: CallContext
callvalue_prf: noOverflowOrUnderflowInTransfer 
  (caller context) contract_address
  (callvalue context) (balance prevSt) = true
r: unit
contract_state_after: global_abstract_data_type
case_donate_prf: runStateT
  (Crowdfunding_donate_opt
     (make_machine_env contract_address prevSt
        context address_accepts_funds_assumption))
  (contract_state prevSt) =
Some (r, contract_state_after)
prevList: list Step
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
H0: True
get_default 0 user (Crowdfunding_backers contract_state_after) > 0
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
context: CallContext
callvalue_prf: noOverflowOrUnderflowInTransfer 
  (caller context) contract_address
  (callvalue context) (balance prevSt) = true
r: unit
contract_state_after: global_abstract_data_type
case_getFunds_prf: runStateT
  (Crowdfunding_getFunds_opt
     (make_machine_env contract_address prevSt
        context address_accepts_funds_assumption))
  (contract_state prevSt) =
Some (r, contract_state_after)
prevList: list Step
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
H0: True
get_default 0 user (Crowdfunding_backers contract_state_after) > 0
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
context: CallContext
callvalue_prf: noOverflowOrUnderflowInTransfer 
  (caller context) contract_address
  (callvalue context) (balance prevSt) = true
r: unit
contract_state_after: global_abstract_data_type
case_claim_prf: runStateT
  (Crowdfunding_claim_opt
     (make_machine_env contract_address prevSt
        context address_accepts_funds_assumption))
  (contract_state prevSt) =
Some (r, contract_state_after)
prevList: list Step
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
H0: False
get_default 0 user (Crowdfunding_backers contract_state_after) > 0
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
sender, recipient: addr
amount0: wei
prf: sender <> contract_address /\
noOverflowOrUnderflowInTransfer sender recipient amount0
  (balance prevSt) &&
address_accepts_funds_assumption None sender recipient amount0 =
true
prevList: list Step
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
H0: True
get_default 0 user (Crowdfunding_backers (contract_state prevSt)) > 0
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
block_count, time_passing: int256
prf: validTimeChange block_count time_passing 
  (block_number prevSt) 
  (timestamp prevSt) = true
prevList: list Step
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
H0: True
get_default 0 user (Crowdfunding_backers (contract_state prevSt)) > 0
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
prevList: list Step
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
H0: True
get_default 0 user (Crowdfunding_backers (contract_state prevSt)) > 0
  -
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
context: CallContext
callvalue_prf: noOverflowOrUnderflowInTransfer 
  (caller context) contract_address
  (callvalue context) (balance prevSt) = true
r: unit
contract_state_after: global_abstract_data_type
case_donate_prf: runStateT
  (Crowdfunding_donate_opt
     (make_machine_env contract_address prevSt
        context address_accepts_funds_assumption))
  (contract_state prevSt) =
Some (r, contract_state_after)
prevList: list Step
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
H0: True
get_default 0 user (Crowdfunding_backers contract_state_after) > 0 Transparent Crowdfunding_donate_opt.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
context: CallContext
callvalue_prf: noOverflowOrUnderflowInTransfer 
  (caller context) contract_address
  (callvalue context) (balance prevSt) = true
r: unit
contract_state_after: global_abstract_data_type
case_donate_prf: runStateT
  (Crowdfunding_donate_opt
     (make_machine_env contract_address prevSt
        context address_accepts_funds_assumption))
  (contract_state prevSt) =
Some (r, contract_state_after)
prevList: list Step
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
H0: True
get_default 0 user (Crowdfunding_backers contract_state_after) > 0 unfold Crowdfunding_donate_opt in case_donate_prf.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
context: CallContext
callvalue_prf: noOverflowOrUnderflowInTransfer 
  (caller context) contract_address
  (callvalue context) (balance prevSt) = true
r: unit
contract_state_after: global_abstract_data_type
case_donate_prf: runStateT
  ((v <-
    ret
      (negb
         (me_caller
            (make_machine_env contract_address
               prevSt context
               address_accepts_funds_assumption) =?
          me_address
            (make_machine_env contract_address
               prevSt context
               address_accepts_funds_assumption)));;
    guard v);;
   (v <-
    ret
      ((let (intval, _) :=
          me_callvalue
            (make_machine_env contract_address
               prevSt context
               address_accepts_funds_assumption) in
        intval) >=? 0);; 
    guard v);;
   gets Crowdfunding_backers;;
   spec2 <-
   ret
     (me_number
        (make_machine_env contract_address prevSt
           context address_accepts_funds_assumption));;
   spec3 <- gets Crowdfunding_max_block;;
   (if Int256.ltu spec3 spec2
    then ret tt;; v <- ret false;; guard v
    else
     spec4 <-
     gets
       (fun s : GetHighData =>
        get_default 0
          (me_caller
             (make_machine_env contract_address
                prevSt context
                address_accepts_funds_assumption))
          (Crowdfunding_backers s));;
     (if (spec4 =? 0)%Z
      then
       MonadState.modify
         (fun s : GetHighData =>
          update_Crowdfunding_backers
            (set
               (me_caller
                  (make_machine_env
                     contract_address prevSt
                     context
                     address_accepts_funds_assumption))
               (let (intval, _) :=
                  me_callvalue
                    (make_machine_env
                       contract_address prevSt
                       context
                       address_accepts_funds_assumption) in
                intval) 
               (Crowdfunding_backers s)) s)
      else ret tt;; v <- ret false;; guard v)))
  (contract_state prevSt) =
Some (r, contract_state_after)
prevList: list Step
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
H0: True
get_default 0 user (Crowdfunding_backers contract_state_after) > 0
    ds_inv; subst; simpl.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
context: CallContext
callvalue_prf: noOverflowOrUnderflowInTransfer 
  (caller context) contract_address
  (callvalue context) (balance prevSt) = true
r: unit
prevList: list Step
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
H0: True
a: unit
H3: negb
  (me_caller
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption) =?
   me_address
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption)) = true
a1: unit
H7: ((let (intval, _) :=
    me_callvalue
      (make_machine_env contract_address prevSt context
         address_accepts_funds_assumption) in
  intval) >=? 0) = true
Heqb: Int256.ltu (Crowdfunding_max_block (contract_state prevSt))
  (me_number
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption)) = true
H19: false = true
get_default 0 user (Crowdfunding_backers (contract_state prevSt)) > 0
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
context: CallContext
callvalue_prf: noOverflowOrUnderflowInTransfer 
  (caller context) contract_address
  (callvalue context) (balance prevSt) = true
prevList: list Step
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
H0: True
a: unit
H3: negb
  (me_caller
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption) =?
   me_address
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption)) = true
a1: unit
H7: ((let (intval, _) :=
    me_callvalue
      (make_machine_env contract_address prevSt context
         address_accepts_funds_assumption) in
  intval) >=? 0) = true
Heqb: Int256.ltu (Crowdfunding_max_block (contract_state prevSt))
  (me_number
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption)) = false
Heqb0: (get_default 0
   (me_caller
      (make_machine_env contract_address prevSt context
         address_accepts_funds_assumption))
   (Crowdfunding_backers (contract_state prevSt)) =? 0)%Z =
true
get_default 0 user
  (set (caller context)
     (let (intval, _) := callvalue context in intval)
     (Crowdfunding_backers (contract_state prevSt))) > 0
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
context: CallContext
callvalue_prf: noOverflowOrUnderflowInTransfer 
  (caller context) contract_address
  (callvalue context) (balance prevSt) = true
r: unit
prevList: list Step
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
H0: True
a: unit
H3: negb
  (me_caller
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption) =?
   me_address
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption)) = true
a1: unit
H7: ((let (intval, _) :=
    me_callvalue
      (make_machine_env contract_address prevSt context
         address_accepts_funds_assumption) in
  intval) >=? 0) = true
Heqb: Int256.ltu (Crowdfunding_max_block (contract_state prevSt))
  (me_number
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption)) = false
Heqb0: (get_default 0
   (me_caller
      (make_machine_env contract_address prevSt context
         address_accepts_funds_assumption))
   (Crowdfunding_backers (contract_state prevSt)) =? 0)%Z =
false
H21: false = true
get_default 0 user (Crowdfunding_backers (contract_state prevSt)) > 0
    +
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
context: CallContext
callvalue_prf: noOverflowOrUnderflowInTransfer 
  (caller context) contract_address
  (callvalue context) (balance prevSt) = true
r: unit
prevList: list Step
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
H0: True
a: unit
H3: negb
  (me_caller
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption) =?
   me_address
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption)) = true
a1: unit
H7: ((let (intval, _) :=
    me_callvalue
      (make_machine_env contract_address prevSt context
         address_accepts_funds_assumption) in
  intval) >=? 0) = true
Heqb: Int256.ltu (Crowdfunding_max_block (contract_state prevSt))
  (me_number
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption)) = true
H19: false = true
get_default 0 user (Crowdfunding_backers (contract_state prevSt)) > 0 match goal with H : false = true |- _ => inversion H end.
    +
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
context: CallContext
callvalue_prf: noOverflowOrUnderflowInTransfer 
  (caller context) contract_address
  (callvalue context) (balance prevSt) = true
prevList: list Step
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
H0: True
a: unit
H3: negb
  (me_caller
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption) =?
   me_address
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption)) = true
a1: unit
H7: ((let (intval, _) :=
    me_callvalue
      (make_machine_env contract_address prevSt context
         address_accepts_funds_assumption) in
  intval) >=? 0) = true
Heqb: Int256.ltu (Crowdfunding_max_block (contract_state prevSt))
  (me_number
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption)) = false
Heqb0: (get_default 0
   (me_caller
      (make_machine_env contract_address prevSt context
         address_accepts_funds_assumption))
   (Crowdfunding_backers (contract_state prevSt)) =? 0)%Z =
true
get_default 0 user
  (set (caller context)
     (let (intval, _) := callvalue context in intval)
     (Crowdfunding_backers (contract_state prevSt))) > 0 destruct (user =? (caller context))%int256 eqn:Case.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
context: CallContext
callvalue_prf: noOverflowOrUnderflowInTransfer 
  (caller context) contract_address
  (callvalue context) (balance prevSt) = true
prevList: list Step
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
H0: True
a: unit
H3: negb
  (me_caller
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption) =?
   me_address
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption)) = true
a1: unit
H7: ((let (intval, _) :=
    me_callvalue
      (make_machine_env contract_address prevSt context
         address_accepts_funds_assumption) in
  intval) >=? 0) = true
Heqb: Int256.ltu (Crowdfunding_max_block (contract_state prevSt))
  (me_number
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption)) = false
Heqb0: (get_default 0
   (me_caller
      (make_machine_env contract_address prevSt context
         address_accepts_funds_assumption))
   (Crowdfunding_backers (contract_state prevSt)) =? 0)%Z =
true
Case: (user =? caller context) = true
get_default 0 user
  (set (caller context)
     (let (intval, _) := callvalue context in intval)
     (Crowdfunding_backers (contract_state prevSt))) > 0
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
context: CallContext
callvalue_prf: noOverflowOrUnderflowInTransfer 
  (caller context) contract_address
  (callvalue context) (balance prevSt) = true
prevList: list Step
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
H0: True
a: unit
H3: negb
  (me_caller
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption) =?
   me_address
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption)) = true
a1: unit
H7: ((let (intval, _) :=
    me_callvalue
      (make_machine_env contract_address prevSt context
         address_accepts_funds_assumption) in
  intval) >=? 0) = true
Heqb: Int256.ltu (Crowdfunding_max_block (contract_state prevSt))
  (me_number
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption)) = false
Heqb0: (get_default 0
   (me_caller
      (make_machine_env contract_address prevSt context
         address_accepts_funds_assumption))
   (Crowdfunding_backers (contract_state prevSt)) =? 0)%Z =
true
Case: (user =? caller context) = false
get_default 0 user
  (set (caller context)
     (let (intval, _) := callvalue context in intval)
     (Crowdfunding_backers (contract_state prevSt))) > 0
      *
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
context: CallContext
callvalue_prf: noOverflowOrUnderflowInTransfer 
  (caller context) contract_address
  (callvalue context) (balance prevSt) = true
prevList: list Step
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
H0: True
a: unit
H3: negb
  (me_caller
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption) =?
   me_address
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption)) = true
a1: unit
H7: ((let (intval, _) :=
    me_callvalue
      (make_machine_env contract_address prevSt context
         address_accepts_funds_assumption) in
  intval) >=? 0) = true
Heqb: Int256.ltu (Crowdfunding_max_block (contract_state prevSt))
  (me_number
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption)) = false
Heqb0: (get_default 0
   (me_caller
      (make_machine_env contract_address prevSt context
         address_accepts_funds_assumption))
   (Crowdfunding_backers (contract_state prevSt)) =? 0)%Z =
true
Case: (user =? caller context) = true
get_default 0 user
  (set (caller context)
     (let (intval, _) := callvalue context in intval)
     (Crowdfunding_backers (contract_state prevSt))) > 0 apply Int256eq_true in Case.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
context: CallContext
callvalue_prf: noOverflowOrUnderflowInTransfer 
  (caller context) contract_address
  (callvalue context) (balance prevSt) = true
prevList: list Step
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
H0: True
a: unit
H3: negb
  (me_caller
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption) =?
   me_address
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption)) = true
a1: unit
H7: ((let (intval, _) :=
    me_callvalue
      (make_machine_env contract_address prevSt context
         address_accepts_funds_assumption) in
  intval) >=? 0) = true
Heqb: Int256.ltu (Crowdfunding_max_block (contract_state prevSt))
  (me_number
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption)) = false
Heqb0: (get_default 0
   (me_caller
      (make_machine_env contract_address prevSt context
         address_accepts_funds_assumption))
   (Crowdfunding_backers (contract_state prevSt)) =? 0)%Z =
true
Case: user = caller context
get_default 0 user
  (set (caller context)
     (let (intval, _) := callvalue context in intval)
     (Crowdfunding_backers (contract_state prevSt))) > 0 rewrite <- Case.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
context: CallContext
callvalue_prf: noOverflowOrUnderflowInTransfer 
  (caller context) contract_address
  (callvalue context) (balance prevSt) = true
prevList: list Step
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
H0: True
a: unit
H3: negb
  (me_caller
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption) =?
   me_address
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption)) = true
a1: unit
H7: ((let (intval, _) :=
    me_callvalue
      (make_machine_env contract_address prevSt context
         address_accepts_funds_assumption) in
  intval) >=? 0) = true
Heqb: Int256.ltu (Crowdfunding_max_block (contract_state prevSt))
  (me_number
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption)) = false
Heqb0: (get_default 0
   (me_caller
      (make_machine_env contract_address prevSt context
         address_accepts_funds_assumption))
   (Crowdfunding_backers (contract_state prevSt)) =? 0)%Z =
true
Case: user = caller context
get_default 0 user
  (set user (let (intval, _) := callvalue context in intval)
     (Crowdfunding_backers (contract_state prevSt))) > 0
        rewrite get_default_ss.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
context: CallContext
callvalue_prf: noOverflowOrUnderflowInTransfer 
  (caller context) contract_address
  (callvalue context) (balance prevSt) = true
prevList: list Step
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
H0: True
a: unit
H3: negb
  (me_caller
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption) =?
   me_address
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption)) = true
a1: unit
H7: ((let (intval, _) :=
    me_callvalue
      (make_machine_env contract_address prevSt context
         address_accepts_funds_assumption) in
  intval) >=? 0) = true
Heqb: Int256.ltu (Crowdfunding_max_block (contract_state prevSt))
  (me_number
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption)) = false
Heqb0: (get_default 0
   (me_caller
      (make_machine_env contract_address prevSt context
         address_accepts_funds_assumption))
   (Crowdfunding_backers (contract_state prevSt)) =? 0)%Z =
true
Case: user = caller context
(let (intval, _) := callvalue context in intval) > 0
        exfalso.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
context: CallContext
callvalue_prf: noOverflowOrUnderflowInTransfer 
  (caller context) contract_address
  (callvalue context) (balance prevSt) = true
prevList: list Step
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
H0: True
a: unit
H3: negb
  (me_caller
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption) =?
   me_address
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption)) = true
a1: unit
H7: ((let (intval, _) :=
    me_callvalue
      (make_machine_env contract_address prevSt context
         address_accepts_funds_assumption) in
  intval) >=? 0) = true
Heqb: Int256.ltu (Crowdfunding_max_block (contract_state prevSt))
  (me_number
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption)) = false
Heqb0: (get_default 0
   (me_caller
      (make_machine_env contract_address prevSt context
         address_accepts_funds_assumption))
   (Crowdfunding_backers (contract_state prevSt)) =? 0)%Z =
true
Case: user = caller context
False
        subst.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
amount: Z
start, prevSt: BlockchainState
context: CallContext
callvalue_prf: noOverflowOrUnderflowInTransfer 
  (caller context) contract_address
  (callvalue context) (balance prevSt) = true
prevList: list Step
H2: get_default 0 (caller context)
  (Crowdfunding_backers (contract_state prevSt)) > 0
H0: True
a: unit
H3: negb
  (me_caller
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption) =?
   me_address
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption)) = true
a1: unit
H7: ((let (intval, _) :=
    me_callvalue
      (make_machine_env contract_address prevSt context
         address_accepts_funds_assumption) in
  intval) >=? 0) = true
Heqb: Int256.ltu (Crowdfunding_max_block (contract_state prevSt))
  (me_number
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption)) = false
Heqb0: (get_default 0
   (me_caller
      (make_machine_env contract_address prevSt context
         address_accepts_funds_assumption))
   (Crowdfunding_backers (contract_state prevSt)) =? 0)%Z =
true
False
        unfold make_machine_env in Heqb0; simpl in Heqb0.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
amount: Z
start, prevSt: BlockchainState
context: CallContext
callvalue_prf: noOverflowOrUnderflowInTransfer 
  (caller context) contract_address
  (callvalue context) (balance prevSt) = true
prevList: list Step
H2: get_default 0 (caller context)
  (Crowdfunding_backers (contract_state prevSt)) > 0
H0: True
a: unit
H3: negb
  (me_caller
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption) =?
   me_address
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption)) = true
a1: unit
H7: ((let (intval, _) :=
    me_callvalue
      (make_machine_env contract_address prevSt context
         address_accepts_funds_assumption) in
  intval) >=? 0) = true
Heqb: Int256.ltu (Crowdfunding_max_block (contract_state prevSt))
  (me_number
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption)) = false
Heqb0: (get_default 0 (caller context)
   (Crowdfunding_backers (contract_state prevSt)) =? 0)%Z =
true
False
        apply Z.eqb_eq in Heqb0.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
amount: Z
start, prevSt: BlockchainState
context: CallContext
callvalue_prf: noOverflowOrUnderflowInTransfer 
  (caller context) contract_address
  (callvalue context) (balance prevSt) = true
prevList: list Step
H2: get_default 0 (caller context)
  (Crowdfunding_backers (contract_state prevSt)) > 0
H0: True
a: unit
H3: negb
  (me_caller
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption) =?
   me_address
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption)) = true
a1: unit
H7: ((let (intval, _) :=
    me_callvalue
      (make_machine_env contract_address prevSt context
         address_accepts_funds_assumption) in
  intval) >=? 0) = true
Heqb: Int256.ltu (Crowdfunding_max_block (contract_state prevSt))
  (me_number
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption)) = false
Heqb0: get_default 0 (caller context)
  (Crowdfunding_backers (contract_state prevSt)) = 0
False
        rewrite Heqb0 in H2.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
amount: Z
start, prevSt: BlockchainState
context: CallContext
callvalue_prf: noOverflowOrUnderflowInTransfer 
  (caller context) contract_address
  (callvalue context) (balance prevSt) = true
prevList: list Step
H2: 0 > 0
H0: True
a: unit
H3: negb
  (me_caller
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption) =?
   me_address
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption)) = true
a1: unit
H7: ((let (intval, _) :=
    me_callvalue
      (make_machine_env contract_address prevSt context
         address_accepts_funds_assumption) in
  intval) >=? 0) = true
Heqb: Int256.ltu (Crowdfunding_max_block (contract_state prevSt))
  (me_number
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption)) = false
Heqb0: get_default 0 (caller context)
  (Crowdfunding_backers (contract_state prevSt)) = 0
False
        lia.
      *
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
context: CallContext
callvalue_prf: noOverflowOrUnderflowInTransfer 
  (caller context) contract_address
  (callvalue context) (balance prevSt) = true
prevList: list Step
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
H0: True
a: unit
H3: negb
  (me_caller
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption) =?
   me_address
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption)) = true
a1: unit
H7: ((let (intval, _) :=
    me_callvalue
      (make_machine_env contract_address prevSt context
         address_accepts_funds_assumption) in
  intval) >=? 0) = true
Heqb: Int256.ltu (Crowdfunding_max_block (contract_state prevSt))
  (me_number
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption)) = false
Heqb0: (get_default 0
   (me_caller
      (make_machine_env contract_address prevSt context
         address_accepts_funds_assumption))
   (Crowdfunding_backers (contract_state prevSt)) =? 0)%Z =
true
Case: (user =? caller context) = false
get_default 0 user
  (set (caller context)
     (let (intval, _) := callvalue context in intval)
     (Crowdfunding_backers (contract_state prevSt))) > 0 apply Int256eq_false in Case.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
context: CallContext
callvalue_prf: noOverflowOrUnderflowInTransfer 
  (caller context) contract_address
  (callvalue context) (balance prevSt) = true
prevList: list Step
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
H0: True
a: unit
H3: negb
  (me_caller
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption) =?
   me_address
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption)) = true
a1: unit
H7: ((let (intval, _) :=
    me_callvalue
      (make_machine_env contract_address prevSt context
         address_accepts_funds_assumption) in
  intval) >=? 0) = true
Heqb: Int256.ltu (Crowdfunding_max_block (contract_state prevSt))
  (me_number
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption)) = false
Heqb0: (get_default 0
   (me_caller
      (make_machine_env contract_address prevSt context
         address_accepts_funds_assumption))
   (Crowdfunding_backers (contract_state prevSt)) =? 0)%Z =
true
Case: user <> caller context
get_default 0 user
  (set (caller context)
     (let (intval, _) := callvalue context in intval)
     (Crowdfunding_backers (contract_state prevSt))) > 0
        rewrite get_default_so; assumption.
    +
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
context: CallContext
callvalue_prf: noOverflowOrUnderflowInTransfer 
  (caller context) contract_address
  (callvalue context) (balance prevSt) = true
r: unit
prevList: list Step
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
H0: True
a: unit
H3: negb
  (me_caller
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption) =?
   me_address
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption)) = true
a1: unit
H7: ((let (intval, _) :=
    me_callvalue
      (make_machine_env contract_address prevSt context
         address_accepts_funds_assumption) in
  intval) >=? 0) = true
Heqb: Int256.ltu (Crowdfunding_max_block (contract_state prevSt))
  (me_number
     (make_machine_env contract_address prevSt context
        address_accepts_funds_assumption)) = false
Heqb0: (get_default 0
   (me_caller
      (make_machine_env contract_address prevSt context
         address_accepts_funds_assumption))
   (Crowdfunding_backers (contract_state prevSt)) =? 0)%Z =
false
H21: false = true
get_default 0 user (Crowdfunding_backers (contract_state prevSt)) > 0 match goal with H : false = true |- _ => inversion H end.
  -
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
context: CallContext
callvalue_prf: noOverflowOrUnderflowInTransfer 
  (caller context) contract_address
  (callvalue context) (balance prevSt) = true
r: unit
contract_state_after: global_abstract_data_type
case_getFunds_prf: runStateT
  (Crowdfunding_getFunds_opt
     (make_machine_env contract_address prevSt
        context address_accepts_funds_assumption))
  (contract_state prevSt) =
Some (r, contract_state_after)
prevList: list Step
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
H0: True
get_default 0 user (Crowdfunding_backers contract_state_after) > 0 Transparent Crowdfunding_getFunds_opt.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
context: CallContext
callvalue_prf: noOverflowOrUnderflowInTransfer 
  (caller context) contract_address
  (callvalue context) (balance prevSt) = true
r: unit
contract_state_after: global_abstract_data_type
case_getFunds_prf: runStateT
  (Crowdfunding_getFunds_opt
     (make_machine_env contract_address prevSt
        context address_accepts_funds_assumption))
  (contract_state prevSt) =
Some (r, contract_state_after)
prevList: list Step
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
H0: True
get_default 0 user (Crowdfunding_backers contract_state_after) > 0 unfold Crowdfunding_getFunds_opt in case_getFunds_prf.
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
context: CallContext
callvalue_prf: noOverflowOrUnderflowInTransfer 
  (caller context) contract_address
  (callvalue context) (balance prevSt) = true
r: unit
contract_state_after: global_abstract_data_type
case_getFunds_prf: runStateT
  ((v <-
    ret
      (negb
         (me_caller
            (make_machine_env contract_address
               prevSt context
               address_accepts_funds_assumption) =?
          me_address
            (make_machine_env contract_address
               prevSt context
               address_accepts_funds_assumption)));;
    guard v);;
   (v <-
    ret
      ((let (intval, _) :=
          me_callvalue
            (make_machine_env contract_address
               prevSt context
               address_accepts_funds_assumption) in
        intval) =? 0)%Z;; 
    guard v);;
   spec1 <- gets Crowdfunding_owner;;
   (if
     me_caller
       (make_machine_env contract_address prevSt
          context
          address_accepts_funds_assumption) =?
     spec1
    then
     spec2 <-
     ret
       (me_number
          (make_machine_env contract_address
             prevSt context
             address_accepts_funds_assumption));;
     spec3 <-
     ret
       (let (intval, _) :=
          me_balance
            (make_machine_env contract_address
               prevSt context
               address_accepts_funds_assumption)
            (me_address
               (make_machine_env contract_address
                  prevSt context
                  address_accepts_funds_assumption)) in
        intval);;
     spec4 <- gets Crowdfunding_max_block;;
     (if Int256.ltu spec4 spec2
      then
       spec5 <- gets Crowdfunding_goal;;
       (if spec5 <=? spec3
        then
         MonadState.modify
           (update_Crowdfunding_funded true);;
         ret tt;;
         d <- MonadState.get;;
         (let (success, d') :=
            me_transfer (...) spec1 (...) d in
          if success =? Int256.one
          then put d'
          else mzero)
        else ret tt)
      else ret tt)
    else ret tt)) (contract_state prevSt) =
Some (r, contract_state_after)
prevList: list Step
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
H0: True
get_default 0 user (Crowdfunding_backers contract_state_after) > 0
    ds_inv; subst; simpl; try lia.
  -
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
context: CallContext
callvalue_prf: noOverflowOrUnderflowInTransfer 
  (caller context) contract_address
  (callvalue context) (balance prevSt) = true
r: unit
contract_state_after: global_abstract_data_type
case_claim_prf: runStateT
  (Crowdfunding_claim_opt
     (make_machine_env contract_address prevSt
        context address_accepts_funds_assumption))
  (contract_state prevSt) =
Some (r, contract_state_after)
prevList: list Step
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
H0: False
get_default 0 user (Crowdfunding_backers contract_state_after) > 0 contradiction.
  -
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
sender, recipient: addr
amount0: wei
prf: sender <> contract_address /\
noOverflowOrUnderflowInTransfer sender recipient amount0
  (balance prevSt) &&
address_accepts_funds_assumption None sender recipient amount0 =
true
prevList: list Step
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
H0: True
get_default 0 user (Crowdfunding_backers (contract_state prevSt)) > 0 assumption.
  -
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
block_count, time_passing: int256
prf: validTimeChange block_count time_passing 
  (block_number prevSt) 
  (timestamp prevSt) = true
prevList: list Step
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
H0: True
get_default 0 user (Crowdfunding_backers (contract_state prevSt)) > 0 assumption.
  -
snapshot_timestamp, snapshot_number: int256
snapshot_blockhash: int256 -> int256
snapshot_balances: addr -> wei
HmemOps, memModelOps: MemoryModelOps mem
contract_address: addr
address_accepts_funds: option ContractState ->
addr -> addr -> wei -> bool
user: addr
amount: Z
start, prevSt: BlockchainState
prevList: list Step
H2: get_default 0 user
  (Crowdfunding_backers (contract_state prevSt)) > 0
H0: True
get_default 0 user (Crowdfunding_backers (contract_state prevSt)) > 0 assumption.
Qed.