View on GitHub
File Changes
-
section \<open> No Double-Spending Property \<close>
-

                      
-
theory Ledger_Rules
-
  imports Main
-
begin
-

                      
-
subsection \<open> Non-standard map operators \<close>
-
definition dom_exc :: "'a set \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" ("_ \<lhd>'/ _" [61, 61] 60) where
-
  "s \<lhd>/ m = m |` (- s)"
-

                      
-
lemma dom_exc_distr: "(s\<^sub>1 \<union> s\<^sub>2) \<lhd>/ m = s\<^sub>1 \<lhd>/ (s\<^sub>2 \<lhd>/ m)"
-
  by (simp add: dom_exc_def inf_commute)
-

                      
-
lemma dom_exc_assoc: 
-
  assumes "dom m\<^sub>1 \<inter> dom m\<^sub>2 = {}"
-
  and "s \<inter> dom m\<^sub>2 = {}"
-
  shows "(s \<lhd>/ m\<^sub>1) ++ m\<^sub>2 = s \<lhd>/ (m\<^sub>1 ++ m\<^sub>2)"
-
  using assms
-
proof -
-
  have "dom (s \<lhd>/ m\<^sub>1) \<inter> dom m\<^sub>2 = {}"
-
    by (simp add: assms(1) dom_exc_def inf_commute inf_left_commute)
-
  then have rtl: "(s \<lhd>/ m\<^sub>1) ++ m\<^sub>2 \<subseteq>\<^sub>m s \<lhd>/ (m\<^sub>1 ++ m\<^sub>2)"
-
    by (smt assms(2) disjoint_eq_subset_Compl disjoint_iff_not_equal dom_exc_def map_add_dom_app_simps(1) map_add_dom_app_simps(3) map_le_def restrict_map_def subsetCE) 
-
  moreover have "s \<lhd>/ (m\<^sub>1 ++ m\<^sub>2) \<subseteq>\<^sub>m (s \<lhd>/ m\<^sub>1) ++ m\<^sub>2"
-
    by (smt rtl domIff dom_exc_def map_add_None map_le_def restrict_map_def)
-
  ultimately show ?thesis
-
    using map_le_antisym by blast
-
qed
-

                      
-
subsection \<open> Abstract types \<close>
-

                      
-
typedecl tx_id
-
typedecl ix
-
typedecl addr
-
typedecl tx
-

                      
-
subsection \<open> Derived types \<close>
-

                      
-
type_synonym coin = int
-
type_synonym tx_in = "tx_id \<times> ix"
-
type_synonym tx_out = "addr \<times> coin"
-
type_synonym utxo = "tx_in \<rightharpoonup> tx_out"
-

                      
-
subsection \<open> Transaction Types \<close>
-

                      
-
type_synonym tx_body = "tx_in set \<times> (ix \<rightharpoonup> tx_out)"
-

                      
-
subsection \<open> Abstract functions \<close>
-
fun txid :: "tx \<Rightarrow> tx_id" where
-
  "txid _ = undefined"
-

                      
-
fun txbody :: "tx \<Rightarrow> tx_body" where
-
  "txbody _ = undefined"
-

                      
-
subsection \<open> Accessor functions \<close>
-
fun txins :: "tx \<Rightarrow> tx_in set" where
-
  "txins tx = (let (inputs, _) = txbody tx in inputs)"
-

                      
-
fun txouts :: "tx \<Rightarrow> utxo" where
-
  "txouts tx = (
-
    let (_, outputs) = txbody tx in (
-
    \<lambda>(id, ix). if id \<noteq> txid tx then None else case outputs ix of None \<Rightarrow> None | Some txout \<Rightarrow> Some txout))"
-

                      
-
lemma dom_txouts_is_txid:
-
  shows "\<And>i ix. (i, ix) \<in> dom (txouts tx) \<Longrightarrow> i = txid tx"
-
  by (smt case_prod_conv domIff surj_pair txouts.simps)
