Skip to content

Commit

Permalink
Optimizing definitions for shorter proofs
Browse files Browse the repository at this point in the history
  • Loading branch information
@pirapira
pirapira committed Oct 26, 2016
1 parent 6caf6b7 commit 21a6ae4
Show file tree
Hide file tree
Showing 4 changed files with 93 additions and 58 deletions.
49 changes: 41 additions & 8 deletions ContractSem.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1259,15 +1259,48 @@ transferring value to our contract.*}
inductive build_venv_returned :: "account_state \<Rightarrow> return_result \<Rightarrow> variable_env \<Rightarrow> bool"
where
venv_returned:
" account_ongoing_calls a = recovered # _ \<Longrightarrow> (* finding an ongoing call *)
is_call_like (lookup (program_content (account_code a)) (venv_pc recovered - 1)) \<Longrightarrow>
new_bal \<ge> account_balance a \<Longrightarrow> (* the balance might have increased from the account state *)
build_venv_returned a r
(recovered \<lparr>
venv_stack := 1 # venv_stack recovered (* 1 is pushed, indicating a return *)
, venv_storage := account_storage a
, venv_balance := (update_balance (account_address a)
" is_call_like (lookup (program_content a_code) (v_pc - 1)) \<Longrightarrow>
new_bal \<ge> a_bal \<Longrightarrow> (* the balance might have increased from the account state *)
build_venv_returned
\<lparr> account_address = a_addr
, account_storage = a_storage
, account_code = a_code
, account_balance = a_bal
, account_ongoing_calls =
\<lparr> venv_stack = v_stack
, venv_memory = v_memory
, venv_memory_usage = v_memory_usage
, venv_storage = v_storage
, venv_pc = v_pc
, venv_balance = v_balance
, venv_caller = v_caller
, venv_value_sent = v_value
, venv_data_sent = v_data
, venv_storage_at_call = v_init_storage
, venv_balance_at_call = v_init_balance
, venv_origin = v_origin
, venv_ext_program = v_ext_program
, venv_block = v_block
\<rparr> # _
, account_killed = _
\<rparr>
r
(\<lparr> venv_stack = 1 # v_stack (* 1 is pushed, indicating a return *)
, venv_memory = v_memory
(* TODO: update the memory *)
, venv_memory_usage = v_memory_usage
, venv_storage = a_storage
, venv_pc = v_pc
, venv_balance = (update_balance a_addr
(\<lambda> _. new_bal) (return_balance r))
, venv_caller = v_caller
, venv_value_sent = v_value
, venv_data_sent = v_data
, venv_storage_at_call = v_init_storage
, venv_balance_at_call = v_init_balance
, venv_origin = v_origin
, venv_ext_program = v_ext_program
, venv_block = v_block
\<rparr>)"

declare build_venv_returned.simps [simp]
Expand Down
9 changes: 7 additions & 2 deletions RelationalSem.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -240,8 +240,13 @@ after every possible round. Also the template states that no annotation failure
definition no_assertion_failure :: "(account_state \<Rightarrow> bool) \<Rightarrow> bool"
where
"no_assertion_failure (I :: account_state \<Rightarrow> bool) ==
(\<forall> init callenv. I (fst init) \<longrightarrow> snd init = ProgramInit callenv \<longrightarrow>
(\<forall> fin. star (one_round I) init fin \<longrightarrow>
(\<forall> addr str code bal ongoing killed callenv.
I \<lparr> account_address = addr, account_storage = str, account_code = code,
account_balance = bal, account_ongoing_calls = ongoing, account_killed = killed \<rparr> \<longrightarrow>
(\<forall> fin. star (one_round I) (
\<lparr> account_address = addr, account_storage = str, account_code = code,
account_balance = bal, account_ongoing_calls = ongoing, account_killed = killed \<rparr>
, ProgramInit callenv) fin \<longrightarrow>
I (fst fin) \<and>
snd fin \<noteq> ProgramAnnotationFailure))"

Expand Down
48 changes: 31 additions & 17 deletions example/Deed.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -619,7 +619,11 @@ subsection {* Proof that the Invariant is Kept *}

text {* The following lemma states that, if the account's code is either empty or the
Deed contract's code, that is still the case after an invocation. *}


(*
declare strict_if_split [split]
*)

lemma deed_keeps_invariant :
"no_assertion_failure deed_inv"
apply(simp only: no_assertion_failure_def)
Expand All @@ -631,20 +635,30 @@ apply(rule allI)
apply(rule impI)
apply(drule star_case; auto)
apply(case_tac steps; auto)
apply(split if_splits; auto)
apply(split strict_if_split; auto)
apply(split strict_if_split; auto)
apply(case_tac steps; auto)
apply(split strict_if_split; auto)
apply(split strict_if_split; auto)
apply(split strict_if_split; auto)
apply(case_tac steps; auto)
apply(split strict_if_split; auto)
apply(split strict_if_split; auto)
apply(split strict_if_split; auto)
apply(case_tac steps; auto)
apply(case_tac steps; auto)
apply(case_tac steps; auto)
apply(split strict_if_split; simp)
apply(split strict_if_split; simp)
apply(split strict_if_split; simp)
apply(split strict_if_split; simp)
apply(split strict_if_split; simp)
apply(split strict_if_split; simp)
apply(split strict_if_split; simp)
apply(split strict_if_split; simp)
apply(split strict_if_split; simp)
apply(auto)
apply(split strict_if_split; simp)
apply(auto)
apply(split strict_if_split; simp)
apply(auto)
apply(split strict_if_split; auto)
apply(split if_splits)
apply(split if_splits)
apply(simp)
apply(auto)
apply(drule star_case; auto)
apply(case_tac ac; auto)
(* still need to see pc of something... *)


done


Expand Down Expand Up @@ -683,7 +697,7 @@ apply(simp add: pre_post_conditions_def; auto)
apply(split strict_if_split; auto)
apply(split strict_if_split; auto)
apply(split strict_if_split; auto)
apply(case_tac steps; auto)
(* apply(case_tac steps; auto)
apply(split strict_if_split; auto)
apply(split strict_if_split; auto)
apply(split strict_if_split; auto)
Expand Down Expand Up @@ -749,7 +763,7 @@ apply(simp add: pre_post_conditions_def; auto)
apply(drule star_case; auto)
apply(case_tac steps; case_tac initial_account; auto)
apply(drule star_case; auto)
apply(case_tac steps; case_tac initial_account; auto)
apply(case_tac steps; case_tac initial_account; auto) *)
done

text {* It takes 15 minutes to compile this proof on my machine. Most of the time is spent
Expand Down
45 changes: 14 additions & 31 deletions example/FailOnReentrance.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -134,52 +134,35 @@ lemma invariant_kept:
"no_assertion_failure fail_on_reentrance_invariant"
apply(simp add: no_assertion_failure_def)
apply(rule allI)
apply(rule impI)
apply(rule allI)
apply(rule allI)
apply(rule allI)
apply(rule allI)
apply(rule allI)
apply(rule impI)
apply(drule fail_on_reentrance_invariant.cases; auto)
apply(drule star_case; auto)
apply(rule depth_zero; auto)
apply(case_tac steps; auto)
apply(drule star_case; auto) (* called out and coming back *)
apply(rule depth_one; simp?)
apply(simp)
apply(simp)
apply(simp)
apply(drule fail_on_reentrance_invariant.cases; auto)
apply(case_tac steps; auto)
apply(rule depth_zero; simp?)
apply(drule fail_on_reentrance_invariant.cases; auto)
apply(drule fail_on_reentrance_invariant.cases; auto)
apply(drule fail_on_reentrance_invariant.cases; auto)
apply(drule fail_on_reentrance_invariant.cases; auto)
apply(rule depth_one; simp)
apply(case_tac steps; auto)
apply(drule fail_on_reentrance_invariant.cases; auto)
apply(rule depth_one; simp?)
apply(simp)
apply(simp)
apply(simp)
apply(drule fail_on_reentrance_invariant.cases; auto)
apply(drule fail_on_reentrance_invariant.cases; auto)
apply(drule fail_on_reentrance_invariant.cases; auto)
apply(case_tac steps; auto)
apply(rule depth_zero; simp?)
apply(case_tac steps; auto)
apply(case_tac steps; auto)
apply(rule depth_zero; auto)
apply(drule fail_on_reentrance_invariant.cases; auto)
apply(case_tac steps; auto)
apply(case_tac steps; auto; rule depth_zero; auto)
apply(case_tac steps; auto)
apply(drule star_case; auto)
apply(case_tac steps; auto)
apply(drule star_case; auto)
apply(drule fail_on_reentrance_invariant.cases; auto)
apply(case_tac steps; auto)
apply(drule fail_on_reentrance_invariant.cases; auto)
apply(drule fail_on_reentrance_invariant.cases; auto)
apply(drule fail_on_reentrance_invariant.cases; auto)
apply(drule fail_on_reentrance_invariant.cases; auto)
apply(case_tac steps; auto)
apply(drule fail_on_reentrance_invariant.cases; auto)
apply(drule fail_on_reentrance_invariant.cases; auto)
apply(drule fail_on_reentrance_invariant.cases; auto)
apply(drule fail_on_reentrance_invariant.cases; auto)
apply(case_tac steps; auto)
apply(case_tac steps; auto)
apply(case_tac steps; auto)
apply(drule fail_on_reentrance_invariant.cases; auto)
apply(case_tac steps; auto)
apply(case_tac steps; auto)
apply(drule star_case; auto)
Expand Down

0 comments on commit 21a6ae4

Please sign in to comment.