Theory Casino

theory Casino 
  imports Solidity_Main "HOL-Eisbach.Eisbach" "HOL-Eisbach.Eisbach_Tools"
begin

section ‹Casino Contract›
text ‹
  In the following we verify the Casino contract from the VerifyThis Long-Term Challenge:
  🌐‹https://verifythis.github.io/02casino/›
  🌐‹https://verifythis.github.io/ltc/02casino/›.
›

subsection ‹Specification›

text ‹
  In the following we describe the specification of the contract.
›

text ‹
  Method modifiers are formalized as abbreviations.
  They need to be formalized in the Solidity context to provide access to various contextual information.
›
abbreviation "state ≡ STR ''state''"
abbreviation "operator ≡ STR ''operator''"
abbreviation "player ≡ STR ''player''"
abbreviation "pot ≡ STR ''pot''"
abbreviation "hashedNumber ≡ STR ''hashedNumber''"
abbreviation "bet ≡ STR ''bet''"
abbreviation "guess ≡ STR ''guess''"
abbreviation "hashNum ≡ STR ''hashNum''"
abbreviation "secret ≡ STR ''secret''"
abbreviation "bet_old ≡ STR ''bet_old''"
abbreviation "secretNumber ≡ STR ''secretNumber''"
abbreviation "amount ≡ STR ''amount''"


abbreviation "IDLE ≡ 0"
abbreviation "GAME_AVAILABLE ≡ 1"
abbreviation "BET_PLACED ≡ 2"
abbreviation "HEADS ≡ 0"
abbreviation "TAILS ≡ 1"
abbreviation "CoinT ≡ SType.TValue TSint"
abbreviation "StateT ≡ SType.TValue TSint"
abbreviation "AddressT ≡ SType.TValue TAddress"
abbreviation "IntT ≡ SType.TValue TSint"
abbreviation "Bytes32T ≡ SType.TValue (TBytes 32)"


context Solidity
begin

abbreviation byOperator::"(unit, ex, 'a state) state_monad" where
  "byOperator ≡ assert Err (λs. storage_data.Value (valtype.Address msg_sender) = state.Storage s this operator)"

abbreviation inState:: "'a valtype ⇒ (unit, ex, 'a state) state_monad" where
  "inState st ≡ assert Err (λs. state.Storage s this state = storage_data.Value st)"

abbreviation noActiveBet::"(unit, ex, ('a, 'b) state_scheme) state_monad" where
  "noActiveBet ≡ assert Err (λs. state.Storage s this state ≠ storage_data.Value (Uint 2))"

end

text ‹
  The contract can now be specified using the "contract" command.
  This command requires the following:
  ▪ A sequence of member variables
  ▪ A constructor
  ▪ A sequence of methods
›

contract Casino
  for state: StateT
  and operator: AddressT
  and player: AddressT
  and pot: IntT
  and hashedNumber: Bytes32T
  and bet: IntT
  and guess: CoinT

constructor payable
where
  "⟨skip⟩"

cfunction createGame external payable
  param hashNum: "SType.TValue (TBytes 32)"
where
  "do {
    byOperator;
    inState (valtype.Uint 0);
    hashedNumber [] ::=⇩s hashNum ~ [];
    state [] ::=⇩s ⟨sint⟩ 1
   }",

cfunction placeBet external payable
  param guess: "SType.TValue TSint"
where
  "do {
    inState (valtype.Uint 1);
    ⟨assert⟩ (⟨¬⟩ (⟨sender⟩ ⟨=⟩ operator ~⇩s []));
    ⟨assert⟩ (⟨value⟩ ⟨<⟩ (pot  ~⇩s []) ⟨∨⟩ ⟨value⟩ ⟨=⟩ (pot ~⇩s []));
    state [] ::=⇩s ⟨sint⟩ 2;
    player [] ::=⇩s ⟨sender⟩;
    bet [] ::=⇩s ⟨value⟩;
    guess [] ::=⇩s guess ~ []
  }",