-

                      
-
subsection \<open> UTxO transition-system types \<close>
-

                      
-
\<comment> \<open> UTxO environment \<close>
-
typedecl utxo_env \<comment> \<open> Abstract, don't care for now \<close>
-

                      
-
\<comment> \<open> UTxO states \<close>
-
type_synonym utxo_state = utxo \<comment> \<open> Simplified \<close>
-

                      
-
subsection \<open> UTxO inference rules \<close>
-
inductive utxo_sts :: "utxo_env \<Rightarrow> utxo_state \<Rightarrow> tx \<Rightarrow> utxo_state \<Rightarrow> bool"
-
  ("_ \<turnstile> _ \<rightarrow>\<^bsub>UTXO\<^esub>{_} _" [51, 0, 51] 50)
-
  for \<Gamma>
-
  where
-
    utxo_inductive: "
-
      \<lbrakk>
-
        txins tx \<subseteq> dom utxo_st;
-
        txins tx \<noteq> {};
-
        txouts tx \<noteq> Map.empty;
-
        \<forall>(_, c) \<in> ran (txouts tx). c > 0
-
      \<rbrakk>
-
      \<Longrightarrow>
-
      \<Gamma> \<turnstile> utxo_st \<rightarrow>\<^bsub>UTXO\<^esub>{tx} (txins tx \<lhd>/ utxo_st) ++ txouts tx"
-

                      
-
subsection \<open> Transaction sequences \<close>
-

                      
-
inductive utxows :: "utxo_env \<Rightarrow> utxo_state \<Rightarrow> tx list \<Rightarrow> utxo_state \<Rightarrow> bool"
-
  ("_ \<turnstile> _ \<rightarrow>\<^bsub>UTXOWS\<^esub>{_} _" [51, 0, 51] 50)
-
  for \<Gamma>
-
  where
-
    empty: "\<Gamma> \<turnstile> s \<rightarrow>\<^bsub>UTXOWS\<^esub>{[]} s" |
-
    step: "\<Gamma> \<turnstile> s \<rightarrow>\<^bsub>UTXOWS\<^esub>{txs @ [tx]} s''" if "\<Gamma> \<turnstile> s \<rightarrow>\<^bsub>UTXOWS\<^esub>{txs} s'" and "\<Gamma> \<turnstile> s' \<rightarrow>\<^bsub>UTXO\<^esub>{tx} s''"
-

                      
-
subsection \<open> Auxiliary lemmas and main theorem \<close>
-

                      
-
abbreviation txid_injectivity :: bool where
-
  "txid_injectivity \<equiv> \<forall>tx tx'. txid tx = txid tx' \<longrightarrow> tx = tx'"
-

                      
-
lemma lemma_1:
-
  assumes "\<Gamma> \<turnstile> utxo\<^sub>0 \<rightarrow>\<^bsub>UTXOWS\<^esub>{T} utxo"
-
  and "\<forall>T\<^sub>i \<in> set T. txins T\<^sub>i \<inter> txins tx = {}"
-
  and "dom (txouts tx) \<inter> dom utxo\<^sub>0 = {}"
-
  and txid_injectivity
-
  shows "(\<Union>T\<^sub>i \<in> set T. txins T\<^sub>i) \<inter> dom (txouts tx) = {}"
-
  and "dom (txouts tx) \<inter> dom utxo = {}"
-
  using assms
-
proof (induction rule: utxows.induct)
-
  case (empty s)
-
  { case 1
-
    then show ?case
-
      by force
-
  next
-
    case 2
-
    then show ?case
-
      by blast
-
  }
-
next
-
  case (step utxo\<^sub>0 T utxo tx' utxo')
