diff --git a/Isabelle/Chi_Calculus/Proper_Transition_System.thy b/Isabelle/Chi_Calculus/Proper_Transition_System.thy index 3739800..6c94735 100644 --- a/Isabelle/Chi_Calculus/Proper_Transition_System.thy +++ b/Isabelle/Chi_Calculus/Proper_Transition_System.thy @@ -26,7 +26,7 @@ primrec basic_action_of :: "proper_action \ basic_action" where subsection \Output Rests\ text \ - An output rest bundles the scope openings, the output value, and the target process of an output + An output rest bundles the scope extrudings, the output value, and the target process of an output transition. Its syntax is part of the syntax of output transitions. \ @@ -36,7 +36,7 @@ datatype 'p output_rest = text \ Note that the definition of \output_rest\ is actually more permissive than the verbal definition - of output rests above: the number of scope openings of a particular \output_rest\ value is not + of output rests above: the number of scope extrudings of a particular \output_rest\ value is not necessarily fixed, since the structure of a follow-up output rest in a \WithOpening\ value can depend on the given channel. This is just to keep the definition simple. It does not cause any problems in our later proofs. @@ -55,8 +55,8 @@ where "output_rest_lift \ rel_output_rest" lemmas output_rest_lift_intros = output_rest.rel_intros -lemmas without_opening_lift = output_rest_lift_intros(1) -lemmas with_opening_lift = output_rest_lift_intros(2) +lemmas without_extruding_lift = output_rest_lift_intros(1) +lemmas with_extruding_lift = output_rest_lift_intros(2) lemmas output_rest_lift_cases = output_rest.rel_cases text \ @@ -131,9 +131,9 @@ inductive where simple: "p \\<^sub>\\basic_action_of \\ q \ p \\<^sub>\\\\ q" | - output_without_opening: + output_without_extruding: "p \\<^sub>\\a \ x\ q \ p \\<^sub>\\a \ x\ q" | - output_with_opening: + output_with_extruding: "\ p \\<^sub>\\\ b\ Q b; \b. Q b \\<^sub>\\a \ K b \ \ p \\<^sub>\\a \ \ b. K b" text \ @@ -180,7 +180,7 @@ proof proper.is_simulation_standard then show ?case by (blast intro: proper_transition.simple simple_lift) next - case (output_without_opening p a x p' q) + case (output_without_extruding p a x p' q) from \p \\<^sub>\ q\ and \p \\<^sub>\\a \ x\ p'\ obtain q' where "q \\<^sub>\\a \ x\ q'" and "p' \\<^sub>\ q'" using @@ -191,9 +191,9 @@ proof proper.is_simulation_standard basic_residual.distinct(2) by smt then show ?case - by (blast intro: proper_transition.output_without_opening without_opening_lift output_lift) + by (blast intro: proper_transition.output_without_extruding without_extruding_lift output_lift) next - case (output_with_opening p P a K q) + case (output_with_extruding p P a K q) obtain Q where "q \\<^sub>\\\ a\ Q a" and "\a. P a \\<^sub>\ Q a" proof - from \p \\<^sub>\ q\ and \p \\<^sub>\\\ a\ P a\ @@ -220,7 +220,7 @@ proof proper.is_simulation_standard *) obtain L where "\b. Q b \\<^sub>\\a \ L b" and "\b. output_rest_lift (\\<^sub>\) (K b) (L b)" proof - - from output_with_opening.IH and \\b. P b \\<^sub>\ Q b\ + from output_with_extruding.IH and \\b. P b \\<^sub>\ Q b\ have "\b. \l. Q b \\<^sub>\\a \ l \ output_rest_lift (\\<^sub>\) (K b) l" using proper_lift_cases and @@ -232,9 +232,9 @@ proof proper.is_simulation_standard with that show ?thesis by blast qed from \q \\<^sub>\\\ b\ Q b\ and \\b. Q b \\<^sub>\\a \ L b\ have "q \\<^sub>\\a \ \ b. L b" - by (fact proper_transition.output_with_opening) + by (fact proper_transition.output_with_extruding) with \\a. output_rest_lift (\\<^sub>\) (K a) (L a)\ show ?case - using with_opening_lift and rel_funI and output_lift + using with_extruding_lift and rel_funI and output_lift by smt qed qed diff --git a/Isabelle/Chi_Calculus/Typed_Proper_Transition_System.thy b/Isabelle/Chi_Calculus/Typed_Proper_Transition_System.thy index f7ff3c7..96471d1 100644 --- a/Isabelle/Chi_Calculus/Typed_Proper_Transition_System.thy +++ b/Isabelle/Chi_Calculus/Typed_Proper_Transition_System.thy @@ -21,7 +21,7 @@ primrec untyped_output_rest :: "('a::countable, 'p) typed_output_rest \ K)" abbreviation - typed_with_opening :: "('a channel \ ('b, 'p) typed_output_rest) \ ('b, 'p) typed_output_rest" + typed_with_extruding :: "('a channel \ ('b, 'p) typed_output_rest) \ ('b, 'p) typed_output_rest" (binder "\\" 51) where "\\\. \ \ \ TypedWithOpening (\ \ typed_channel)" @@ -32,10 +32,10 @@ abbreviation where "\\ \\ \ \ \untyped_channel \ \ untyped_output_rest \" -lemma typed_output_without_opening: "p \\<^sub>\\\ \\ \\ q \ p \\<^sub>\\\ \\ \\ q" - by (simp add: output_without_opening) -lemma typed_output_with_opening: +lemma typed_output_without_extruding: "p \\<^sub>\\\ \\ \\ q \ p \\<^sub>\\\ \\ \\ q" + by (simp add: output_without_extruding) +lemma typed_output_with_extruding: "\p \\<^sub>\\\\\\ \ \; \\. \ \ \\<^sub>\\\ \\ \ \\ \ p \\<^sub>\\\ \\ \\\. \ \" - by (simp add: output_with_opening) + by (simp add: output_with_extruding) end diff --git a/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy b/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy index 5008042..62005cb 100644 --- a/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy +++ b/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy @@ -88,7 +88,6 @@ text \ \<^item> A constant that specifies the size (or length) of the VRF values. \<^item> A function that casts a VRF value into a real number. - Also, we postulate some properties on the parameters of the locale: \<^item> We require that the value size be positive. \<^item> We require some properties to hold for VRFs according to the definition in the paper, namely: @@ -99,7 +98,6 @@ text \ be correctly computed, provided that the verification key used to check the correctness is derived from the secret key used to evaluate the VRF. - Theoretically, VRFs must fulfill another property called `pseudorandomness', which is probabilistic and states that it's difficult for an efficient adversary to distinguish a VRF value from a truly random value. Furthermore, the paper uses a special VRF which is more secure than @@ -123,7 +121,7 @@ text \ We also model two special tags that are used as súffixes when calling the VRF: \TEST\ is used in slot leader election, and \NONCE\ when creating and validating block nonces. The purpose of these tags is to provide domain separation, i.e. that we can simulate two independent `virtual VRFs' - from a single VRF. + from a single VRF: \ datatype vrf_query_type = TEST | NONCE @@ -209,14 +207,14 @@ text \ \ definition (in protocol_parameters) slot_epoch :: "slot \ epoch" where - "slot_epoch sl = nat \sl / R\" + [simp]: "slot_epoch sl = nat \sl / R\" text \ and we can check whether a given slot is the first one in its epoch: \ definition (in protocol_parameters) first_in_epoch :: "slot \ bool" where - "first_in_epoch sl = (R dvd (sl - 1))" + [simp]: "first_in_epoch sl = (R dvd (sl - 1))" subsection \ Stake distributions \ @@ -248,7 +246,7 @@ text \ definition absolute_stake_of_set :: "stakeholder_id set \ stake_distr \ stake" (\s\<^sup>+\<^bsub>_\<^esub>'(_')\) where - "s\<^sup>+\<^bsub>X\<^esub>(\) = (\U \ X. \ $$! U)" if "X \ fmdom' \" + [simp]: "s\<^sup>+\<^bsub>X\<^esub>(\) = (\U \ X. \ $$! U)" if "X \ fmdom' \" text \ Based on the previous definition, we define the absolute stake controlled by @{emph \all\} @@ -285,7 +283,7 @@ text \ definition relative_stake_of_set :: "stakeholder_id set \ stake_distr \ relative_stake" (\\\<^sup>+\<^bsub>_\<^esub>'(_')\) where - "\\<^sup>+\<^bsub>X\<^esub>(\) = s\<^sup>+\<^bsub>X\<^esub>(\) / s\<^sup>+\<^sub>\

(\)" if "\ \ {$$}" + [simp]: "\\<^sup>+\<^bsub>X\<^esub>(\) = s\<^sup>+\<^bsub>X\<^esub>(\) / s\<^sup>+\<^sub>\

