Skip to content
Permalink
Browse files

Introduce value preservation lemma for the SNAP subsystem

  • Loading branch information
javierdiaz72 committed Jan 14, 2020
1 parent 2d4484e commit a185c118f15c544ffdb6583cd2996910e385cd08
Showing with 69 additions and 0 deletions.
  1. +30 −0 Isabelle/Shelley/Properties.thy
  2. +39 −0 Isabelle/Shelley/Rewards.thy
@@ -906,4 +906,34 @@ next
qed
qed

fun val_snap_state :: "snapshot_state \<Rightarrow> coin" where
"val_snap_state (_, utxo_st) = val_utxo_state utxo_st"

lemma snap_value_preservation:
assumes "e \<turnstile> s \<rightarrow>\<^bsub>SNAP\<^esub>{\<epsilon>} s'"
shows "val_snap_state s = val_snap_state s'"
proof -
from assms show ?thesis
proof cases
case (snapshot stake delegations oblg decayed deps pp dstate pstate pstake\<^sub>m\<^sub>a\<^sub>r\<^sub>k pstake\<^sub>s\<^sub>e\<^sub>t pstake\<^sub>g\<^sub>o
pools_ss fee_ss utxo fees up pools_params)
from \<open>s' =
(
((stake, delegations), pstake\<^sub>m\<^sub>a\<^sub>r\<^sub>k, pstake\<^sub>s\<^sub>e\<^sub>t, pools_params, fees + decayed),
(utxo, oblg, fees + decayed, up)
)\<close> have "val_snap_state s' = val_utxo_state (utxo, oblg, fees + decayed, up)"
by simp
also have "\<dots> = val_utxo utxo + oblg + (fees + decayed)"
by simp
also from \<open>decayed = deps - oblg\<close> have "\<dots> = val_utxo utxo + deps + fees"
by simp
also have "\<dots> = val_utxo_state (utxo, deps, fees, up)"
by simp
also from \<open>s = ((pstake\<^sub>m\<^sub>a\<^sub>r\<^sub>k, pstake\<^sub>s\<^sub>e\<^sub>t, pstake\<^sub>g\<^sub>o, pools_ss, fee_ss), (utxo, deps, fees, up))\<close>
have "\<dots> = val_snap_state s"
by simp
finally show ?thesis ..
qed
qed

end
@@ -22,6 +22,13 @@ type_synonym stake = "(key_hash, coin) fmap"

subsection \<open> Snapshot Transition \<close>

text \<open> Snapshots environment \<close>

type_synonym snapshot_env = "
p_params \<times> \<comment> \<open>protocol parameters\<close>
d_state \<times> \<comment> \<open>delegation state\<close>
p_state \<comment> \<open>pool state\<close>"

text \<open> Snapshots \<close>

type_synonym snapshots = "
@@ -31,6 +38,38 @@ type_synonym snapshots = "
(key_hash, pool_param) fmap \<times> \<comment> \<open>pool parameters\<close>
coin \<comment> \<open>fee snapshot\<close>"

text \<open> Snapshots states \<close>

type_synonym snapshot_state = "
snapshots \<times> \<comment> \<open>snapshots\<close>
utxo_state \<comment> \<open>utxo state\<close>"

text \<open> Snapshot Inference Rule \<close>

text \<open>
NOTE:
\<^item> \<open>stake\<close>, \<open>delegations\<close> and \<open>oblg\<close> are not defined since they are not related to the
"preservation of value" property.
\<close>
inductive snap_sts :: "snapshot_env \<Rightarrow> snapshot_state \<Rightarrow> epoch \<Rightarrow> snapshot_state \<Rightarrow> bool"
(\<open>_ \<turnstile> _ \<rightarrow>\<^bsub>SNAP\<^esub>{_} _\<close> [51, 0, 51] 50)
where
snapshot: "
(pp, dstate, pstate) \<turnstile>
(
(pstake\<^sub>m\<^sub>a\<^sub>r\<^sub>k, pstake\<^sub>s\<^sub>e\<^sub>t, pstake\<^sub>g\<^sub>o, pools_ss, fee_ss),
(utxo, deps, fees, up)
)
\<rightarrow>\<^bsub>SNAP\<^esub>{e}
(
((stake, delegations), pstake\<^sub>m\<^sub>a\<^sub>r\<^sub>k, pstake\<^sub>s\<^sub>e\<^sub>t, pools_params, fees + decayed),
(utxo, oblg, fees + decayed, up)
)"
if "stake = undefined"
and "delegations = undefined"
and "oblg = undefined"
and "decayed = deps - oblg"

subsection \<open> Pool Reaping Transition \<close>

text \<open> Pool Reap State \<close>

0 comments on commit a185c11

Please sign in to comment.
You can’t perform that action at this time.