-
  { case 1
-
    then have "txins tx' \<inter> dom (txouts tx) = {}"
-
    proof -
-
      have "\<forall>T\<^sub>i \<in> set T. txins T\<^sub>i \<inter> txins tx = {}"
-
        using "1.prems"(1) and assms(4) by auto
-
      then have "(\<Union>T\<^sub>i \<in> set T. txins T\<^sub>i) \<inter> dom (txouts tx) = {}"
-
        using step.IH(1) and "1.prems"(2) and assms(4) by simp
-
      moreover have "txins tx' \<subseteq> dom utxo"
-
        using step.hyps(2) and utxo_sts.simps by blast
-
      ultimately show ?thesis
-
        by (smt "1.prems"(2) assms(4) \<open>\<forall>T\<^sub>i\<in>set T. txins T\<^sub>i \<inter> txins tx = {}\<close> inf.orderE inf_bot_right inf_sup_aci(1) inf_sup_aci(2) step.IH(2))
-
    qed
-
    moreover have "(\<Union>T\<^sub>i \<in> set T. txins T\<^sub>i) \<inter> dom (txouts tx) = {}"
-
      using "1.prems" and step.IH(1) by simp
-
    ultimately show ?case
-
      by (smt Int_empty_right SUP_empty UN_Un UN_insert empty_set inf_commute inf_sup_distrib1 list.simps(15) set_append)
-
  next
-
    case 2
-
    then have "dom (txouts tx) \<inter> dom (txins tx' \<lhd>/ utxo) = {}"
-
      by (smt Int_iff butlast_snoc disjoint_iff_not_equal dom_exc_def dom_restrict in_set_butlastD step.IH(2)) 
-
    moreover have "dom (txouts tx) \<inter> dom (txouts tx') = {}"
-
    proof -
-
      have "txins tx' \<inter> txins tx = {}"
-
        using "2.prems"(1) by (meson in_set_conv_decomp)
-
      then have "txins tx' \<noteq> txins tx"
-
        using inf.idem step.hyps(2) utxo_sts.cases by auto
-
      then have "tx' \<noteq> tx"
-
        by blast
-
      then have "txid tx' \<noteq> txid tx"
-
        using assms(4) by blast
-
      then show ?thesis
-
        using dom_txouts_is_txid by (simp add: ComplI disjoint_eq_subset_Compl subrelI)
-
    qed
-
    ultimately have "dom (txouts tx) \<inter> dom ((txins tx' \<lhd>/ utxo) ++ txouts tx') = {}"
-
      by blast
-
    then show ?case
-
      using utxo_sts.simps and step.hyps(2) by simp
-
    }
-
qed
-

                      
-
lemma aux_lemma:
-
  assumes "\<Gamma> \<turnstile> utxo\<^sub>0 \<rightarrow>\<^bsub>UTXOWS\<^esub>{T} utxo"
-
  and "\<Gamma> \<turnstile> utxo \<rightarrow>\<^bsub>UTXO\<^esub>{tx} utxo'"
-
  and "\<forall>T\<^sub>i \<in> set (T @ [tx]). dom (txouts T\<^sub>i) \<inter> dom utxo\<^sub>0 = {}"
-
  and "\<forall>T\<^sub>i \<in> set T. dom (txouts T\<^sub>i) \<inter> dom utxo\<^sub>0 = {} \<Longrightarrow> \<forall>T\<^sub>i \<in> set T. txins T\<^sub>i \<inter> dom utxo = {}"
-
  and txid_injectivity
-
  shows "txins tx \<inter> dom (txouts tx) = {}"
-
  using assms
-
proof -
-
  have "txins tx \<subseteq> dom utxo"
-
    using assms(2) utxo_sts.simps by blast
-
  then have "\<forall>T\<^sub>i \<in> set T. txins T\<^sub>i \<inter> txins tx = {}"
-
    by (smt assms(3) assms(4) butlast_snoc in_set_butlastD inf.orderE inf_bot_right inf_left_commute) 
-
  then have "(\<Union>T\<^sub>i \<in> set T. txins T\<^sub>i) \<inter> dom (txouts tx) = {}" and "dom (txouts tx) \<inter> dom utxo = {}"
-
    using lemma_1 and assms(1-3,5) by auto
-
  then show ?thesis
-
    by (metis (no_types, lifting) disjoint_iff_not_equal assms(2) subsetCE utxo_sts.simps)