(\)" if "\ \ {$$}" text \ And we define the relative stake controlled by a @{emph \single\} stakeholder \U\ w.r.t. a stake @@ -343,18 +341,14 @@ text \ stake distribution and that the source stakeholder has enough stake for the withdrawal: \ -function +fun apply_transaction :: "'sig transaction \ stake_distr \ stake_distr" where "apply_transaction ((U\<^sub>i, U\<^sub>j, s), _) \ = ( let \' = \(U\<^sub>i $$:= \ $$! U\<^sub>i - s) in - \'(U\<^sub>j $$:= \' $$! U\<^sub>j + s))" if "{U\<^sub>i, U\<^sub>j} \ fmdom' \" and "\ $$! U\<^sub>i \ s" -| "apply_transaction ((U\<^sub>i, U\<^sub>j, s), \) \ = - undefined ((U\<^sub>i, U\<^sub>j, s), \) \" if "\ ({U\<^sub>i, U\<^sub>j} \ fmdom' \ \ \ $$! U\<^sub>i \ s)" - by (atomize, auto) - termination by lexicographic_order + \'(U\<^sub>j $$:= \' $$! U\<^sub>j + s))" subsection \ Blocks \ @@ -399,7 +393,7 @@ text \ definition apply_block :: "('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) block \ stake_distr \ stake_distr" where - "apply_block B = fold apply_transaction (bl_txs B)" + [simp]: "apply_block B = fold apply_transaction (bl_txs B)" subsection \ Chains \ @@ -414,14 +408,7 @@ text \ We let \\\<^sub>1 \ \\<^sub>2\ indicate that the chain \\\<^sub>1\ is a prefix of the chain \\\<^sub>2\: \ -definition - is_prefix_of :: " - ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain \ - ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain \ - bool" - (infix \\\ 50) -where - "\\<^sub>1 \ \\<^sub>2 \ prefix \\<^sub>1 \\<^sub>2" +notation prefix (infix \\\ 50) text \ We define a function to prune the last \m\ blocks in a chain \\\, denoted by \\\<^bsup>\m\<^esup>\ in the @@ -435,7 +422,7 @@ definition ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain" (\_\<^sup>\\<^bsup>_\<^esup>\ [999] 999) where - "\\<^sup>\\<^bsup>m\<^esup> = take (length \ - m) \" + [simp]: "\\<^sup>\\<^bsup>m\<^esup> = take (length \ - m) \" text \ Also, we define a function to prune the blocks in a chain which have slots greater than a @@ -445,7 +432,7 @@ text \ definition prune_after :: "slot \ ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain \ ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain" where - "prune_after sl = takeWhile (\B. bl_slot B \ sl)" + [simp]: "prune_after sl = takeWhile (\B. bl_slot B \ sl)" text \ And we can apply a chain \\\ to a stake distribution \\\ by sequentially applying all blocks @@ -455,7 +442,7 @@ text \ definition apply_chain :: "('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain \ stake_distr \ stake_distr" where - "apply_chain = fold apply_block" + [simp]: "apply_chain = fold apply_block" subsection \ Functionality \\\$^{\tau,r}_{RLB}$ and subprotocol \\\$_{RLB}$ \ @@ -472,7 +459,10 @@ text \ definition fold1 :: "('a \ 'a \ 'a) \ 'a list \ 'a" where - "fold1 f xs = foldl f (hd xs) (tl xs)" + [simp]: "fold1 f xs = foldl f (hd xs) (tl xs)" + +lemma "fold1 (\\) [a,b,c] = (a \\ b) \\ c" + by simp locale \\<^sub>R\<^sub>L\<^sub>B = protocol_parameters + @@ -520,10 +510,10 @@ text \ notation powr (\_\<^bsup>_\<^esup>\ [81,81] 80) -private definition +definition slot_leader_probability :: "relative_stake \ real" (\\'(_')\) where - "\(\) = 1 - (1 - f)\<^bsup>\\<^esup>" + [simp]: "\(\) = 1 - (1 - f)\<^bsup>\\<^esup>" text \ Next, given epoch \j\, the initial stake distribution \\\<^sub>0\, and a chain \\\, we define a function @@ -556,7 +546,7 @@ text \ \threshold value\}, denoted by \T\<^bsub>U\<^esub>\<^bsup>j\<^esup>(\\<^sub>0, \)\ and defined as follows: \ -private definition +private fun slot_leader_threshold :: " stakeholder_id \ epoch \ @@ -577,7 +567,7 @@ text \ can only check this for themselves, not for other stakeholders): \ -definition +fun is_slot_leader :: " stakeholder_id \ slot \ @@ -615,50 +605,47 @@ locale chain_selection = for \\<^sub>B :: "('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) block \ 'block_hash" begin -context -begin - text \ Since the genesis block is not a proper block in a chain, we have to take care of it separately. - So, we need to check whether two chains are `disjoint', i.e., that the only intersection point + So, we need to check whether two chains are `disjoint', i.e., whether the only intersection point between them is the genesis block. This amounts to checking whether their first blocks are different, since, by construction, if they differ in the first block then they must necessarily diverge: \ -private definition +definition disjoint_chains :: " ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain \ ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain \ bool" where - "disjoint_chains \ \' \ \\<^sub>B (hd \) \ \\<^sub>B (hd \')" if "\ \ []" and "\' \ []" + [iff]: "disjoint_chains \ \' \ \\<^sub>B (hd \) \ \\<^sub>B (hd \')" if "\ \ []" and "\' \ []" text \ Also, we can extract the hashed, longest common prefix of two chains: \ -private definition +definition hashed_lcp :: " ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain \ ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain \ 'block_hash list" where - "hashed_lcp \ \' = Longest_common_prefix {map \\<^sub>B \, map \\<^sub>B \'}" + [simp]: "hashed_lcp \ \' = Longest_common_prefix {map \\<^sub>B \, map \\<^sub>B \'}" text \ Now, we can check whether a chain \\\ forks from another chain \\'\ at most \n\ blocks, i.e. that we should roll back at most the most recent \n\ blocks in \\\ in order to switch to \\'\: \ -private definition +definition forks_at_most :: " nat \ ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain \ ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain \ bool" where - "forks_at_most n \ \' \ ( + [iff]: "forks_at_most n \ \' \ ( if disjoint_chains \ \' then @@ -666,27 +653,42 @@ where else length (drop (length (hashed_lcp \ \')) \) \ n)" +text \ + For implementation purposes, we define a function that, given two chains \\\ and \\'\, obtains + the suffix of \\\ after trimming its hashed longest common prefix with \\'\: +\ + +fun + first_suffix :: " + ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain \ + ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain \ + ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain" +where + "first_suffix \ \' = ( + let + hlcp = longest_common_prefix (map \\<^sub>B \) (map \\<^sub>B \') + in + drop (length hlcp) \)" + text \ Also, we can compute the list of the longest chains in a given list of chains \\\: \ -private definition +abbreviation (input) "is_longest_chain \ \ \ \\' \ set \. length \ \ length \'" + +definition longest_chains :: " ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain list \ ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain list" where - "longest_chains \ = ( - let - is_longest_chain = \\ \. \\' \ set \. length \ \ length \' - in - [\. \ \ \, is_longest_chain \ \])" + "longest_chains \ = [\ \ \. is_longest_chain \ \]" text \ Now we can define the function that implements the `longest chain' rule, namely the $\mathsf{maxvalid}$ function in the paper: \ -definition +fun max_valid :: " ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain \ ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain list \ @@ -694,12 +696,10 @@ definition where "max_valid \ \ = ( let - \' = [\'. \' \ \ # \, forks_at_most k \ \']; \ \the \k\ parameter\ - \' = longest_chains \' + \' = [\' \ \ # \. forks_at_most k \ \']; \ \the \k\ parameter\ + \'' = longest_chains \' in - if \ \ set \' then \ else hd \')" - -end + if \ \ set \'' then \ else hd \'')" end @@ -819,7 +819,7 @@ text \ private definition verify_tx :: "'sig transaction \ ('vkey, 'nonce) genesis \ bool" where - "verify_tx tx G \ ( + [iff]: "verify_tx tx G \ ( let (txbody, \) = tx; (U\<^sub>i, U\<^sub>j, s) = txbody; @@ -835,7 +835,7 @@ text \ private definition verify_tx_data :: "'sig transaction list \ ('vkey, 'nonce) genesis \ bool" where - "verify_tx_data txs G \ (\i \ {0.. (\i \ {0.. A key component of block verification is verifying the block proof, i.e. that the stakeholder who @@ -845,7 +845,8 @@ text \ private definition verify_block_proof :: "slot \ 'vkey \ 'nonce \ ('vrf\<^sub>y, 'vrf\<^sub>\) vrf\<^sub>o \ real \ bool" where - "verify_block_proof sl vk \ v T \ verify\<^sub>V\<^sub>R\<^sub>F vk (\ \\ sl \\ TEST) v \ value_to_real (fst v) < T" + [iff]: "verify_block_proof sl vk \ v T \ + verify\<^sub>V\<^sub>R\<^sub>F vk (\ \\ sl \\ TEST) v \ value_to_real (fst v) < T" text \ Furthermore, we verify that the nonce proof in a block was properly created: @@ -854,7 +855,7 @@ text \ private definition verify_block_nonce :: "slot \ 'vkey \ 'nonce \ ('vrf\<^sub>y, 'vrf\<^sub>\) vrf\<^sub>o \ bool" where - "verify_block_nonce sl vk \ v \ verify\<^sub>V\<^sub>R\<^sub>F vk (\ \\ sl \\ NONCE) v" + [iff]: "verify_block_nonce sl vk \ v \ verify\<^sub>V\<^sub>R\<^sub>F vk (\ \\ sl \\ NONCE) v" text \ Armed with these definitions, we can now verify that a block is indeed valid: @@ -869,7 +870,7 @@ private definition real \ bool" where - "verify_block B oh\<^sub>p\<^sub>r\<^sub>e\<^sub>v G \ T \ ( + [iff]: "verify_block B oh\<^sub>p\<^sub>r\<^sub>e\<^sub>v G \ T \ ( let ((sl, st, d, B\<^sub>\, \), \) = B; (U\<^sub>s, y, \) = B\<^sub>\; @@ -886,13 +887,15 @@ where | Some h\<^sub>p\<^sub>r\<^sub>e\<^sub>v \ the st = h\<^sub>p\<^sub>r\<^sub>e\<^sub>v))" \ \ if \oh\<^sub>p\<^sub>r\<^sub>e\<^sub>v\ is not \None\ then \st\ is not \None\ either \ text \ - and we can verify that a chain is indeed valid: + and we can verify that a chain is indeed valid. It is important to mention that candidate chains + cannot be empty since they were diffused by slot leaders, which built them on top of the genesis + block: \ private definition verify_chain :: "('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain \ ('vkey, 'nonce) genesis \ 'nonce \ bool" where - "verify_chain \ G \ \ (\i \ {0..}. + [iff]: "verify_chain \ G \ \ (\i \ {0..}. let (_, \\<^sub>0, _) = G; B = \ ! i; \ \ current block \ @@ -905,10 +908,10 @@ where verify_block B oh\<^sub>p\<^sub>r\<^sub>e\<^sub>v G \ T\<^sub>s)" text \ - We specify what the initial state for each stakeholder should be: + Finally, we specify what the initial state for each stakeholder should be: \ -definition +fun init_stakeholder_state :: " stakeholder_id \ ('vkey, 'nonce) genesis \ @@ -942,7 +945,7 @@ text \ in the stakeholder's current state: \ -private definition +private fun make_block :: " ('skey, 'vkey, 'hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig, 'nonce) stakeholder_state \ slot \ @@ -967,7 +970,7 @@ text \ it and updating its current `state' to the hash of this block: \ -private definition +private fun extend_chain :: " ('skey, 'vkey, 'hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig, 'nonce) stakeholder_state \ slot \ @@ -996,7 +999,7 @@ private definition 'sig transaction \ ('skey, 'vkey, 'hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig, 'nonce) stakeholder_state" where - "store_tx ss tx = ss\ss_txs := tx # ss_txs ss\" + [simp]: "store_tx ss tx = ss\ss_txs := tx # ss_txs ss\" text \ Also, we define a function to store a given chain in the chains mempool of a stakeholder's state, @@ -1004,7 +1007,7 @@ text \ is valid: \ -private definition +private fun store_chain :: " slot \ ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain \ @@ -1026,7 +1029,7 @@ text \ We define a function to compute the new epoch nonce and store it in the stakeholder's state: \ -private definition +private fun compute_new_epoch_randomness :: " slot \ ('skey, 'vkey, 'hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig, 'nonce) stakeholder_state \ @@ -1043,7 +1046,7 @@ text \ chain seen so far by the stakeholder: \ -private definition +private fun update_local_chain :: " ('skey, 'vkey, 'hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig, 'nonce) stakeholder_state \ ('skey, 'vkey, 'hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig, 'nonce) stakeholder_state" @@ -1125,7 +1128,7 @@ text \ Finally, we define a process that implements a stakeholder running the protocol: \ -definition +fun stakeholder :: " stakeholder_id \ ('vkey, 'nonce) genesis \ @@ -1145,4 +1148,1473 @@ end end +subsection \ Proofs \ + +subsubsection \ Slots and epochs \ + +context protocol_parameters +begin + +text \ + A given epoch \e\<^sub>j\ contains the interval of slots \[(e\<^sub>j - 1) * R + 1, e\<^sub>j * R]\: +\ + +lemma slot_epoch_bounds: + fixes n :: nat + assumes "sl \ {n * R + 1..?x\ = Suc n \ Suc n - 1 < ?x \ ?x \ Suc n" + by (simp add: ceiling_eq_iff) + moreover have "Suc n - 1 < ?x" + proof - + have "(n * R + 1) / R \ ?x" + proof - + have "0 < real R \ real (n * R + 1) \ real sl" + proof - + have "(\ 0 < real R) = (real R \ 0)" + by simp + with assms show ?thesis + by force + qed + then show ?thesis + by (simp add: divide_le_cancel) + qed + moreover have "Suc n - 1 < (n * R + 1) / R" + using R_positivity by (simp add: pos_less_divide_eq) + ultimately show ?thesis + by simp + qed + moreover have "?x \ Suc n" + proof - + from assms have "sl \ Suc n * R" + by simp + then have "((of_nat sl)::real) \ of_nat ((Suc n) * R)" + by (blast intro: of_nat_mono) + also have "\ = of_nat (Suc n) * of_nat R" + by (blast intro: of_nat_mult) + finally have "((of_nat sl)::real) \ of_nat (Suc n) * of_nat R" . + moreover have "(0::real) < of_nat R" + by (simp add: R_positivity) + ultimately show ?thesis + by (simp add: pos_divide_le_eq) + qed + ultimately show ?thesis + by simp +qed + +notepad +begin + assume "R = 2" + then have "slot_epoch 1 = 1" + and "slot_epoch 2 = 1" + and "slot_epoch 3 = Suc 1" + and "slot_epoch 4 = Suc 1" + using slot_epoch_bounds by simp_all +end + +end + +subsubsection \ Stake distributions \ + +context +begin + +notepad +begin + + fix \ :: stake_distr and X :: "stakeholder_id set" + assume a\<^sub>\: "\ = {U\<^bsub>1\<^esub> $$:= 10, U\<^bsub>2\<^esub> $$:= 5, U\<^bsub>3\<^esub> $$:= 10}" and a\<^sub>X: "X = {U\<^bsub>1\<^esub>, U\<^bsub>3\<^esub>}" + from a\<^sub>\ have "s\<^sup>+\<^sub>\

(\) = 25" + proof - + from a\<^sub>\ have "fmdom' \ = {U\<^bsub>1\<^esub>, U\<^bsub>2\<^esub>, U\<^bsub>3\<^esub>}" + by auto + with a\<^sub>\ show ?thesis + by simp + qed + moreover have "s\<^sup>+\<^bsub>X\<^esub>(\) = 20" + proof - + from a\<^sub>\ and a\<^sub>X have "X \ fmdom' \" + by simp + with a\<^sub>\ and a\<^sub>X show ?thesis + by simp + qed + moreover have "s\<^sup>+\<^bsub>U\<^bsub>1\<^esub>\<^esub>(\) = 10" + proof - + from a\<^sub>\ have "{U\<^bsub>1\<^esub>} \ fmdom' \" + by simp + with a\<^sub>\ show ?thesis + by simp + qed + ultimately have "\\<^sup>+\<^bsub>U\<^bsub>1\<^esub>\<^esub>(\) = 10/25" and "\\<^sup>+\<^bsub>X\<^esub>(\) = 20/25" + using a\<^sub>\ by simp_all + +end + +end + +subsubsection \ Transactions \ + +context +begin + +inductive + tx_sts :: " + stake_distr \ + 'sig transaction \ + stake_distr \ + bool" + (\_ \{_} _\ [51, 0, 51] 50) +where + tx_sts_base: + "\ \{tx} \'" + if "((U\<^sub>i, U\<^sub>j, s), _) = tx" + and "{U\<^sub>i, U\<^sub>j} \ fmdom' \" + and "\ $$! U\<^sub>i \ s" + \ \\\\''\ + and "fmdom' \'' = fmdom' \" + and "\'' $$! U\<^sub>i = \ $$! U\<^sub>i - s" + and "\U \ fmdom' \''. U \ U\<^sub>i \ \'' $$! U = \ $$! U" + \ \\\\'\ + and "fmdom' \' = fmdom' \" + and "\' $$! U\<^sub>j = \'' $$! U\<^sub>j + s" + and "\U \ fmdom' \'. U \ U\<^sub>j \ \' $$! U = \'' $$! U" + +lemma apply_transaction_soundness: + assumes "apply_transaction tx \ = \'" + and "((U\<^sub>i, U\<^sub>j, s), \) = tx" + and "{U\<^sub>i, U\<^sub>j} \ fmdom' \" + and "\ $$! U\<^sub>i \ s" + shows "\ \{tx} \'" +proof - + let ?\'' = "\(U\<^sub>i $$:= \ $$! U\<^sub>i - s)" + from assms(3) have "fmdom' ?\'' = fmdom' \" + by auto + moreover have "?\'' $$! U\<^sub>i = \ $$! U\<^sub>i - s" + by simp + moreover have "?\'' $$! U = \ $$! U" if "U \ fmdom' ?\''" and "U \ U\<^sub>i" for U + using \U \ U\<^sub>i\ by auto + moreover from assms have "fmdom' \' = fmdom' \" + by auto + moreover from assms have "\' $$! U\<^sub>j = ?\'' $$! U\<^sub>j + s" + by auto + moreover from assms have "\' $$! U = ?\'' $$! U" if "U \ fmdom' \'" and "U \ U\<^sub>j" for U + using \U \ U\<^sub>j\ by auto + ultimately show ?thesis + using assms(2-4) and tx_sts.simps[of \ tx \'] by metis +qed + +lemma apply_transaction_completeness: + assumes "\ \{tx} \'" + shows "apply_transaction tx \ = \'" +proof - + from assms show ?thesis + proof cases + case (tx_sts_base U\<^sub>i U\<^sub>j s _ \'') + then show ?thesis + proof (intro fsubset_antisym) + show "apply_transaction tx \ \\<^sub>f \'" + unfolding fmsubset.rep_eq proof (unfold map_le_def, intro ballI) + fix U + assume *: "U \ dom (($$) (apply_transaction tx \))" + then show "apply_transaction tx \ $$ U = \' $$ U" + proof (cases "U \ dom (($$) \)") + case True + from tx_sts_base(1,2,3) have "apply_transaction tx \ $$ U = + (let \\<^sub>1 = \(U\<^sub>i $$:= \ $$! U\<^sub>i - s) in \\<^sub>1(U\<^sub>j $$:= \\<^sub>1 $$! U\<^sub>j + s)) $$ U" + by auto + also have "\ = Some (\' $$! U)" + proof - + consider (a) "U = U\<^sub>i" | (b) "U = U\<^sub>j" | (c) "U \ U\<^sub>i" and "U \ U\<^sub>j" + by auto + then show ?thesis + using True and tx_sts_base(4-9) by cases (auto simp add: fmlookup_dom'_iff) + qed + also have "\ = \' $$ U" + proof - + from True and tx_sts_base(7) have "U \ fmdom' \'" + by simp + then show ?thesis + by (simp add: fmlookup_dom'_iff) + qed + finally show "apply_transaction tx \ $$ U = \' $$ U" . + next + case False + with * and tx_sts_base(1,2,3) show ?thesis + by auto + qed + qed + then show "\' \\<^sub>f apply_transaction tx \" + unfolding fmsubset.rep_eq proof (unfold map_le_def, intro ballI) + fix U + assume *: "U \ dom (($$) \')" + then show "\' $$ U = apply_transaction tx \ $$ U" + proof - + from tx_sts_base(1,2,3) have "dom (($$) (apply_transaction tx \)) = + insert U\<^sub>j (fmdom' (\(U\<^sub>i $$:= \ $$! U\<^sub>i - s)))" + by auto + with * and tx_sts_base(7) have "U \ dom (($$) (apply_transaction tx \))" + by simp + with \apply_transaction tx \ \\<^sub>f \'\ show ?thesis + by (simp add: fmsubset.rep_eq map_le_def) + qed + qed + qed + qed +qed + +text \ + Applying a transaction with the same stakeholder as sender and recipient does not change the + stake distribution: +\ + +lemma self_transfer_invariancy: + assumes "U\<^sub>i \ fmdom' \" + and "\ $$! U\<^sub>i \ s" + shows "apply_transaction ((U\<^sub>i, U\<^sub>i, s), \) \ = \" + using assms +proof (intro fsubset_antisym) + let ?\' = "apply_transaction ((U\<^sub>i, U\<^sub>i, s), \) \" + show "?\' \\<^sub>f \" + unfolding fmsubset.rep_eq proof (unfold map_le_def, intro ballI) + fix U + assume "U \ dom (($$) ?\')" + then show "?\' $$ U = \ $$ U" + proof (cases "U = U\<^sub>i") + case True + with assms have "?\' $$ U = Some (\ $$! U - s + s)" + by simp + also from True and assms have "\ = \ $$ U" + by (simp add: fmlookup_dom'_iff) + finally show ?thesis . + next + case False + with assms show ?thesis + by simp + qed + qed + with assms show "\ \\<^sub>f apply_transaction ((U\<^sub>i, U\<^sub>i, s), \) \" + unfolding fmsubset.rep_eq and map_le_def by simp +qed + +end + +subsubsection \ Blocks \ + +context +begin + +inductive + txs_sts :: " + stake_distr \ + 'sig transaction list \ + stake_distr \ + bool" + (\_ \\<^sup>*{_} _\ [51, 0, 51] 50) +where + txs_sts_base: + "\ \\<^sup>*{[]} \" +| txs_sts_ind: + "\ \\<^sup>*{txs @ [tx]} \'" + if "\ \\<^sup>*{txs} \''" + and "\'' \{tx} \'" + +abbreviation + bl_sts :: " + stake_distr \ + ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) block \ + stake_distr \ + bool" + (\_ \\<^sub>b{_} _\ [51, 0, 51] 50) +where + "\ \\<^sub>b{B} \' \ \ \\<^sup>*{bl_txs B} \'" + +definition + are_applicable_txs :: "'sig transaction list \ stake_distr \ bool" +where + [iff]: "are_applicable_txs txs \ \ (\\'' U\<^sub>i U\<^sub>j s. \i \ {0..i, U\<^sub>j, s) = fst (txs ! i) \ \ \\<^sup>*{take i txs} \'' \ \'' $$! U\<^sub>i \ s)" + +lemma txs_init_is_applicable: + assumes "are_applicable_txs txs \" + shows "are_applicable_txs (butlast txs) \" + using assms +proof (unfold are_applicable_txs_def, intro allI ballI impI, elim conjE) + fix \'' U\<^sub>i U\<^sub>j s i + let ?txs' = "butlast txs" + assume a\<^sub>1: "i \ {0..2: "(U\<^sub>i, U\<^sub>j, s) = fst (?txs' ! i)" + and a\<^sub>3: "\ \\<^sup>*{take i ?txs'} \''" + from a\<^sub>1 have *: "i \ {0..1 and a\<^sub>2 have "(U\<^sub>i, U\<^sub>j, s) = fst (txs ! i)" + by (simp add: nth_butlast) + moreover from * and a\<^sub>3 have "\ \\<^sup>*{take i txs} \''" + by (simp add: take_butlast) + ultimately show "\'' $$! U\<^sub>i \ s" + using assms by blast +qed + +abbreviation + are_known_stakeholders :: "'sig transaction list \ stake_distr \ bool" +where + "are_known_stakeholders txs \ \ \((U\<^sub>i, U\<^sub>j, _), _) \ set txs. {U\<^sub>i, U\<^sub>j} \ fmdom' \" + +lemma fold_apply_transaction_fmdom': + assumes "are_known_stakeholders txs \" + shows "fmdom' (fold apply_transaction txs \) = fmdom' \" + using assms +proof (induction txs arbitrary: \) + case Nil + then show ?case + by simp +next + case (Cons tx txs) + let ?\' = "apply_transaction tx \" + obtain U\<^sub>i U\<^sub>j s \ where *: "tx = ((U\<^sub>i, U\<^sub>j, s), \)" + by (metis prod.collapse) + have "fmdom' (fold apply_transaction (tx # txs) \) = fmdom' (fold apply_transaction txs ?\')" + by simp + also from Cons.prems and Cons.IH and * have "\ = fmdom' \" + by (simp add: insert_absorb) + finally show ?case . +qed + +lemma fold_apply_transaction_soundness: + assumes "fold apply_transaction txs \ = \'" + and "are_applicable_txs txs \" + and "are_known_stakeholders txs \" + shows "\ \\<^sup>*{txs} \'" + using assms +proof (induction txs arbitrary: \' rule: rev_induct) + case Nil + then show ?case + by (simp add: txs_sts_base) +next + case (snoc tx txs) + let ?\'' = "fold apply_transaction txs \" + have f\<^sub>1: "\ \\<^sup>*{txs} ?\''" + proof - + from snoc.prems(2) have "are_applicable_txs txs \" + using txs_init_is_applicable[of "txs @ [tx]" \] by fastforce + moreover from snoc.prems(3) have "are_known_stakeholders txs \" + by simp + ultimately show ?thesis + using snoc.IH by simp + qed + moreover have "?\'' \{tx} \'" + proof - + obtain U\<^sub>i U\<^sub>j s \ where f\<^sub>2: "tx = ((U\<^sub>i, U\<^sub>j, s), \)" + by (metis prod.collapse) + moreover from snoc.prems(1) have "apply_transaction tx ?\'' = \'" + by simp + moreover have "{U\<^sub>i, U\<^sub>j} \ fmdom' ?\''" + proof - + from f\<^sub>2 and snoc.prems(3) have "{U\<^sub>i, U\<^sub>j} \ fmdom' \" + by simp + with snoc.prems(3) show ?thesis + by (simp add: fold_apply_transaction_fmdom') + qed + moreover have "?\'' $$! U\<^sub>i \ s" + proof - + let ?txs = "txs @ [tx]" + let ?i = "length ?txs - 1" + have "?i \ {0..2 have "(U\<^sub>i, U\<^sub>j, s) = fst (?txs ! ?i)" + by simp + moreover from f\<^sub>1 have "\ \\<^sup>*{take ?i ?txs} ?\''" + by simp + ultimately show ?thesis + using snoc.prems(2) by blast + qed + ultimately show ?thesis + by (simp add: apply_transaction_soundness) + qed + ultimately show ?case + by (blast intro: txs_sts_ind) +qed + +corollary apply_block_soundness: + assumes "apply_block B \ = \'" + and "txs = bl_txs B" + and "are_applicable_txs txs \" + and "are_known_stakeholders txs \" + shows "\ \\<^sub>b{B} \'" + using assms and fold_apply_transaction_soundness by simp + +lemma fold_apply_transaction_completeness: + assumes "\ \\<^sup>*{txs} \'" + shows "fold apply_transaction txs \ = \'" + using assms + by induction (simp_all add: apply_transaction_completeness) + +corollary apply_block_completeness: + assumes "\ \\<^sub>b{B} \'" + shows "apply_block B \ = \'" + using assms and fold_apply_transaction_completeness unfolding apply_block_def by blast + +text \ + Applying a block including only a transaction and its corresponding refund transaction does not + affect the stake distribution: +\ + +lemma transaction_refund_invariancy: + assumes "bl_txs B = [((U\<^sub>i, U\<^sub>j, s), \\<^sub>1), ((U\<^sub>j, U\<^sub>i, s), \\<^sub>2)]" + and "{U\<^sub>i, U\<^sub>j} \ fmdom' \" + and "\ $$! U\<^sub>i \ s" + shows "apply_block B \ = \" +proof - + let ?\\<^sub>1 = "\(U\<^sub>i $$:= \ $$! U\<^sub>i - s)" + let ?\\<^sub>2 = "?\\<^sub>1(U\<^sub>j $$:= ?\\<^sub>1 $$! U\<^sub>j + s)" + let ?\\<^sub>3 = "?\\<^sub>2(U\<^sub>j $$:= ?\\<^sub>2 $$! U\<^sub>j - s)" + let ?\\<^sub>4 = "?\\<^sub>3(U\<^sub>i $$:= ?\\<^sub>3 $$! U\<^sub>i + s)" + from assms(1) have "apply_block B \ = + fold apply_transaction [((U\<^sub>j, U\<^sub>i, s), \\<^sub>2)] (apply_transaction ((U\<^sub>i, U\<^sub>j, s), \\<^sub>1) \)" + by simp + also have "\ = fold apply_transaction [((U\<^sub>j, U\<^sub>i, s), \\<^sub>2)] ?\\<^sub>2" + by simp + also have "\ = ?\\<^sub>4" + by simp + also have "\ = \" + proof (rule fsubset_antisym) + show "?\\<^sub>4 \\<^sub>f \" + unfolding fmsubset.rep_eq proof (unfold map_le_def, intro ballI) + fix U + assume "U \ dom (($$) ?\\<^sub>4)" + consider (a) "U = U\<^sub>i" | (b) "U = U\<^sub>j" | (c) "U \ U\<^sub>i" and "U \ U\<^sub>j" + by auto + then show "?\\<^sub>4 $$ U = \ $$ U" + proof cases + case a + then have "?\\<^sub>4 $$ U = Some (\ $$! U - s + s)" + by simp + also from a and assms(2,3) have "\ = \ $$ U" + by (simp add: fmlookup_dom'_iff) + finally show ?thesis . + next + case b + with assms(3) have "?\\<^sub>4 $$ U = Some (\ $$! U + s - s)" + by auto + also from b and assms(2) have "\ = \ $$ U" + by (simp add: fmlookup_dom'_iff) + finally show ?thesis . + next + case c + then show ?thesis + by simp + qed + qed + show "\ \\<^sub>f ?\\<^sub>4" + using \?\\<^sub>4 \\<^sub>f \\ unfolding fmsubset.rep_eq and map_le_def by auto + qed + finally show ?thesis . +qed + +end + +subsubsection \ Chains \ + +inductive + chain_sts :: " + stake_distr \ + ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain \ + stake_distr \ + bool" + (\_ \\<^sub>c{_} _\ [51, 0, 51] 50) +where + chain_sts_base: + "\ \\<^sub>c{[]} \" +| chain_sts_ind: + "\ \\<^sub>c{\ @ [B]} \'" + if "\ \\<^sub>c{\} \''" + and "\'' \\<^sub>b{B} \'" + +abbreviation chain_txs :: "('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain \ ('sig transaction) list" where + "chain_txs \ List.concat \ map bl_txs" + +lemma apply_chain_txs_is_apply_chain: + shows "fold apply_transaction (chain_txs \) \ = apply_chain \ \" + by (induction \ arbitrary: \) (unfold apply_block_def apply_chain_def, simp_all) + +lemma fold_apply_block_fmdom': + assumes "\B \ set \. are_known_stakeholders (bl_txs B) \" + shows "fmdom' (fold apply_block \ \) = fmdom' \" + using assms +proof (induction \ arbitrary: \) + case Nil + then show ?case + by simp +next + case (Cons B \) + let ?\' = "apply_block B \" + have "fmdom' (fold apply_block (B # \) \) = fmdom' (fold apply_block \ ?\')" + by simp + also from Cons.prems and Cons.IH have "\ = fmdom' \" + unfolding apply_block_def by (simp add: fold_apply_transaction_fmdom') + finally show ?case . +qed + +lemma tx_append_applicability: + assumes "are_applicable_txs [tx] (fold apply_transaction txs \)" + and "are_applicable_txs txs \" + shows "are_applicable_txs (txs @ [tx]) \" + using assms +proof (unfold are_applicable_txs_def, intro allI ballI impI, elim conjE) + fix \'' U\<^sub>i U\<^sub>j s i + assume a\<^sub>1: "i \ {0..2: "(U\<^sub>i, U\<^sub>j, s) = fst ((txs @ [tx]) ! i)" + and a\<^sub>3: "\ \\<^sup>*{take i (txs @ [tx])} \''" + then show "s \ \'' $$! U\<^sub>i" + proof (cases "i < length txs") + case True + from True have "i \ {0..2 have "(U\<^sub>i, U\<^sub>j, s) = fst (txs ! i)" + by (simp add: nth_append) + moreover from True and a\<^sub>3 have "\ \\<^sup>*{take i txs} \''" + by simp + ultimately show ?thesis + using assms(2) by blast + next + case False + from False and a\<^sub>1 and a\<^sub>2 have "(U\<^sub>i, U\<^sub>j, s) = fst tx" + by (simp add: less_Suc_eq) + moreover from False and a\<^sub>1 and a\<^sub>3 have "\ \\<^sup>*{txs} \''" + by simp + then have "fold apply_transaction txs \ = \''" + by (rule fold_apply_transaction_completeness) + then have "fold apply_transaction txs \ \\<^sup>*{[]} \''" + using fold_apply_transaction_soundness and txs_sts_base by simp + ultimately show ?thesis + using assms(1) and a\<^sub>1 by auto + qed +qed + +lemma last_tx_applicability: + assumes "are_applicable_txs (txs @ [tx]) \" + and "are_known_stakeholders txs \" + shows "are_applicable_txs [tx] (fold apply_transaction txs \)" + using assms +proof (unfold are_applicable_txs_def, intro allI ballI impI, elim conjE) + fix \'' U\<^sub>i U\<^sub>j s i + assume a\<^sub>1: "i \ {0..2: "(U\<^sub>i, U\<^sub>j, s) = fst ([tx] ! i)" + and a\<^sub>3: "fold apply_transaction txs \ \\<^sup>*{take i [tx]} \''" + from a\<^sub>1 have f\<^sub>1: "i = 0" + by simp + moreover from a\<^sub>2 and f\<^sub>1 have f\<^sub>2: "(U\<^sub>i, U\<^sub>j, s) = fst tx" + by simp + moreover from a\<^sub>3 and f\<^sub>1 have "fold apply_transaction txs \ \\<^sup>*{[]} \''" + using fold_apply_transaction_completeness and txs_sts_base by fastforce + then have f\<^sub>3: "fold apply_transaction txs \ = \''" + using fold_apply_transaction_completeness by force + ultimately have "\ \\<^sup>*{txs} \''" + proof - + from assms(1) have "are_applicable_txs txs \" + using txs_init_is_applicable by fastforce + moreover from assms(2) have "are_known_stakeholders txs \" + by blast + ultimately show ?thesis + using f\<^sub>3 and fold_apply_transaction_soundness by simp + qed + with assms(1) and f\<^sub>2 show "s \ \'' $$! U\<^sub>i" + by force +qed + +lemma txs_prefix_applicability: + assumes "are_applicable_txs txs \" + and "n \ {0..length txs}" + shows "are_applicable_txs (take n txs) \" + using assms +proof (unfold are_applicable_txs_def, intro allI ballI impI, elim conjE) + fix \'' U\<^sub>i U\<^sub>j s i + assume a\<^sub>1: "i \ {0..2: "(U\<^sub>i, U\<^sub>j, s) = fst ((take n txs) ! i)" + and a\<^sub>3: "\ \\<^sup>*{take i (take n txs)} \''" + then show "s \ \'' $$! U\<^sub>i" + proof (cases "i < n") + case True + then show ?thesis + proof - + from True and a\<^sub>2 have "(U\<^sub>i, U\<^sub>j, s) = fst (txs ! i)" + by simp + moreover from a\<^sub>1 have "i < length txs" + by simp + moreover from True and a\<^sub>3 have "\ \\<^sup>*{take i txs} \''" + by (simp add: min.strict_order_iff) + ultimately show ?thesis + using assms(1) by fastforce + qed + next + case False + with a\<^sub>1 show ?thesis + by simp + qed +qed + +lemma singleton_last_block_applicability: + assumes "bl_txs B = [tx]" + and "are_applicable_txs (chain_txs (\ @ [B])) \" + and "are_known_stakeholders (chain_txs \) \" + shows "are_applicable_txs [tx] (fold apply_block \ \)" +proof - + from assms(1,2) have "are_applicable_txs (chain_txs \ @ [tx]) \" + by simp + with assms(2,3) have "are_applicable_txs [tx] (fold apply_transaction (chain_txs \) \)" + using last_tx_applicability by metis + then show ?thesis + using apply_chain_txs_is_apply_chain unfolding apply_chain_def by metis +qed + +lemma last_tx_in_last_block_applicability: + fixes txs :: "'sig transaction list" + and B :: "('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) block" + assumes "bl_txs B = txs @ [tx]" + and "are_applicable_txs (chain_txs (\ @ [B])) \" + and "are_known_stakeholders (chain_txs (\ @ [B])) \" + shows "are_applicable_txs [tx] (fold apply_transaction txs (fold apply_block \ \))" + using assms +proof (induction txs arbitrary: B \) + case Nil + from Nil.prems(1) have "bl_txs B = [tx]" + by simp + moreover from Nil.prems(3) have "are_known_stakeholders (chain_txs \) \" + by simp + ultimately have "are_applicable_txs [tx] (fold apply_block \ \)" + using Nil.prems(2) and singleton_last_block_applicability by metis + then show ?case + by (metis fold_simps(1)) +next + case (Cons tx' txs') + let ?\' = "fold apply_block \ \" + obtain B' :: "('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) block" where f1: "bl_txs B' = txs' @ [tx]" + by force + obtain B'' :: "('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) block" where f2: "bl_txs B'' = [tx']" + by force + from f2 have "fold apply_transaction (tx' # txs') ?\' = + fold apply_transaction txs' (apply_block B'' ?\')" + by simp + also have "\ = fold apply_transaction txs' (fold apply_block (\ @ [B'']) \)" + by simp + finally have "are_applicable_txs [tx] (fold apply_transaction (tx' # txs') ?\') = + are_applicable_txs [tx] (fold apply_transaction txs' (fold apply_block (\ @ [B'']) \))" + by simp + moreover from Cons.prems(1,2) and f1 and f2 + have "are_applicable_txs (chain_txs ((\ @ [B'']) @ [B'])) \" + by simp + moreover from Cons.prems(1,3) and f1 and f2 + have "are_known_stakeholders (chain_txs (((\ @ [B'']) @ [B']))) \" + by simp + ultimately show ?case + using f1 and Cons.IH by presburger +qed + +lemma last_block_applicability: + fixes txs :: "'sig transaction list" + and B :: "('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) block" + assumes "bl_txs B = txs" + and "are_applicable_txs (chain_txs (\ @ [B])) \" + and "are_known_stakeholders (chain_txs (\ @ [B])) \" + shows "are_applicable_txs txs (fold apply_block \ \)" + using assms +proof (induction txs arbitrary: B rule: rev_induct) + case Nil + then show ?case + unfolding are_applicable_txs_def by simp +next + case (snoc tx txs) + obtain B' :: "('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) block" where f1: "txs = bl_txs B'" + by force + have "are_applicable_txs [tx] (fold apply_transaction txs (fold apply_block \ \))" + proof - + from snoc.prems(3) have "are_known_stakeholders (chain_txs (\ @ [B])) \" + by simp + with snoc.prems(1,2) show ?thesis + using last_tx_in_last_block_applicability by metis + qed + moreover have "are_applicable_txs txs (fold apply_block \ \)" + proof - + from snoc.prems(1,2) and f1 have "are_applicable_txs (chain_txs (\ @ [B'])) \" + using txs_init_is_applicable[of "chain_txs \ @ txs @ [tx]" \] + by (simp add: butlast_append) + moreover from snoc.prems(1,3) and f1 have "are_known_stakeholders (chain_txs (\ @ [B'])) \" + by simp + ultimately show ?thesis + using snoc.IH and f1 by blast + qed + ultimately show ?case + using tx_append_applicability by metis +qed + +theorem apply_chain_soundness: + assumes "apply_chain \ \ = \'" + and "are_applicable_txs (List.concat (map bl_txs \)) \" + and "are_known_stakeholders (List.concat (map bl_txs \)) \" + shows "\ \\<^sub>c{\} \'" + using assms +proof (induction \ arbitrary: \' rule: rev_induct) + case Nil + then show ?case + using chain_sts_base by simp +next + case (snoc B \) + let ?\'' = "apply_chain \ \" + have "\ \\<^sub>c{\} ?\''" + proof - + have "are_applicable_txs (chain_txs \) \" + proof - + from snoc.prems(2) have "are_applicable_txs (chain_txs \ @ bl_txs B) \" + by simp + moreover have "length (chain_txs \) \ {0..length (chain_txs \ @ bl_txs B)}" + by simp + ultimately have "are_applicable_txs (take (length (chain_txs \)) (chain_txs \ @ bl_txs B)) \" + using txs_prefix_applicability by metis + then show ?thesis + by simp + qed + moreover from snoc.prems(3) have "are_known_stakeholders (chain_txs \) \" + by simp + ultimately show ?thesis + using snoc.IH by simp + qed + moreover have "?\'' \\<^sub>b{B} \'" + proof - + from snoc(2) have "apply_block B ?\'' = \'" + by simp + moreover from snoc.prems(2,3) have "are_applicable_txs (bl_txs B) ?\''" + unfolding apply_chain_def using last_block_applicability by (metis comp_apply) + moreover have "are_known_stakeholders (bl_txs B) ?\''" + proof - + from snoc.prems(3) have "are_known_stakeholders (chain_txs \) \" + by simp + then have "fmdom' (fold apply_transaction (chain_txs \) \) = fmdom' \" + using fold_apply_transaction_fmdom' by blast + then have "fmdom' (apply_chain \ \) = fmdom' \" + using apply_chain_txs_is_apply_chain by metis + with snoc.prems(3) show ?thesis + by simp + qed + ultimately show ?thesis + by (simp add: apply_block_soundness) + qed + ultimately show ?case + using chain_sts_ind by blast +qed + +corollary apply_chain_completeness: + assumes "\ \\<^sub>c{\} \'" + shows "apply_chain \ \ = \'" + using assms unfolding apply_chain_def +proof induction + case chain_sts_base + then show ?case + by simp +next + case (chain_sts_ind \ _ \'' B \') + from \\'' \\<^sub>b{B} \'\ have "apply_block B \'' = \'" + by (rule apply_block_completeness) + with chain_sts_ind.IH show ?case + by simp +qed + +text \ + For the sake of simplicity, we regard a chain as @{emph \valid\} whenever it contains a + strictly increasing sequence of slots: +\ + +abbreviation + is_slot_increasing :: "('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain \ bool" +where + "is_slot_increasing \ \ sorted_wrt (\B B'. bl_slot B < bl_slot B') \" + +abbreviation + is_valid_chain :: "('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain \ bool" +where + "is_valid_chain \ \ is_slot_increasing \" + +text \ + A prefix of a valid chain is a valid chain: +\ + +lemma chain_prefix_validity: + assumes "is_valid_chain \\<^sub>2" + and "\\<^sub>1 \ \\<^sub>2" + shows "is_valid_chain \\<^sub>1" + using assms and sorted_wrt_append unfolding prefix_def by blast + +text \ + A prefix of a chain keeps all properties on its elements that hold for the original chain: +\ + +lemma prefix_invariancy: + assumes "\B \ set \\<^sub>2. P B" + and "\\<^sub>1 \ \\<^sub>2" + shows "\B \ set \\<^sub>1. P B" + using assms +proof (intro ballI) + fix B + assume "B \ set \\<^sub>1" + from assms(2) have "\\\<^sub>3. \\<^sub>2 = \\<^sub>1 @ \\<^sub>3" + by (blast dest: prefixE) + with \B \ set \\<^sub>1\ have "B \ set \\<^sub>2" + by auto + with assms(1) show "P B" + by simp +qed + +text \ + The \\\<^bsup>\m\<^esup>\ operator satisfies some simple laws: +\ + +lemma zero_blocks_chain_prunning_identity: + shows "\\<^sup>\\<^bsup>0\<^esup> = \" + by simp + +lemma long_chain_prunning_emptiness: + assumes "m \ length \" + shows "\\<^sup>\\<^bsup>m\<^esup> = []" + using assms by simp + +lemma append_prune_chain_drop_identity: + shows "\\<^sup>\\<^bsup>m\<^esup> @ drop (length \ - m) \ = \" + by simp + +text \ + Now we prove some properties about @{const prune_after}. As expected, chain validity is + preserved by @{const prune_after}: +\ + +lemma prune_after_validity_invariancy: + assumes "is_valid_chain \" + shows "is_valid_chain (prune_after sl \)" + using assms unfolding prune_after_def + by (metis (no_types, lifting) sorted_wrt_append takeWhile_dropWhile_id) + +text \ + And the pruned chain returned by @{const prune_after} is obviously a prefix of the original chain: +\ + +lemma prune_after_is_prefix: + shows "prune_after sl \ \ \" +proof - + let ?P = "\B. bl_slot B \ sl" + have "\ = takeWhile ?P \ @ dropWhile ?P \" + by simp + then have "\\'. \ = prune_after sl \ @ \'" + unfolding prune_after_def by blast + then show ?thesis + by (blast intro: prefixI) +qed + +text \ + Now, we define two auxiliary predicates: One predicate to check whether the slots in a chain are + bounded by a given slot, and another predicate to check whether a chain is both a prefix of a + given chain and bounded by a given slot: +\ + +abbreviation + is_slot_bounded_chain :: "('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain \ slot \ bool" (infix \\\ 50) +where + "\ \ sl \ \B \ set \. bl_slot B \ sl" + +abbreviation + is_slot_bounded_prefix :: " + ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain \ + slot \ + ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain \ + bool" +where + "is_slot_bounded_prefix \\<^sub>1 sl \\<^sub>2 \ \\<^sub>1 \ \\<^sub>2 \ \\<^sub>1 \ sl" + +text \ + Any chain \\\<^sub>1\ which is a subsequence of another chain \\\<^sub>2\ that is slot-bounded by \sl\ is also + slot-bounded by \sl\: +\ + +lemma subseq_is_slot_bounded: + assumes "subseq \\<^sub>1 \\<^sub>2" + and "\\<^sub>2 \ sl" + shows "\\<^sub>1 \ sl" + using assms + by (metis (mono_tags, lifting) list_emb_set) + +text \ + The tail of a chain that is slot-bounded by \sl\ is also slot-bounded by \sl\: +\ + +lemma tail_is_slot_bounded: + assumes "\ \ sl" + shows "tl \ \ sl" + using assms and subseq_is_slot_bounded by blast + +text \ + Armed with these predicates, we can prove more complex properties. For example, given a slot \sl\ + \prune_after sl \\ is bounded by any slot \sl'\ such that \sl \ sl'\: +\ + +lemma prune_after_is_slot_bounded: + assumes "sl \ sl'" + shows "prune_after sl \ \ sl'" + using assms by (induction \) (simp, fastforce) + +text \ + Any \sl\-bounded prefix \\'\ of a chain \\\ is a prefix of \\\ when pruned after \sl\: +\ + +lemma prune_after_includes_slot_bounded_prefix: + assumes "is_slot_bounded_prefix \' sl \" + shows "\' \ prune_after sl \" + using assms unfolding prefix_def by auto + +text \ + A chain \\\, when pruned after \sl\, is a \sl\-bounded prefix of \\\: +\ + +lemma prune_after_is_slot_bounded_prefix: + shows "is_slot_bounded_prefix (prune_after sl \) sl \" + using prune_after_is_prefix and prune_after_is_slot_bounded by fastforce + +text \ + A chain \\\, when pruned after \sl\, is the longest \sl\-bounded prefix of \\\ +\ + +lemma prune_after_is_longest_slot_bounded_prefix: + assumes "is_slot_bounded_prefix \\<^sub>l sl \" + and "\\'. is_slot_bounded_prefix \' sl \ \ \ length \\<^sub>l < length \'" + shows "prune_after sl \ = \\<^sub>l" +proof - + from assms(1) have "\\<^sub>l \ prune_after sl \" + by (rule prune_after_includes_slot_bounded_prefix) + moreover have "prune_after sl \ \ \\<^sub>l" + proof - + from assms(2) have "length (prune_after sl \) \ length \\<^sub>l" + using prune_after_is_slot_bounded_prefix and not_less by metis + with \\\<^sub>l \ prune_after sl \\ show ?thesis + by (blast intro: prefix_length_prefix) + qed + ultimately show ?thesis + by (simp add: prefix_order.antisym) +qed + +text \ + TODO: Complete. +\ + +lemma prune_after_longer_than_slot_bounded_prefix: + assumes "is_slot_bounded_prefix \' sl \" + shows "\ length \' > length (prune_after sl \)" +proof - + from assms have "\' \ prune_after sl \" + by (rule prune_after_includes_slot_bounded_prefix) + then have "length \' \ length (prune_after sl \)" + by (simp add: prefix_length_le) + then show ?thesis + by simp +qed + +text \ + We define the specification of @{const \prune_after\}: The longest prefix of a given chain that + is slot-bounded by a given slot: +\ + +definition + prune_after_spec :: " + slot \ + ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain \ + ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain" +where + [simp]: "prune_after_spec sl \ = (ARG_MAX length \'. is_slot_bounded_prefix \' sl \)" + +text \ + TODO: Complete. +\ + +lemma prune_after_spec_satisfaction: + shows "prune_after_spec sl \ = prune_after sl \" + unfolding prune_after_spec_def + using + prune_after_is_slot_bounded_prefix and + prune_after_longer_than_slot_bounded_prefix and + prune_after_is_longest_slot_bounded_prefix[symmetric] + by (rule arg_maxI) + +subsubsection \ Leader election \ + +context leader_election +begin + +notepad +begin + + fix oh\<^sub>1 oh\<^sub>2 oh\<^sub>3 oh\<^sub>4 oh\<^sub>5 oh\<^sub>6 :: "'hash option" + and t\\<^sub>1\<^sub>1 t\\<^sub>1\<^sub>2 t\\<^sub>2 t\\<^sub>3 t\\<^sub>4 t\\<^sub>5 t\\<^sub>6 B\\<^sub>1 B\\<^sub>2 B\\<^sub>3 B\\<^sub>4 B\\<^sub>5 B\\<^sub>6 :: 'sig + and B\<^sub>\\<^sub>1 B\<^sub>\\<^sub>2 B\<^sub>\\<^sub>3 B\<^sub>\\<^sub>4 B\<^sub>\\<^sub>5 B\<^sub>\\<^sub>6 :: "('vrf\<^sub>y, 'vrf\<^sub>\) block_proof" + and \\<^sub>1 \\<^sub>2 \\<^sub>3 \\<^sub>4 \\<^sub>5 \\<^sub>6 :: "('vrf\<^sub>y, 'vrf\<^sub>\) vrf\<^sub>o" + + let ?\\<^sub>0 = "{U\<^bsub>1\<^esub> $$:= 10, U\<^bsub>2\<^esub> $$:= 20}::stake_distr" + let ?tx\<^sub>1\<^sub>1 = "((U\<^bsub>1\<^esub>, U\<^bsub>2\<^esub>, 1), t\\<^sub>1\<^sub>1)::'sig transaction" + let ?tx\<^sub>1\<^sub>2 = "((U\<^bsub>1\<^esub>, U\<^bsub>2\<^esub>, 1), t\\<^sub>1\<^sub>2)::'sig transaction" + let ?tx\<^sub>2 = "((U\<^bsub>2\<^esub>, U\<^bsub>1\<^esub>, 1), t\\<^sub>2)::'sig transaction" + let ?tx\<^sub>3 = "((U\<^bsub>2\<^esub>, U\<^bsub>1\<^esub>, 5), t\\<^sub>3)::'sig transaction" + let ?tx\<^sub>4 = "((U\<^bsub>1\<^esub>, U\<^bsub>2\<^esub>, 2), t\\<^sub>4)::'sig transaction" + let ?tx\<^sub>5 = "((U\<^bsub>1\<^esub>, U\<^bsub>2\<^esub>, 1), t\\<^sub>5)::'sig transaction" + let ?tx\<^sub>6 = "((U\<^bsub>2\<^esub>, U\<^bsub>1\<^esub>, 2), t\\<^sub>6)::'sig transaction" + let ?B\<^sub>1 = "((1, oh\<^sub>1, [?tx\<^sub>1\<^sub>1, ?tx\<^sub>1\<^sub>2], B\<^sub>\\<^sub>1, \\<^sub>1), B\\<^sub>1)::('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) block" + let ?B\<^sub>2 = "((3, oh\<^sub>2, [?tx\<^sub>2], B\<^sub>\\<^sub>2, \\<^sub>2), B\\<^sub>2)::('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) block" + let ?B\<^sub>3 = "((4, oh\<^sub>3, [?tx\<^sub>3], B\<^sub>\\<^sub>3, \\<^sub>3), B\\<^sub>3)::('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) block" + let ?B\<^sub>4 = "((6, oh\<^sub>4, [?tx\<^sub>4], B\<^sub>\\<^sub>4, \\<^sub>4), B\\<^sub>4)::('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) block" + let ?B\<^sub>5 = "((7, oh\<^sub>5, [?tx\<^sub>5], B\<^sub>\\<^sub>5, \\<^sub>5), B\\<^sub>5)::('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) block" + let ?B\<^sub>6 = "((8, oh\<^sub>6, [?tx\<^sub>6], B\<^sub>\\<^sub>6, \\<^sub>6), B\\<^sub>6)::('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) block" + let ?\ = "[?B\<^sub>1, ?B\<^sub>2, ?B\<^sub>3, ?B\<^sub>4, ?B\<^sub>5, ?B\<^sub>6]::('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain" + + have "\\<^bsub>1\<^esub>(?\\<^sub>0, ?\) = ?\\<^sub>0" + by simp + + have "\\<^bsub>2\<^esub>(?\\<^sub>0, ?\) = ?\\<^sub>0" + proof - + have "prune_after 0 ?\ = []" + by simp + then have "apply_chain [] ?\\<^sub>0 = ?\\<^sub>0" + by simp + with \prune_after 0 ?\ = []\ show ?thesis + by simp + qed + + let ?\\<^sub>3 = "{U\<^bsub>1\<^esub> $$:= 8, U\<^bsub>2\<^esub> $$:= 22}::stake_distr" + + assume "R = 2" + have "\\<^bsub>3\<^esub>(?\\<^sub>0, ?\) = ?\\<^sub>3" + proof - + have "\\<^bsub>Suc (Suc 1)\<^esub>(?\\<^sub>0, ?\) = apply_chain (prune_after (Suc 1) ?\) ?\\<^sub>0" + proof - + from \R = 2\ have "Suc 1 = R" + by simp + then show ?thesis + by simp + qed + moreover have "prune_after (Suc 1) ?\ = [?B\<^sub>1]" + by simp + moreover have "apply_chain [?B\<^sub>1] ?\\<^sub>0 = ?\\<^sub>3" + proof - + let ?\ = "{U\<^bsub>1\<^esub> $$:= 9, U\<^bsub>2\<^esub> $$:= 21}::stake_distr" + have "apply_transaction ?tx\<^sub>1\<^sub>1 ?\\<^sub>0 = ?\" + proof - + let ?\' = "?\\<^sub>0(U\<^bsub>1\<^esub> $$:= (?\\<^sub>0 $$! U\<^bsub>1\<^esub>) - 1)" + have "?\' = ({U\<^bsub>1\<^esub> $$:= 9, U\<^bsub>2\<^esub> $$:= 20}::stake_distr)" + by eval + have "?\'(U\<^bsub>2\<^esub> $$:= ?\' $$! U\<^bsub>2\<^esub> + 1) = ?\" + by eval + then show ?thesis + by simp + qed + moreover have "apply_transaction ?tx\<^sub>1\<^sub>2 ?\ = ?\\<^sub>3" + proof - + let ?\' = "?\(U\<^bsub>1\<^esub> $$:= (?\ $$! U\<^bsub>1\<^esub>) - 1)" + have "?\' = ({U\<^bsub>1\<^esub> $$:= 8, U\<^bsub>2\<^esub> $$:= 21}::stake_distr)" + by eval + have "?\'(U\<^bsub>2\<^esub> $$:= ?\' $$! U\<^bsub>2\<^esub> + 1) = ?\\<^sub>3" + by eval + then show ?thesis + by simp + qed + ultimately have "apply_block ?B\<^sub>1 ?\\<^sub>0 = ?\\<^sub>3" + by simp + then show ?thesis + by simp + qed + ultimately show ?thesis + by simp + qed + + assume "f = 1/2" + have "\(1/3) = 1 - (1/2)\<^bsup>(1/3)\<^esup>" + proof - + from \f = 1/2\ have "1 - f = f" + by simp + with \f = 1/2\ show ?thesis + unfolding slot_leader_probability_def by presburger + qed + +end + +lemma independent_aggregation_aux: + assumes "finite A" + and "\ \ A" + shows "\(\) * \(\A) = \(\) - (1 - f)\<^bsup>\A\<^esup> + (1 - f)\<^bsup>\({\} \ A)\<^esup>" +proof - + have "\(\) * \(\A) = \(\) * (1 - (1 - f)\<^bsup>\A\<^esup>)" + unfolding slot_leader_probability_def .. + also have "\ = \(\) - \(\) * (1 - f)\<^bsup>\A\<^esup>" + by (simp add: right_diff_distrib') + also have "\ = \(\) - (1 - (1 - f)\<^bsup>\\<^esup>) * (1 - f)\<^bsup>\A\<^esup>" + unfolding slot_leader_probability_def .. + also have "\ = \(\) - ((1 - f)\<^bsup>\A\<^esup> - (1 - f)\<^bsup>\\<^esup> * (1 - f)\<^bsup>\A\<^esup>)" + by (simp add: left_diff_distrib) + also have "\ = \(\) - ((1 - f)\<^bsup>\A\<^esup> - (1 - f)\<^bsup>(\ + \A)\<^esup>)" + by (simp add: powr_add) + also from assms have "\ = \(\) - (1 - f)\<^bsup>\A\<^esup> + (1 - f)\<^bsup>\({\} \ A)\<^esup>" + by simp + finally show ?thesis . +qed + +theorem independent_aggregation: + assumes "finite A" + and "A \ {}" + shows "1 - \(\\ \ A. \) = (\\ \ A. (1 - \(\)))" + using assms +proof induction + case empty + then show ?case + by simp +next + case (insert \' A') + from insert.hyps show ?case + proof cases + case emptyI + then show ?thesis + by simp + next + case insertI + let ?A = "A' \ {\'}" + from insert.hyps(1,2) have "(\\ \ ?A. (1 - \(\))) = (1 - \(\')) * (\\ \ A'. (1 - \(\)))" + by simp + also from insert.IH and insertI(1) have "\ = (1 - \(\')) * (1 - \(\A'))" + by simp + also have "\ = 1 - \(\A') - \(\') + \(\') * \(\A')" + by argo + also from insert.hyps(1,2) + have "\ = 1 - \(\A') - \(\') + \(\') - (1 - f)\<^bsup>\A'\<^esup> + (1 - f)\<^bsup>\?A\<^esup>" + using independent_aggregation_aux by simp + \ \for clarity:\ + also have "\ = 1 - 1 + (1 - f)\<^bsup>\A'\<^esup> - \(\') + \(\') - (1 - f)\<^bsup>\A'\<^esup> + (1 - f)\<^bsup>\?A\<^esup>" + by simp + also have "\ = 1 - 1 + (1 - f)\<^bsup>\?A\<^esup>" \ \for clarity\ + by simp + finally show ?thesis + by simp + qed +qed + +end + +subsubsection \ Chain selection \ + +context chain_selection +begin + +lemma first_suffix_eq_chains: + shows "first_suffix \ \ = []" +proof - + have "longest_common_prefix (map \\<^sub>B \) (map \\<^sub>B \) = map \\<^sub>B \" + by (simp add: longest_common_prefix_max_prefix longest_common_prefix_prefix1 + prefix_order.eq_iff) + then show ?thesis + by simp +qed + +lemma longest_chains_shorter_element: + assumes "\ is_longest_chain \ \" + shows "longest_chains (\ # \) = longest_chains \" +proof - + from assms have "[\' \ \. is_longest_chain \' (\ # \)] = [\' \ \. is_longest_chain \' \]" + by (metis (mono_tags, hide_lams) dual_order.trans le_cases list.set_intros(2) set_ConsD) + with assms show ?thesis + unfolding longest_chains_def by auto +qed + +lemma longest_chains_empty: + shows "longest_chains [] = []" + unfolding longest_chains_def by simp + +lemma longest_chains_elem_is_longest: + assumes "is_longest_chain \ \" + shows "\ \ set (longest_chains (\ # \))" +proof - + have "\ \ set (\ # \)" + by simp + moreover from assms have "is_longest_chain \ (\ # \)" + by simp + ultimately show ?thesis + unfolding longest_chains_def by simp +qed + +lemma longest_chains_singleton: + shows "longest_chains [\] = [\]" + unfolding longest_chains_def by simp + +lemma trimmed_hashed_lcp_is_first_suffix: + assumes "\ disjoint_chains \ \'" + shows "drop (length (hashed_lcp \ \')) \ = first_suffix \ \'" + using assms +proof (induction \ \' rule: longest_common_prefix.induct) + case (1 B \ B' \') + from \\ disjoint_chains (B # \) (B' # \')\ have "\\<^sub>B B = \\<^sub>B B'" + by simp + have "hashed_lcp (B # \) (B' # \') = \\<^sub>B B # hashed_lcp \ \'" + proof - + from \\\<^sub>B B = \\<^sub>B B'\ + have "{map \\<^sub>B (B # \), map \\<^sub>B (B' # \')} = (#) (\\<^sub>B B) ` {map \\<^sub>B \, map \\<^sub>B \'}" + by simp + then show ?thesis + unfolding hashed_lcp_def by (metis Longest_common_prefix_image_Cons insert_not_empty) + qed + then + have "drop (length (hashed_lcp (B # \) (B' # \'))) (B # \) = drop (length (hashed_lcp \ \')) \" + by simp + also have "\ = first_suffix \ \'" + proof (cases "\ disjoint_chains \ \'") + case True + from \\\<^sub>B B = \\<^sub>B B'\ have "B = B'" + using collision_resistance by (meson inj_eq) + with True and "1.IH" show ?thesis + by simp + next + case False + then show ?thesis + proof (induction \ \' rule: longest_common_prefix.induct) + case (1 B \ B' \') + have "\\<^sub>B B # map \\<^sub>B \ \ {map \\<^sub>B (B # \), map \\<^sub>B (B' # \')}" + by simp + moreover have "\\<^sub>B B' # map \\<^sub>B \' \ {map \\<^sub>B (B # \), map \\<^sub>B (B' # \')}" + by simp + moreover from "1.prems" have "\\<^sub>B B \ \\<^sub>B B'" + by simp + ultimately have "Longest_common_prefix {map \\<^sub>B (B # \), map \\<^sub>B (B' # \')} = []" + by (metis Longest_common_prefix_eq_Nil) + with \\\<^sub>B B \ \\<^sub>B B'\ show ?case + by simp + next + case ("2_1" \') + then show ?case + by simp + next + case ("2_2" \) + then show ?case + by (simp add: Longest_common_prefix_Nil) + qed + qed + finally show ?case + using \\\<^sub>B B = \\<^sub>B B'\ by simp +next + case ("2_1" \') + then show ?case + by simp +next + case ("2_2" \) + then show ?case + by (simp add: Longest_common_prefix_Nil) +qed + +lemma first_chain_length_bound: + assumes "disjoint_chains \ \'" + and "length (first_suffix \ \') \ n" + shows "length \ \ n" +proof - + from \disjoint_chains \ \'\ have "first_suffix \ \' = \" + by (induction \ \' rule: longest_common_prefix.induct) simp_all + with \length (first_suffix \ \') \ n\ show ?thesis + by (simp del: first_suffix.simps) +qed + +lemma forks_at_most_impl [code]: + shows "forks_at_most n \ \' \ length (first_suffix \ \') \ n" +proof (intro iffI) + assume "forks_at_most n \ \'" + show "length (first_suffix \ \') \ n" + proof (cases "disjoint_chains \ \'") + case True + with \forks_at_most n \ \'\ show ?thesis + by simp + next + case False + with \forks_at_most n \ \'\ show ?thesis + using trimmed_hashed_lcp_is_first_suffix by force + qed +next + assume "length (first_suffix \ \') \ n" + show "forks_at_most n \ \'" + proof (cases "disjoint_chains \ \'") + case True + with \length (first_suffix \ \') \ n\ show ?thesis + using first_chain_length_bound unfolding forks_at_most_def by presburger + next + case False + with \length (first_suffix \ \') \ n\ show ?thesis + using trimmed_hashed_lcp_is_first_suffix by simp + qed +qed + +lemma forks_at_mostI [intro]: + shows "forks_at_most k \ \" + using first_suffix_eq_chains and forks_at_most_impl by simp + +lemma max_valid_no_candidates: + shows "max_valid \ [] = \" +proof - + have "longest_chains [\] = [\]" + by (rule longest_chains_singleton) + moreover have "forks_at_most k \ \" + by (intro forks_at_mostI) + ultimately show ?thesis + by auto +qed + +lemma max_valid_local_bias: + assumes "is_longest_chain \ \" + shows "max_valid \ \ = \" +proof - + from assms have "\ \ set (longest_chains (\ # [\' \ \. forks_at_most k \ \']))" + using longest_chains_elem_is_longest by auto + moreover have "forks_at_most k \ \" + by (intro forks_at_mostI) + ultimately have "\ \ set (longest_chains [\' \ \ # \. forks_at_most k \ \'])" + by auto + then show ?thesis + by (simp del: forks_at_most_def) +qed + +lemma max_valid_preserves_order: + assumes "\ is_longest_chain \ [\' \ \. forks_at_most k \ \']" + and "\\<^sub>m\<^sub>a\<^sub>x = longest_chains [\' \ \. forks_at_most k \ \']" + and "\\<^sub>m\<^sub>a\<^sub>x \ []" + shows "max_valid \ \ = hd \\<^sub>m\<^sub>a\<^sub>x" +proof - + from assms have "\\<^sub>m\<^sub>a\<^sub>x = longest_chains [\' \ \ # \. forks_at_most k \ \']" + using longest_chains_shorter_element by simp + moreover from assms have "\ \ set \\<^sub>m\<^sub>a\<^sub>x" + unfolding longest_chains_def by simp + ultimately show ?thesis + by (simp del: forks_at_most_def) +qed + +end + +text \ + Now we will test the chain selection rule algorithm using a test interpretation of + @{locale chain_selection}, in which blocks are basically `empty' except for the slot number, and + the block hash function is simply the identity function: +\ + +abbreviation (input) test_k :: nat where "test_k \ 2" +abbreviation (input) test_R :: nat where "test_R \ 4" \ \unused\ +abbreviation (input) test_f :: real where "test_f \ 1/2" \ \unused\ +abbreviation (input) test_ha :: real where "test_ha \ 3/4" \ \unused\ + +type_synonym test_block = "(unit, unit, unit, unit) block" +type_synonym test_chain = "(unit, unit, unit, unit) chain" + +abbreviation test_\\<^sub>B :: "test_block \ test_block" where "test_\\<^sub>B \ id" + +definition "test_forks_at_most = chain_selection.forks_at_most test_\\<^sub>B" +definition "test_first_suffix = chain_selection.first_suffix test_\\<^sub>B" +definition "test_max_valid = chain_selection.max_valid test_k test_\\<^sub>B" +definition test_longest_chains :: "test_chain list \ test_chain list" where + "test_longest_chains = chain_selection.longest_chains" + +interpretation test_chain_selection: chain_selection test_k test_R test_f test_ha test_\\<^sub>B + rewrites "chain_selection.forks_at_most test_\\<^sub>B = test_forks_at_most" + and "chain_selection.first_suffix test_\\<^sub>B = test_first_suffix" + and "chain_selection.longest_chains = test_longest_chains" + and "chain_selection.max_valid test_k test_\\<^sub>B = test_max_valid" + unfolding test_forks_at_most_def + and test_first_suffix_def + and test_longest_chains_def + and test_max_valid_def + by unfold_locales simp_all + +lemmas [code] = test_chain_selection.longest_chains_def + +abbreviation make_test_block :: "slot \ test_block" ("B\<^bsub>_\<^esub>") where + "B\<^bsub>sl\<^esub> \ ((sl, None, [], (U\<^bsub>0\<^esub>, ((), ())), ((), ())), ())" + +abbreviation make_test_chain :: "slot list \ test_chain" ("\_\") where + "\ss\ \ map make_test_block ss" + +notepad +begin + + let ?is_valid_fork = "\n \ \'. test_chain_selection.forks_at_most n \ \'" + + text \ + In this part we test the correctness of @{const chain_selection.forks_at_most}. To do so, we + check that the following graphs represent @{emph \valid\} forks, with the chain at the top of + each graph being the current local chain and the chain below the candidate chain: + + For \k = 2\: @{verbatim " + + G-0-1 G-0-1 G-0-1 G-0-1-2-3 + | | | | + -2-3-4 -2-3 -2-3 -4-5 + "} + \ + value "?is_valid_fork 2 \[0, 1]\ \[2, 3, 4]\" + value "?is_valid_fork 2 \[0, 1]\ \[0, 2, 3]\" + value "?is_valid_fork 2 \[0, 1]\ \[0, 1, 2, 3]\" + value "?is_valid_fork 2 \[0, 1, 2, 3]\ \[0, 1, 4, 5]\" + + text \ + And we check that the following graphs represent @{emph \invalid\} forks: + + For \k = 2\: @{verbatim " + + G-0-1-2 G-0-1-2-3 + | | + -3-4 -4-5 + "} + + For \k = 1\: @{verbatim " + + G-0-1 + | + -2-3-4 + "} + \ + value "\ ?is_valid_fork 2 \[0, 1, 2]\ \[3, 4]\" + value "\ ?is_valid_fork 2 \[0, 1, 2, 3]\ \[0, 4, 5]\" + value "\ ?is_valid_fork 1 \[0, 1]\ \[2, 3, 4]\" + + text \ + Now we test the correctness of the @{const chain_selection.max_valid} function using the + following test cases: + \ + + \ \No candidate chains were broadcast during the current slot, so the local chain is not updated:\ + value "test_chain_selection.max_valid \[0, 1]\ [] = \[0, 1]\" + + \ \The only candidate chain is longer than the local chain and is a valid fork, so it is adopted:\ + value "test_chain_selection.max_valid \[0, 1]\ [\[0, 1, 2]\] = \[0, 1, 2]\" + + \ \ + The only candidate chain is shorter than the local chain and a is valid fork, so it's not + adopted: + \ + value "test_chain_selection.max_valid \[0, 1, 2]\ [\[0, 1]\] = \[0, 1, 2]\" + + \ \ + The only candidate chain is equal length as the local chain and is a valid fork, so it's not + adopted (bias towards the local chain): + \ + value "test_chain_selection.max_valid \[0, 1]\ [\[3, 4]\] = \[0, 1]\" + + \ \ + The only candidate chain is longer than the local chain but is an invalid fork, so it's not + adopted: + \ + value "test_chain_selection.max_valid \[0, 1, 2]\ [\[3, 4, 5, 6]\] = \[0, 1, 2]\" + + \ \The longest candidate is adopted:\ + value "test_chain_selection.max_valid \[0, 1]\ [\[3, 4, 5, 6]\, \[0, 1, 2]\] = \[3, 4, 5, 6]\" + + \ \The first longest candidate is adopted:\ + value "test_chain_selection.max_valid \[0, 1]\ [\[0, 1, 2]\, \[0, 1, 3]\] = \[0, 1, 2]\" + + \ \Invalid forks are filtered out:\ + value "test_chain_selection.max_valid \[0, 1, 2]\ [\[3, 4, 5, 6]\, \[0, 1, 2, 3]\] = \[0, 1, 2, 3]\" + + code_thms test_chain_selection.forks_at_most test_chain_selection.max_valid + +end + end diff --git a/Isabelle/Thorn_Calculus/Thorn_Calculus-Semantics-Asynchronous.thy b/Isabelle/Thorn_Calculus/Thorn_Calculus-Semantics-Asynchronous.thy deleted file mode 100644 index 8c9b5b6..0000000 --- a/Isabelle/Thorn_Calculus/Thorn_Calculus-Semantics-Asynchronous.thy +++ /dev/null @@ -1,18 +0,0 @@ -section \Asynchronous Semantics\ - -theory "Thorn_Calculus-Semantics-Asynchronous" -imports - "Thorn_Calculus-Semantics-Synchronous" -begin - -fun asynchronous_transition :: "action \ process family relation" (\'(\\<^sub>a\_\')\) where - "(\\<^sub>a\A \ \\<^bsup>n\<^esup> X\) = {\ \ suffix n} OO {A \ suffix n \ X \ \}" | - "(\\<^sub>a\\\) = (\\<^sub>s\\\)" - -abbreviation - asynchronous_transition_std :: "process family \ action \ process family \ bool" - (\(_ \\<^sub>a\_\/ _)\ [51, 0, 51] 50) -where - "P \\<^sub>a\\\ Q \ (\\<^sub>a\\\) P Q" - -end