From 2d651dd8b9dd1b12059f877ede60eda06255ddd0 Mon Sep 17 00:00:00 2001 From: Javier Diaz Date: Mon, 5 Oct 2020 19:14:00 -0300 Subject: [PATCH 01/12] Axiomatize the injectivity property of hash functions --- .../Ouroboros/Ouroboros_Praos_Implementation.thy | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy b/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy index 3208bb0..1d3e4d1 100644 --- a/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy +++ b/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy @@ -83,10 +83,10 @@ text \ typedecl hash \ \ Hash values (i.e. $\{0,1\}^w$ in the paper) \ axiomatization - where - hash_finite: "OFCLASS(hash, finite_class)" - and - hash_equal: "OFCLASS(hash, equal_class)" +where + hash_finite: "OFCLASS(hash, finite_class)" +and + hash_equal: "OFCLASS(hash, equal_class)" instance hash :: finite by (rule hash_finite) @@ -94,7 +94,10 @@ instance hash :: finite instance hash :: equal by (rule hash_equal) -consts \ :: "'a \ hash" \ \ A collision-resistant hash function \ +axiomatization + \ :: "'a \ hash" \ \ A collision-resistant hash function \ +where + hash_inj: "inj \" text \ with no way of recovering @{typ 'a} from @{type hash}. From 7b7443e5188ea985a0bc140df103f22d858f1e68 Mon Sep 17 00:00:00 2001 From: Javier Diaz Date: Mon, 5 Oct 2020 19:18:41 -0300 Subject: [PATCH 02/12] Axiomatize the property that `f` is a non-zero probability --- Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy b/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy index 1d3e4d1..7752bb4 100644 --- a/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy +++ b/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy @@ -134,7 +134,10 @@ text \ stakeholder is elected as a slot leader, that is, the probability that a slot is not empty: \ -consts f :: real +axiomatization + f :: real +where + f_non_zero_probability: "0 < f \ f \ 1" text \ \<^item> Two special, but arbitrary, values that we use when calling the VRF in slot leader selection From 79f667f26b095f28f151f913e5209cc387ec4450 Mon Sep 17 00:00:00 2001 From: Javier Diaz Date: Mon, 5 Oct 2020 19:30:59 -0300 Subject: [PATCH 03/12] Axiomatize the cancellation property of VRF functions --- .../Ouroboros_Praos_Implementation.thy | 31 ++++++++++++------- 1 file changed, 19 insertions(+), 12 deletions(-) diff --git a/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy b/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy index 7752bb4..f1c5b00 100644 --- a/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy +++ b/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy @@ -33,6 +33,13 @@ typedecl secret_key typedecl verification_key + +text \ + such that it is possible to derive the verification key from the secret key: +\ + +consts verification_key_of :: "secret_key \ verification_key" + subsubsection \ The Semi-Synchronous model \ text \ @@ -160,7 +167,8 @@ paragraph \ Functionality \\\$_{\mathsf{VRF}}$. \ text \ We model the evaluation of a VRF as a function that, given an input value and a secret key, - produces a random value and a proof: + produces a random value and a proof. Also, we can verify that a particular random value was + produced correctly: \ typedecl vrf_output @@ -168,10 +176,10 @@ typedecl vrf_output typedecl vrf_proof axiomatization - where - vrf_output_finite: "OFCLASS(vrf_output, finite_class)" - and - vrf_proof_finite: "OFCLASS(vrf_proof, finite_class)" +where + vrf_output_finite: "OFCLASS(vrf_output, finite_class)" +and + vrf_proof_finite: "OFCLASS(vrf_proof, finite_class)" instance vrf_output :: finite by (rule vrf_output_finite) @@ -183,13 +191,12 @@ type_synonym vrf_value = "vrf_output \ vrf_proof" consts vrf_output_size :: nat (\l\<^sub>V\<^sub>R\<^sub>F\) -consts evaluate_vrf :: "secret_key \ 'a \ vrf_value" - -text \ - Also, we can verify that a particular random value was produced correctly: -\ - -consts verify_vrf :: "verification_key \ 'a \ vrf_value \ bool" +axiomatization + evaluate_vrf :: "secret_key \ 'a \ vrf_value" +and + verify_vrf :: "verification_key \ 'a \ vrf_value \ bool" +where + vrf_eval_ver_cancellation: "verify_vrf vk x (evaluate_vrf sk x)" if "vk = verification_key_of sk" text \ Finally, we can cast a VRF output into a real number: From f1ab8672427ff36d28b9e745f9f57c22ec8a38e5 Mon Sep 17 00:00:00 2001 From: Javier Diaz Date: Mon, 5 Oct 2020 19:36:46 -0300 Subject: [PATCH 04/12] Axiomatize the cancellation property of digital signatures --- .../Ouroboros/Ouroboros_Praos_Implementation.thy | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy b/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy index f1c5b00..adad4fb 100644 --- a/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy +++ b/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy @@ -212,7 +212,7 @@ text \ capability of allowing the signing key to ``evolve'' in such a way that the adversary cannot forge past signatures, and is used to sign blocks. Therefore, we model these two functionalities as a single, ordinary digital signature scheme. With this scheme, we can sign a - value using a secret key: + value using a secret key and verify that a value is properly signed using a verification key: \ typedecl signature @@ -224,13 +224,12 @@ axiomatization instance signature :: finite by (rule signature_finite) -consts sign :: "secret_key \ 'a \ signature" - -text \ - and verify that a value is properly signed using a verification key: -\ - -consts verify :: "verification_key \ 'a \ signature \ bool" +axiomatization + sign :: "secret_key \ 'a \ signature" +and + verify :: "verification_key \ 'a \ signature \ bool" +where + sig_ver_cancellation: "verify vk x (sign sk x)" if "vk = verification_key_of sk" paragraph \ Functionality \\\$^{\tau,r}_{RLB}$. \ From f57d1f8f37783ede38f953166d96527e16a9d6cf Mon Sep 17 00:00:00 2001 From: Javier Diaz Date: Mon, 5 Oct 2020 19:39:01 -0300 Subject: [PATCH 05/12] Document `new_epoch_rnd` function --- Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy b/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy index adad4fb..398ab6d 100644 --- a/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy +++ b/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy @@ -238,7 +238,8 @@ text \ provides a fresh nonce for each epoch to (re)seed the election process. Also, this beacon is resettable and leaky in order to strengthen the adversary, which we evidently ignore. Finally, the beacon (via \\\$_{\mathsf{INIT}}$) provides the stakeholders with the genesis block; instead - our implementation passes the genesis block as a parameter to each stakeholder. + our implementation passes the genesis block as a parameter to each stakeholder. Therefore, we + only provide a function to produce a fresh nonce: \ typedecl nonce From c8e1c2f0398870c375f7544870ce56582f9f4f74 Mon Sep 17 00:00:00 2001 From: Javier Diaz Date: Mon, 5 Oct 2020 20:01:10 -0300 Subject: [PATCH 06/12] Change to finite maps to implement stake distributions --- Isabelle/Ouroboros/Finite_Map_Extras.thy | 705 ++++++++++++++++++ .../Ouroboros_Praos_Implementation.thy | 15 +- Isabelle/Ouroboros/ROOT | 1 + 3 files changed, 716 insertions(+), 5 deletions(-) create mode 100644 Isabelle/Ouroboros/Finite_Map_Extras.thy diff --git a/Isabelle/Ouroboros/Finite_Map_Extras.thy b/Isabelle/Ouroboros/Finite_Map_Extras.thy new file mode 100644 index 0000000..9f0e6d0 --- /dev/null +++ b/Isabelle/Ouroboros/Finite_Map_Extras.thy @@ -0,0 +1,705 @@ +section \ Extra Features for Finite Maps \ + +theory Finite_Map_Extras + imports "HOL-Library.Finite_Map" +begin + +text \ Extra lemmas and syntactic sugar for \fmap\ \ + +notation fmlookup (infixl \$$\ 900) + +notation fmempty (\{$$}\) + +nonterminal fmaplets and fmaplet + +syntax + "_fmaplet" :: "['a, 'a] \ fmaplet" ("_ /$$:=/ _") + "_fmaplets" :: "['a, 'a] \ fmaplet" ("_ /[$$:=]/ _") + "" :: "fmaplet \ fmaplets" ("_") + "_Fmaplets" :: "[fmaplet, fmaplets] \ fmaplets" ("_,/ _") + "_FmapUpd" :: "[('a, 'b) fmap, fmaplets] \ ('a, 'b) fmap" ("_/'(_')" [900, 0] 900) + "_Fmap" :: "fmaplets \ ('a, 'b) fmap" ("(1{_})") + +translations + "_FmapUpd m (_Fmaplets xy ms)" \ "_FmapUpd (_FmapUpd m xy) ms" + "_FmapUpd m (_fmaplet x y)" \ "CONST fmupd x y m" + "_Fmap ms" \ "_FmapUpd (CONST fmempty) ms" + "_Fmap (_Fmaplets ms1 ms2)" \ "_FmapUpd (_Fmap ms1) ms2" + "_Fmaplets ms1 (_Fmaplets ms2 ms3)" \ "_Fmaplets (_Fmaplets ms1 ms2) ms3" + +abbreviation fmap_lookup_the (infixl \$$!\ 900) where + "m $$! k \ the (m $$ k)" + +value "{$$}::(nat, nat) fmap" +value "{1::nat $$:= 2::nat, 3 $$:= 4}(1 $$:= 0) $$! 1" + + +lemma fmadd_singletons_comm: + assumes "k\<^sub>1 \ k\<^sub>2" + shows "{k\<^sub>1 $$:= v\<^sub>1} ++\<^sub>f {k\<^sub>2 $$:= v\<^sub>2} = {k\<^sub>2 $$:= v\<^sub>2} ++\<^sub>f {k\<^sub>1 $$:= v\<^sub>1}" +proof (intro fmap_ext) + fix k + consider + (a) "k = k\<^sub>1" | + (b) "k = k\<^sub>2" | + (c) "k \ k\<^sub>1 \ k \ k\<^sub>2" + by auto + with assms show "({k\<^sub>1 $$:= v\<^sub>1} ++\<^sub>f {k\<^sub>2 $$:= v\<^sub>2}) $$ k = ({k\<^sub>2 $$:= v\<^sub>2} ++\<^sub>f {k\<^sub>1 $$:= v\<^sub>1}) $$ k" + by auto +qed + +lemma fmap_singleton_comm: + assumes "m $$ k = None" + shows "m ++\<^sub>f {k $$:= v} = {k $$:= v} ++\<^sub>f m" + using assms +proof (induction m arbitrary: k v) + case fmempty + then show ?case + by simp +next + case (fmupd x y m) + have "m(x $$:= y) ++\<^sub>f {k $$:= v} = m ++\<^sub>f {x $$:= y} ++\<^sub>f {k $$:= v}" + by simp + also from fmupd.hyps and fmupd.IH have "\ = {x $$:= y} ++\<^sub>f m ++\<^sub>f {k $$:= v}" + by simp + also from fmupd.prems and fmupd.hyps and fmupd.IH have "\ = {x $$:= y} ++\<^sub>f {k $$:= v} ++\<^sub>f m" + by (metis fmadd_assoc fmupd_lookup) + also have "\ = {k $$:= v} ++\<^sub>f m(x $$:= y)" + proof (cases "x \ k") + case True + then have "{x $$:= y} ++\<^sub>f {k $$:= v} ++\<^sub>f m = {k $$:= v} ++\<^sub>f {x $$:= y} ++\<^sub>f m" + using fmadd_singletons_comm by metis + also from fmupd.prems and fmupd.hyps and fmupd.IH have "\ = {k $$:= v} ++\<^sub>f m ++\<^sub>f {x $$:= y}" + by (metis fmadd_assoc) + finally show ?thesis + by simp + next + case False + with fmupd.prems show ?thesis + by auto + qed + finally show ?case . +qed + +lemma fmap_disj_comm: + assumes "fmdom' m\<^sub>1 \ fmdom' m\<^sub>2 = {}" + shows "m\<^sub>1 ++\<^sub>f m\<^sub>2 = m\<^sub>2 ++\<^sub>f m\<^sub>1" + using assms +proof (induction m\<^sub>2 arbitrary: m\<^sub>1) + case fmempty + then show ?case + by simp +next + case (fmupd k v m\<^sub>2) + then show ?case + proof (cases "m\<^sub>1 $$ k = None") + case True + from fmupd.hyps have "m\<^sub>1 ++\<^sub>f m\<^sub>2(k $$:= v) = m\<^sub>1 ++\<^sub>f m\<^sub>2 ++\<^sub>f {k $$:= v}" + by simp + also from fmupd.prems and fmupd.hyps and fmupd.IH have "\ = m\<^sub>2 ++\<^sub>f m\<^sub>1 ++\<^sub>f {k $$:= v}" + by simp + also from True have "\ = m\<^sub>2 ++\<^sub>f {k $$:= v} ++\<^sub>f m\<^sub>1" + using fmap_singleton_comm by (metis fmadd_assoc) + finally show ?thesis + by simp + next + case False + with fmupd.prems show ?thesis + by auto + qed +qed + +lemma fmran_singleton: "fmran {k $$:= v} = {|v|}" +proof - + have "v' |\| fmran {k $$:= v} \ v' = v" for v' + proof - + assume "v' |\| fmran {k $$:= v}" + fix k' + have "fmdom' {k $$:= v} = {k}" + by simp + then show "v' = v" + proof (cases "k' = k") + case True + with \v' |\| fmran {k $$:= v}\ show ?thesis + using fmdom'I by fastforce + next + case False + with \fmdom' {k $$:= v} = {k}\ and \v' |\| fmran {k $$:= v}\ show ?thesis + using fmdom'I by fastforce + qed + qed + moreover have "v |\| fmran {k $$:= v}" + by (simp add: fmranI) + ultimately show ?thesis + by (simp add: fsubsetI fsubset_antisym) +qed + +lemma fmmap_keys_hom: + assumes "fmdom' m\<^sub>1 \ fmdom' m\<^sub>2 = {}" + shows "fmmap_keys f (m\<^sub>1 ++\<^sub>f m\<^sub>2) = fmmap_keys f m\<^sub>1 ++\<^sub>f fmmap_keys f m\<^sub>2" + using assms + by (simp add: fmap_ext) + +lemma map_insort_is_insort_key: + assumes "m $$ k = None" + shows "map (\k'. (k', m(k $$:= v) $$! k')) (insort k xs) = + insort_key fst (k, v) (map (\k'. (k', m(k $$:= v) $$! k')) xs)" + using assms by (induction xs) auto + +lemma sorted_list_of_fmap_is_insort_key_fst: + assumes "m $$ k = None" + shows "sorted_list_of_fmap (m(k $$:= v)) = insort_key fst (k, v) (sorted_list_of_fmap m)" +proof - + have "sorted_list_of_fmap (m(k $$:= v)) = + map (\k'. (k', m(k $$:= v) $$! k')) (sorted_list_of_fset (fmdom (m(k $$:= v))))" + unfolding sorted_list_of_fmap_def .. + also have "\ = map (\k'. (k', m(k $$:= v) $$! k')) (sorted_list_of_fset (finsert k (fmdom m)))" + by simp + also from \m $$ k = None\ have "\ = + map (\k'. (k', m(k $$:= v) $$! k')) (insort k (sorted_list_of_fset (fmdom m - {|k|})))" + by (simp add: sorted_list_of_fset.rep_eq) + also from \m $$ k = None\ have "\ = + map (\k'. (k', m(k $$:= v) $$! k')) (insort k (sorted_list_of_fset (fmdom m)))" + by (simp add: fmdom_notI) + also from \m $$ k = None\ have "\ = + insort_key fst (k, v) (map (\k'. (k', m(k $$:= v) $$! k')) (sorted_list_of_fset (fmdom m)))" + using map_insort_is_insort_key by fastforce + also have "\ = insort_key fst (k, v) (map (\k'. (k', m $$! k')) (sorted_list_of_fset (fmdom m)))" + proof - + from \m $$ k = None\ have "\k'. k' \ fmdom' m \ m(k $$:= v) $$! k' = m $$! k'" + using fmdom'_notI by force + moreover from \m $$ k = None\ have "k \ set (sorted_list_of_fset (fmdom m))" + using fmdom'_alt_def and fmdom'_notI and in_set_member by force + ultimately show ?thesis + by (metis (mono_tags, lifting) fmdom'_alt_def map_eq_conv sorted_list_of_fset_simps(1)) + qed + finally show ?thesis + unfolding sorted_list_of_fmap_def by simp +qed + +lemma distinct_fst_inj: + assumes "distinct (map fst ps)" + and "inj f" + shows "distinct (map fst (map (\(k, v). (f k, v)) ps))" +proof - + have "map fst (map (\(k, v). (f k, v)) ps) = map f (map fst ps)" + by (induction ps) auto + moreover from assms have "distinct (map f (map fst ps))" + by (simp add: distinct_map inj_on_def) + ultimately show ?thesis + by presburger +qed + +lemma distinct_sorted_list_of_fmap: + shows "distinct (map fst (sorted_list_of_fmap m))" + unfolding sorted_list_of_fmap_def and sorted_list_of_fset_def + by (simp add: distinct_map inj_on_def) + +lemma map_inj_pair_non_membership: + assumes "k \ set (map fst ps)" + and "inj f" + shows "f k \ set (map fst (map (\(k, v). (f k, v)) ps))" + using assms by (induction ps) (simp add: member_rec(2), fastforce simp add: injD) + +lemma map_insort_key_fst: + assumes "distinct (map fst ps)" + and "k \ set (map fst ps)" + and "inj f" + and "mono f" + shows "map (\(k, v). (f k, v)) (insort_key fst (k, v) ps) = + insort_key fst (f k, v) (map (\(k, v). (f k, v)) ps)" + using assms +proof (induction ps) + case Nil + then show ?case + by simp +next + let ?g = "(\(k, v). (f k, v))" + case (Cons p ps) + then show ?case + proof (cases "k \ fst p") + case True + let ?f_p = "(f (fst p), snd p)" + have "insort_key fst (f k, v) (map ?g (p # ps)) = insort_key fst (f k, v) (?f_p # map ?g ps)" + by (simp add: prod.case_eq_if) + moreover from Cons.prems(4) and True have "f k \ f (fst p)" + by (auto dest: monoE) + then have "insort_key fst (f k, v) (?f_p # map ?g ps) = (f k, v) # ?f_p # map ?g ps" + by simp + ultimately have "insort_key fst (f k, v) (map ?g (p # ps)) = (f k, v) # ?f_p # map ?g ps" + by simp + moreover from True have "map ?g (insort_key fst (k, v) (p # ps)) = (f k, v) # ?f_p # map ?g ps" + by (simp add: case_prod_beta') + ultimately show ?thesis + by simp + next + case False + let ?f_p = "(f (fst p), snd p)" + have "insort_key fst (f k, v) (map ?g (p # ps)) = insort_key fst (f k, v) (?f_p # map ?g ps)" + by (simp add: prod.case_eq_if) + moreover from \mono f\ and False have "f (fst p) \ f k" + using not_le by (blast dest: mono_invE) + ultimately have "insort_key fst (f k, v) (map ?g (p # ps)) = + ?f_p # insort_key fst (f k, v) (map ?g ps)" + using False and \inj f\ by (fastforce dest: injD) + also from Cons.IH and Cons.prems(1,2) and assms(3,4) have "\ = + ?f_p # (map ?g (insort_key fst (k, v) ps))" + by (fastforce simp add: member_rec(1)) + also have "\ = map ?g (p # insort_key fst (k, v) ps)" + by (simp add: case_prod_beta) + finally show ?thesis + using False by simp + qed +qed + +lemma map_sorted_list_of_fmap: + assumes "inj f" + and "mono f" + and "m $$ k = None" + shows "map (\(k, v). (f k, v)) (sorted_list_of_fmap (m(k $$:= v))) = + insort_key fst (f k, v) (map (\(k, v). (f k, v)) (sorted_list_of_fmap m))" +proof - + let ?g = "(\(k, v). (f k, v))" + from \m $$ k = None\ have "map ?g (sorted_list_of_fmap (m(k $$:= v))) = + map ?g (insort_key fst (k, v) (sorted_list_of_fmap m))" + using sorted_list_of_fmap_is_insort_key_fst by fastforce + also have "\ = insort_key fst (f k, v) (map ?g (sorted_list_of_fmap m))" + proof - + have "distinct (map fst (sorted_list_of_fmap m))" + by (simp add: distinct_sorted_list_of_fmap) + moreover from \m $$ k = None\ have "k \ set (map fst (sorted_list_of_fmap m))" + by (metis image_set map_of_eq_None_iff map_of_sorted_list) + ultimately show ?thesis + by (simp add: map_insort_key_fst assms(1,2)) + qed + finally show ?thesis . +qed + +lemma fmap_of_list_insort_key_fst: + assumes "distinct (map fst ps)" + and "k \ set (map fst ps)" + shows "fmap_of_list (insort_key fst (k, v) ps) = (fmap_of_list ps)(k $$:= v)" + using assms +proof (induction ps) + case Nil + then show ?case + by simp +next + case (Cons p ps) + then show ?case + proof (cases "k \ fst p") + case True + then show ?thesis + by simp + next + case False + then have "fmap_of_list (insort_key fst (k, v) (p # ps)) = + fmap_of_list (p # insort_key fst (k, v) ps)" + by simp + also have "\ = (fmap_of_list (insort_key fst (k, v) ps))(fst p $$:= snd p)" + by (metis fmap_of_list_simps(2) prod.collapse) + also from Cons.prems(1,2) and Cons.IH have "\ = (fmap_of_list ps)(k $$:= v)(fst p $$:= snd p)" + by (fastforce simp add: member_rec(1)) + finally show ?thesis + proof - + assume *: "fmap_of_list (insort_key fst (k, v) (p # ps)) = + (fmap_of_list ps)(k $$:= v)(fst p $$:= snd p)" + from Cons.prems(2) have "k \ set (fst p # map fst ps)" + by simp + then have **: "{k $$:= v} $$ (fst p) = None" + by (fastforce simp add: member_rec(1)) + have "fmap_of_list (p # ps) = (fmap_of_list ps)(fst p $$:= snd p)" + by (metis fmap_of_list_simps(2) prod.collapse) + with * and ** show ?thesis + using fmap_singleton_comm by (metis fmadd_fmupd fmap_of_list_simps(1,2) fmupd_alt_def) + qed + qed +qed + +lemma fmap_of_list_insort_key_fst_map: + assumes "inj f" + and "m $$ k = None" + shows "fmap_of_list (insort_key fst (f k, v) (map (\(k, v). (f k, v)) (sorted_list_of_fmap m))) = + (fmap_of_list (map (\(k, v). (f k, v)) (sorted_list_of_fmap m)))(f k $$:= v)" +proof - + let ?g = "\(k, v). (f k, v)" + let ?ps = "map ?g (sorted_list_of_fmap m)" + from \inj f\ have "distinct (map fst ?ps)" + using distinct_fst_inj and distinct_sorted_list_of_fmap by fastforce + moreover have "f k \ set (map fst ?ps)" + proof - + from \m $$ k = None\ have "k \ set (map fst (sorted_list_of_fmap m))" + by (metis map_of_eq_None_iff map_of_sorted_list set_map) + with \inj f\ show ?thesis + using map_inj_pair_non_membership by force + qed + ultimately show ?thesis + using fmap_of_list_insort_key_fst by fast +qed + +lemma fmap_of_list_sorted_list_of_fmap: + fixes m :: "('a::linorder, 'b) fmap" + and f :: "'a \ 'c::linorder" + assumes "inj f" + and "mono f" + and "m $$ k = None" + shows "fmap_of_list (map (\(k, v). (f k, v)) (sorted_list_of_fmap (m(k $$:= v)))) = + (fmap_of_list (map (\(k, v). (f k, v)) (sorted_list_of_fmap m)))(f k $$:= v)" +proof - + let ?g = "\(k, v). (f k, v)" + from assms(3) have "fmap_of_list (map ?g (sorted_list_of_fmap (m(k $$:= v)))) = + fmap_of_list (map ?g (insort_key fst (k, v) (sorted_list_of_fmap m)))" + by (simp add: sorted_list_of_fmap_is_insort_key_fst) + also from assms have "\ = fmap_of_list (insort_key fst (f k, v) (map ?g (sorted_list_of_fmap m)))" + using calculation and map_sorted_list_of_fmap by fastforce + also from assms(1,3) have "\ = (fmap_of_list (map ?g (sorted_list_of_fmap m)))(f k $$:= v)" + by (simp add: fmap_of_list_insort_key_fst_map) + finally show ?thesis . +qed + +text \ Map difference \ + +lemma fsubset_antisym: + assumes "m \\<^sub>f n" + and "n \\<^sub>f m" + shows "m = n" +proof - + from \m \\<^sub>f n\ have "\k \ dom (($$) m). (($$) m) k = (($$) n) k" + by (simp add: fmsubset.rep_eq map_le_def) + moreover from \n \\<^sub>f m\ have "\k \ dom (($$) n). (($$) n) k = (($$) m) k" + by (simp add: fmsubset.rep_eq map_le_def) + ultimately show ?thesis + proof (intro fmap_ext) + fix k + consider + (a) "k \ dom (($$) m)" | + (b) "k \ dom (($$) n)" | + (c) "k \ dom (($$) m) \ k \ dom (($$) n)" + by auto + then show "m $$ k = n $$ k" + proof cases + case a + with \\k \ dom (($$) m). m $$ k = n $$ k\ show ?thesis + by simp + next + case b + with \\k \ dom (($$) n). n $$ k = m $$ k\ show ?thesis + by simp + next + case c + then show ?thesis + by (simp add: fmdom'_notD) + qed + qed +qed + +abbreviation + fmdiff :: "('a, 'b) fmap \ ('a, 'b) fmap \ ('a, 'b) fmap" (infixl \--\<^sub>f\ 100) where + "m\<^sub>1 --\<^sub>f m\<^sub>2 \ fmfilter (\x. x \ fmdom' m\<^sub>2) m\<^sub>1" + +lemma fmdiff_partition: + assumes "m\<^sub>2 \\<^sub>f m\<^sub>1" + shows "m\<^sub>2 ++\<^sub>f (m\<^sub>1 --\<^sub>f m\<^sub>2) = m\<^sub>1" +proof - + have *: "m\<^sub>2 ++\<^sub>f (m\<^sub>1 --\<^sub>f m\<^sub>2) \\<^sub>f m\<^sub>1" + proof - + have "\k v. (m\<^sub>2 ++\<^sub>f (m\<^sub>1 --\<^sub>f m\<^sub>2)) $$ k = Some v \ m\<^sub>1 $$ k = Some v" + proof (intro allI impI) + fix k v + assume "(m\<^sub>2 ++\<^sub>f (m\<^sub>1 --\<^sub>f m\<^sub>2)) $$ k = Some v" + then have **: "(if k |\| fmdom (m\<^sub>1 --\<^sub>f m\<^sub>2) then (m\<^sub>1 --\<^sub>f m\<^sub>2) $$ k else m\<^sub>2 $$ k) = Some v" + by simp + then show "m\<^sub>1 $$ k = Some v" + proof (cases "k |\| fmdom (m\<^sub>1 --\<^sub>f m\<^sub>2)") + case True + with ** show ?thesis + by simp + next + case False + with ** and \m\<^sub>2 \\<^sub>f m\<^sub>1\ show ?thesis + by (metis (mono_tags, lifting) fmpredD fmsubset_alt_def) + qed + qed + then have "fmpred (\k v. m\<^sub>1 $$ k = Some v) (m\<^sub>2 ++\<^sub>f (m\<^sub>1 --\<^sub>f m\<^sub>2))" + by (blast intro: fmpred_iff) + then show ?thesis + by (auto simp add: fmsubset_alt_def) + qed + then have "m\<^sub>1 \\<^sub>f m\<^sub>2 ++\<^sub>f (m\<^sub>1 --\<^sub>f m\<^sub>2)" + by (simp add: fmsubset.rep_eq map_le_def) + with * show ?thesis + by (simp add: fsubset_antisym) +qed + +lemma fmdiff_fmupd: + assumes "m $$ k = None" + shows "m(k $$:= v) --\<^sub>f {k $$:= v} = m" +proof - + let ?P = "(\k'. k' \ {k})" + have "m(k $$:= v) --\<^sub>f {k $$:= v} = fmfilter (\x. x \ fmdom' {k $$:= v}) (m(k $$:= v))" .. + also have "\ = fmfilter ?P (m(k $$:= v))" + by simp + also have "\ = (if ?P k then (fmfilter ?P m)(k $$:= v) else fmfilter ?P m)" + by simp + also have "\ = fmfilter ?P m" + by simp + finally show ?thesis + proof - + from \m $$ k = None\ have "\k' v'. m $$ k' = Some v' \ ?P k'" + by fastforce + then show ?thesis + by simp + qed +qed + +text \ Map symmetric difference \ + +abbreviation fmsym_diff :: "('a, 'b) fmap \ ('a, 'b) fmap \ ('a, 'b) fmap" (infixl \\\<^sub>f\ 100) where + "m\<^sub>1 \\<^sub>f m\<^sub>2 \ (m\<^sub>1 --\<^sub>f m\<^sub>2) ++\<^sub>f (m\<^sub>2 --\<^sub>f m\<^sub>1)" + +text \ Domain restriction \ + +abbreviation dom_res :: "'a set \ ('a, 'b) fmap \ ('a, 'b) fmap" (infixl \\\ 150) where + "s \ m \ fmfilter (\x. x \ s) m" + +text \ Domain exclusion \ + +abbreviation dom_exc :: "'a set \ ('a, 'b) fmap \ ('a, 'b) fmap" (infixl \\'/\ 150) where + "s \/ m \ fmfilter (\x. x \ s) m" + +text \ Intersection plus \ + +abbreviation intersection_plus :: "('a, 'b::monoid_add) fmap \ ('a, 'b) fmap \ ('a, 'b) fmap" + (infixl \\\<^sub>+\ 100) +where + "m\<^sub>1 \\<^sub>+ m\<^sub>2 \ fmmap_keys (\k v. v + m\<^sub>1 $$! k) (fmdom' m\<^sub>1 \ m\<^sub>2)" + +text \ Union override right \ + +abbreviation union_override_right :: "('a, 'b) fmap \ ('a, 'b) fmap \ ('a, 'b) fmap" + (infixl \\\<^sub>\\ 100) +where + "m\<^sub>1 \\<^sub>\ m\<^sub>2 \ (fmdom' m\<^sub>2 \/ m\<^sub>1) ++\<^sub>f m\<^sub>2" + +text \ Union override left \ + +abbreviation union_override_left :: "('a, 'b) fmap \ ('a, 'b) fmap \ ('a, 'b) fmap" + (infixl \\\<^sub>\\ 100) +where + "m\<^sub>1 \\<^sub>\ m\<^sub>2 \ m\<^sub>1 ++\<^sub>f (fmdom' m\<^sub>1 \/ m\<^sub>2)" + +text \ Union override plus \ + +abbreviation union_override_plus :: "('a, 'b::monoid_add) fmap \ ('a, 'b) fmap \ ('a, 'b) fmap" + (infixl \\\<^sub>+\ 100) +where + "m\<^sub>1 \\<^sub>+ m\<^sub>2 \ (m\<^sub>1 \\<^sub>f m\<^sub>2) ++\<^sub>f (m\<^sub>1 \\<^sub>+ m\<^sub>2)" + +text \ Extra lemmas for the non-standard map operators \ + +lemma dom_res_singleton: + assumes "m $$ k = Some v" + shows "{k} \ m = {k $$:= v}" + using assms +proof (induction m) + case fmempty + then show ?case + by simp +next + case (fmupd k' v' m) + then show ?case + proof (cases "k = k'") + case True + with \m(k' $$:= v') $$ k = Some v\ have "v = v'" + by simp + with True have "{k} \ m(k' $$:= v') = ({k} \ m)(k $$:= v)" + by simp + also from True and \m $$ k' = None\ have "\ = {$$}(k $$:= v)" + by (simp add: fmap_ext) + finally show ?thesis + by simp + next + case False + with \m(k' $$:= v') $$ k = Some v\ have *: "m $$ k = Some v" + by simp + with False have "{k} \ m(k' $$:= v') = {k} \ m" + by simp + with * and fmupd.IH show ?thesis + by simp + qed +qed + +lemma dom_res_union_distr: + shows "(A \ B) \ m = A \ m ++\<^sub>f B \ m" +proof - + have "($$) ((A \ B) \ m) \\<^sub>m ($$) (A \ m ++\<^sub>f B \ m)" + proof (unfold map_le_def, intro ballI) + fix k + assume "k \ dom (($$) ((A \ B) \ m))" + then show "((A \ B) \ m) $$ k = (A \ m ++\<^sub>f B \ m) $$ k" + by auto + qed + moreover have "($$) (A \ m ++\<^sub>f B \ m) \\<^sub>m ($$) ((A \ B) \ m)" + proof (unfold map_le_def, intro ballI) + fix k + assume "k \ dom (($$) (A \ m ++\<^sub>f B \ m))" + then show "(A \ m ++\<^sub>f B \ m) $$ k = ((A \ B) \ m) $$ k" + by auto + qed + ultimately show ?thesis + using fmlookup_inject and map_le_antisym by blast +qed + +lemma dom_exc_add_distr: + shows "s \/ (m\<^sub>1 ++\<^sub>f m\<^sub>2) = (s \/ m\<^sub>1) ++\<^sub>f (s \/ m\<^sub>2)" + by (blast intro: fmfilter_add_distrib) + +lemma fmap_partition: + shows "m = s \/ m ++\<^sub>f s \ m" +proof (induction m) + case fmempty + then show ?case + by simp +next + case (fmupd k v m) + from fmupd.hyps have "s \/ m(k $$:= v) ++\<^sub>f s \ m(k $$:= v) = + s \/ (m ++\<^sub>f {k $$:= v}) ++\<^sub>f s \ (m ++\<^sub>f {k $$:= v})" + by simp + also have "\ = s \/ m ++\<^sub>f s \/ {k $$:= v} ++\<^sub>f s \ m ++\<^sub>f s \ {k $$:= v}" + using dom_exc_add_distr by simp + finally show ?case + proof (cases "k \ s") + case True + then have "s \/ m ++\<^sub>f s \/ {k $$:= v} ++\<^sub>f s \ m ++\<^sub>f s \ {k $$:= v} = + s \/ m ++\<^sub>f {$$} ++\<^sub>f s \ m ++\<^sub>f {k $$:= v}" + by simp + also have "\ = s \/ m ++\<^sub>f s \ m ++\<^sub>f {k $$:= v}" + by simp + also from fmupd.IH have "\ = m ++\<^sub>f {k $$:= v}" + by simp + finally show ?thesis using fmupd.hyps + by auto + next + case False + then have "s \/ m ++\<^sub>f s \/ {k $$:= v} ++\<^sub>f s \ m ++\<^sub>f s \ {k $$:= v} = + s \/ m ++\<^sub>f {k $$:= v} ++\<^sub>f s \ m ++\<^sub>f {$$}" + by simp + also have "\ = s \/ m ++\<^sub>f {k $$:= v} ++\<^sub>f s \ m" + by simp + also from fmupd.hyps have "\ = s \/ m ++\<^sub>f s \ m ++\<^sub>f {k $$:= v}" + using fmap_singleton_comm by (metis (full_types) fmadd_assoc fmlookup_filter) + also from fmupd.IH have "\ = m ++\<^sub>f {k $$:= v}" + by simp + finally show ?thesis + by auto + qed +qed + +lemma dom_res_addition_in: + assumes "m\<^sub>1 $$ k = None" + and "m\<^sub>2 $$ k = Some v'" + shows "fmdom' (m\<^sub>1(k $$:= v)) \ m\<^sub>2 = fmdom' m\<^sub>1 \ m\<^sub>2 ++\<^sub>f {k $$:= v'}" +proof - + from \m\<^sub>1 $$ k = None\ have "fmdom' (m\<^sub>1(k $$:= v)) \ m\<^sub>2 = (fmdom' m\<^sub>1 \ {k}) \ m\<^sub>2" + by simp + also have "\ = fmdom' m\<^sub>1 \ m\<^sub>2 ++\<^sub>f {k} \ m\<^sub>2" + using dom_res_union_distr . + finally show ?thesis + using \m\<^sub>2 $$ k = Some v'\ and dom_res_singleton by fastforce +qed + +lemma dom_res_addition_not_in: + assumes "m\<^sub>2 $$ k = None" + shows "fmdom' (m\<^sub>1(k $$:= v)) \ m\<^sub>2 = fmdom' m\<^sub>1 \ m\<^sub>2" +proof - + have "fmdom' (m\<^sub>1(k $$:= v)) \ m\<^sub>2 = fmfilter (\k'. k' = k \ k' \ fmdom' m\<^sub>1) m\<^sub>2" + by simp + also have "\ = fmdom' m\<^sub>1 \ m\<^sub>2" + proof (intro fmfilter_cong') + show "m\<^sub>2 = m\<^sub>2" .. + next + from assms show "k' \ fmdom' m\<^sub>2 \ (k' = k \ k' \ fmdom' m\<^sub>1) = (k' \ fmdom' m\<^sub>1)" for k' + by (cases "k' = k") (simp_all add: fmdom'_notI) + qed + finally show ?thesis . +qed + +lemma inter_plus_addition_in: + assumes "m\<^sub>1 $$ k = None" + and "m\<^sub>2 $$ k = Some v'" + shows "m\<^sub>1(k $$:= v) \\<^sub>+ m\<^sub>2 = (m\<^sub>1 \\<^sub>+ m\<^sub>2) ++\<^sub>f {k $$:= v' + v}" +proof - + let ?f = "\k' v'. v' + m\<^sub>1(k $$:= v) $$! k'" + from assms have "m\<^sub>1(k $$:= v) \\<^sub>+ m\<^sub>2 = fmmap_keys ?f ((fmdom' m\<^sub>1 \ m\<^sub>2) ++\<^sub>f {k $$:= v'})" + using dom_res_addition_in by fastforce + also have "\ = fmmap_keys ?f (fmdom' m\<^sub>1 \ m\<^sub>2) ++\<^sub>f fmmap_keys ?f {k $$:= v'}" + proof - + from \m\<^sub>1 $$ k = None\ have "fmdom' (fmdom' m\<^sub>1 \ m\<^sub>2) \ fmdom' {k $$:= v'} = {}" + by (simp add: fmdom'_notI) + then show ?thesis + using fmmap_keys_hom by blast + qed + also from assms + have "\ = fmmap_keys ?f (fmdom' m\<^sub>1 \ m\<^sub>2) ++\<^sub>f {k $$:= v' + v}" + proof - + have "fmmap_keys ?f {k $$:= v'} = {k $$:= v' + v}" + proof (intro fmap_ext) + fix k' + have "fmmap_keys ?f {k $$:= v'} $$ k' = map_option (?f k') ({k $$:= v'} $$ k')" + using fmlookup_fmmap_keys . + also have "\ = map_option (?f k') (if k = k' then Some v' else {$$} $$ k')" + by simp + also have "\ = {k $$:= v' + v} $$ k'" + by (cases "k' = k") simp_all + finally show "fmmap_keys ?f {k $$:= v'} $$ k' = {k $$:= v' + v} $$ k'" . + qed + then show ?thesis + by simp + qed + also have "\ = fmmap_keys (\k' v'. v' + m\<^sub>1 $$! k') (fmdom' m\<^sub>1 \ m\<^sub>2) ++\<^sub>f {k $$:= v' + v}" + by (simp add: fmap_ext) + finally show ?thesis . +qed + +lemma inter_plus_addition_notin: + assumes "m\<^sub>1 $$ k = None" + and "m\<^sub>2 $$ k = None" + shows "m\<^sub>1(k $$:= v) \\<^sub>+ m\<^sub>2 = (m\<^sub>1 \\<^sub>+ m\<^sub>2)" +proof - + let ?f = "\k' v'. v' + m\<^sub>1(k $$:= v) $$! k'" + from \m\<^sub>2 $$ k = None\ + have "m\<^sub>1(k $$:= v) \\<^sub>+ m\<^sub>2 = fmmap_keys ?f (fmdom' m\<^sub>1 \ m\<^sub>2)" + using dom_res_addition_not_in by metis + also have "\ = fmmap_keys (\k' v'. v' + m\<^sub>1 $$! k') (fmdom' m\<^sub>1 \ m\<^sub>2)" + proof (intro fmap_ext) + fix k' + have "fmmap_keys ?f (fmdom' m\<^sub>1 \ m\<^sub>2) $$ k' = map_option (?f k') ((fmdom' m\<^sub>1 \ m\<^sub>2) $$ k')" + using fmlookup_fmmap_keys . + also from \m\<^sub>1 $$ k = None\ have "\ = fmmap_keys (\k' v'. v' + m\<^sub>1 $$! k') (fmdom' m\<^sub>1 \ m\<^sub>2) $$ k'" + by (cases "k' = k") (simp_all add: fmdom'_notI) + finally show "fmmap_keys ?f (fmdom' m\<^sub>1 \ m\<^sub>2) $$ k' = + fmmap_keys (\k' v'. v' + m\<^sub>1 $$! k') (fmdom' m\<^sub>1 \ m\<^sub>2) $$ k'" . + qed + finally show ?thesis . +qed + +lemma union_plus_addition_notin: (* TODO: Find nicer proofs for SMT calls. *) + assumes "m\<^sub>1 $$ k = None" + and "m\<^sub>2 $$ k = None" + shows "m\<^sub>1(k $$:= v) \\<^sub>+ m\<^sub>2 = (m\<^sub>1 \\<^sub>+ m\<^sub>2) ++\<^sub>f {k $$:= v}" +proof - + from \m\<^sub>2 $$ k = None\ have "(m\<^sub>1(k $$:= v)) \\<^sub>+ m\<^sub>2 = + fmdom' m\<^sub>2 \/ m\<^sub>1 ++\<^sub>f {k $$:= v} ++\<^sub>f fmdom' (m\<^sub>1(k $$:= v)) \/ m\<^sub>2 ++\<^sub>f (m\<^sub>1(k $$:= v) \\<^sub>+ m\<^sub>2)" + by (simp add: fmdom'_notI) + also from assms have "\ = + fmdom' m\<^sub>2 \/ m\<^sub>1 ++\<^sub>f {k $$:= v} ++\<^sub>f fmdom' m\<^sub>1 \/ m\<^sub>2 ++\<^sub>f (m\<^sub>1(k $$:= v) \\<^sub>+ m\<^sub>2)" + by (smt fmdom'_fmupd fmfilter_cong insert_iff option.distinct(1)) + also from assms have "\ = fmdom' m\<^sub>2 \/ m\<^sub>1 ++\<^sub>f {k $$:= v} ++\<^sub>f fmdom' m\<^sub>1 \/ m\<^sub>2 ++\<^sub>f (m\<^sub>1 \\<^sub>+ m\<^sub>2)" + using inter_plus_addition_notin by metis + also from assms have "\ = fmdom' m\<^sub>2 \/ m\<^sub>1 ++\<^sub>f fmdom' m\<^sub>1 \/ m\<^sub>2 ++\<^sub>f (m\<^sub>1 \\<^sub>+ m\<^sub>2) ++\<^sub>f {k $$:= v}" + using fmap_singleton_comm + by (smt fmadd_assoc fmfilter_fmmap_keys fmlookup_filter fmlookup_fmmap_keys) + finally show ?thesis . +qed + +end diff --git a/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy b/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy index 398ab6d..38e2403 100644 --- a/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy +++ b/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy @@ -3,6 +3,7 @@ section \ Implementation of the Ouroboros Praos protocol \ theory Ouroboros_Praos_Implementation imports Chi_Calculus.Typed_Basic_Transition_System + Finite_Map_Extras "HOL-Library.BNF_Corec" Complex_Main begin @@ -262,7 +263,7 @@ type_synonym stakeholder_id = nat type_synonym stake = nat -type_synonym stake_distr = "stakeholder_id \ stake" +type_synonym stake_distr = "(stakeholder_id, stake) fmap" paragraph \ Genesis block. \ @@ -310,7 +311,11 @@ text \ \ fun apply_transaction :: "transaction \ stake_distr \ stake_distr" where - "apply_transaction ((U\<^sub>i, U\<^sub>j, s), _) \ = \(U\<^sub>i \ the (\ U\<^sub>i) - s, U\<^sub>j \ the (\ U\<^sub>j) + s)" + "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))" paragraph \ Block. \ @@ -405,7 +410,7 @@ text \ \ abbreviation absolute_stake :: "stake_distr \ stake" (\s\<^sup>+'(_')\) where - "s\<^sup>+(\) \ \U\<^sub>j \ dom \. the (\ U\<^sub>j)" + "s\<^sup>+(\) \ \U\<^sub>j \ fmdom' \. \ $$! U\<^sub>j" text \ and the relative stake controlled by @{emph \a single\} stakeholder \U\<^sub>i\, taken as @@ -420,7 +425,7 @@ abbreviation where "\\<^sup>+(U\<^sub>i, \) \ let - s\<^sub>i = the (\ U\<^sub>i); + s\<^sub>i = \ $$! U\<^sub>i; s\<^sub>\

= s\<^sup>+(\) in s\<^sub>i / s\<^sub>\

" @@ -517,7 +522,7 @@ abbreviation verify_tx :: "transaction \ genesis \ bool" (vks, \\<^sub>0, _) = G; (_, _, vk\<^sub>i) = the (vks U\<^sub>i) \ \\U\<^sub>i\'s DSIG verification key\ in - \s\<^sub>i s\<^sub>j. \\<^sub>0 U\<^sub>i = Some s\<^sub>i \ \\<^sub>0 U\<^sub>j = Some s\<^sub>j \ s\<^sub>i \ s \ verify vk\<^sub>i txbody \" + \s\<^sub>i s\<^sub>j. \\<^sub>0 $$ U\<^sub>i = Some s\<^sub>i \ \\<^sub>0 $$ U\<^sub>j = Some s\<^sub>j \ s\<^sub>i \ s \ verify vk\<^sub>i txbody \" text \ and thus we can trivially verify whether a list of transactions is valid w.r.t. a genesis block: diff --git a/Isabelle/Ouroboros/ROOT b/Isabelle/Ouroboros/ROOT index d8f4937..4ad2434 100644 --- a/Isabelle/Ouroboros/ROOT +++ b/Isabelle/Ouroboros/ROOT @@ -4,6 +4,7 @@ session Ouroboros (ouroboros) = Chi_Calculus + description \Formalization of the Ouroboros protocol.\ theories Ouroboros_Praos_Implementation + Finite_Map_Extras document_files "root.tex" "root.bib" From 479e616bc39b249221cf567235408346d929b39e Mon Sep 17 00:00:00 2001 From: Javier Diaz Date: Mon, 5 Oct 2020 20:43:49 -0300 Subject: [PATCH 07/12] Change to use `Sublist.prefix` for `is_prefix_of` --- .../Ouroboros/Ouroboros_Praos_Implementation.thy | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy b/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy index 38e2403..4700298 100644 --- a/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy +++ b/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy @@ -5,6 +5,7 @@ theory Ouroboros_Praos_Implementation Chi_Calculus.Typed_Basic_Transition_System Finite_Map_Extras "HOL-Library.BNF_Corec" + "HOL-Library.Sublist" Complex_Main begin @@ -369,6 +370,13 @@ text \ type_synonym blockchain = "block list" +text \ + We let \\\<^sub>1 \ \\<^sub>2\ indicate that the blockchain \\\<^sub>1\ is a prefix of the blockchain \\\<^sub>2\: +\ + +abbreviation is_prefix_of :: "blockchain \ blockchain \ bool" (infix \\\ 50) where + "\\<^sub>1 \ \\<^sub>2 \ prefix \\<^sub>1 \\<^sub>2" + text \ We define a function to prune the last \m\ blocks in a blockchain \\\, denoted by \\\<^bsup>\m\<^esup>\ in the paper: @@ -384,13 +392,6 @@ text \ abbreviation prune_after :: "slot \ blockchain \ blockchain" where "prune_after sl \ \ takeWhile (\B. bl_slot B \ sl) \" -text \ - We let \\\<^sub>1 \ \\<^sub>2\ indicate that the blockchain \\\<^sub>1\ is a prefix of the blockchain \\\<^sub>2\: -\ - -abbreviation is_prefix_of :: "blockchain \ blockchain \ bool" (infixl \\\ 50) where - "\\<^sub>1 \ \\<^sub>2 \ \m. \\<^sub>2 \m = \\<^sub>1" - text \ And we can apply a blockchain \\\ to a stake distribution \\\ by sequentially applying all blocks in \\\ to \\\: From abcc5ae06e9849a7af0cb1ec1385356f325cfe4c Mon Sep 17 00:00:00 2001 From: Javier Diaz Date: Tue, 6 Oct 2020 13:03:16 -0300 Subject: [PATCH 08/12] Add sanity check for `apply_transaction` --- .../Ouroboros_Praos_Implementation.thy | 33 +++++++++++++++++++ 1 file changed, 33 insertions(+) diff --git a/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy b/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy index 4700298..88f8bb0 100644 --- a/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy +++ b/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy @@ -318,6 +318,39 @@ fun apply_transaction :: "transaction \ stake_distr \ st in \'(U\<^sub>j $$:= \' $$! U\<^sub>j + s))" +text \ + Applying a transaction with the same stakeholder as sender and receiver 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), \) \ = \" +proof (rule 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 + then have "?\' $$ U = Some (\ $$! U - s + s)" + by simp + also from True and assms have "\ = \ $$ U" + by auto + finally show ?thesis . + next + case False + then show ?thesis + by simp + qed + qed + then show "\ \\<^sub>f apply_transaction ((U\<^sub>i, U\<^sub>i, s), \) \" + unfolding fmsubset.rep_eq and map_le_def by simp +qed + paragraph \ Block. \ text \ From bc70b020738db8aae6fb86d0f11011dac37dfa34 Mon Sep 17 00:00:00 2001 From: Javier Diaz Date: Tue, 6 Oct 2020 19:13:16 -0300 Subject: [PATCH 09/12] Add sanity check for `apply_block` --- .../Ouroboros_Praos_Implementation.thy | 59 ++++++++++++++++++- 1 file changed, 58 insertions(+), 1 deletion(-) diff --git a/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy b/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy index 88f8bb0..13fb254 100644 --- a/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy +++ b/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy @@ -394,11 +394,68 @@ text \ abbreviation apply_block :: "block \ stake_distr \ stake_distr" where "apply_block B \ \ fold apply_transaction (bl_txs B) \" +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 + paragraph \ Blockchain. \ text \ A blockchain is simply a sequence of blocks. We do not record the genesis block explicitly as - part of the blockchain: + part of the blockchain: \ type_synonym blockchain = "block list" From b7c6d877208333cd89878073345676e3d70b81ea Mon Sep 17 00:00:00 2001 From: Javier Diaz Date: Wed, 7 Oct 2020 13:15:15 -0300 Subject: [PATCH 10/12] Add sanity check for `is_prefix_of` --- .../Ouroboros_Praos_Implementation.thy | 21 +++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy b/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy index 13fb254..799b9ff 100644 --- a/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy +++ b/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy @@ -467,6 +467,27 @@ text \ abbreviation is_prefix_of :: "blockchain \ blockchain \ bool" (infix \\\ 50) where "\\<^sub>1 \ \\<^sub>2 \ prefix \\<^sub>1 \\<^sub>2" +text \ + A prefix of a blockchain keeps all properties on its elements that hold for the original blockchain: +\ + +lemma prefix_invariancy: + assumes "\i \ {0..\<^sub>2}. P (\\<^sub>2 ! i)" + and "\\<^sub>1 \ \\<^sub>2" + shows "\i \ {0..\<^sub>1}. P (\\<^sub>1 ! i)" + using assms +proof (intro ballI) + fix i + assume "i \ {0..\<^sub>1}" + then have *: "i < length \\<^sub>1" + by simp + moreover from assms(2) obtain \\<^sub>3 where **: "\\<^sub>2 = \\<^sub>1 @ \\<^sub>3" .. + ultimately have "P (\\<^sub>2 ! i)" + using assms(1) by simp + with * and ** show "P (\\<^sub>1 ! i)" + by (simp add: nth_append) +qed + text \ We define a function to prune the last \m\ blocks in a blockchain \\\, denoted by \\\<^bsup>\m\<^esup>\ in the paper: From 7e76f3daa3adb9b080283b50f971f025999e0124 Mon Sep 17 00:00:00 2001 From: Javier Diaz Date: Wed, 7 Oct 2020 13:51:07 -0300 Subject: [PATCH 11/12] Add sanity checks for `prune_chain` --- .../Ouroboros_Praos_Implementation.thy | 21 ++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) diff --git a/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy b/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy index 799b9ff..38e7da8 100644 --- a/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy +++ b/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy @@ -497,7 +497,26 @@ abbreviation prune_chain :: "blockchain \ nat \ blockcha "\ \m \ take (length \ - m) \" text \ - and a function to prune the blocks in a blockchain which have slots greater than a given slot: + The \\\<^bsup>\m\<^esup>\ operator satisfies some simple laws: +\ + +lemma zero_blocks_chain_prunning_identity: + shows "\ \0 = \" + by simp + +lemma long_chain_prunning_emptiness: + assumes "m \ length \" + shows "\ \m = []" + using assms + by simp + +lemma append_prune_chain_drop_identity: + shows "\ \m @ drop (length \ - m) \ = \" + by simp + +text \ + Also, we define a function to prune the blocks in a blockchain which have slots greater than a + given slot: \ abbreviation prune_after :: "slot \ blockchain \ blockchain" where From 091199de81ca793c456ba4651e981a724485672e Mon Sep 17 00:00:00 2001 From: javierdiaz72 Date: Fri, 21 Jan 2022 13:23:44 -0300 Subject: [PATCH 12/12] Save WIP in preparation for repository split --- .../Chi_Calculus/Basic_Transition_System.thy | 88 +- Isabelle/Chi_Calculus/Core_Bisimilarities.thy | 214 +- .../Chi_Calculus/Proper_Transition_System.thy | 24 +- .../Typed_Basic_Transition_System.thy | 32 +- .../Typed_Proper_Transition_System.thy | 10 +- .../Ouroboros_Praos_Implementation.thy | 2828 +++++++++++++---- 6 files changed, 2438 insertions(+), 758 deletions(-) diff --git a/Isabelle/Chi_Calculus/Basic_Transition_System.thy b/Isabelle/Chi_Calculus/Basic_Transition_System.thy index 6d6e248..bc8d789 100644 --- a/Isabelle/Chi_Calculus/Basic_Transition_System.thy +++ b/Isabelle/Chi_Calculus/Basic_Transition_System.thy @@ -25,7 +25,7 @@ subsection \Residuals\ text \ There are two kinds of residuals in the basic transition system: acting residuals, written \\\\ q\ - where \\\ is an action, and scope opening residuals, written \\\ a\ Q a\ where \a\ is a channel + where \\\ is an action, and scope extruding residuals, written \\\ a\ Q a\ where \a\ is a channel variable. \ @@ -55,7 +55,7 @@ where lemmas basic_lift_intros = basic_residual.rel_intros lemmas acting_lift = basic_lift_intros(1) -lemmas opening_lift = basic_lift_intros(2) +lemmas extruding_lift = basic_lift_intros(2) lemmas basic_lift_cases = basic_residual.rel_cases text \ @@ -117,23 +117,23 @@ where "a \ x. P x \\<^sub>\\a \ x\ P x" | communication: "\ \ \ \; p \\<^sub>\\IO \\ p'; q \\<^sub>\\IO \\ q' \ \ p \ q \\<^sub>\\\\ p' \ q'" | - opening: + extruding: "\ a. P a \\<^sub>\\\ a\ P a" | acting_left: "p \\<^sub>\\\\ p' \ p \ q \\<^sub>\\\\ p' \ q" | acting_right: "q \\<^sub>\\\\ q' \ p \ q \\<^sub>\\\\ p \ q'" | - opening_left: + extruding_left: "p \\<^sub>\\\ a\ P a \ p \ q \\<^sub>\\\ a\ P a \ q" | - opening_right: + extruding_right: "q \\<^sub>\\\ a\ Q a \ p \ q \\<^sub>\\\ a\ p \ Q a" | scoped_acting: "\ p \\<^sub>\\\ a\ Q a; \a. Q a \\<^sub>\\\\ R a \ \ p \\<^sub>\\\\ \ a. R a" | - scoped_opening: + scoped_extruding: "\ p \\<^sub>\\\ a\ Q a; \a. Q a \\<^sub>\\\ b\ R a b \ \ p \\<^sub>\\\ b\ \ a. R a b" text \ - Note that \scoped_acting\ and\scoped_opening\ are the rules that perform closing. + Note that \scoped_acting\ and\scoped_extruding\ are the rules that perform closing. \ text \ @@ -153,24 +153,24 @@ notation basic.bisimilarity (infix \\\<^sub>\\ 50) subsection \Fundamental Properties of the Transition System\ text \ - Edsko's \texttt{Com} rule can be simulated using a combination of \opening_left\ (or, in the - right-to-left case, \opening_right\), \communication\, and \scoped_acting\. Reordering of openings - can be simulated using \scoped_opening\. + Edsko's \texttt{Com} rule can be simulated using a combination of \extruding_left\ (or, in the + right-to-left case, \extruding_right\), \communication\, and \scoped_acting\. Reordering of extrudings + can be simulated using \scoped_extruding\. \ text \ - An acting and an opening version of the \texttt{Scope} rule in Edsko's definition can be derived - by combining \opening\ with the closing rules. + An acting and an extruding version of the \texttt{Scope} rule in Edsko's definition can be derived + by combining \extruding\ with the closing rules. \ lemma acting_scope: "(\a. P a \\<^sub>\\\\ Q a) \ \ a. P a \\<^sub>\\\\ \ a. Q a" - using opening by (intro scoped_acting) -lemma opening_scope: "(\a. P a \\<^sub>\\\ b\ Q a b) \ \ a. P a \\<^sub>\\\ b\ \ a. Q a b" - using opening by (intro scoped_opening) + using extruding by (intro scoped_acting) +lemma extruding_scope: "(\a. P a \\<^sub>\\\ b\ Q a b) \ \ a. P a \\<^sub>\\\ b\ \ a. Q a b" + using extruding by (intro scoped_extruding) text \ No transitions are possible from~\\\. This is not as trivial as it might seem, because also - \scoped_acting\ and \scoped_opening\ have to be taken into account. + \scoped_acting\ and \scoped_extruding\ have to be taken into account. \ lemma no_basic_transitions_from_stop: "\ \ \\<^sub>\c" @@ -196,7 +196,7 @@ proof - case scoped_acting then show ?case by simp next - case scoped_opening + case scoped_extruding then show ?case by simp qed qed @@ -210,17 +210,17 @@ next case scoped_acting then show ?case by blast next - case scoped_opening + case scoped_extruding then show ?case by blast qed text \ - No opening transitions are possible from send and receive processes. + No extruding transitions are possible from send and receive processes. \ -lemma no_opening_transitions_from_send: "\ a \ x \\<^sub>\\\ b\ Q b" +lemma no_extruding_transitions_from_send: "\ a \ x \\<^sub>\\\ b\ Q b" using basic_transitions_from_send by blast -lemma no_opening_transitions_from_receive: "\ a \ x. P x \\<^sub>\\\ b\ Q b" +lemma no_extruding_transitions_from_receive: "\ a \ x. P x \\<^sub>\\\ b\ Q b" using basic_transitions_from_receive by blast subsection \Proof Tools\ @@ -291,7 +291,7 @@ proof - by smt qed -private lemma sim_scoped_opening_intro: +private lemma sim_scoped_extruding_intro: assumes with_new_channel: "\P Q. (\a. \ (P a) (Q a)) \ \ (\ a. P a) (\ a. Q a)" assumes step_1: @@ -326,9 +326,9 @@ proof - with that show ?thesis by blast qed from \t \\<^sub>\\\ a\ T\<^sub>1 a\ and \\a. T\<^sub>1 a \\<^sub>\\\ b\ T\<^sub>2 a b\ have "t \\<^sub>\\\ b\ \ a. T\<^sub>2 a b" - by (fact basic_transition.scoped_opening) + by (fact basic_transition.scoped_extruding) with \\a b. \ (S\<^sub>2 a b) (T\<^sub>2 a b)\ show ?thesis - using with_new_channel and opening_lift and rel_funI + using with_new_channel and extruding_lift and rel_funI by smt qed @@ -346,7 +346,7 @@ private method solve_sim_scoped uses with_new_channel = ( "\d\<^sub>2. _ \\<^sub>\d\<^sub>2 \ basic_lift _ (\\ b\ \ a. _ a b) d\<^sub>2" (cut) \ \ match premises in "s \\<^sub>\\\ a\ S\<^sub>1 a" for s and S\<^sub>1 \ \ match premises in prems [thin]: _ (multi) \ \ - intro sim_scoped_opening_intro [where s = s and S\<^sub>1 = S\<^sub>1], + intro sim_scoped_extruding_intro [where s = s and S\<^sub>1 = S\<^sub>1], simp add: with_new_channel, simp_all add: prems \ @@ -376,7 +376,7 @@ proof (standard, intro allI, intro impI) unfolding basic.bisimilarity_def using basic_transition.receiving and acting_lift by (metis (no_types, lifting)) - qed (simp_all add: no_opening_transitions_from_receive) + qed (simp_all add: no_extruding_transitions_from_receive) qed lemma basic_receive_preservation: "(\x. P x \\<^sub>\ Q x) \ a \ x. P x \\<^sub>\ a \ x. Q x" @@ -426,12 +426,12 @@ next by auto qed next - case opening - from opening.prems show ?case + case extruding + from extruding.prems show ?case proof cases case with_new_channel then show ?thesis - using basic_transition.opening and opening_lift and rel_funI + using basic_transition.extruding and extruding_lift and rel_funI by (metis (full_types)) qed next @@ -466,8 +466,8 @@ next by metis qed next - case (opening_left p P r t) - from opening_left.prems show ?case + case (extruding_left p P r t) + from extruding_left.prems show ?case proof cases case (without_new_channel q) from \p \\<^sub>\ q\ and \p \\<^sub>\\\ a\ P a\ @@ -475,25 +475,25 @@ next unfolding basic.bisimilarity_def by (force elim: basic.pre_bisimilarity.cases basic_lift_cases rel_funE) from \q \\<^sub>\\\ a\ Q a\ have "q \ r \\<^sub>\\\ a\ Q a \ r" - by (fact basic_transition.opening_left) + by (fact basic_transition.extruding_left) with \t = q \ r\ and \\a. P a \\<^sub>\ Q a\ show ?thesis using parallel_preservation_left_aux.without_new_channel and - opening_lift and + extruding_lift and rel_funI by smt qed next - case (opening_right r R p t) - from opening_right.prems show ?case + case (extruding_right r R p t) + from extruding_right.prems show ?case proof cases case (without_new_channel q) from \r \\<^sub>\\\ a\ R a\ have "q \ r \\<^sub>\\\ a\ q \ R a" - by (fact basic_transition.opening_right) + by (fact basic_transition.extruding_right) from \p \\<^sub>\ q\ have "\a. parallel_preservation_left_aux (p \ R a) (q \ R a)" by (fact parallel_preservation_left_aux.without_new_channel) with \t = q \ r\ and \q \ r \\<^sub>\\\ a\ q \ R a\ show ?thesis - using opening_lift and rel_funI + using extruding_lift and rel_funI by smt qed qed (blast elim: parallel_preservation_left_aux.cases)+ @@ -551,12 +551,12 @@ next from communication.prems show ?case by cases new_channel_preservation_aux_trivial_conveyance next - case opening - from opening.prems show ?case + case extruding + from extruding.prems show ?case proof cases case with_new_channel then show ?thesis - using basic_transition.opening and opening_lift + using basic_transition.extruding and extruding_lift by blast qed new_channel_preservation_aux_trivial_conveyance next @@ -568,12 +568,12 @@ next from acting_right.prems show ?case by cases new_channel_preservation_aux_trivial_conveyance next - case opening_left - from opening_left.prems show ?case + case extruding_left + from extruding_left.prems show ?case by cases new_channel_preservation_aux_trivial_conveyance next - case opening_right - from opening_right.prems show ?case + case extruding_right + from extruding_right.prems show ?case by cases new_channel_preservation_aux_trivial_conveyance qed qed diff --git a/Isabelle/Chi_Calculus/Core_Bisimilarities.thy b/Isabelle/Chi_Calculus/Core_Bisimilarities.thy index df75bc3..453917f 100644 --- a/Isabelle/Chi_Calculus/Core_Bisimilarities.thy +++ b/Isabelle/Chi_Calculus/Core_Bisimilarities.thy @@ -31,35 +31,35 @@ private method parallel_scope_extension_left_subaux_communication_conveyance = private method parallel_scope_extension_left_subaux_acting_left_conveyance = (parallel_scope_extension_left_subaux_trivial_conveyance intro: acting_left) -private method parallel_scope_extension_left_subaux_opening_left_conveyance = - (parallel_scope_extension_left_subaux_trivial_conveyance intro: opening_left) +private method parallel_scope_extension_left_subaux_extruding_left_conveyance = + (parallel_scope_extension_left_subaux_trivial_conveyance intro: extruding_left) -private lemma parallel_scope_extension_left_subaux_opening_conveyance: +private lemma parallel_scope_extension_left_subaux_extruding_conveyance: assumes initial_relation: "parallel_scope_extension_left_subaux q p t" assumes transition: "p \\<^sub>\\\ a\ P a" shows "\T. t \\<^sub>\\\ a\ T a \ (\a. parallel_scope_extension_left_subaux q (P a) (T a))" using transition and initial_relation and transition proof (induction (no_simp) p "\\ a\ P a" arbitrary: P t) - case (opening P P' t) - from opening.prems show ?case + case (extruding P P' t) + from extruding.prems show ?case proof cases case with_new_channel with \\\ a\ P a = \\ a\ P' a\ show ?thesis - using basic_transition.opening + using basic_transition.extruding by blast - qed parallel_scope_extension_left_subaux_opening_left_conveyance + qed parallel_scope_extension_left_subaux_extruding_left_conveyance next - case opening_left - from opening_left.prems show ?case - by cases parallel_scope_extension_left_subaux_opening_left_conveyance + case extruding_left + from extruding_left.prems show ?case + by cases parallel_scope_extension_left_subaux_extruding_left_conveyance next - case opening_right - from opening_right.prems show ?case - by cases parallel_scope_extension_left_subaux_opening_left_conveyance + case extruding_right + from extruding_right.prems show ?case + by cases parallel_scope_extension_left_subaux_extruding_left_conveyance next - case (scoped_opening p P\<^sub>1 P\<^sub>2 P' t) + case (scoped_extruding p P\<^sub>1 P\<^sub>2 P' t) from - scoped_opening.IH(1) and + scoped_extruding.IH(1) and \parallel_scope_extension_left_subaux q p t\ and \p \\<^sub>\\\ a\ P\<^sub>1 a\ obtain T\<^sub>1 where @@ -71,7 +71,7 @@ next "\a b. parallel_scope_extension_left_subaux q (P\<^sub>2 a b) (T\<^sub>2 a b)" proof - from - scoped_opening.IH(2) and + scoped_extruding.IH(2) and \\a. parallel_scope_extension_left_subaux q (P\<^sub>1 a) (T\<^sub>1 a)\ and \\a. P\<^sub>1 a \\<^sub>\\\ b\ P\<^sub>2 a b\ have " @@ -83,7 +83,7 @@ next with that show ?thesis by blast qed from \t \\<^sub>\\\ a\ T\<^sub>1 a\ and \\a. T\<^sub>1 a \\<^sub>\\\ b\ T\<^sub>2 a b\ have "t \\<^sub>\\\ b\ \ a. T\<^sub>2 a b" - by (fact basic_transition.scoped_opening) + by (fact basic_transition.scoped_extruding) with \\\ b\ \ a. P\<^sub>2 a b = \\ b\ P' b\ and \\a b. parallel_scope_extension_left_subaux q (P\<^sub>2 a b) (T\<^sub>2 a b)\ @@ -161,7 +161,7 @@ next obtain T\<^sub>1 where "t \\<^sub>\\\ a\ T\<^sub>1 a" and "\a. parallel_scope_extension_left_subaux q (P\<^sub>1 a) (T\<^sub>1 a)" - using parallel_scope_extension_left_subaux_opening_conveyance + using parallel_scope_extension_left_subaux_extruding_conveyance by blast obtain T\<^sub>2 where "\a. T\<^sub>1 a \\<^sub>\\\\ T\<^sub>2 a" and @@ -192,8 +192,8 @@ next using parallel_scope_extension_left_aux.without_new_channel_ltr and acting_lift by auto next - case (opening S t) - from opening.prems show ?case + case (extruding S t) + from extruding.prems show ?case proof cases case (without_new_channel_rtl q p) from \parallel_scope_extension_left_subaux q p (\ a. S a)\ show ?thesis @@ -201,17 +201,17 @@ next case with_new_channel with \t = p \ q\ show ?thesis using - basic_transition.opening and - opening_left and + basic_transition.extruding and + extruding_left and parallel_scope_extension_left_aux.without_new_channel_rtl and - opening_lift and + extruding_lift and rel_funI by (metis (mono_tags, lifting)) qed next case with_new_channel then show ?thesis - using basic_transition.opening and opening_lift and rel_funI + using basic_transition.extruding and extruding_lift and rel_funI by metis qed next @@ -248,7 +248,7 @@ next obtain T\<^sub>1 where "t \\<^sub>\\\ a\ T\<^sub>1 a" and "\a. parallel_scope_extension_left_subaux q (P\<^sub>1 a) (T\<^sub>1 a)" - using parallel_scope_extension_left_subaux_opening_conveyance + using parallel_scope_extension_left_subaux_extruding_conveyance by blast obtain T\<^sub>2 where "\a. T\<^sub>1 a \\<^sub>\\\\ T\<^sub>2 a" and @@ -302,30 +302,30 @@ next by metis qed then show ?case - using parallel_scope_extension_left_aux.without_new_channel_ltr and opening_lift + using parallel_scope_extension_left_aux.without_new_channel_ltr and extruding_lift by auto next - case (opening_left p P q t) - from opening_left.prems have "parallel_scope_extension_left_subaux q p t" + case (extruding_left p P q t) + from extruding_left.prems have "parallel_scope_extension_left_subaux q p t" by (fact parallel_scope_extension_left_aux_without_new_channel_normalization) - with opening_left.hyps show ?case + with extruding_left.hyps show ?case using - parallel_scope_extension_left_subaux_opening_conveyance and + parallel_scope_extension_left_subaux_extruding_conveyance and parallel_scope_extension_left_aux.without_new_channel_ltr and - opening_lift and + extruding_lift and rel_funI by smt next - case (opening_right q Q p t) - from opening_right.prems have "parallel_scope_extension_left_subaux q p t" + case (extruding_right q Q p t) + from extruding_right.prems have "parallel_scope_extension_left_subaux q p t" by (fact parallel_scope_extension_left_aux_without_new_channel_normalization) - from this and opening_right.hyps + from this and extruding_right.hyps have "\T. t \\<^sub>\\\ a\ T a \ (\a. parallel_scope_extension_left_subaux (Q a) p (T a))" proof induction case without_new_channel then show ?case using - basic_transition.opening_right and + basic_transition.extruding_right and parallel_scope_extension_left_subaux.without_new_channel by blast next @@ -337,13 +337,13 @@ next \T'. \a. T a \\<^sub>\\\ b\ T' a b \ (\b. parallel_scope_extension_left_subaux (Q b) (P a) (T' a b))" by (fact choice) then show ?case - using opening_scope and parallel_scope_extension_left_subaux.with_new_channel + using extruding_scope and parallel_scope_extension_left_subaux.with_new_channel by metis qed then show ?case using parallel_scope_extension_left_aux.without_new_channel_ltr and - opening_lift and + extruding_lift and rel_funI by smt qed (blast elim: @@ -364,14 +364,14 @@ proof (standard, intro allI, intro impI) assume "\ b. \ a. P a b \\<^sub>\c" then have "\ a. \ b. P a b \\<^sub>\c" proof (induction "\ b. \ a. P a b" c) - case opening - show ?case using basic_transition.opening by (intro opening_scope) + case extruding + show ?case using basic_transition.extruding by (intro extruding_scope) next case scoped_acting then show ?case by (simp add: basic_transition.scoped_acting) next - case scoped_opening - then show ?case by (simp add: basic_transition.scoped_opening) + case scoped_extruding + then show ?case by (simp add: basic_transition.scoped_extruding) qed show "\d. \ a. \ b. P a b \\<^sub>\d \ basic_lift (\p q. p \\<^sub>\ q \ q \\<^sub>\ p) c d" proof - @@ -406,7 +406,7 @@ where private method parallel_neutrality_left_aux_trivial_conveyance = (blast intro: acting_right - opening_right + extruding_right parallel_neutrality_left_aux.without_new_channel_rtl basic_lift_intros ) @@ -438,12 +438,12 @@ next by (simp add: no_basic_transitions_from_stop) qed parallel_neutrality_left_aux_trivial_conveyance next - case opening - from opening.prems show ?case + case extruding + from extruding.prems show ?case proof cases case with_new_channel then show ?thesis - using basic_transition.opening and opening_lift and rel_funI + using basic_transition.extruding and extruding_lift and rel_funI by metis qed parallel_neutrality_left_aux_trivial_conveyance next @@ -464,22 +464,22 @@ next by auto qed parallel_neutrality_left_aux_trivial_conveyance next - case opening_left - from opening_left.prems show ?case + case extruding_left + from extruding_left.prems show ?case proof cases case without_new_channel_ltr - with opening_left.hyps show ?thesis + with extruding_left.hyps show ?thesis by (simp add: no_basic_transitions_from_stop) qed parallel_neutrality_left_aux_trivial_conveyance next - case opening_right - from opening_right.prems show ?case + case extruding_right + from extruding_right.prems show ?case proof cases case without_new_channel_ltr - with opening_right.hyps show ?thesis + with extruding_right.hyps show ?thesis using parallel_neutrality_left_aux.without_new_channel_ltr and - opening_lift and + extruding_lift and rel_funI by smt qed parallel_neutrality_left_aux_trivial_conveyance @@ -503,45 +503,45 @@ where (\a. nested_parallel_commutativity_subaux r (U a) (T a)) \ nested_parallel_commutativity_subaux r (\ a. U a) (\ a. T a)" -private lemma nested_parallel_commutativity_subaux_opening_conveyance: +private lemma nested_parallel_commutativity_subaux_extruding_conveyance: assumes initial_relation: "nested_parallel_commutativity_subaux r u t" assumes transition: "u \\<^sub>\\\ a\ U a" shows "\T. t \\<^sub>\\\ a\ T a \ (\a. nested_parallel_commutativity_subaux r (U a) (T a))" using transition and initial_relation proof (induction u "\\ a\ U a" arbitrary: U t) - case (opening U t) - from opening.prems show ?case + case (extruding U t) + from extruding.prems show ?case proof cases case with_new_channel then show ?thesis - using basic_transition.opening + using basic_transition.extruding by blast qed next - case (opening_left p P q t) - from opening_left.prems show ?case + case (extruding_left p P q t) + from extruding_left.prems show ?case proof cases case without_new_channel with \p \\<^sub>\\\ a\ P a\ show ?thesis using - basic_transition.opening_left and + basic_transition.extruding_left and nested_parallel_commutativity_subaux.without_new_channel by blast qed next - case (opening_right q Q p t) - from opening_right.prems show ?case + case (extruding_right q Q p t) + from extruding_right.prems show ?case proof cases case without_new_channel with \q \\<^sub>\\\ a\ Q a\ show ?thesis using - basic_transition.opening_right and + basic_transition.extruding_right and nested_parallel_commutativity_subaux.without_new_channel by blast qed next - case (scoped_opening u U\<^sub>1 U\<^sub>2 t) - from scoped_opening.hyps(2) and \nested_parallel_commutativity_subaux r u t\ + case (scoped_extruding u U\<^sub>1 U\<^sub>2 t) + from scoped_extruding.hyps(2) and \nested_parallel_commutativity_subaux r u t\ obtain T\<^sub>1 where "t \\<^sub>\\\ a\ T\<^sub>1 a" and "\a. nested_parallel_commutativity_subaux r (U\<^sub>1 a) (T\<^sub>1 a)" @@ -550,7 +550,7 @@ next "\a. T\<^sub>1 a \\<^sub>\\\ b\ T\<^sub>2 a b" and "\a b. nested_parallel_commutativity_subaux r (U\<^sub>2 a b) (T\<^sub>2 a b)" proof - - from scoped_opening.hyps(4) and \\a. nested_parallel_commutativity_subaux r (U\<^sub>1 a) (T\<^sub>1 a)\ + from scoped_extruding.hyps(4) and \\a. nested_parallel_commutativity_subaux r (U\<^sub>1 a) (T\<^sub>1 a)\ have " \a. \V. T\<^sub>1 a \\<^sub>\\\ b\ V b \ (\b. nested_parallel_commutativity_subaux r (U\<^sub>2 a b) (V b))" by blast @@ -560,7 +560,7 @@ next with that show ?thesis by blast qed from \t \\<^sub>\\\ a\ T\<^sub>1 a\ and \\a. T\<^sub>1 a \\<^sub>\\\ b\ T\<^sub>2 a b\ have "t \\<^sub>\\\ b\ \ a. T\<^sub>2 a b" - by (fact basic_transition.scoped_opening) + by (fact basic_transition.scoped_extruding) with \\a b. nested_parallel_commutativity_subaux r (U\<^sub>2 a b) (T\<^sub>2 a b)\ show ?case using nested_parallel_commutativity_subaux.with_new_channel by metis @@ -644,7 +644,7 @@ next obtain T\<^sub>1 where "t \\<^sub>\\\ a\ T\<^sub>1 a" and "\a. nested_parallel_commutativity_subaux r (U\<^sub>1 a) (T\<^sub>1 a)" - using nested_parallel_commutativity_subaux_opening_conveyance + using nested_parallel_commutativity_subaux_extruding_conveyance by blast obtain T\<^sub>2 where "\a. T\<^sub>1 a \\<^sub>\\\\ T\<^sub>2 a" and @@ -673,8 +673,8 @@ next acting_lift by auto next - case (opening S t) - from opening.prems show ?case + case (extruding S t) + from extruding.prems show ?case proof cases case (without_new_channel_rtl r u) from \nested_parallel_commutativity_subaux r u (\ a. S a)\ show ?thesis @@ -682,17 +682,17 @@ next case with_new_channel with \t = u \ r\ show ?thesis using - basic_transition.opening and - opening_left and + basic_transition.extruding and + extruding_left and nested_parallel_commutativity_aux.without_new_channel_rtl and - opening_lift and + extruding_lift and rel_funI by (metis (mono_tags, lifting)) qed next case with_new_channel then show ?thesis - using basic_transition.opening and opening_lift + using basic_transition.extruding and extruding_lift by blast qed next @@ -741,7 +741,7 @@ next obtain T\<^sub>1 where "t \\<^sub>\\\ a\ T\<^sub>1 a" and "\a. nested_parallel_commutativity_subaux r (U\<^sub>1 a) (T\<^sub>1 a)" - using nested_parallel_commutativity_subaux_opening_conveyance + using nested_parallel_commutativity_subaux_extruding_conveyance by blast obtain T\<^sub>2 where "\a. T\<^sub>1 a \\<^sub>\\\\ T\<^sub>2 a" and @@ -801,28 +801,28 @@ next acting_lift by auto next - case (opening_left u U r t) - from opening_left.prems have "nested_parallel_commutativity_subaux r u t" + case (extruding_left u U r t) + from extruding_left.prems have "nested_parallel_commutativity_subaux r u t" by (fact nested_parallel_commutativity_aux_without_new_channel_normalization) - with opening_left.hyps show ?case + with extruding_left.hyps show ?case using - nested_parallel_commutativity_subaux_opening_conveyance and + nested_parallel_commutativity_subaux_extruding_conveyance and nested_parallel_commutativity_aux.without_new_channel_ltr and - opening_lift and + extruding_lift and rel_funI by smt next - case (opening_right r R u t) - from opening_right.prems have "nested_parallel_commutativity_subaux r u t" + case (extruding_right r R u t) + from extruding_right.prems have "nested_parallel_commutativity_subaux r u t" by (fact nested_parallel_commutativity_aux_without_new_channel_normalization) - from this and opening_right.hyps + from this and extruding_right.hyps have "\T. t \\<^sub>\\\ a\ T a \ (\a. nested_parallel_commutativity_subaux (R a) u (T a))" proof induction case without_new_channel then show ?case using - basic_transition.opening_right and - basic_transition.opening_left and + basic_transition.extruding_right and + basic_transition.extruding_left and nested_parallel_commutativity_subaux.without_new_channel by blast next @@ -835,13 +835,13 @@ next T a \\<^sub>\\\ b\ T' a b \ (\b. nested_parallel_commutativity_subaux (R b) (U a) (T' a b))" by (fact choice) then show ?case - using opening_scope and nested_parallel_commutativity_subaux.with_new_channel + using extruding_scope and nested_parallel_commutativity_subaux.with_new_channel by metis qed then show ?case using nested_parallel_commutativity_aux.without_new_channel_ltr and - opening_lift and + extruding_lift and rel_funI by smt next @@ -913,25 +913,25 @@ proof (standard, intro allI, intro impI) with \\ b. a \ x. P x b \\<^sub>\c\ show ?thesis by blast qed next - case (output_without_opening a x q) + case (output_without_extruding a x q) then show ?thesis by (blast elim: basic_transitions_from_receive) next - case output_with_opening + case output_with_extruding then show ?thesis - using no_opening_transitions_from_receive + using no_extruding_transitions_from_receive by simp qed qed -private lemma opening_transitions_from_new_channel_receive: +private lemma extruding_transitions_from_new_channel_receive: "\ b. a \ x. P x b \\<^sub>\\\ b\ Q b \ Q b = a \ x . P x b" proof (induction "\ b. a \ x. P x b" "\\ b\ Q b" arbitrary: Q rule: basic_transition.induct) - case opening + case extruding show ?case by (fact refl) next - case scoped_opening - then show ?case using no_opening_transitions_from_receive by metis + case scoped_extruding + then show ?case using no_extruding_transitions_from_receive by metis qed private lemma pre_receive_scope_extension_rtl: "\ b. a \ x. P x b \\<^sub>\ a \ x. \ b. P x b" @@ -945,7 +945,7 @@ proof (standard, intro allI, intro impI) proof cases case (scoped_acting Q R) from \\ b. a \ x. P x b \\<^sub>\\\ b\ Q b\ have "\b. Q b = a \ x . P x b" - by (fact opening_transitions_from_new_channel_receive) + by (fact extruding_transitions_from_new_channel_receive) with \\b. Q b \\<^sub>\\basic_action_of \\ R b\ obtain x where "basic_action_of \ = a \ x" and "\b. R b = P x b" using @@ -972,30 +972,30 @@ proof (standard, intro allI, intro impI) qed qed next - case (output_without_opening a' x r) + case (output_without_extruding a' x r) from \\ b. a \ x. P x b \\<^sub>\\a' \ x\ r\ show ?thesis proof cases case (scoped_acting Q R) from \\ b. a \ x. P x b \\<^sub>\\\ b\ Q b\ have "\b. Q b = a \ x. P x b" - by (fact opening_transitions_from_new_channel_receive) + by (fact extruding_transitions_from_new_channel_receive) with \\b. Q b \\<^sub>\\a' \ x\ R b\ show ?thesis by (auto elim: basic_transitions_from_receive) qed next - case (output_with_opening Q a' K) + case (output_with_extruding Q a' K) from \\ b. a \ x. P x b \\<^sub>\\\ b\ Q b\ have "\b. Q b = a \ x. P x b" - by (fact opening_transitions_from_new_channel_receive) + by (fact extruding_transitions_from_new_channel_receive) with \\b. Q b \\<^sub>\\a' \ K b\ have "a \ x. P x undefined \\<^sub>\\a' \ K undefined" by simp then show ?thesis proof cases - case (output_without_opening x q) + case (output_without_extruding x q) then show ?thesis by (blast elim: basic_transitions_from_receive) next - case output_with_opening + case output_with_extruding then show ?thesis - using no_opening_transitions_from_receive + using no_extruding_transitions_from_receive by simp qed qed @@ -1012,16 +1012,16 @@ end context begin -private lemma opening_transitions_from_new_channel_stop: "\ a. \ \\<^sub>\\\ a\ P a \ P a = \" +private lemma extruding_transitions_from_new_channel_stop: "\ a. \ \\<^sub>\\\ a\ P a \ P a = \" proof - fix P and a assume "\ a. \ \\<^sub>\\\ a\ P a" then show "P a = \" proof (induction "\ a. \" "\\ a\ P a" arbitrary: P) - case opening + case extruding show ?case by (fact refl) next - case scoped_opening + case scoped_extruding then show ?case using no_basic_transitions_from_stop by metis qed qed @@ -1034,7 +1034,7 @@ proof proof cases case (scoped_acting Q\<^sub>1 Q\<^sub>2) from \\ a. \ \\<^sub>\\\ a\ Q\<^sub>1 a\ have "\a. Q\<^sub>1 a = \" - by (fact opening_transitions_from_new_channel_stop) + by (fact extruding_transitions_from_new_channel_stop) with \\a. Q\<^sub>1 a \\<^sub>\\\\ Q\<^sub>2 a\ show ?thesis by (simp add: no_basic_transitions_from_stop) qed @@ -1046,9 +1046,9 @@ proof assume "\ a. \ \\<^sub>\c" then show False proof cases - case (output_with_opening P a K) + case (output_with_extruding P a K) from \\ b. \ \\<^sub>\\\ b\ P b\ have "\b. P b = \" - by (fact opening_transitions_from_new_channel_stop) + by (fact extruding_transitions_from_new_channel_stop) with \\b. P b \\<^sub>\\a \ K b\ show ?thesis by (simp add: no_proper_transitions_from_stop) qed (simp_all add: no_acting_transitions_from_new_channel_stop) diff --git a/Isabelle/Chi_Calculus/Proper_Transition_System.thy b/Isabelle/Chi_Calculus/Proper_Transition_System.thy index 99cba9b..f4c55c1 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_Basic_Transition_System.thy b/Isabelle/Chi_Calculus/Typed_Basic_Transition_System.thy index bea04e1..6ca5fe9 100644 --- a/Isabelle/Chi_Calculus/Typed_Basic_Transition_System.thy +++ b/Isabelle/Chi_Calculus/Typed_Basic_Transition_System.thy @@ -19,18 +19,18 @@ abbreviation where "\ \\ \ \ untyped_channel \ \ untyped_value \" -abbreviation typed_opening :: "('a channel \ 'p) \ 'p basic_residual" where - "typed_opening \ \ \\ a\ \ (typed_channel a)" +abbreviation typed_extruding :: "('a channel \ 'p) \ 'p basic_residual" where + "typed_extruding \ \ \\ a\ \ (typed_channel a)" syntax - "_typed_opening" :: "pttrn \ process \ 'p basic_residual" + "_typed_extruding" :: "pttrn \ process \ 'p basic_residual" (\\\\_\ _\ [0, 51] 51) translations - "\\\\\ \" \ "CONST typed_opening (\\. \)" + "\\\\\ \" \ "CONST typed_extruding (\\. \)" print_translation \ [ Syntax_Trans.preserve_binder_abs_tr' - @{const_syntax typed_opening} - @{syntax_const "_typed_opening"} + @{const_syntax typed_extruding} + @{syntax_const "_typed_extruding"} ] \ (* FIXME: @@ -48,18 +48,18 @@ lemma typed_sending: "\ \\ \ \\<^sub>\ lemma typed_receiving: "\ \\ \. \ \ \\<^sub>\\\ \\ \\ \ \" using receiving and typed_untyped_value by metis -lemma typed_opening: "\\\. \ \ \\<^sub>\\\\\\ \ \" - by (fact opening) -lemma typed_opening_left: "p \\<^sub>\\\\\\ \ \ \ p \ q \\<^sub>\\\\\\ \ \ \ q" - by (fact opening_left) -lemma typed_opening_right: "q \\<^sub>\\\\\\ \ \ \ p \ q \\<^sub>\\\\\\ p \ \ \" - by (fact opening_right) +lemma typed_extruding: "\\\. \ \ \\<^sub>\\\\\\ \ \" + by (fact extruding) +lemma typed_extruding_left: "p \\<^sub>\\\\\\ \ \ \ p \ q \\<^sub>\\\\\\ \ \ \ q" + by (fact extruding_left) +lemma typed_extruding_right: "q \\<^sub>\\\\\\ \ \ \ p \ q \\<^sub>\\\\\\ p \ \ \" + by (fact extruding_right) lemma typed_scoped_acting: "\p \\<^sub>\\\\\\ \ \; \\. \ \ \\<^sub>\\\\ \ \\ \ p \\<^sub>\\\\ \\\. \ \" by (simp add: scoped_acting) -lemma typed_scoped_opening: "\p \\<^sub>\\\\\\ \ \; \\. \ \ \\<^sub>\\\\\\ \ \ \\ \ p \\<^sub>\\\\\\ \\\. \ \ \" - by (simp add: scoped_opening) +lemma typed_scoped_extruding: "\p \\<^sub>\\\\\\ \ \; \\. \ \ \\<^sub>\\\\\\ \ \ \\ \ p \\<^sub>\\\\\\ \\\. \ \ \" + by (simp add: scoped_extruding) -lemma typed_opening_scope: "(\\. \ \ \\<^sub>\\\\\\ \ \ \) \ \\\. \ \ \\<^sub>\\\\\\ \\\. \ \ \" - by (simp add: opening_scope) +lemma typed_extruding_scope: "(\\. \ \ \\<^sub>\\\\\\ \ \ \) \ \\\. \ \ \\<^sub>\\\\\\ \\\. \ \ \" + by (simp add: extruding_scope) end 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 38e7da8..20caf4e 100644 --- a/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy +++ b/Isabelle/Ouroboros/Ouroboros_Praos_Implementation.thy @@ -2,287 +2,317 @@ section \ Implementation of the Ouroboros Praos protocol \ theory Ouroboros_Praos_Implementation imports - Chi_Calculus.Typed_Basic_Transition_System Finite_Map_Extras "HOL-Library.BNF_Corec" "HOL-Library.Sublist" + Chi_Calculus.Typed_Basic_Transition_System Complex_Main begin -subsection \ Introduction \ - text \ In this section we present an implementation of the Ouroboros Praos protocol as defined in @{cite praos}. Since a security analysis of the protocol is out of scope, we do not model the environment \\\, the adversary \\\, etc. However, we retain the use of the Universal - Composability (UC) framework for the sake of design modularity. + Composability (UC) framework for the sake of design modularity. It's important to mention that in + the paper the protocol is described in the so-called `hybrid model', in which the protocol assumes + the availability of idealized versions of some cryptographic primitives, called `ideal + functionalities', that can be invoked by the protocol participants, much like sub-routines. These + ideal functionalities can be replaced later with concrete implementations without affecting the + security properties of the protocol. Thus, we model these ideal functionalities as locale's. \ +no_notation Sublist.parallel (infixl "\" 50) + subsection \ Preliminaries \ text \ - We let \v \\ w\ denote concatenation of ``strings'' (i.e. arbitrary values): + We let \v \\ w\ denote concatenation of `strings' (i.e. arbitrary values): \ -abbreviation concat :: "'a \ 'b \ 'a \ 'b" (infixr \\\\ 65) where - "v \\ w \ (v, w)" +consts concat :: "'a \ 'b \ 'a" (infixl \\\\ 65) + +subsection \ Public-key cryptography \ text \ - Public-key cryptography depends on a pair of a secret key and a verification key: + The Praos protocol is based on a public-key cryptographic system. We define a locale with two + parameters: a key generation function and a function to derive the verification key from the + secret key. Also, we state an assumption that establishes a relationship between the two + parameters, namely that if we generate \sk\ and \vk\ using the key generation function then it + holds that \vk\ is the verification key of \sk\. Furthermore, this locale is parametrized with the + type of the security parameter: \ -typedecl secret_key - -typedecl verification_key +locale keys = + fixes generate :: "'security_parameter \ 'vkey \ 'skey" + and verification_key_of :: "'skey \ 'vkey" + assumes correctness: "(vk, sk) = generate \ \ verification_key_of sk = vk" +subsection \ Cryptographic hash functions \ text \ - such that it is possible to derive the verification key from the secret key: + The paper uses the random oracle model (ROM). In the ROM a hash function is modeled as a random + oracle, which is basically a magical black box that implements a truly random function. As the ROM + is used just for the purposes of the security proof, we model a collision-free cryptographic hash + functions instead. To do so, we define a locale which is parametric in the type \'a\ of values to + be hashed and in the type \'hash\ of hash values. Now, theoretically, cryptographic hash functions + have certain properties, e.g. they are one-way functions, meaning that they are difficult to + invert by an efficient adversary. But, the terms `difficult' and `efficient' are probabilistic in + nature, so we cannot enforce these properties in the code: \ -consts verification_key_of :: "secret_key \ verification_key" +locale hashable = + fixes \ :: "'a \ 'hash" + assumes collision_resistance: "inj \" -subsubsection \ The Semi-Synchronous model \ +subsection \ Verifiable random functions (VRFs) \ text \ - \label{sec:semi-sync-model-ref} - In the paper, a semi-synchronous model with an upper bound \\\ in message delay is used. Regarding - \\\, we stress that the protocol is oblivious of \\\ and this bound is only used in the security - analysis. Hence from the protocol's point of view the network is no better than an eventual - delivery network (without a concrete bound), which can be modeled using our process calculus using - for example a reliable broadcasting server process. - Regarding synchrony, we simply assume that an external ``clock process'' signals each stakeholder - when a round (i.e. slot) ends, and that messages sent in one round are received at the onset of - the next round. + A VRF is basically a pseudorandom function such that everyone can check that the values of the + function were computed correctly. In particular, in the Praos protocol, the stakeholders use a VRF + for executing the private lottery to check whether they're slot leaders for a particular slot. + Also, stakeholders use a VRF to include a pseudorandom value in each block they produce. \ -paragraph \ Time and slots. \ - text \ - We define the concepts of epoch and slot. As defined in the paper, slots and epochs begin at 1: + We model the output of a VRF as a pair comprised by a pseudorandom value and a proof that the + value was computed correctly: \ - -type_synonym epoch = nat - -type_synonym slot = nat - -abbreviation first_slot :: slot where - "first_slot \ 1" - -abbreviation first_epoch :: epoch where - "first_epoch \ 1" - -paragraph \ The Delayed Diffuse Functionality. \ +type_synonym ('vrf\<^sub>y, 'vrf\<^sub>\) vrf\<^sub>o = "'vrf\<^sub>y \ 'vrf\<^sub>\" text \ - We do not model the network as a separate ideal functionality \textsf{DDiffuse}\\<^sub>\\ but rely on - our process calculus features for communication. In particular, a single channel is used both to - read the received messages from a stakeholder's ``incoming string'' (or ``mailbox'') and to - ``diffuse'' a message. Also, the restriction that a stakeholder is allowed to diffuse once in a - round is explicitly enforced by the stakeholder process implementation, see Section - \ref{sec:sh-process-ref}. + We define a locale with four parameters: + \<^item> A function that, given a secret key and an input value of an arbitrary type, evaluates the VRF + and produces a VRF output. + \<^item> A function that, given a verification key, an input value, and a VRF output, verifies that the + VRF value was produced correctly. + \<^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: + \<^descr> Uníqueness: This establishes that for any input \x\ there exists a unique value \y\ that can + be proved to be valid. That is, if we can verify the correctness of both \y\ and \y'\ for \x\ + then \y\ and \y'\ must be equal. + \<^descr> Provability: This establishes that the value produced by evaluating the VRF can be proved to + 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 + standard VRFs, since it guarantees that VRF values cannot be predicted even if the adversary is + allowed to generate the secret and verification keys. Naturally, for this work, we stick to the + regular definition of a VRF: \ -paragraph \ Random Oracle. \ +locale vrf = keys generate verification_key_of + for generate :: "'security_parameter \ 'vkey \ 'skey" + and verification_key_of :: "'skey \ 'vkey" + + fixes evaluate :: "'skey \ 'a \ ('vrf\<^sub>y, 'vrf\<^sub>\) vrf\<^sub>o" + and verify :: "'vkey \ 'a \ ('vrf\<^sub>y, 'vrf\<^sub>\) vrf\<^sub>o \ bool" + and value_size :: nat (\l\<^sub>V\<^sub>R\<^sub>F\) + and value_to_real :: "'vrf\<^sub>y \ real" + assumes value_size_positivity: "value_size > 0" + and uniqueness: "verify vk x (y, \) = verify vk x (y', \') \ y = y'" + and provability: "vk = verification_key_of sk \ verify vk x (evaluate sk x)" text \ - We will simply assume that we can compute the hash value of any value: + 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: \ -typedecl hash \ \ Hash values (i.e. $\{0,1\}^w$ in the paper) \ - -axiomatization -where - hash_finite: "OFCLASS(hash, finite_class)" -and - hash_equal: "OFCLASS(hash, equal_class)" - -instance hash :: finite - by (rule hash_finite) - -instance hash :: equal - by (rule hash_equal) +datatype vrf_query_type = TEST | NONCE -axiomatization - \ :: "'a \ hash" \ \ A collision-resistant hash function \ -where - hash_inj: "inj \" +subsection \ Digital signatures \ text \ - with no way of recovering @{typ 'a} from @{type hash}. + In the paper, digital signature schemes are modeled as ideal functionalities. Moreover, the paper + describes two digital signature schemes: A regular digital signature scheme (denoted by + \\\$_{\mathsf{DSIG}}$) which is used to sign transactions, and a digital signature scheme (denoted + by \\\$_{\mathsf{KES}}$) which is used to sign blocks and has the capability of allowing the + signing key to evolve, in such a way that the adversary cannot forge past signatures. For our + purposes, though, we model a single, ordinary digital signature scheme for signing both + transactions and blocks. To do so, we define a locale with two parameters: + \<^item> A function that, given a secret key and a message of an arbitrary type, produces a signature for + the message. + \<^item> A function that, given a verification key, a message and a signature, verifies that the + signature is a legitimate signature for the message. + + + Also, we only require a provability property, stating that the signature produced by signing a + message can be proved to be valid, provided that the verification key used to check the validity + of the signature is derived from the secret key used to sign the message: \ -subsection \ The Full Protocol \ +locale digital_signature_scheme = keys generate verification_key_of + for generate :: "'security_parameter \ 'vkey \ 'skey" + and verification_key_of :: "'skey \ 'vkey" + + fixes sign :: "'skey \ 'm \ 'sig" + and verify :: "'vkey \ 'm \ 'sig \ bool" + assumes provability: "vk = verification_key_of sk \ verify vk x (sign sk x)" -text \ - We only implement the protocol that handles the dynamic case (i.e. $\pi_{\mathrm{DPoS}}$), since - the static case is used as the base case in the ``inductive'' security proof. -\ - -subsubsection \ Protocol parameters \ +subsection \ Protocol parameters \ text \ - The protocol's implementation depends on a number of parameters. In this section we define such - parameters. + The protocol depends on a number of parameters. We use a locale for specifying those parameters + and some properties on them. Namely, the parameters are: + + \<^item> \k\: Establishes how deep in the chain (in terms of number of blocks) a transaction needs to be + in order to be declared as stable. Must be positive. + \<^item> \R\: The length of an epoch, measured in number of slots. Must be positive. + \<^item> \f\: The `active slot coefficient'. Establishes the probability that at least one stakeholder + is elected as a slot leader in each slot, that is, the probability that a slot is not empty. + Must be a strictly positive probability. + \<^item> \\\: The advantage in terms of stake of the honest stakeholders against the adversarial ones. + Must be a probability strictly between 0 and 1. \ -text \ - \<^item> A transaction is declared stable if it is in a block more than \k\ blocks deep in the ledger: -\ +locale protocol_parameters = + fixes k :: nat + and R :: nat + and f :: real + and honest_advantage :: real (\\\) + assumes k_positivity: "k > 0" + and R_positivity: "R > 0" + and f_non_zero_probability: "f \ {0<..1}" + and honest_advantage_bounded_probability: "\ \ {0<..<1}" -consts k :: nat +subsection \ Slots \ text \ - \<^item> The length \R\ of an epoch, measured in slots: + As defined in the paper, we model the concept of slot as a natural number, beginning at 1: \ -consts R :: nat +type_synonym slot = nat -text \ - \<^item> The active slot coefficient $f \in (0, 1]$. Establishes the probability that at least one - stakeholder is elected as a slot leader, that is, the probability that a slot is not empty: -\ +abbreviation (input) first_slot :: slot where + "first_slot \ 1" -axiomatization - f :: real -where - f_non_zero_probability: "0 < f \ f \ 1" +subsection \ Epochs \ text \ - \<^item> Two special, but arbitrary, values that we use when calling the VRF in slot leader selection - ($\mathtt{TEST}$) and block nonce creation/validation ($\mathtt{NONCE}$). They are used to - provide domain separation: + As defined in the paper, we model the concept of epoch as a natural number, beginning at 1: \ -datatype vrf_query_type = TEST | NONCE +type_synonym epoch = nat -subsubsection \ Ideal functionalities \ +abbreviation (input) first_epoch :: epoch where + "first_epoch \ 1" text \ - In the paper, the protocol is described with respect to ideal functionalities. In this section we - model the functionalities available to our protocol implementation. For the sake of simplicity, - we do not model the key generation algorithms for \\\$_{\mathsf{VRF}}$, \\\$_{\mathsf{KES}}$ and - \\\$_{\mathsf{DSIG}}$ but these keys are given as parameters to each stakeholder. + By using basic arithmetic, we can compute the epoch to which a given slot belongs: \ -paragraph \ Functionality \\\$_{\mathsf{VRF}}$. \ +definition (in protocol_parameters) slot_epoch :: "slot \ epoch" where + [simp]: "slot_epoch sl = nat \sl / R\" text \ - We model the evaluation of a VRF as a function that, given an input value and a secret key, - produces a random value and a proof. Also, we can verify that a particular random value was - produced correctly: + and we can check whether a given slot is the first one in its epoch: \ -typedecl vrf_output - -typedecl vrf_proof - -axiomatization -where - vrf_output_finite: "OFCLASS(vrf_output, finite_class)" -and - vrf_proof_finite: "OFCLASS(vrf_proof, finite_class)" - -instance vrf_output :: finite - by (rule vrf_output_finite) - -instance vrf_proof :: finite - by (rule vrf_proof_finite) - -type_synonym vrf_value = "vrf_output \ vrf_proof" - -consts vrf_output_size :: nat (\l\<^sub>V\<^sub>R\<^sub>F\) +definition (in protocol_parameters) first_in_epoch :: "slot \ bool" where + [simp]: "first_in_epoch sl = (R dvd (sl - 1))" -axiomatization - evaluate_vrf :: "secret_key \ 'a \ vrf_value" -and - verify_vrf :: "verification_key \ 'a \ vrf_value \ bool" -where - vrf_eval_ver_cancellation: "verify_vrf vk x (evaluate_vrf sk x)" if "vk = verification_key_of sk" +subsection \ Stake distributions \ text \ - Finally, we can cast a VRF output into a real number: + We model a stakeholder ID as a natural number and use a special syntax to match the notation used + in the paper: \ -consts vrf_output_to_real :: "vrf_output \ real" +datatype stakeholder_id = StakeholderId nat (\U\<^bsub>_\<^esub>\) -paragraph \ Functionalities \\\$_{\mathsf{KES}}$ and \\\$_{\mathsf{DSIG}}$. \ +instance stakeholder_id :: countable + by countable_datatype text \ - In the paper, the functionality \\\$_{\mathsf{DSIG}}$ models a regular digital signature scheme - which is used to sign transactions. Also, the functionality \\\$_{\mathsf{KES}}$ adds the - capability of allowing the signing key to ``evolve'' in such a way that the adversary - cannot forge past signatures, and is used to sign blocks. Therefore, we model these two - functionalities as a single, ordinary digital signature scheme. With this scheme, we can sign a - value using a secret key and verify that a value is properly signed using a verification key: + Now we model a stake distribution simply as a finite map from stakeholder IDs to their respective + stakes: \ -typedecl signature +type_synonym stake = nat -axiomatization - where - signature_finite: "OFCLASS(signature, finite_class)" +type_synonym stake_distr = "(stakeholder_id, stake) fmap" -instance signature :: finite - by (rule signature_finite) +text \ + Given a set \X\ of stakeholder IDs and a stake distribution \\\, we can calculate the absolute + maximum stake controlled by \X\, denoted by \s\<^sup>+\<^bsub>X\<^esub>(\)\, as simply the sum of the stakes in \\\ + belonging to \X\, provided that \X\ is included in the domain of \\\: +\ -axiomatization - sign :: "secret_key \ 'a \ signature" -and - verify :: "verification_key \ 'a \ signature \ bool" +definition + absolute_stake_of_set :: "stakeholder_id set \ stake_distr \ stake" (\s\<^sup>+\<^bsub>_\<^esub>'(_')\) where - sig_ver_cancellation: "verify vk x (sign sk x)" if "vk = verification_key_of sk" - -paragraph \ Functionality \\\$^{\tau,r}_{RLB}$. \ + [simp]: "s\<^sup>+\<^bsub>X\<^esub>(\) = (\U \ X. \ $$! U)" if "X \ fmdom' \" text \ - In the paper, the functionality \\\$^{\tau,r}_{RLB}$ models a randomness beacon that basically - provides a fresh nonce for each epoch to (re)seed the election process. Also, this beacon is - resettable and leaky in order to strengthen the adversary, which we evidently ignore. Finally, - the beacon (via \\\$_{\mathsf{INIT}}$) provides the stakeholders with the genesis block; instead - our implementation passes the genesis block as a parameter to each stakeholder. Therefore, we - only provide a function to produce a fresh nonce: + Based on the previous definition, we define the absolute stake controlled by @{emph \all\} + stakeholders appearing in a stake distribution \\\, denoted by \s\<^sup>+\<^sub>\

(\)\: \ -typedecl nonce +abbreviation (input) + absolute_stake_of_univ :: "stake_distr \ stake" (\s\<^sup>+\<^sub>\

'(_')\) +where + "s\<^sup>+\<^sub>\

(\) \ s\<^sup>+\<^bsub>fmdom' \\<^esub>(\)" -consts new_epoch_rnd :: nonce +text \ + And we define the absolute stake controlled by a @{emph \single\} stakeholder \U\ appearing in a + stake distribution \\\, denoted by \s\<^sup>+\<^bsub>U\<^esub>(\)\: +\ -subsubsection \ Basic definitions \ +abbreviation (input) + absolute_stake_of :: "stakeholder_id \ stake_distr \ stake" (\s\<^sup>+\<^bsub>_\<^esub>'(_')\) +where + "s\<^sup>+\<^bsub>U\<^esub>(\) \ s\<^sup>+\<^bsub>{U}\<^esub>(\)" text \ - In this section we introduce basic definitions for the protocol. + A relative stake is simply a proportion of stake, so we define it as a real number: \ -paragraph \ Stake Distribution. \ +type_synonym relative_stake = real text \ - A stake distribution is simply a map from stakeholder labels \U\<^sub>i\ to their respectives stakes \s\<^sub>i\: + Now, we define the relative stake controlled by a set \X\ of stakeholder IDs w.r.t. a stake + distribution \\\, namely, the proportion of stake controlled by \X\ with respect to the whole + stake in \\\, denoted by \\\<^sup>+\<^bsub>X\<^esub>(\)\: \ -type_synonym stakeholder_id = nat +definition + relative_stake_of_set :: "stakeholder_id set \ stake_distr \ relative_stake" (\\\<^sup>+\<^bsub>_\<^esub>'(_')\) +where + [simp]: "\\<^sup>+\<^bsub>X\<^esub>(\) = s\<^sup>+\<^bsub>X\<^esub>(\) / s\<^sup>+\<^sub>\

(\)" if "\ \ {$$}" -type_synonym stake = nat +text \ + And we define the relative stake controlled by a @{emph \single\} stakeholder \U\ w.r.t. a stake + distribution \\\, denoted by \\\<^sup>+\<^bsub>U\<^esub>(\)\: +\ -type_synonym stake_distr = "(stakeholder_id, stake) fmap" +abbreviation (input) + relative_stake_of :: "stakeholder_id \ stake_distr \ relative_stake" (\\\<^sup>+\<^bsub>_\<^esub>'(_')\) +where + "\\<^sup>+\<^bsub>U\<^esub>(\) \ \\<^sup>+\<^bsub>{U}\<^esub>(\)" -paragraph \ Genesis block. \ +subsection \ Genesis block \ text \ - As defined in the paper, we have a genesis block associated to a blockchain: + As defined in the paper, we have a genesis block associated to a chain. We assume that the same + genesis block is used by all chains and stakeholders: \ -type_synonym stakeholder_keys = " - verification_key \ \ \ $v^\\mathrm{vrf}$ \ - verification_key \ \ \ $v^\\mathrm{kes}$ \ - verification_key" \ \ $v^\mathrm{dsig}$ \ +type_synonym 'vkey stakeholder_keys = " + 'vkey \ \ \ $v^\\mathrm{vrf}$ \ + 'vkey \ \ \ $v^\\mathrm{kes}$ \ + 'vkey" \ \ $v^\mathrm{dsig}$ \ -type_synonym genesis = " - (stakeholder_id \ stakeholder_keys) \ \ \ stakeholders' verification keys \ +type_synonym ('vkey, 'nonce) genesis = " + (stakeholder_id \ 'vkey stakeholder_keys) \ \ \ stakeholders' verification keys \ stake_distr \ \ \ initial stake distribution $\\mathbb{S}_0$ \ - nonce" \ \ initial nonce \\\<^sub>0\ \ + 'nonce" \ \ initial nonce \\\<^sub>0\ \ -paragraph \ Transactions. \ +subsection \ Transactions \ text \ In the paper, the environment \\\ issues transactions on behalf of any stakeholder \U\<^sub>i\ by @@ -290,7 +320,7 @@ text \ stakeholders to put them into blocks. We decide not to model transaction processing this way but use a more realistic approach instead: Transactions are assumed to be received by stakeholders through the network. A transaction body is assumed to be a simple assertion of the form - ``Stakeholder \U\<^sub>i\ transfers stake \s\ to Stakeholder \U\<^sub>j\'': + `Stakeholder \U\<^sub>i\ transfers stake \s\ to Stakeholder \U\<^sub>j\': \ type_synonym transaction_body = " @@ -303,7 +333,7 @@ text \ signing key corresponding to \U\<^sub>i\: \ -type_synonym transaction = "transaction_body \ signature" +type_synonym 'sig transaction = "transaction_body \ 'sig" text \ We can apply a transaction to a stake distribution. The paper does not define how this is done, @@ -311,411 +341,415 @@ text \ stake distribution and that the source stakeholder has enough stake for the withdrawal: \ -fun apply_transaction :: "transaction \ stake_distr \ stake_distr" where +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))" -text \ - Applying a transaction with the same stakeholder as sender and receiver 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), \) \ = \" -proof (rule 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 - then have "?\' $$ U = Some (\ $$! U - s + s)" - by simp - also from True and assms have "\ = \ $$ U" - by auto - finally show ?thesis . - next - case False - then show ?thesis - by simp - qed - qed - then show "\ \\<^sub>f apply_transaction ((U\<^sub>i, U\<^sub>i, s), \) \" - unfolding fmsubset.rep_eq and map_le_def by simp -qed - -paragraph \ Block. \ +subsection \ Blocks \ text \ - We define a block proof, denoted by \B\<^sub>\ = (U\<^sub>i, y, \)\ in the paper: + We define a block proof, denoted by \B\<^sub>\ = (U\<^sub>i, y, \)\ in the paper, which represents the `proof of + leadership' of the block creator: \ -type_synonym block_proof = " +type_synonym ('vrf\<^sub>y, 'vrf\<^sub>\) block_proof = " stakeholder_id \ \ \ Stakeholder who created the block \ - vrf_value" \ \ VRF value used for slot leader selection \ + ('vrf\<^sub>y, 'vrf\<^sub>\) vrf\<^sub>o" \ \ VRF output used for slot leader election \ text \ - \label{sec:block-ref} and we distinguish between an \unsigned block\ (a block without a signature, a concept not explicitly present in the paper) and a signed block. Since the latter corresponds to the concept - of a block in the paper, we refer to a signed block as simply a \block\. For the sake of - completeness, we include the nonce proof in a block (denoted by $\rho = (\rho_y, \rho_\pi)$ in the - paper), despite this datum is actually used by the protocol $\pi_{RLB}$ and not by our protocol - implementation: + of a block in the paper, we refer to a signed block as simply a \block\: \ -type_synonym unsigned_block = " +type_synonym ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) unsigned_block = " slot \ \ \ Slot when the block was created \ - hash option \ \ \ Previous block hash (if any), denoted by \st\ in the paper \ - transaction list \ \ \ Transaction data, denoted by \d\ in the paper \ - block_proof \ \ \ Block proof (proof of leadership), denoted by \B\<^sub>\\ in the paper \ - vrf_value" \ \ Nonce proof \ + 'hash option \ \ \ Previous block hash (if any), denoted by \st\ in the paper \ + 'sig transaction list \ \ \ Transaction data, denoted by \d\ in the paper \ + ('vrf\<^sub>y, 'vrf\<^sub>\) block_proof \ \ \ Block proof, denoted by \B\<^sub>\\ in the paper \ + ('vrf\<^sub>y, 'vrf\<^sub>\) vrf\<^sub>o" \ \ Nonce proof, denoted by $\rho = (\rho_y, \rho_\pi)$ in the paper \ -type_synonym block = "unsigned_block \ signature" +type_synonym ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) block = "('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) unsigned_block \ 'sig" -fun bl_slot :: "block \ slot" where - "bl_slot ((sl, _, _, _), _) = sl" +fun bl_slot :: "('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) block \ slot" where + "bl_slot ((sl, _, _, _, _), _) = sl" -fun bl_txs :: "block \ transaction list" where - "bl_txs ((_, _, d, _), _) = d" +fun bl_txs :: "('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) block \ 'sig transaction list" where + "bl_txs ((_, _, d, _, _), _) = d" + +fun bl_nonce_proof :: "('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) block \ ('vrf\<^sub>y, 'vrf\<^sub>\) vrf\<^sub>o" where + "bl_nonce_proof ((_, _, _, _, \), _) = \" text \ We can apply a block to a stake distribution by applying all transactions in the block to the stake distribution: \ -abbreviation apply_block :: "block \ stake_distr \ stake_distr" where - "apply_block B \ \ fold apply_transaction (bl_txs B) \" - -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 - -paragraph \ Blockchain. \ - -text \ - A blockchain is simply a sequence of blocks. We do not record the genesis block explicitly as - part of the blockchain: -\ +definition + apply_block :: "('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) block \ stake_distr \ stake_distr" +where + [simp]: "apply_block B = fold apply_transaction (bl_txs B)" -type_synonym blockchain = "block list" +subsection \ Chains \ text \ - We let \\\<^sub>1 \ \\<^sub>2\ indicate that the blockchain \\\<^sub>1\ is a prefix of the blockchain \\\<^sub>2\: + A chain is simply a sequence of blocks. As stated earlier, we do not record the genesis block + explicitly as part of the chain: \ -abbreviation is_prefix_of :: "blockchain \ blockchain \ bool" (infix \\\ 50) where - "\\<^sub>1 \ \\<^sub>2 \ prefix \\<^sub>1 \\<^sub>2" +type_synonym ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain = "('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) block list" text \ - A prefix of a blockchain keeps all properties on its elements that hold for the original blockchain: + We let \\\<^sub>1 \ \\<^sub>2\ indicate that the chain \\\<^sub>1\ is a prefix of the chain \\\<^sub>2\: \ -lemma prefix_invariancy: - assumes "\i \ {0..\<^sub>2}. P (\\<^sub>2 ! i)" - and "\\<^sub>1 \ \\<^sub>2" - shows "\i \ {0..\<^sub>1}. P (\\<^sub>1 ! i)" - using assms -proof (intro ballI) - fix i - assume "i \ {0..\<^sub>1}" - then have *: "i < length \\<^sub>1" - by simp - moreover from assms(2) obtain \\<^sub>3 where **: "\\<^sub>2 = \\<^sub>1 @ \\<^sub>3" .. - ultimately have "P (\\<^sub>2 ! i)" - using assms(1) by simp - with * and ** show "P (\\<^sub>1 ! i)" - by (simp add: nth_append) -qed +notation prefix (infix \\\ 50) text \ - We define a function to prune the last \m\ blocks in a blockchain \\\, denoted by \\\<^bsup>\m\<^esup>\ in the + We define a function to prune the last \m\ blocks in a chain \\\, denoted by \\\<^bsup>\m\<^esup>\ in the paper: \ -abbreviation prune_chain :: "blockchain \ nat \ blockchain" (infixl \\\ 999) where - "\ \m \ take (length \ - m) \" - -text \ - The \\\<^bsup>\m\<^esup>\ operator satisfies some simple laws: -\ - -lemma zero_blocks_chain_prunning_identity: - shows "\ \0 = \" - by simp - -lemma long_chain_prunning_emptiness: - assumes "m \ length \" - shows "\ \m = []" - using assms - by simp - -lemma append_prune_chain_drop_identity: - shows "\ \m @ drop (length \ - m) \ = \" - by simp +definition + prune_chain :: " + ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain \ + nat \ + ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain" + (\_\<^sup>\\<^bsup>_\<^esup>\ [999] 999) +where + [simp]: "\\<^sup>\\<^bsup>m\<^esup> = take (length \ - m) \" text \ - Also, we define a function to prune the blocks in a blockchain which have slots greater than a + Also, we define a function to prune the blocks in a chain which have slots greater than a given slot: \ -abbreviation prune_after :: "slot \ blockchain \ blockchain" where - "prune_after sl \ \ takeWhile (\B. bl_slot B \ sl) \" +definition + prune_after :: "slot \ ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain \ ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain" +where + [simp]: "prune_after sl = takeWhile (\B. bl_slot B \ sl)" text \ - And we can apply a blockchain \\\ to a stake distribution \\\ by sequentially applying all blocks + And we can apply a chain \\\ to a stake distribution \\\ by sequentially applying all blocks in \\\ to \\\: \ -abbreviation apply_blockchain :: "blockchain \ stake_distr \ stake_distr" where - "apply_blockchain \ \ \ fold apply_block \ \" +definition + apply_chain :: "('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain \ stake_distr \ stake_distr" +where + [simp]: "apply_chain = fold apply_block" -paragraph \ Absolute and Relative Stake. \ +subsection \ Functionality \\\$^{\tau,r}_{RLB}$ and subprotocol \\\$_{RLB}$ \ text \ - The paper defines the (somewhat vague) concepts of @{emph \maximum\} and @{emph \minimum\} - absolute stake controlled by a set of parties, as well as the concepts of - @{emph \adversarial stake ratio\} and @{emph \honest stake ratio\}. However, for our - implementation we only need the absolute @{emph \maximum\} stake controlled by @{emph \all\} - stakeholders, denoted by \s\<^sup>+(\)\ where \\\ is an arbitrary stake distribution: + In the paper, the functionality \\\$^{\tau,r}_{RLB}$ models a randomness beacon that basically + provides a fresh nonce for each epoch to (re)seed the election process. Furthermore, this beacon + is resettable and leaky in order to strengthen the adversary. The paper also presents a + subprotocol \\\$_{RLB}$ that simulates the beacon in the \\\$_\mathsf{INIT}$-hybrid model. So, we + choose to directly model \\\$_{RLB}$, and not explicitly model \\\$_\mathsf{INIT}$ but instead + assume that each stakeholder is given the genesis block as a parameter (see Section + \ref{sec:sh-process-ref}): \ -abbreviation absolute_stake :: "stake_distr \ stake" (\s\<^sup>+'(_')\) where - "s\<^sup>+(\) \ \U\<^sub>j \ fmdom' \. \ $$! U\<^sub>j" +definition + fold1 :: "('a \ 'a \ 'a) \ 'a list \ 'a" +where + [simp]: "fold1 f xs = foldl f (hd xs) (tl xs)" -text \ - and the relative stake controlled by @{emph \a single\} stakeholder \U\<^sub>i\, taken as - @{emph \maximum\} across of the view of @{emph \all\} stakeholders w.r.t. a stake distribution - \\\, denoted by \\\<^sup>+(U\<^sub>i, \)\. For this definition we assume that \U\<^sub>i\ exists in \\\: -\ +lemma "fold1 (\\) [a,b,c] = (a \\ b) \\ c" + by simp -type_synonym relative_stake = real +locale \\<^sub>R\<^sub>L\<^sub>B = + protocol_parameters + + hashable \\<^sub>\ + for \\<^sub>\ :: "'nonce \ 'nonce" +begin -abbreviation - relative_stake_of :: "stakeholder_id \ stake_distr \ relative_stake" (\\\<^sup>+'(_,_')\) +function + next_epoch_nonce :: "'nonce \ epoch \ ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain \ 'nonce" where - "\\<^sup>+(U\<^sub>i, \) \ + "next_epoch_nonce \\<^sub>p\<^sub>r\<^sub>e\<^sub>v j \ = ( let - s\<^sub>i = \ $$! U\<^sub>i; - s\<^sub>\

= s\<^sup>+(\) + sl\<^sub>e\<^sub>n\<^sub>d = (j - (first_epoch + 1)) * R + 16 * nat \of_nat k / (1 + \)\; + \' = prune_after sl\<^sub>e\<^sub>n\<^sub>d \; + v = fold1 (\\) (map bl_nonce_proof \') in - s\<^sub>i / s\<^sub>\

" + \\<^sub>\ (\\<^sub>p\<^sub>r\<^sub>e\<^sub>v \\ j \\ v))" if "j \ first_epoch + 1" +| "next_epoch_nonce \\<^sub>p\<^sub>r\<^sub>e\<^sub>v j \ = undefined \\<^sub>p\<^sub>r\<^sub>e\<^sub>v j \" if "j < first_epoch + 1" + by (atomize, auto) + termination by lexicographic_order -subsubsection \ Leader election \ +end + +subsection \ Leader election \ + +text \ + In this section we model the procedure which determines whether a stakeholder is elected as a slot + leader or not for a given slot: +\ + +locale leader_election = + protocol_parameters + + vrf _ _ evaluate\<^sub>V\<^sub>R\<^sub>F verify\<^sub>V\<^sub>R\<^sub>F + for evaluate\<^sub>V\<^sub>R\<^sub>F :: "'skey \ 'nonce \ ('vrf\<^sub>y, 'vrf\<^sub>\) vrf\<^sub>o" + and verify\<^sub>V\<^sub>R\<^sub>F :: "'vkey \ 'nonce \ ('vrf\<^sub>y, 'vrf\<^sub>\) vrf\<^sub>o \ bool" +begin + +context +begin text \ - In this section we model the staking procedure which is used for the slot leader to compute and - send the next block. We define the probability \\(\)\ that a stakeholder with relative stake \\\ - is elected as a slot leader: + We define the probability \\(\)\ that a stakeholder with relative stake \\\ is elected as a slot + leader: \ -abbreviation slot_leader_probability :: "relative_stake \ real" (\\'(_')\) where - "\(\) \ 1 - (1 - f) powr \" +notation powr (\_\<^bsup>_\<^esup>\ [81,81] 80) + +definition + slot_leader_probability :: "relative_stake \ real" (\\'(_')\) +where + [simp]: "\(\) = 1 - (1 - f)\<^bsup>\\<^esup>" text \ - Next, given epoch \j\, genesis block \G\ and blockchain \\\, we define a function \\(j, G, \)\ - that computes the stake distribution at the end of epoch \j - 2\ as reflected in \\\ if \j \ 2\; - otherwise returns the initial stake distribution in \G\: + Next, given epoch \j\, the initial stake distribution \\\<^sub>0\, and a chain \\\, we define a function + \\\<^bsub>j\<^esub>(\\<^sub>0, \)\ that computes the stake distribution at the end of epoch \j - (first_epoch + 1)\ as + reflected in \\\ if \j > first_epoch\; otherwise returns \\\<^sub>0\: \ -fun epoch_stake_distr :: "epoch \ genesis \ blockchain \ stake_distr" (\\'(_,_,_')\) where - "\(Suc 0, (_, \\<^sub>0, _), _) = \\<^sub>0" | - "\(j, (_, \\<^sub>0, _), \) = ( +private function + epoch_stake_distr :: " + epoch \ + stake_distr \ + ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain \ + stake_distr" + (\\\<^bsub>_\<^esub>'(_,_')\) +where + "\\<^bsub>j\<^esub>(\\<^sub>0, _) = \\<^sub>0" if "j = first_epoch" +| "\\<^bsub>j\<^esub>(\\<^sub>0, \) = ( let - sl\<^sub>e\<^sub>n\<^sub>d = (j - 2) * R; + sl\<^sub>e\<^sub>n\<^sub>d = (j - (Suc first_epoch)) * R; \' = prune_after sl\<^sub>e\<^sub>n\<^sub>d \ in - apply_blockchain \' \\<^sub>0)" + apply_chain \' \\<^sub>0)" if "j > first_epoch" +| "\\<^bsub>j\<^esub>(\\<^sub>0, \) = undefined j \\<^sub>0 \" if "j < first_epoch" + by (auto, fastforce) + termination by lexicographic_order text \ - Now, given a genesis block \G\ and a blockchain \\\, a stakeholder \U\<^sub>i\ is an eligible slot leader - for a particular slot in an epoch \j\ if its VRF output is smaller than a threshold value, denoted - by \T(U\<^sub>i, j, G, \)\, and defined as follows: + Now, given the initial stake distribution \\\<^sub>0\ and a chain \\\, a stakeholder \U\ is an eligible + slot leader for a particular slot in an epoch \j\ if its VRF output is smaller than a @{emph + \threshold value\}, denoted by \T\<^bsub>U\<^esub>\<^bsup>j\<^esup>(\\<^sub>0, \)\ and defined as follows: \ -abbreviation slot_leader_threshold :: " - stakeholder_id - \ epoch - \ genesis - \ blockchain - \ real" - (\T'(_,_,_,_')\) +private fun + slot_leader_threshold :: " + stakeholder_id \ + epoch \ + stake_distr \ + ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain \ + real" + (\T\<^bsub>_\<^esub>\<^bsup>_\<^esup>'(_,_')\) where - "T(U\<^sub>i, j, G, \) \ + "T\<^bsub>U\<^esub>\<^bsup>j\<^esup>(\\<^sub>0, \) = ( let - \\<^sub>j = \(j, G, \); - \ = \\<^sup>+(U\<^sub>i, \\<^sub>j) + \\<^sub>j = \\<^bsub>j\<^esub>(\\<^sub>0, \); + \ = \\<^sup>+\<^bsub>U\<^esub>(\\<^sub>j) in - 2 ^ l\<^sub>V\<^sub>R\<^sub>F * \(\)" + 2\<^bsup>l\<^sub>V\<^sub>R\<^sub>F\<^esup> * \(\))" text \ Finally, a stakeholder can ask if they are a slot leader for a given slot (note that stakeholders can only check this for themselves, not for other stakeholders): \ -abbreviation is_slot_leader :: "slot \ secret_key \ nonce \ real \ vrf_value option" where - "is_slot_leader sl sk \ T \ +fun + is_slot_leader :: " + stakeholder_id \ + slot \ + 'skey \ + 'nonce \ + stake_distr \ + ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain \ + (('vrf\<^sub>y, 'vrf\<^sub>\) vrf\<^sub>o) option" +where + "is_slot_leader U sl sk \ \\<^sub>0 \ = ( let - (y, \) = evaluate_vrf sk (\ \\ sl \\ TEST) + j = slot_epoch sl; + T = T\<^bsub>U\<^esub>\<^bsup>j\<^esup>(\\<^sub>0, \); + (y, \) = evaluate\<^sub>V\<^sub>R\<^sub>F sk (\ \\ sl \\ TEST) in - if vrf_output_to_real y < T then Some (y, \) else None" + if value_to_real y < T then Some (y, \) else None)" + +end + +end -subsubsection \ Auxiliary functions \ +subsection \ Chain update \ text \ - We can compute the epoch to which a given slot belongs: + In this section we model the procedure by which a stakeholder decides which chain to adopt + given a set of alternatives received over the network in the current round (the `longest chain' + rule, i.e. that the intersection between the alternative chain and the current best chain is no + more than \k\ blocks back, and the alternative chain is strictly longer than the current best + chain): \ -abbreviation slot_epoch :: "slot \ epoch" where - "slot_epoch sl \ nat \sl / R\" +locale chain_selection = + protocol_parameters + + hashable \\<^sub>B + for \\<^sub>B :: "('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) block \ 'block_hash" +begin text \ - and check whether a given slot is the first one in its epoch: + 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., 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: \ -abbreviation first_in_epoch :: "slot \ bool" where - "first_in_epoch sl \ R dvd (sl - 1)" - -subsubsection \ Verification \ +definition + disjoint_chains :: " + ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain \ + ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain \ + bool" +where + [iff]: "disjoint_chains \ \' \ \\<^sub>B (hd \) \ \\<^sub>B (hd \')" if "\ \ []" and "\' \ []" text \ - We can verify that a transaction is valid w.r.t. a genesis block, namely that the source and - target stakeholders exist in the genesis block's stake distribution, that the source stakeholder - has enough stake for the withdrawal, and that the signature is valid. Here we assume that the - given genesis block is well-formed, in particular that the domain of both maps coincide: + Also, we can extract the hashed, longest common prefix of two chains: \ -abbreviation verify_tx :: "transaction \ genesis \ bool" where - "verify_tx tx G \ - let - (txbody, \) = tx; - (U\<^sub>i, U\<^sub>j, s) = txbody; - (vks, \\<^sub>0, _) = G; - (_, _, vk\<^sub>i) = the (vks U\<^sub>i) \ \\U\<^sub>i\'s DSIG verification key\ - in - \s\<^sub>i s\<^sub>j. \\<^sub>0 $$ U\<^sub>i = Some s\<^sub>i \ \\<^sub>0 $$ U\<^sub>j = Some s\<^sub>j \ s\<^sub>i \ s \ verify vk\<^sub>i txbody \" +definition + hashed_lcp :: " + ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain \ + ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain \ + 'block_hash list" +where + [simp]: "hashed_lcp \ \' = Longest_common_prefix {map \\<^sub>B \, map \\<^sub>B \'}" text \ - and thus we can trivially verify whether a list of transactions is valid w.r.t. a genesis block: + 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 \\'\: \ -abbreviation verify_tx_data :: "transaction list \ genesis \ bool" where - "verify_tx_data txs G \ \i \ {0.. + ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain \ + ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain \ + bool" +where + [iff]: "forks_at_most n \ \' \ ( + if + disjoint_chains \ \' + then + length \ \ n + else + length (drop (length (hashed_lcp \ \')) \) \ n)" text \ - A key component of block verification is verifying the block proof, i.e. that the stakeholder who - created the block was in the slot leader set of the slot in which the block was created: + For implementation purposes, we define a function that, given two chains \\\ and \\'\, obtains + the suffix of \\\ after trimming its hashed longest common prefix with \\'\: \ -abbreviation - verify_block_proof :: "slot \ verification_key \ nonce \ vrf_value \ real \ bool" +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 - "verify_block_proof sl vk \ v T \ - verify_vrf vk (\ \\ sl \\ TEST) v \ vrf_output_to_real (fst v) < T" + "first_suffix \ \' = ( + let + hlcp = longest_common_prefix (map \\<^sub>B \) (map \\<^sub>B \') + in + drop (length hlcp) \)" text \ - Although the block nonce is not used (as explained in Section \ref{sec:block-ref}), we verify that - it was properly created nonetheless: + Also, we can compute the list of the longest chains in a given list of chains \\\: \ -abbreviation verify_block_nonce :: "slot \ verification_key \ nonce \ vrf_value \ bool" where - "verify_block_nonce sl vk \ v \ verify_vrf vk (\ \\ sl \\ NONCE) v" +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 \ = [\ \ \. is_longest_chain \ \]" text \ - Armed with these definitions, we can now verify that a block is indeed valid: + Now we can define the function that implements the `longest chain' rule, namely the + $\mathsf{maxvalid}$ function in the paper: \ -abbreviation verify_block :: "block \ hash option \ genesis \ nonce \ real \ bool" where - "verify_block B oh\<^sub>p\<^sub>r\<^sub>e\<^sub>v G \ T \ +fun + max_valid :: " + ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain \ + ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain list \ + ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain" +where + "max_valid \ \ = ( let - ((sl, st, d, B\<^sub>\, \), \) = B; - (U\<^sub>s, y, \) = B\<^sub>\; - (\\<^sub>y, \\<^sub>\) = \ + \' = [\' \ \ # \. forks_at_most k \ \']; \ \the \k\ parameter\ + \'' = longest_chains \' in - verify_tx_data d G \ ( - \v\<^sub>v\<^sub>r\<^sub>f v\<^sub>k\<^sub>e\<^sub>s v\<^sub>d\<^sub>s\<^sub>i\<^sub>g. - Some (v\<^sub>v\<^sub>r\<^sub>f, v\<^sub>k\<^sub>e\<^sub>s, v\<^sub>d\<^sub>s\<^sub>i\<^sub>g) = (fst G) U\<^sub>s \ \ \ \U\<^sub>s\'s verification keys \ - verify_block_proof sl v\<^sub>v\<^sub>r\<^sub>f \ (y, \) T \ - verify_block_nonce sl v\<^sub>v\<^sub>r\<^sub>f \ (\\<^sub>y, \\<^sub>\) \ - verify v\<^sub>k\<^sub>e\<^sub>s (sl, st, d, B\<^sub>\, \) \) \ ( - case oh\<^sub>p\<^sub>r\<^sub>e\<^sub>v of - None \ True - | 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 \ + if \ \ set \'' then \ else hd \'')" + +end + +subsection \ The semi-synchronous model \label{sec:semi-sync-model-ref} \ text \ - and we can verify that a blockchain is indeed valid: + In the paper, a semi-synchronous model with an upper bound \\\ in message delay is used. Regarding + \\\, we stress the fact that the protocol is oblivious of \\\ and this bound is only used in the + security analysis. Hence, from the protocol's point of view, the network is no better than an + eventual delivery network (without a concrete bound), which can be modeled using our process + calculus, for example, as a reliable broadcasting server process. Regarding synchrony, we simply + assume that an external `clock process' signals each stakeholder when a round (i.e. slot) ends, + and that messages sent in one round are guaranteed to be received at the onset of the next round. \ -abbreviation verify_chain :: "blockchain \ genesis \ nonce \ bool" where - "verify_chain \ G \ \ \i \ {0..}. - let - B = \ ! i; \ \ current block \ - ((sl, _, _, B\<^sub>\, _), _) = B; - U\<^sub>s = fst B\<^sub>\; - oh\<^sub>p\<^sub>r\<^sub>e\<^sub>v = if i = 0 then None else fst (snd (fst (\ ! (i - 1)))); \ \ previous block hash \ - T\<^sub>s = T(U\<^sub>s, slot_epoch sl, G, \) - in - verify_block B oh\<^sub>p\<^sub>r\<^sub>e\<^sub>v G \ T\<^sub>s" +paragraph \ The Delayed Diffuse Functionality. \ + +text \ + We do not model the network as a separate ideal functionality \textsf{DDiffuse}\\<^sub>\\ but rely on + our process calculus features for communication. In particular, a single channel is used both to + read the received messages from a stakeholder's `incoming string' (or `mailbox') and to + `diffuse' a message. Also, the restriction that a stakeholder is allowed to diffuse once in a + round is explicitly enforced by the stakeholder process implementation, see Section + \ref{sec:sh-process-ref}. +\ + +subsection \ Broadcast messages \ + +text \ + In addition to broadcasting transactions and chains, we also assume that there is a `clock + process' broadcasting the next slot at the end of each current slot, see Section + \ref{sec:semi-sync-model-ref}: +\ + +datatype ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) broadcast_msg = + BroadcastTx (bm_tx: "'sig transaction") + | BroadcastChain (bm_\: "('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain") + | BroadcastEndSlot (bm_sl: slot) + +instance broadcast_msg :: (countable, countable, countable, countable) countable + by countable_datatype + +type_synonym ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) broadcast_channel = " + ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) broadcast_msg channel" + +subsection \ The stakeholder process \label{sec:sh-process-ref} \ + +text \ + Now we are ready to define the process representing a stakeholder running the protocol. +\ subsubsection \ Stakeholder state \ @@ -724,202 +758,1848 @@ text \ in a record type: \ -record stakeholder_state = +record ('skey, 'vkey, 'hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig, 'nonce) stakeholder_state = ss_id :: stakeholder_id \ \ ID of the stakeholder in the set \U\<^sub>1, ..., U\<^sub>n\ \ - ss_G :: genesis \ \ genesis block \ - ss_\ :: blockchain \ \ current blockchain \ - ss_\ :: nonce \ \ current epoch nonce \\\<^sub>j\ \ - ss_\ :: "blockchain list" \ \ blockchains received during the current slot \ - ss_txs :: "transaction list" \ \ transactions received during the current slot \ - ss_st :: "hash option" \ \ current state, namely the hash of the head of \ss_\\ \ - ss_sk\<^sub>v\<^sub>r\<^sub>f :: secret_key \ \ secret key for \\\$_{\mathsf{VRF}}$ \ - ss_sk\<^sub>k\<^sub>e\<^sub>s :: secret_key \ \ secret key for \\\$_{\mathsf{KES}}$ \ - ss_sk\<^sub>d\<^sub>s\<^sub>i\<^sub>g :: secret_key \ \ secret key for \\\$_{\mathsf{DSIG}}$ \ + ss_G :: "('vkey, 'nonce) genesis" \ \ genesis block \ + ss_\ :: "('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain" \ \ current chain \ + ss_\ :: 'nonce \ \ current epoch nonce \\\<^sub>j\ \ + ss_\ :: "('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain list" \ \ chains received during the current slot \ + ss_txs :: "'sig transaction list" \ \ transactions received during the current slot \ + ss_st :: "'hash option" \ \ current state, namely the hash of the head of \ss_\\ \ + ss_sk\<^sub>v\<^sub>r\<^sub>f :: 'skey \ \ secret key for \\\$_{\mathsf{VRF}}$ \ + ss_sk\<^sub>k\<^sub>e\<^sub>s :: 'skey \ \ secret key for \\\$_{\mathsf{KES}}$ \ + ss_sk\<^sub>d\<^sub>s\<^sub>i\<^sub>g :: 'skey \ \ secret key for \\\$_{\mathsf{DSIG}}$ \ + +locale stakeholders = + digital_signature_scheme _ _ sign\<^sub>K\<^sub>E\<^sub>S verify\<^sub>K\<^sub>E\<^sub>S + + digital_signature_scheme _ _ sign\<^sub>D\<^sub>S\<^sub>I\<^sub>G verify\<^sub>D\<^sub>S\<^sub>I\<^sub>G + + chain_selection _ _ _ _ \\<^sub>B + + leader_election _ _ _ _ _ _ _ _ evaluate\<^sub>V\<^sub>R\<^sub>F verify\<^sub>V\<^sub>R\<^sub>F + + \\<^sub>R\<^sub>L\<^sub>B _ _ _ _ \\<^sub>\ + for sign\<^sub>K\<^sub>E\<^sub>S :: " + 'skey \ + ('hash::countable, 'vrf\<^sub>y::countable, 'vrf\<^sub>\::countable, 'sig::countable) unsigned_block \ + 'sig" + and verify\<^sub>K\<^sub>E\<^sub>S :: "'vkey \ ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) unsigned_block \ 'sig \ bool" + and sign\<^sub>D\<^sub>S\<^sub>I\<^sub>G :: "'skey \ transaction_body \ 'sig" + and verify\<^sub>D\<^sub>S\<^sub>I\<^sub>G :: "'vkey \ transaction_body \ 'sig \ bool" + and \\<^sub>B :: "('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) block \ 'hash" + and evaluate\<^sub>V\<^sub>R\<^sub>F :: "'skey \ 'nonce \ ('vrf\<^sub>y, 'vrf\<^sub>\) vrf\<^sub>o" + and verify\<^sub>V\<^sub>R\<^sub>F :: "'vkey \ 'nonce \ ('vrf\<^sub>y, 'vrf\<^sub>\) vrf\<^sub>o \ bool" + and \\<^sub>\ :: "'nonce \ 'nonce" +begin + +context +begin + +subsubsection \ Verification \ text \ - We can specify what the initial state for each stakeholder should be: + We can verify that a transaction is valid w.r.t. a genesis block, namely that the source and + target stakeholders exist in the genesis block's stake distribution, that the source stakeholder + has enough stake for the withdrawal, and that the signature is valid. Here we assume that the + given genesis block is well-formed, in particular that the domain of both maps coincide: \ -abbreviation init_stakeholder_state :: " - stakeholder_id - \ genesis - \ secret_key - \ secret_key - \ secret_key - \ stakeholder_state" +private definition + verify_tx :: "'sig transaction \ ('vkey, 'nonce) genesis \ bool" where - "init_stakeholder_state U\<^sub>i G sk\<^sub>v\<^sub>r\<^sub>f sk\<^sub>k\<^sub>e\<^sub>s sk\<^sub>d\<^sub>s\<^sub>i\<^sub>g \ + [iff]: "verify_tx tx G \ ( let - (_, _, \\<^sub>0) = G + (txbody, \) = tx; + (U\<^sub>i, U\<^sub>j, s) = txbody; + (vks, \\<^sub>0, _) = G; + (_, _, vk\<^sub>i) = the (vks U\<^sub>i) \ \\U\<^sub>i\'s DSIG verification key\ in - \ - ss_id = U\<^sub>i, - ss_G = G, - ss_\ = [], - ss_\ = \\<^sub>0, - ss_\ = [], - ss_txs = [], - ss_st = None, - ss_sk\<^sub>v\<^sub>r\<^sub>f = sk\<^sub>v\<^sub>r\<^sub>f, - ss_sk\<^sub>k\<^sub>e\<^sub>s = sk\<^sub>k\<^sub>e\<^sub>s, - ss_sk\<^sub>d\<^sub>s\<^sub>i\<^sub>g = sk\<^sub>d\<^sub>s\<^sub>i\<^sub>g - \" + \s\<^sub>i s\<^sub>j. \\<^sub>0 $$ U\<^sub>i = Some s\<^sub>i \ \\<^sub>0 $$ U\<^sub>j = Some s\<^sub>j \ s\<^sub>i \ s \ verify\<^sub>D\<^sub>S\<^sub>I\<^sub>G vk\<^sub>i txbody \)" + +text \ + and thus we can trivially verify whether a list of transactions is valid w.r.t. a genesis block: +\ -subsubsection \ Blockchain update \ +private definition + verify_tx_data :: "'sig transaction list \ ('vkey, 'nonce) genesis \ bool" +where + [iff]: "verify_tx_data txs G \ (\i \ {0.. - In this section we model the procedure by which a stakeholder decides which blockchain to adopt - given a set of alternatives received over the network in the current round (the ``longest chain'' - rule). We can check whether a blockchain forks from another at most \m\ blocks: + A key component of block verification is verifying the block proof, i.e. that the stakeholder who + created the block was in the slot leader set of the slot in which the block was created: \ -abbreviation forks_at_most :: "nat \ blockchain \ blockchain \ bool" where - "forks_at_most n \ \' \ - if - \i. \ (\ ! i) \ \ (\' ! i) - then - length (drop (LEAST i. \ (\ ! i) \ \ (\' ! i)) \') \ n - else - True" +private definition + verify_block_proof :: "slot \ 'vkey \ 'nonce \ ('vrf\<^sub>y, 'vrf\<^sub>\) vrf\<^sub>o \ real \ bool" +where + [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: +\ + +private definition + verify_block_nonce :: "slot \ 'vkey \ 'nonce \ ('vrf\<^sub>y, 'vrf\<^sub>\) vrf\<^sub>o \ bool" +where + [iff]: "verify_block_nonce sl vk \ v \ verify\<^sub>V\<^sub>R\<^sub>F vk (\ \\ sl \\ NONCE) v" text \ - Also, we can compute the list of the longest blockchains in a given list of blockchains: + Armed with these definitions, we can now verify that a block is indeed valid: \ -abbreviation longest_chains :: "blockchain list \ blockchain list" where - "longest_chains \ \ +private definition + verify_block :: " + ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) block \ + 'hash option \ + ('vkey, 'nonce) genesis \ + 'nonce \ + real \ + bool" +where + [iff]: "verify_block B oh\<^sub>p\<^sub>r\<^sub>e\<^sub>v G \ T \ ( let - is_longest_chain = \\ \. \\' \ set \. length \ \ length \' + ((sl, st, d, B\<^sub>\, \), \) = B; + (U\<^sub>s, y, \) = B\<^sub>\; + (\\<^sub>y, \\<^sub>\) = \ in - [\. \ \ \, is_longest_chain \ \]" + verify_tx_data d G \ ( + \v\<^sub>v\<^sub>r\<^sub>f v\<^sub>k\<^sub>e\<^sub>s v\<^sub>d\<^sub>s\<^sub>i\<^sub>g. + Some (v\<^sub>v\<^sub>r\<^sub>f, v\<^sub>k\<^sub>e\<^sub>s, v\<^sub>d\<^sub>s\<^sub>i\<^sub>g) = (fst G) U\<^sub>s \ \ \ \U\<^sub>s\'s verification keys \ + verify_block_proof sl v\<^sub>v\<^sub>r\<^sub>f \ (y, \) T \ + verify_block_nonce sl v\<^sub>v\<^sub>r\<^sub>f \ (\\<^sub>y, \\<^sub>\) \ + verify\<^sub>K\<^sub>E\<^sub>S v\<^sub>k\<^sub>e\<^sub>s (sl, st, d, B\<^sub>\, \) \) \ ( + case oh\<^sub>p\<^sub>r\<^sub>e\<^sub>v of + None \ True + | 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 \ - Now we can define the function that implements the ``longest chain'' rule, namely the - $\mathsf{maxvalid}$ function in the paper: + 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: \ -abbreviation max_valid :: "blockchain \ blockchain list \ blockchain" where - "max_valid \ \ \ +private definition + verify_chain :: "('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) chain \ ('vkey, 'nonce) genesis \ 'nonce \ bool" +where + [iff]: "verify_chain \ G \ \ (\i \ {0..}. let - \' = [\'. \' \ \ # \, forks_at_most k \ \']; - \'' = longest_chains \' + (_, \\<^sub>0, _) = G; + B = \ ! i; \ \ current block \ + ((sl, _, _, B\<^sub>\, _), _) = B; + U\<^sub>s = fst B\<^sub>\; + oh\<^sub>p\<^sub>r\<^sub>e\<^sub>v = if i = 0 then None else fst (snd (fst (\ ! (i - 1)))); \ \ previous block hash \ + j = slot_epoch sl; + T\<^sub>s = T\<^bsub>U\<^sub>s\<^esub>\<^bsup>j\<^esup>(\\<^sub>0, \) + in + verify_block B oh\<^sub>p\<^sub>r\<^sub>e\<^sub>v G \ T\<^sub>s)" + +text \ + Finally, we specify what the initial state for each stakeholder should be: +\ + +fun + init_stakeholder_state :: " + stakeholder_id \ + ('vkey, 'nonce) genesis \ + 'skey \ + 'skey \ + 'skey \ + ('skey, 'vkey, 'hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig, 'nonce) stakeholder_state" +where + "init_stakeholder_state U\<^sub>i G sk\<^sub>v\<^sub>r\<^sub>f sk\<^sub>k\<^sub>e\<^sub>s sk\<^sub>d\<^sub>s\<^sub>i\<^sub>g = ( + let + (_, _, \\<^sub>0) = G in - if \ \ set \'' then \ else hd \''" + \ + ss_id = U\<^sub>i, + ss_G = G, + ss_\ = [], + ss_\ = \\<^sub>0, + ss_\ = [], + ss_txs = [], + ss_st = None, + ss_sk\<^sub>v\<^sub>r\<^sub>f = sk\<^sub>v\<^sub>r\<^sub>f, + ss_sk\<^sub>k\<^sub>e\<^sub>s = sk\<^sub>k\<^sub>e\<^sub>s, + ss_sk\<^sub>d\<^sub>s\<^sub>i\<^sub>g = sk\<^sub>d\<^sub>s\<^sub>i\<^sub>g + \)" -subsubsection \ Blockchain extension \ +subsubsection \ Chain extension \ text \ In this section we model the procedure by which a stakeholder elected as a slot leader extends its - current blockchain. We define a function that constructs a new block containing the transactions + current chain. We define a function that constructs a new block containing the transactions in the stakeholder's current state: \ -abbreviation make_block :: "stakeholder_state \ slot \ vrf_value \ block" where - "make_block ss sl v \ +private fun + make_block :: " + ('skey, 'vkey, 'hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig, 'nonce) stakeholder_state \ + slot \ + ('vrf\<^sub>y, 'vrf\<^sub>\) vrf\<^sub>o \ + ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) block" +where + "make_block ss sl v = ( let - U\<^sub>i = ss_id ss; + U = ss_id ss; \ = ss_\ ss; - st = if ss_\ ss = [] then None else Some (\ (last (ss_\ ss))); + st = if ss_\ ss = [] then None else Some (\\<^sub>B (last (ss_\ ss))); d = ss_txs ss; - B\<^sub>\ = (U\<^sub>i, v); - \ = evaluate_vrf (ss_sk\<^sub>v\<^sub>r\<^sub>f ss) (\ \\ sl \\ NONCE); + B\<^sub>\ = (U, v); + \ = evaluate\<^sub>V\<^sub>R\<^sub>F (ss_sk\<^sub>v\<^sub>r\<^sub>f ss) (\ \\ sl \\ NONCE); uB = (sl, st, d, B\<^sub>\, \); - \ = sign (ss_sk\<^sub>k\<^sub>e\<^sub>s ss) uB + \ = sign\<^sub>K\<^sub>E\<^sub>S (ss_sk\<^sub>k\<^sub>e\<^sub>s ss) uB in - (uB, \)" + (uB, \))" text \ - We can extend a stakeholder's current blockchain simply by appending a newly constructed block to - it and updating its current state to the hash of this block: + We can extend a stakeholder's current chain simply by appending a newly constructed block to + it and updating its current `state' to the hash of this block: \ -abbreviation extend_chain :: "stakeholder_state \ block \ stakeholder_state" where - "extend_chain ss B\<^sub>n\<^sub>e\<^sub>w \ ss\ss_\ := ss_\ ss @ [B\<^sub>n\<^sub>e\<^sub>w], ss_st := Some (\ B\<^sub>n\<^sub>e\<^sub>w)\" - -subsubsection \ Broadcast messages \ +private fun + extend_chain :: " + ('skey, 'vkey, 'hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig, 'nonce) stakeholder_state \ + slot \ + ('vrf\<^sub>y, 'vrf\<^sub>\) vrf\<^sub>o \ + ('skey, 'vkey, 'hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig, 'nonce) stakeholder_state" +where + "extend_chain ss sl v = ( + let + B\<^sub>n\<^sub>e\<^sub>w = make_block ss sl v + in + ss + \ + ss_\ := ss_\ ss @ [B\<^sub>n\<^sub>e\<^sub>w], + ss_st := Some (\\<^sub>B B\<^sub>n\<^sub>e\<^sub>w), + ss_txs := [] + \)" text \ - In addition to broadcasting transactions and blockchains, we also assume that there is a ``clock - process'' broadcasting the next slot at the end of each current slot, see Section - \ref{sec:semi-sync-model-ref}: + We can easily define a function to store a given transaction in the transactions mempool of a + stakeholder's state: \ -datatype broadcast_msg = - BroadcastTx (bm_tx: transaction) - | BroadcastChain (bm_\: blockchain) - | BroadcastEndSlot (bm_sl: slot) +private definition + store_tx :: " + ('skey, 'vkey, 'hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig, 'nonce) stakeholder_state \ + 'sig transaction \ + ('skey, 'vkey, 'hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig, 'nonce) stakeholder_state" +where + [simp]: "store_tx ss tx = ss\ss_txs := tx # ss_txs ss\" -instance broadcast_msg :: countable - by countable_datatype +text \ + Also, we define a function to store a given chain in the chains mempool of a stakeholder's state, + after pruning blocks belonging to future slots in the chain, and provided that the pruned chain + is valid: +\ + +private fun + store_chain :: " + slot \ + ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) 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" +where + "store_chain sl \ ss = ( + let + \\<^sub>p = prune_after sl \ + in + if + verify_chain \\<^sub>p (ss_G ss) (ss_\ ss) + then + ss\ss_\ := \\<^sub>p # ss_\ ss\ + else + ss)" -type_synonym broadcast_channel = "broadcast_msg channel" +text \ + We define a function to compute the new epoch nonce and store it in the stakeholder's state: +\ -subsubsection \ The stakeholder process \ +private fun + compute_new_epoch_randomness :: " + slot \ + ('skey, 'vkey, 'hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig, 'nonce) stakeholder_state \ + ('skey, 'vkey, 'hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig, 'nonce) stakeholder_state" +where + "compute_new_epoch_randomness sl\<^sub>n\<^sub>e\<^sub>x\<^sub>t ss = ( + let + j = slot_epoch sl\<^sub>n\<^sub>e\<^sub>x\<^sub>t + in + ss\ss_\ := next_epoch_nonce (ss_\ ss) j (ss_\ ss)\)" text \ - \label{sec:sh-process-ref} - Now we are ready to define the process representing a stakeholder running the protocol: + We define a function to update the current best chain in a stakeholder's state to the longest + chain seen so far by the stakeholder: \ -corec (friend) start_of_slot :: " - broadcast_channel - \ stakeholder_state - \ slot - \ (broadcast_channel \ stakeholder_state \ slot \ process) - \ process" +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" where - "start_of_slot bc ss sl cont = ( + "update_local_chain ss = ( let - T\<^sub>i = T(ss_id ss, slot_epoch sl, ss_G ss, ss_\ ss) + \\<^sub>m\<^sub>a\<^sub>x = max_valid (ss_\ ss) (ss_\ ss) in - case is_slot_leader sl (ss_sk\<^sub>v\<^sub>r\<^sub>f ss) (ss_\ ss) T\<^sub>i of - None \ \ \ cont bc ss sl \ \\\ \\ is added to fulfill corecursive function requirements\ + ss\ + ss_\ := \\<^sub>m\<^sub>a\<^sub>x, + ss_st := Some (\\<^sub>B (last \\<^sub>m\<^sub>a\<^sub>x)), \ \ update `state' with hash of best chain's head \ + ss_\ := [] \ \ empty chains mempool \ + \)" + +text \ + We define a process that is executed when an end-of-slot signal is received and that basically + checks whether the associated stakeholder is a slot leader for the current slot, and, if so, + extends its current chain, broadcasts it to the network, and runs a continuation process: +\ + +private abbreviation + start_of_slot :: " + ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) broadcast_channel \ + ('skey, 'vkey, 'hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig, 'nonce) stakeholder_state \ + slot \ + (('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) broadcast_channel \ + ('skey, 'vkey, 'hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig, 'nonce) stakeholder_state \ slot \ process) \ + process" +where + "start_of_slot bc ss sl \ \ ( + let + (U, sk\<^sub>v\<^sub>r\<^sub>f, \, (_, \\<^sub>0, _), \) = (ss_id ss, ss_sk\<^sub>v\<^sub>r\<^sub>f ss, ss_\ ss, ss_G ss, ss_\ ss) + in ( + case is_slot_leader U sl sk\<^sub>v\<^sub>r\<^sub>f \ \\<^sub>0 \ of + None \ + \ \ \ bc ss sl \ \\\ \\ is added to fulfill corecursive function requirements\ | Some v \ let - B\<^sub>n\<^sub>e\<^sub>w = make_block ss sl v; - ss' = extend_chain ss B\<^sub>n\<^sub>e\<^sub>w; - ss'' = ss'\ss_txs := []\ + ss' = extend_chain ss sl v in - bc \\ BroadcastChain (ss_\ ss'') \ cont bc ss'' sl)" + bc \\ BroadcastChain (ss_\ ss') \ \ bc ss' sl))" + +text \ + Then we define a process that executes the `main loop' of the protocol: +\ -corec main_loop :: "broadcast_channel \ stakeholder_state \ slot \ process" where +private corec + main_loop :: " + ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) broadcast_channel \ + ('skey, 'vkey, 'hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig, 'nonce) stakeholder_state \ + slot \ + process" +where "main_loop bc ss sl = bc \\ msg. ( case msg of BroadcastTx tx \ ( + \ \Store new transaction\ let - ss' = ss\ss_txs := tx # ss_txs ss\ + ss' = store_tx ss tx in main_loop bc ss' sl) | BroadcastChain \ \ ( + \ \Store new chain\ let - \\<^sub>p = prune_after sl \; \ \pruned blocks belonging to future slots\ - ss' = if verify_chain \\<^sub>p (ss_G ss) (ss_\ ss) then ss\ss_\ := \\<^sub>p # ss_\ ss\ else ss + ss' = store_chain sl \ ss in main_loop bc ss' sl) | BroadcastEndSlot sl\<^sub>n\<^sub>e\<^sub>x\<^sub>t \ ( let - \ \If new epoch, compute epoch randomness\ - ss' = if first_in_epoch sl\<^sub>n\<^sub>e\<^sub>x\<^sub>t then ss\ss_\ := new_epoch_rnd\ else ss; + \ \If new epoch, compute and store new epoch randomness\ + ss' = if first_in_epoch sl\<^sub>n\<^sub>e\<^sub>x\<^sub>t then compute_new_epoch_randomness sl\<^sub>n\<^sub>e\<^sub>x\<^sub>t ss else ss; \ \Update local chain\ - \\<^sub>m\<^sub>a\<^sub>x = max_valid (ss_\ ss') (ss_\ ss'); - ss'' = ss'\ss_\ := \\<^sub>m\<^sub>a\<^sub>x, ss_st := Some (\ (last \\<^sub>m\<^sub>a\<^sub>x)), ss_\ := []\ + ss' = update_local_chain ss' in - start_of_slot bc ss'' sl\<^sub>n\<^sub>e\<^sub>x\<^sub>t main_loop))" - -abbreviation stakeholder :: " - stakeholder_id - \ genesis - \ secret_key - \ secret_key - \ secret_key - \ broadcast_channel - \ process" -where - "stakeholder U\<^sub>i G sk\<^sub>v\<^sub>r\<^sub>f sk\<^sub>k\<^sub>e\<^sub>s sk\<^sub>d\<^sub>s\<^sub>i\<^sub>g bc \ + start_of_slot bc ss' sl\<^sub>n\<^sub>e\<^sub>x\<^sub>t main_loop))" + +text \ + Finally, we define a process that implements a stakeholder running the protocol: +\ + +fun + stakeholder :: " + stakeholder_id \ + ('vkey, 'nonce) genesis \ + 'skey \ + 'skey \ + 'skey \ + ('hash, 'vrf\<^sub>y, 'vrf\<^sub>\, 'sig) broadcast_channel \ + process" +where + "stakeholder U\<^sub>i G sk\<^sub>v\<^sub>r\<^sub>f sk\<^sub>k\<^sub>e\<^sub>s sk\<^sub>d\<^sub>s\<^sub>i\<^sub>g bc = ( let ss\<^sub>i\<^sub>n\<^sub>i\<^sub>t = init_stakeholder_state U\<^sub>i G sk\<^sub>v\<^sub>r\<^sub>f sk\<^sub>k\<^sub>e\<^sub>s sk\<^sub>d\<^sub>s\<^sub>i\<^sub>g in - start_of_slot bc ss\<^sub>i\<^sub>n\<^sub>i\<^sub>t first_slot main_loop" + start_of_slot bc ss\<^sub>i\<^sub>n\<^sub>i\<^sub>t first_slot main_loop)" + +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