-
qed
-

                      
-
lemma lemma_3:
-
  assumes "\<Gamma> \<turnstile> utxo\<^sub>0 \<rightarrow>\<^bsub>UTXOWS\<^esub>{T} utxo"
-
  and "\<forall>T\<^sub>i \<in> set T. dom (txouts T\<^sub>i) \<inter> dom utxo\<^sub>0 = {}"
-
  and txid_injectivity
-
  shows "\<forall>T\<^sub>i \<in> set T. txins T\<^sub>i \<inter> dom utxo = {}"
-
using assms
-
proof (induction rule: utxows.induct)
-
  case (empty s)
-
  then show ?case
-
    by simp
-
next
-
  case (step utxo\<^sub>0 T utxo tx utxo')
-
  then have "\<And>T\<^sub>i. T\<^sub>i \<in> set T \<Longrightarrow> txins T\<^sub>i \<inter> dom utxo' = {}"
-
  proof -
-
    fix T\<^sub>i
-
    assume "T\<^sub>i \<in> set T"
+
section \<open> Proofs \<close>
+

                      
+
theory Ledger_Rules
+
  imports Main
+
begin
+

                      
+
text \<open> Non-standard map operators \<close>
+

                      
+
definition dom_exc :: "'a set \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" ("_ \<lhd>'/ _" [61, 61] 60) where
+
  "s \<lhd>/ m = m |` (- s)"
+

                      
+
lemma dom_exc_unit:
+
  assumes "dom m \<inter> s = {}"
+
  shows "s \<lhd>/ m = m"
+
proof -
+
  have "s \<lhd>/ m \<subseteq>\<^sub>m m"
+
    by (simp add: dom_exc_def map_le_def)
+
  moreover from assms have "m \<subseteq>\<^sub>m s \<lhd>/ m"
+
    by (metis disjoint_eq_subset_Compl dom_exc_def map_le_def restrict_in rev_subsetD)
+
  ultimately show ?thesis
+
    by (simp add: map_le_antisym)
+
qed
+

                      
+
lemma dom_exc_empty:
+
  shows "{} \<lhd>/ m = m"
+
  by (simp add: dom_exc_unit) 
+

                      
+
lemma dom_exc_union_sec:
+
  shows "(s\<^sub>1 \<union> s\<^sub>2) \<lhd>/ m = s\<^sub>1 \<lhd>/ (s\<^sub>2 \<lhd>/ m)"
+
  by (simp add: dom_exc_def inf_commute)
+

                      
+
lemma dom_exc_append_distr:
+
  shows "s \<lhd>/ (m\<^sub>1 ++ m\<^sub>2) = (s \<lhd>/ m\<^sub>1) ++ (s \<lhd>/ m\<^sub>2)"
+
proof -
+
  have ltr: "s \<lhd>/ (m\<^sub>1 ++ m\<^sub>2) \<subseteq>\<^sub>m (s \<lhd>/ m\<^sub>1) ++ (s \<lhd>/ m\<^sub>2)"
+
    by (simp add: dom_exc_def map_add_def map_le_def restrict_map_def)
+
  then have "(s \<lhd>/ m\<^sub>1) ++ (s \<lhd>/ m\<^sub>2) \<subseteq>\<^sub>m s \<lhd>/ (m\<^sub>1 ++ m\<^sub>2)"
+
    by (simp add: dom_exc_def dom_map_add dom_restrict inf_sup_distrib2 map_le_def)
+
  then show ?thesis
+
    by (simp add: ltr map_le_antisym)
+
qed
+

                      
+
lemma dom_exc_assoc:
+
  assumes "dom m\<^sub>1 \<inter> dom m\<^sub>2 = {}"
+
  and "s \<inter> dom m\<^sub>2 = {}"
+
  shows "(s \<lhd>/ m\<^sub>1) ++ m\<^sub>2 = s \<lhd>/ (m\<^sub>1 ++ m\<^sub>2)"
+
proof -
+
  from assms(1) have "dom (s \<lhd>/ m\<^sub>1) \<inter> dom m\<^sub>2 = {}"
+
    by (simp add: dom_exc_def inf_commute inf_left_commute)
+
  with assms(2) have rtl: "(s \<lhd>/ m\<^sub>1) ++ m\<^sub>2 \<subseteq>\<^sub>m s \<lhd>/ (m\<^sub>1 ++ m\<^sub>2)"
+
    by (smt disjoint_eq_subset_Compl disjoint_iff_not_equal dom_exc_def map_add_dom_app_simps(1) map_add_dom_app_simps(3) map_le_def restrict_map_def subsetCE)
+
  moreover have "s \<lhd>/ (m\<^sub>1 ++ m\<^sub>2) \<subseteq>\<^sub>m (s \<lhd>/ m\<^sub>1) ++ m\<^sub>2"
+
    by (smt rtl domIff dom_exc_def map_add_None map_le_def restrict_map_def)
+
  ultimately show ?thesis
+
    using map_le_antisym by blast
+
qed
+

                      
+
text \<open> Abstract types \<close>
+

                      
+
typedecl tx_id
+
typedecl ix
+
typedecl addr
+
typedecl tx
+

                      
+
text \<open> Derived types \<close>
+

                      
+
type_synonym coin = int
+
type_synonym tx_in = "tx_id \<times> ix"
+
type_synonym tx_out = "addr \<times> coin"
+
type_synonym utxo = "tx_in \<rightharpoonup> tx_out"
+

                      
+
text \<open> Transaction Types \<close>
+

                      
+
type_synonym tx_body = "tx_in set \<times> (ix \<rightharpoonup> tx_out)"
+

                      
+
text \<open> Abstract functions \<close>
+

                      
+
fun txid :: "tx \<Rightarrow> tx_id" where
+
  "txid _ = undefined"
+

                      
+
fun txbody :: "tx \<Rightarrow> tx_body" where
+
  "txbody _ = undefined"
+

                      
+
text \<open> Accessor functions \<close>
+

                      
+
fun txins :: "tx \<Rightarrow> tx_in set" where
+
  "txins tx = (let (inputs, _) = txbody tx in inputs)"
+

                      
+
fun txouts :: "tx \<Rightarrow> utxo" where
+
  "txouts tx = (
+
    let (_, outputs) = txbody tx in (
+
    \<lambda>(id, ix). if id \<noteq> txid tx then None else case outputs ix of None \<Rightarrow> None | Some txout \<Rightarrow> Some txout))"
