From 21a6ae430b3a3e0c6922d026215adde994eaa8bd Mon Sep 17 00:00:00 2001 From: Yoichi Hirai Date: Wed, 26 Oct 2016 12:03:39 +0200 Subject: [PATCH] Optimizing definitions for shorter proofs --- ContractSem.thy | 49 ++++++++++++++++++++++++++++++------ RelationalSem.thy | 9 +++++-- example/Deed.thy | 48 ++++++++++++++++++++++------------- example/FailOnReentrance.thy | 45 +++++++++++---------------------- 4 files changed, 93 insertions(+), 58 deletions(-) diff --git a/ContractSem.thy b/ContractSem.thy index caee5b2..d658a14 100644 --- a/ContractSem.thy +++ b/ContractSem.thy @@ -1259,15 +1259,48 @@ transferring value to our contract.*} inductive build_venv_returned :: "account_state \ return_result \ variable_env \ bool" where venv_returned: -" account_ongoing_calls a = recovered # _ \ (* finding an ongoing call *) - is_call_like (lookup (program_content (account_code a)) (venv_pc recovered - 1)) \ - new_bal \ account_balance a \ (* the balance might have increased from the account state *) - build_venv_returned a r - (recovered \ - 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)) \ + new_bal \ a_bal \ (* the balance might have increased from the account state *) + build_venv_returned + \ account_address = a_addr + , account_storage = a_storage + , account_code = a_code + , account_balance = a_bal + , account_ongoing_calls = + \ 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 + \ # _ + , account_killed = _ + \ + r + (\ 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 (\ _. 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 \)" declare build_venv_returned.simps [simp] diff --git a/RelationalSem.thy b/RelationalSem.thy index 3291bfd..77aa7ff 100644 --- a/RelationalSem.thy +++ b/RelationalSem.thy @@ -240,8 +240,13 @@ after every possible round. Also the template states that no annotation failure definition no_assertion_failure :: "(account_state \ bool) \ bool" where "no_assertion_failure (I :: account_state \ bool) == - (\ init callenv. I (fst init) \ snd init = ProgramInit callenv \ - (\ fin. star (one_round I) init fin \ + (\ addr str code bal ongoing killed callenv. + I \ account_address = addr, account_storage = str, account_code = code, + account_balance = bal, account_ongoing_calls = ongoing, account_killed = killed \ \ + (\ fin. star (one_round I) ( + \ account_address = addr, account_storage = str, account_code = code, + account_balance = bal, account_ongoing_calls = ongoing, account_killed = killed \ + , ProgramInit callenv) fin \ I (fst fin) \ snd fin \ ProgramAnnotationFailure))" diff --git a/example/Deed.thy b/example/Deed.thy index dafebc6..dc832d6 100644 --- a/example/Deed.thy +++ b/example/Deed.thy @@ -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) @@ -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 @@ -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) @@ -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 diff --git a/example/FailOnReentrance.thy b/example/FailOnReentrance.thy index e240af8..5001017 100644 --- a/example/FailOnReentrance.thy +++ b/example/FailOnReentrance.thy @@ -134,7 +134,10 @@ 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) @@ -142,44 +145,24 @@ apply(drule fail_on_reentrance_invariant.cases; 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)