Theory Merkle_Interface
theory Merkle_Interface
imports
Main
"HOL-Library.Conditional_Parametricity"
"HOL-Library.Monad_Syntax"
begin
alias vimage2p = BNF_Def.vimage2p
alias Grp = BNF_Def.Grp
alias setl = Basic_BNFs.setl
alias setr = Basic_BNFs.setr
alias fsts = Basic_BNFs.fsts
alias snds = Basic_BNFs.snds
attribute_setup locale_witness = ‹Scan.succeed Locale.witness_add›
lemma vimage2p_mono': "R ≤ S ⟹ vimage2p f g R ≤ vimage2p f g S"
by(auto simp add: vimage2p_def le_fun_def)
lemma vimage2p_map_rel_prod:
"vimage2p (map_prod f g) (map_prod f' g') (rel_prod A B) = rel_prod (vimage2p f f' A) (vimage2p g g' B)"
by(simp add: vimage2p_def prod.rel_map)
lemma vimage2p_map_list_all2:
"vimage2p (map f) (map g) (list_all2 A) = list_all2 (vimage2p f g A)"
by(simp add: vimage2p_def list.rel_map)
lemma equivclp_least:
assumes le: "r ≤ s" and s: "equivp s"
shows "equivclp r ≤ s"
apply(rule predicate2I)
subgoal by(induction rule: equivclp_induct)(auto 4 3 intro: equivp_reflp[OF s] equivp_transp[OF s] equivp_symp[OF s] le[THEN predicate2D])
done
lemma reflp_eq_onp: "reflp R ⟷ eq_onp (λx. True) ≤ R"
by(auto simp add: reflp_def eq_onp_def)
lemma eq_onpE:
assumes "eq_onp P x y"
obtains "x = y" "P y"
using assms by(auto simp add: eq_onp_def)
lemma case_unit_parametric [transfer_rule]: "rel_fun A (rel_fun (=) A) case_unit case_unit"
by(simp add: rel_fun_def split: unit.split)
section ‹Authenticated Data Structures›
subsection ‹Interface›
subsubsection ‹ Types ›
type_synonym ('a⇩m, 'a⇩h) hash = "'a⇩m ⇒ 'a⇩h"
type_synonym 'a⇩m blinding_of = "'a⇩m ⇒ 'a⇩m ⇒ bool"
type_synonym 'a⇩m merge = "'a⇩m ⇒ 'a⇩m ⇒ 'a⇩m option"
subsubsection ‹ Properties ›
locale merkle_interface =
fixes h :: "('a⇩m, 'a⇩h) hash"
and bo :: "'a⇩m blinding_of"
and m :: "'a⇩m merge"
assumes merge_respects_hashes: "h a = h b ⟷ (∃ab. m a b = Some ab)"
and idem: "m a a = Some a"
and commute: "m a b = m b a"
and assoc: "m a b ⤜ m c = m b c ⤜ m a"
and bo_def: "bo a b ⟷ m a b = Some b"
begin
lemma reflp: "reflp bo"
unfolding bo_def by(rule reflpI)(simp add: idem)
lemma antisymp: "antisymp bo"
unfolding bo_def by(rule antisympI)(simp add: commute)
lemma transp: "transp bo"
apply(rule transpI)
subgoal for x y z using assoc[of x y z] by(simp add: commute bo_def)
done
lemma hash: "bo ≤ vimage2p h h (=)"
unfolding bo_def by(auto simp add: vimage2p_def merge_respects_hashes)
lemma join: "m a b = Some ab ⟷ bo a ab ∧ bo b ab ∧ (∀u. bo a u ⟶ bo b u ⟶ bo ab u)"
unfolding bo_def
by (smt Option.bind_cong bind.bind_lunit commute idem merkle_interface.assoc merkle_interface_axioms)
text ‹The equivalence closure of the blinding relation are the equivalence classes of the hash function (the kernel).›
lemma equivclp_blinding_of: "equivclp bo = vimage2p h h (=)" (is "?lhs = ?rhs")
proof(rule antisym)
show "?lhs ≤ ?rhs" by(rule equivclp_least[OF hash])(rule equivp_vimage2p[OF identity_equivp])
show "?rhs ≤ ?lhs" unfolding vimage2p_def
proof(rule predicate2I)
fix x y
assume "h x = h y"
then obtain xy where "m x y = Some xy" unfolding merge_respects_hashes ..
hence "bo x xy" "bo y xy" unfolding join by blast+
hence "equivclp bo x xy" "equivclp bo xy y" by(blast)+
thus "equivclp bo x y" by(rule equivclp_trans)
qed
qed
end
subsection ‹ Auxiliary definitions ›
text ‹ Directly proving that an interface satisfies the specification of a Merkle interface as given
above is difficult. Instead, we provide several layers of auxiliary definitions that can easily be
proved layer-by-layer.
In particular, proving that an interface on recursive datatypes is a Merkle interface requires
induction. As the induction hypothesis only applies to a subset of values of a type, we add
auxiliary definitions equipped with an explicit set @{term A} of values to which the definition
applies. Once the induction proof is complete, we can typically instantiate @{term A} with @{term
UNIV}. In particular, in the induction proof for a layer, we can assume that properties for the
earlier layers hold for ∗‹all› values, not just those in the induction hypothesis.
›
subsubsection ‹ Blinding ›
locale blinding_respects_hashes =
fixes h :: "('a⇩m, 'a⇩h) hash"
and bo :: "'a⇩m blinding_of"
assumes hash: "bo ≤ vimage2p h h (=)"
begin
lemma blinding_hash_eq: "bo x y ⟹ h x = h y"
by(drule hash[THEN predicate2D])(simp add: vimage2p_def)
end
locale blinding_of_on =
blinding_respects_hashes h bo
for A :: "'a⇩m set"
and h :: "('a⇩m, 'a⇩h) hash"
and bo :: "'a⇩m blinding_of"
+ assumes refl: "x ∈ A ⟹ bo x x"
and trans: "⟦ bo x y; bo y z; x ∈ A ⟧ ⟹ bo x z"
and antisym: "⟦ bo x y; bo y x; x ∈ A ⟧ ⟹ x = y"
begin
lemma refl_pointfree: "eq_onp (λx. x ∈ A) ≤ bo"
by(auto elim!: eq_onpE intro: refl)
lemma blinding_respects_hashes: "blinding_respects_hashes h bo" ..
lemmas hash = hash
lemma trans_pointfree: "eq_onp (λx. x ∈ A) OO bo OO bo ≤ bo"
by(auto elim!: eq_onpE intro: trans)
lemma antisym_pointfree: "inf (eq_onp (λx. x ∈ A) OO bo) bo¯¯ ≤ (=)"
by(auto elim!: eq_onpE dest: antisym)
end
subsubsection ‹ Merging ›
text ‹ In general, we prove the properties of blinding before the properties of merging. Thus,
in the following definitions we assume that the blinding properties already hold on @{term UNIV}.
The @{term Ball} restricts the argument of the merge operation on which induction will be done. ›
locale merge_on =
blinding_of_on UNIV h bo
for A :: "'a⇩m set"
and h :: "('a⇩m, 'a⇩h) hash"
and bo :: "'a⇩m blinding_of"
and m :: "'a⇩m merge" +
assumes join: "⟦ h a = h b; a ∈ A ⟧
⟹ ∃ab. m a b = Some ab ∧ bo a ab ∧ bo b ab ∧ (∀u. bo a u ⟶ bo b u ⟶ bo ab u)"
and undefined: "⟦ h a ≠ h b; a ∈ A ⟧ ⟹ m a b = None"
begin
lemma same: "a ∈ A ⟹ m a a = Some a"
using join[of a a] refl[of a] by(auto 4 3 intro: antisym)
lemma blinding_of_antisym_on: "blinding_of_on UNIV h bo" ..
lemma transp: "transp bo"
by(auto intro: transpI trans)
lemmas hash = hash
and refl = refl
and antisym = antisym[OF _ _ UNIV_I]
lemma respects_hashes:
"a ∈ A ⟹ h a = h b ⟷ (∃ab. m a b = Some ab)"
using join undefined
by fastforce
lemma join':
"a ∈ A ⟹ ∀ab. m a b = Some ab ⟷ bo a ab ∧ bo b ab ∧ (∀u. bo a u ⟶ bo b u ⟶ bo ab u)"
using join undefined
by (metis (full_types) hash local.antisym option.distinct(1) option.sel predicate2D vimage2p_def)
lemma merge_on_subset:
"B ⊆ A ⟹ merge_on B h bo m"
by unfold_locales (auto dest: same join undefined)
end
subsection ‹ Interface equality ›
text ‹ Here, we prove that the auxiliary definitions specify the same interface as the original ones.›
lemma merkle_interface_aux: "merkle_interface h bo m = merge_on UNIV h bo m"
(is "?lhs = ?rhs")
proof
show ?rhs if ?lhs
proof
interpret merkle_interface h bo m by(fact that)
show "bo ≤ vimage2p h h (=)" by(fact hash)
show "bo x x" for x using reflp by(simp add: reflp_def)
show "bo x z" if "bo x y" "bo y z" for x y z using transp that by(rule transpD)
show "x = y" if "bo x y" "bo y x" for x y using antisymp that by(rule antisympD)
show "∃ab. m a b = Some ab ∧ bo a ab ∧ bo b ab ∧ (∀u. bo a u ⟶ bo b u ⟶ bo ab u)" if "h a = h b" for a b
using that by(simp add: merge_respects_hashes join)
show "m a b = None" if "h a ≠ h b" for a b using that by(simp add: merge_respects_hashes)
qed
show ?lhs if ?rhs
proof
interpret merge_on UNIV h bo m by(fact that)
show eq: "h a = h b ⟷ (∃ab. m a b = Some ab)" for a b by(simp add: respects_hashes)
show idem: "m a a = Some a" for a by(simp add: same)
show commute: "m a b = m b a" for a b
using join[of a b] join[of b a] undefined antisym by(cases "m a b") force+
have undefined_partitioned: "m a c = None" if "m a b = None" "m b c = Some bc" for a b c bc
using that eq by (metis option.distinct(1) option.exhaust)
have merge_twice: "m a b = Some c ⟹ m a c = Some c" for a b c by (simp add: join')
show "m a b ⤜ m c = m b c ⤜ m a" for a b c
proof(simp split: Option.bind_split; safe)
show "None = m a d" if "m a b = None" "m b c = Some d" for d using that
by(metis undefined_partitioned merge_twice)
show "m c d = None" if "m a b = Some d" "m b c = None" for d using that
by(metis commute merge_twice undefined_partitioned)
next
fix ab bc
assume assms: "m a b = Some ab" "m b c = Some bc"
then obtain cab and abc where cab: "m c ab = Some cab" and abc: "m a bc = Some abc"
using eq[THEN iffD2, OF exI] eq[THEN iffD1] by (metis merge_twice)
thus "m c ab = m a bc" using assms
by(clarsimp simp add: join')(metis UNIV_I abc cab local.antisym local.trans)
qed
show "bo a b ⟷ m a b = Some b" for a b using idem join' by auto
qed
qed
lemma merkle_interfaceI [locale_witness]:
assumes "merge_on UNIV h bo m"
shows "merkle_interface h bo m"
using assms unfolding merkle_interface_aux by auto
lemma (in merkle_interface) merkle_interfaceD: "merge_on UNIV h bo m"
using merkle_interface_aux[of h bo m, symmetric]
by simp unfold_locales
subsection ‹ Parametricity rules ›
context includes lifting_syntax begin
parametric_constant le_fun_parametric[transfer_rule]: le_fun_def
parametric_constant vimage2p_parametric[transfer_rule]: vimage2p_def
parametric_constant blinding_respects_hashes_parametric_aux: blinding_respects_hashes_def
lemma blinding_respects_hashes_parametric [transfer_rule]:
"((A1 ===> A2) ===> (A1 ===> A1 ===> (⟷)) ===> (⟷))
blinding_respects_hashes blinding_respects_hashes"
if [transfer_rule]: "bi_unique A2" "bi_total A1"
by(rule blinding_respects_hashes_parametric_aux that le_fun_parametric | simp add: rel_fun_eq)+
parametric_constant blinding_of_on_axioms_parametric [transfer_rule]:
blinding_of_on_axioms_def[folded Ball_def, unfolded le_fun_def le_bool_def eq_onp_def relcompp.simps, simplified]
parametric_constant blinding_of_on_parametric [transfer_rule]: blinding_of_on_def
parametric_constant antisymp_parametric[transfer_rule]: antisymp_def
parametric_constant transp_parametric[transfer_rule]: transp_def
parametric_constant merge_on_axioms_parametric [transfer_rule]: merge_on_axioms_def
parametric_constant merge_on_parametric[transfer_rule]: merge_on_def
parametric_constant merkle_interface_parametric[transfer_rule]: merkle_interface_def
end
end