+

                      
+
lemma dom_txouts_is_txid:
+
  shows "\<And>i ix. (i, ix) \<in> dom (txouts tx) \<Longrightarrow> i = txid tx"
+
  by (smt case_prod_conv domIff surj_pair txouts.simps)
+

                      
+
text \<open> UTxO transition-system types \<close>
+

                      
+
\<comment> \<open> UTxO environment \<close>
+
typedecl utxo_env \<comment> \<open> Abstract, don't care for now \<close>
+

                      
+
\<comment> \<open> UTxO states \<close>
+
type_synonym utxo_state = utxo \<comment> \<open> Simplified \<close>
+

                      
+
text \<open> UTxO inference rules \<close>
+

                      
+
inductive utxo_sts :: "utxo_env \<Rightarrow> utxo_state \<Rightarrow> tx \<Rightarrow> utxo_state \<Rightarrow> bool"
+
  ("_ \<turnstile> _ \<rightarrow>\<^bsub>UTXO\<^esub>{_} _" [51, 0, 51] 50)
+
  for \<Gamma>
+
  where
+
    utxo_inductive: "
+
      \<lbrakk>
+
        txins tx \<subseteq> dom utxo_st;
+
        txins tx \<noteq> {};
+
        txouts tx \<noteq> Map.empty;
+
        \<forall>(_, c) \<in> ran (txouts tx). c > 0
+
      \<rbrakk>
+
      \<Longrightarrow>