cfunction decideBet external payable
  param secretNumber: IntT
where
  "do {
    byOperator;
    inState (Uint BET_PLACED);
    ⟨assert⟩ (hashedNumber ~⇩s [] ⟨=⟩ (⟨keccak256⟩ (secretNumber ~ [])));
    decl TSint secret;
    secret [] ::= IF ((secretNumber ~ []) ⟨%⟩ ⟨sint⟩ 2) ⟨=⟩ (⟨sint⟩ 0) THEN ⟨sint⟩ HEADS ELSE ⟨sint⟩ TAILS;
    IF (secret ~ []) ⟨=⟩ (guess ~⇩s []) THEN
      do {
        pot [] ::=⇩s ((pot ~⇩s []) ⟨-⟩ (bet ~⇩s []));
        bet [] ::=⇩s ⟨sint⟩ 0;
        ⟨transfer⟩ (player ~⇩s []) ((bet ~⇩s []) ⟨*⟩ (⟨sint⟩ 2))
      }
    ELSE
      do {
        pot [] ::=⇩s pot ~⇩s [] ⟨+⟩ bet ~⇩s [];
        bet [] ::=⇩s ⟨sint⟩ 0
      };
    state [] ::=⇩s ⟨sint⟩ IDLE
  }",

cfunction addToPot external payable
where
  "do {
    byOperator;
    pot [] ::=⇩s pot ~⇩s [] ⟨+⟩ ⟨value⟩
  }",

cfunction removeFromPot external payable
  param amount: "SType.TValue TSint"
where
  "do {
    byOperator;
    noActiveBet;
    pot [] ::=⇩s ((pot ~⇩s []) ⟨-⟩ (amount ~ []));
    ⟨transfer⟩ (operator ~⇩s []) (amount ~ [])
  }"

thm casino.addToPot_def

invariant pot_balance sb where
    "(fst sb state = storage_data.Value (Uint BET_PLACED)
      ⟶ snd sb ≥ unat (valtype.uint (storage_data.vt (fst sb pot))) + unat (valtype.uint (storage_data.vt (fst sb bet)))
        ∧ valtype.uint (storage_data.vt (fst sb bet)) ≤ valtype.uint (storage_data.vt (fst sb pot))) ∧
    (fst sb state ≠ storage_data.Value (Uint BET_PLACED)
      ⟶ snd sb ≥ unat (valtype.uint (storage_data.vt (fst sb pot))))"
  for "casino"

section ‹Verifying an Invariant›

text ‹
  We start by verifying an invariant regarding the relationship between pot and balance.
  To this end we need to add type information to the invariant.
  Note that an invariant is formalized as a predicate over the contracts state and balance.
›

text ‹We need to create introduction and elimination rules for the invariant and add it to the wprules and wperule lists.›

text ‹
  Now we can start verifying the invariant.
  To this end our package provides a keyword invariant which takes a property as parameter and generates proof obligations.
›

context casino
begin

lemma sym2:
  assumes "storage_data.Value v = state.Storage s this x"
    shows "state.Storage s this x = storage_data.Value v"
  using assms by simp

lemma kdequals_true_dest[wpdrules]:
  assumes "kdequals a b = Some (rvalue.Value (Bool True))"
  shows "a = b"
  using assms
  apply (cases a;simp add: kdequals_def)
  apply (cases b;simp add: kdequals_def)
  by (case_tac x4;case_tac x4a;simp add: kdequals_def split: if_split_asm)


lemma kdequals_false_dest[wpdrules]:
assumes "kdequals a b = Some (rvalue.Value (Bool False))"
shows "a ≠ b"
  using assms
  apply (cases a;simp add: kdequals_def)
  apply (cases b;simp add: kdequals_def)
  by (case_tac x4;case_tac x4a;simp add: kdequals_def split: if_split_asm)