+
      \<Gamma> \<turnstile> utxo_st \<rightarrow>\<^bsub>UTXO\<^esub>{tx} (txins tx \<lhd>/ utxo_st) ++ txouts tx"
+

                      
+
text \<open> Transaction sequences \<close>
+

                      
+
inductive utxows :: "utxo_env \<Rightarrow> utxo_state \<Rightarrow> tx list \<Rightarrow> utxo_state \<Rightarrow> bool"
+
  ("_ \<turnstile> _ \<rightarrow>\<^bsub>UTXOWS\<^esub>{_} _" [51, 0, 51] 50)
+
  for \<Gamma>
+
  where
+
    empty: "\<Gamma> \<turnstile> s \<rightarrow>\<^bsub>UTXOWS\<^esub>{[]} s" |
+
    step: "\<Gamma> \<turnstile> s \<rightarrow>\<^bsub>UTXOWS\<^esub>{txs @ [tx]} s''" if "\<Gamma> \<turnstile> s \<rightarrow>\<^bsub>UTXOWS\<^esub>{txs} s'" and "\<Gamma> \<turnstile> s' \<rightarrow>\<^bsub>UTXO\<^esub>{tx} s''"
+

                      
+
text \<open> Auxiliary lemmas \<close>
+

                      
+
abbreviation txid_injectivity :: bool where
+
  "txid_injectivity \<equiv> \<forall>tx tx'. txid tx = txid tx' \<longrightarrow> tx = tx'"
+

                      
+
lemma lemma_1:
+
  assumes "\<Gamma> \<turnstile> utxo\<^sub>0 \<rightarrow>\<^bsub>UTXOWS\<^esub>{T} utxo"
+
  and "\<forall>T\<^sub>i \<in> set T. txins T\<^sub>i \<inter> txins tx = {}"
+
  and "dom (txouts tx) \<inter> dom utxo\<^sub>0 = {}"
+
  and txid_injectivity
+
  shows "(\<Union>T\<^sub>i \<in> set T. txins T\<^sub>i) \<inter> dom (txouts tx) = {}"
+
  and "dom (txouts tx) \<inter> dom utxo = {}"
+
  using assms
+
proof (induction rule: utxows.induct)
+
  case (empty s)
+
  { case 1
+
    then show ?case
+
      by force
+
  next
+
    case 2
+
    then show ?case
+
      by blast
+
  }
+
next
+
  case (step utxo\<^sub>0 T utxo tx' utxo')
+
  { case 1
+
    then have "txins tx' \<inter> dom (txouts tx) = {}"
+
    proof -
+
      from "1.prems"(1) and assms(4) have tx_excl: "\<forall>T\<^sub>i \<in> set T. txins T\<^sub>i \<inter> txins tx = {}"
+
        by auto
+
      with step.IH(1) and "1.prems"(2) and assms(4)
+
      have "(\<Union>T\<^sub>i \<in> set T. txins T\<^sub>i) \<inter> dom (txouts tx) = {}"
+
        by simp
+
      moreover from step.hyps(2) have "txins tx' \<subseteq> dom utxo"
+
        using utxo_sts.simps by blast
+
      ultimately show ?thesis
+
        by (smt "1.prems"(2) assms(4) tx_excl inf.orderE inf_bot_right inf_sup_aci(1) inf_sup_aci(2) step.IH(2))
+
    qed
+
    moreover from "1.prems" and step.IH(1) have "(\<Union>T\<^sub>i \<in> set T. txins T\<^sub>i) \<inter> dom (txouts tx) = {}"
+
      by simp
+
    ultimately show ?case
+
      by (smt Int_empty_right SUP_empty UN_Un UN_insert empty_set inf_commute inf_sup_distrib1 list.simps(15) set_append)
+
  next
+
    case 2
+
    from "2.prems"(1) and assms(4) and step.hyps(2) and step.IH(2)
+
    have "dom (txouts tx) \<inter> dom (txins tx' \<lhd>/ utxo) = {}"
+
      using utxo_sts.simps by auto
+
    moreover have "dom (txouts tx) \<inter> dom (txouts tx') = {}"
+
    proof -
+
      from "2.prems"(1) have "txins tx' \<inter> txins tx = {}"
+
        by (meson in_set_conv_decomp)
+
      with step.hyps(2) have "txins tx' \<noteq> txins tx"
+
        using inf.idem and utxo_sts.cases by auto
+
      then have "tx' \<noteq> tx"
+
        by blast
+
      with assms(4) have "txid tx' \<noteq> txid tx"
+
        by blast
+
      then show ?thesis
+
        using dom_txouts_is_txid by (simp add: ComplI disjoint_eq_subset_Compl subrelI)
+
    qed
+
    ultimately have "dom (txouts tx) \<inter> dom ((txins tx' \<lhd>/ utxo) ++ txouts tx') = {}"
+
      by blast
+
    with step.hyps(2) show ?case
+
      using utxo_sts.simps by simp
+
    }