lemma kdnot_dest[wpdrules]:
  assumes "kdnot ya = Some (rvalue.Value (Bool True))"
  shows "ya=rvalue.Value (Bool False)"
  using assms apply (cases ya;simp add:assms kdnot_def)
  by (case_tac x4;simp add:assms vtnot_def)

lemma vt_or_dest:
  assumes "lift_value_binary vtor ye yg = Some (rvalue.Value (Bool True))"
  shows "ye = rvalue.Value (Bool True) ∨ yg = rvalue.Value (Bool True)"
 using assms
  apply (cases ye;simp add: vtor_def)
  apply (cases yg;simp add: vtor_def)
  by (case_tac x4;case_tac x4a;simp)
 

lemma kdless_dest[wpdrules]:
  assumes "kdless (rvalue.Value (Uint x)) (rvalue.Value (Uint y)) = Some (rvalue.Value (Bool True))"
  shows "x < y"
 using assms
  apply (cases x;simp add: kdless_def)
  apply (cases y;simp add: kdless_def)
  by (case_tac n;case_tac na;simp add: vtless_def)

lemma kdequals_bool_sint[wpsimps]: "kdequals (rvalue.Value (Bool x)) (rvalue.Value (Uint y)) = None"
  unfolding kdequals_def by simp 

lemma unat_add_imp:
  assumes "(unat (x::256 word) + unat y < 115792089237316195423570985008687907853269984665640564039457584007913129639936)"
    shows "(unat (x + y) = unat x + unat y)" using assms Word.unat_add_lem[where ?'a=256, of x y] by simp

lemma unat_mult_imp:
  assumes "(unat (x::256 word) * unat y < 115792089237316195423570985008687907853269984665640564039457584007913129639936)"
    shows "(unat (x * y) = unat x * unat y)" using assms Word.unat_mult_lem[where ?'a=256, of x y] by simp

lemma unat_sub_imp:
  assumes "(y::256 word) ≤ (x::256 word)"
    shows "(unat (x - y) = unat x - unat y)" using assms Word.unat_sub[where ?'a=256, of y x] by simp

lemma no_plus_overflow_leq:
  assumes a:"(x ::256 word) ≤ y"
      and b: "unat y + unat z < 2 ^ 256"
    shows "x ≤ y + z" using no_plus_overflow_unat_size[of z y] le_no_overflow[OF a, of z]
proof -
  have "size z = 256" using word_size[of z] by simp
  with b have "z ≤ z + y" using no_plus_overflow_unat_size[of z y] by simp
  then have "x ≤ z + y" using le_no_overflow[OF a, of z] by simp
  then show ?thesis by (simp add: add.commute)
qed

lemma 111:
  fixes pot
  assumes "unat pot ≤ Balances s this"
      and *: "x ≤ pot"
    shows "unat (pot - x) ≤ Balances s this + unat msg_value - unat x"
 using assms unat_sub[OF *]  by simp

lemma 222: "⋀pot. unat pot ≤ Balances s this ⟹
       x ≤ pot ⟹
    unat (pot - x) ≤ Balances s this + unat msg_value"
  using 111 by fastforce

end

method solve methods m = (m ; fail)

lemma (in Contract) wp_assign_storage111[wperules]:
  assumes "rvalue.Value v=y"
      and "wp (storage_update_monad [] is (K (storage_data.Value v)) i) P E s"
    shows "wp (assign_storage i is y) P E s"
  using assms by auto

lemma notwp[wperules]: "¬ wp m P E s ⟹ wp m P E s ⟹ R" using notE by simp

abbreviation(in Contract) createGame_post where
"createGame_post hN start_state return_value end_state ≡
  state.Storage end_state this STR ''state'' = storage_data.Value (Uint 1)"

abbreviation(in Contract) placeBet_post where
"placeBet_post hn start_state return_value end_state ≡
  state.Storage end_state this STR ''state'' = storage_data.Value (Uint 2)"

abbreviation(in Contract) decideBet_post where
"decideBet_post hn start_state return_value end_state ≡
  state.Storage end_state this STR ''state'' = storage_data.Value (Uint 0)"

declare(in casino) pot_balanceI[wprules del]

verification pot_balance:
  pot_balance
  "(K True)" "K (K (K True))"
  "createGame" "(K (K True))" "createGame_post" and
  "placeBet" "(K (K True))" "placeBet_post" and
  "decideBet" "(K (K True))" "decideBet_post" and
  "addToPot" "(K True)" "K (K (K True))" and
  "removeFromPot" "(K (K True))" "K (K (K (K True)))"
  for "casino"
proof -
  show "⋀call. (⋀x h r. effect (call x) h r ⟹ vcond x h r)
        ⟹ effect (constructor call) s r
        ⟹ post s r pot_balance (K True) (K (K (K True)))"
    unfolding constructor_def
    apply (erule post_exc_true, erule_tac post_wp)
    unfolding  inv_state_def
  by (vcg wprules: pot_balanceI | auto)+

  show "⋀call hashNum. (⋀x h r. effect (call x) h r ⟹ vcond x h r)
        ⟹ effect (createGame call hashNum) s r
        ⟹ inv_state pot_balance s
        ⟹ post s r pot_balance (K True) (createGame_post hashNum)"
    unfolding createGame_def
    apply (erule post_exc_true, erule_tac post_wp)
    unfolding  inv_state_def
  by (vcg wprules: pot_balanceI | solve‹auto simp add:wpsimps›)+

  show "⋀call guess. (⋀x h r. effect (call x) h r ⟹ vcond x h r)
        ⟹ effect (placeBet call guess) s r
        ⟹ inv_state pot_balance s
        ⟹ post s r pot_balance (K True) (placeBet_post guess)"
    unfolding placeBet_def
    apply (erule post_exc_true, erule_tac post_wp)
    unfolding  inv_state_def
    apply (vcg | solve‹auto simp add:wpsimps dest:sym›)+
    apply (auto dest!: vt_or_dest)[1]
    apply (vcg wprules: pot_balanceI | solve‹auto simp add:wpsimps dest:sym›)+
  done

  show "⋀call secretNumber. (⋀x h r. effect (call x) h r ⟹ vcond x h r)
        ⟹ effect (decideBet call secretNumber) s r
        ⟹ inv_state pot_balance s
        ⟹ post s r pot_balance (K True) (decideBet_post secretNumber)"
    unfolding decideBet_def
    apply (erule post_exc_true, erule_tac post_wp)
    unfolding  inv_state_def
    apply (vcg wprules: pot_balanceI | solve‹auto simp add:wpsimps›)+
    apply (auto simp add:wpsimps)[1]
    apply (vcg wprules: pot_balanceI | solve‹auto simp add:wpsimps›)+
    apply (auto simp add:wpsimps unat_sub_imp)[1]
    apply (case_tac "this = ada")
    apply (vcg wprules: pot_balanceI | solve‹auto simp add:wpsimps›)+
    apply (auto simp add:wpsimps dest:sym)[1]
    apply (case_tac "this = ada")
    apply (vcg wprules: pot_balanceI | solve‹auto simp add:wpsimps dest:sym2›)+
    apply (auto simp add:wpsimps)[1]
    apply (metis trans_le_add1 unat_add_imp)
    apply (auto simp add:wpsimps dest:sym)[1]
    apply (vcg wprules: pot_balanceI | solve‹auto simp add:wpsimps dest:sym›)+
    apply (auto simp add:wpsimps)[1]
    apply (case_tac "this = ada")
    apply (vcg wprules: pot_balanceI | solve‹auto simp add:wpsimps dest:sym›)+
    apply (auto simp add:wpsimps dest:sym)[1]
    apply (vcg wprules: pot_balanceI | solve‹auto simp add:wpsimps dest:sym›)+
    apply (auto simp add:wpsimps unat_sub_imp dest:sym)[9]
    apply (vcg wprules: pot_balanceI | solve‹auto simp add:wpsimps dest:sym2›)+
    apply (auto simp add:wpsimps unat_sub_imp dest:sym)[9]
    apply (vcg wprules: pot_balanceI | solve‹auto simp add:wpsimps dest:sym2›)+
    apply (auto simp add:wpsimps)[1]
    apply (case_tac "this = ada")
    apply (vcg wprules: pot_balanceI | solve‹auto simp add:wpsimps dest:sym2›)+
    apply (auto simp add:wpsimps)[1]
    apply (metis trans_le_add1 unat_add_imp)
    apply (metis trans_le_add1 unat_add_imp)
    apply (auto simp add:wpsimps dest:sym)
    apply (vcg wprules: pot_balanceI | solve‹auto simp add:wpsimps›)+
    done

  show "⋀call.
       (⋀x h r. effect (call x) h r ⟹ vcond x h r) ⟹
       effect (addToPot call) s r ⟹
       inv_state pot_balance s ⟹ post s r pot_balance (K True) (K (K (K True)))"
    unfolding addToPot_def
    apply (erule post_exc_true, erule_tac post_wp)
    unfolding  inv_state_def
    apply (vcg wprules: pot_balanceI | solve‹auto simp add:wpsimps dest:unat_add_imp sym›)+
    apply (auto simp add:wpsimps no_plus_overflow_leq unat_sub_imp unat_mult_imp unat_add_imp dest:sym)
    apply (vcg wprules: pot_balanceI | solve‹auto simp add:wpsimps dest:unat_add_imp sym›)+
  done
      
  show "⋀call amount.
       (⋀x h r. effect (call x) h r ⟹ vcond x h r) ⟹
       effect (removeFromPot call amount) s r ⟹
       inv_state pot_balance s ⟹
       post s r pot_balance (K True) (K (K (K (K True))) amount)"
    unfolding removeFromPot_def
    apply (erule post_exc_true, erule_tac post_wp)
    apply (cases "msg_sender=this")
    unfolding inv_state_def
    apply (vcg | solve‹auto simp add:wpsimps dest:unat_add_imp sym›)+
    apply (drule_tac s = this in sym)
    apply (auto simp add:wpsimps dest:unat_add_imp sym)
    apply (vcg | solve‹auto simp add:wpsimps dest:unat_add_imp sym›)+
    apply (auto simp add:wpsimps dest:unat_add_imp sym)
    apply (vcg | solve‹auto simp add:wpsimps dest:unat_add_imp sym›)+
    apply (auto simp add:wpsimps dest:unat_add_imp sym)
    apply (vcg | solve‹auto simp add:wpsimps dest:unat_add_imp sym›)+
    apply (rule_tac pot_balanceI)
    apply (auto simp add:wpsimps intro: 111 222 dest:unat_add_imp sym)
    apply (vcg | solve‹auto simp add:wpsimps dest:unat_add_imp sym›)+
    apply (rule_tac pot_balanceI)
    apply (auto simp add:wpsimps dest:unat_add_imp sym)
    apply (vcg | solve‹auto simp add:wpsimps dest:unat_add_imp sym›)+
    apply (auto simp add:wpsimps dest:unat_add_imp sym)
    apply (vcg | solve‹auto simp add:wpsimps dest:unat_add_imp sym›)+
    apply (auto simp add:wpsimps dest:unat_add_imp sym)
    apply (vcg | solve‹auto simp add:wpsimps dest:unat_add_imp sym›)+
    apply (rule_tac pot_balanceI)
    apply (auto simp add:wpsimps intro: 111 dest:unat_add_imp sym)
    apply (vcg | solve‹auto simp add:wpsimps dest:unat_add_imp sym›)+
    apply (rule_tac pot_balanceI)
    apply (auto simp add:wpsimps dest:unat_add_imp sym)
    apply (vcg | solve‹auto simp add:wpsimps dest:unat_add_imp sym›)+
  done
qed

context casino_external
begin
  thm pot_balance
  thm vcond_def
end

end