+
qed
+

                      
+
lemma aux_lemma:
+
  assumes "\<Gamma> \<turnstile> utxo\<^sub>0 \<rightarrow>\<^bsub>UTXOWS\<^esub>{T} utxo"
+
chapter Ledger_Rules
+

                      
+
session Ledger_Rules_Formalization(ledgerrules) = HOL +
+
  description \<open>Formalization of Ledger Rules in Isabelle/HOL\<close>
+
  theories
+
    Ledger_Rules
+
  document_files
+
    "root.tex"
+
\documentclass[a4paper,11pt]{article}
+

                      
+
\usepackage{typearea}
+

                      
+
\usepackage{lmodern}
+
\usepackage[T1]{fontenc}
+
\usepackage{textcomp}
+

                      
+
\usepackage{isabelle,isabellesym}
+

                      
+
\usepackage{latexsym}
+

                      
+
\usepackage{pdfsetup}
+

                      
+
\urlstyle{rm}
+
\isabellestyle{it}
+

                      
+
\begin{document}
+

                      
+
\title{Formalization of the Ledger Rules in Isabelle/HOL}
+
\author{Javier D\'iaz\\\small\texttt{[email protected]}\\\small\texttt{github.com/input-output-hk/fm-ouroboros}}
+

                      
+
\maketitle
+

                      
+
\tableofcontents
+

                      
+
\parindent 0pt\parskip 0.5ex
+

                      
+
\input{session}
+

                      
+
\end{document}
+
build_options = -o document=pdf -g ledgerrules
+

                      
+
properly:
+
	isabelle build $(build_options)
+

                      
+
qnd:
+
	isabelle build -o quick_and_dirty $(build_options)
+
Requirements
+
============
+

                      
+
You need Isabelle2018 to use the Isabelle developments in this
+
directory. You can obtain Isabelle2018 from the [Isabelle
+
website][isabelle].
+

                      
+
[isabelle]:
+
    http://isabelle.in.tum.de/
+
    "Isabelle"
+

                      
+

                      
+
Setup
+
=====
+

                      
+
To make the Isabelle developments in this directory available to your
+
Isabelle installation, please add the path of this directory to the file
+
`$ISABELLE_HOME_USER/ROOTS`. You can find out the value of
+
`$ISABELLE_HOME_USER` by running the following command:
+

                      
+
    isabelle getenv ISABELLE_HOME_USER
+

                      
+

                      
+
Building
+
========
+

                      
+
Running `make` builds the PDF documents for the different Isabelle
+
libraries and places them in `$ISABELLE_BROWSER_INFO/Ledger_Rules`. You can
+
find out the value of `$ISABELLE_BROWSER_INFO` by running the following
+
command:
+

                      
+
    isabelle getenv ISABELLE_BROWSER_INFO
+

                      
+
The makefile specifies two targets: `properly`, which is the default,
+
and `qnd`. With `properly`, fake proofs (`sorry`) are not accepted; with
+
`qnd`, quick-and-dirty mode is used and thus fake proofs are accepted.
+

                      
+
Ledger_Rules_Formalization
\ No newline at end of file