Theory Accounts
section‹Accounts›
theory Accounts
imports Valuetypes
begin
type_synonym Balance = Valuetype
type_synonym Accounts = "Address ⇒ Balance"
fun emptyAccount :: "Accounts"
where
"emptyAccount _ = ShowL⇩i⇩n⇩t 0"
fun accessBalance :: "Accounts ⇒ Address ⇒ Balance"
where
"accessBalance acc ad = acc ad"
fun updateBalance :: "Address ⇒ Balance ⇒ Accounts ⇒ Accounts"
where
"updateBalance ad bal acc = (λi. (if i = ad then bal else acc i))"
fun addBalance :: "Address ⇒ Valuetype ⇒ Accounts ⇒ Accounts option"
where
"addBalance ad val acc =
(if ReadL⇩i⇩n⇩t val ≥ 0
then (let v = ReadL⇩i⇩n⇩t (accessBalance acc ad) + ReadL⇩i⇩n⇩t val
in if (v < 2^256)
then Some (updateBalance ad (ShowL⇩i⇩n⇩t v) acc)
else None)
else None)"
lemma addBalance_val:
assumes "addBalance ad val acc = Some acc'"
shows "ReadL⇩i⇩n⇩t (accessBalance acc ad) + ReadL⇩i⇩n⇩t val < 2^256"
using assms by (simp add:Let_def split:if_split_asm)
lemma addBalance_limit:
assumes "addBalance ad val acc = Some acc'"
and "∀ad. ReadL⇩i⇩n⇩t (accessBalance acc ad) ≥ 0 ∧ ReadL⇩i⇩n⇩t (accessBalance acc ad) < 2 ^ 256"
shows "∀ad. ReadL⇩i⇩n⇩t (accessBalance acc' ad) ≥ 0 ∧ ReadL⇩i⇩n⇩t (accessBalance acc' ad) < 2 ^ 256"
proof
fix ad'
show "ReadL⇩i⇩n⇩t (accessBalance acc' ad') ≥ 0 ∧ ReadL⇩i⇩n⇩t (accessBalance acc' ad') < 2 ^ 256"
proof (cases "ReadL⇩i⇩n⇩t val ≥ 0")
case t1: True
define v where v_def: "v = ReadL⇩i⇩n⇩t (accessBalance acc ad) + ReadL⇩i⇩n⇩t val"
with assms(2) have "v ≥0" by (simp add: t1)
then show ?thesis
proof (cases "v < 2^256")
case t2: True
with t1 v_def have "addBalance ad val acc = Some (updateBalance ad (ShowL⇩i⇩n⇩t v) acc)" by simp
with t2 `v ≥0` show ?thesis using assms Read_ShowL_id by auto
next
case False
with t1 v_def show ?thesis using assms(1) by simp
qed
next
case False
then show ?thesis using assms(1) by simp
qed
qed
lemma addBalance_add:
assumes "addBalance ad val acc = Some acc'"
shows "ReadL⇩i⇩n⇩t (accessBalance acc' ad) = ReadL⇩i⇩n⇩t (accessBalance acc ad) + ReadL⇩i⇩n⇩t val"
proof -
define v where "v = ReadL⇩i⇩n⇩t (accessBalance acc ad) + ReadL⇩i⇩n⇩t val"
with assms have "acc' = updateBalance ad (ShowL⇩i⇩n⇩t v) acc" by (simp add:Let_def split:if_split_asm)
thus ?thesis using v_def Read_ShowL_id assms by (simp split:if_split_asm)
qed
lemma addBalance_mono:
assumes "addBalance ad val acc = Some acc'"
shows "ReadL⇩i⇩n⇩t (accessBalance acc' ad) ≥ ReadL⇩i⇩n⇩t (accessBalance acc ad)"
proof -
define v where "v = ReadL⇩i⇩n⇩t (accessBalance acc ad) + ReadL⇩i⇩n⇩t val"
with assms have "acc' = updateBalance ad (ShowL⇩i⇩n⇩t v) acc" by (simp add:Let_def split:if_split_asm)
thus ?thesis using v_def Read_ShowL_id assms by (simp split:if_split_asm)
qed
lemma addBalance_eq:
assumes "addBalance ad val acc = Some acc'"
and "ad ≠ ad'"
shows "(accessBalance acc ad') = (accessBalance acc' ad')"
proof -
define v where "v = ReadL⇩i⇩n⇩t (accessBalance acc ad) + ReadL⇩i⇩n⇩t val"
with assms have "acc' = updateBalance ad (ShowL⇩i⇩n⇩t v) acc" by (simp add:Let_def split:if_split_asm)
thus ?thesis using v_def Read_ShowL_id assms by (simp split:if_split_asm)
qed
fun subBalance :: "Address ⇒ Valuetype ⇒ Accounts ⇒ Accounts option"
where
"subBalance ad val acc =
(if ReadL⇩i⇩n⇩t val ≥ 0
then (let v = ReadL⇩i⇩n⇩t (accessBalance acc ad) - ReadL⇩i⇩n⇩t val
in if (v ≥ 0)
then Some (updateBalance ad (ShowL⇩i⇩n⇩t v) acc)
else None)
else None)"
lemma subBalance_val:
assumes "subBalance ad val acc = Some acc'"
shows "ReadL⇩i⇩n⇩t val ≥ 0"
using assms by (simp split:if_split_asm)
lemma subBalance_sub:
assumes "subBalance ad val acc = Some acc'"
shows "ReadL⇩i⇩n⇩t (accessBalance acc' ad) = ReadL⇩i⇩n⇩t (accessBalance acc ad) - ReadL⇩i⇩n⇩t val"
proof -
define v where "v = ReadL⇩i⇩n⇩t (accessBalance acc ad) - ReadL⇩i⇩n⇩t val"
with assms have "acc' = updateBalance ad (ShowL⇩i⇩n⇩t v) acc" by (simp add:Let_def split:if_split_asm)
thus ?thesis using v_def Read_ShowL_id assms by (simp split:if_split_asm)
qed
lemma subBalance_limit:
assumes "subBalance ad val acc = Some acc'"
and "∀ad. ReadL⇩i⇩n⇩t (accessBalance acc ad) ≥ 0 ∧ ReadL⇩i⇩n⇩t (accessBalance acc ad) < 2 ^ 256"
shows "∀ad. ReadL⇩i⇩n⇩t (accessBalance acc' ad) ≥ 0 ∧ ReadL⇩i⇩n⇩t (accessBalance acc' ad) < 2 ^ 256"
proof
fix ad'
show "ReadL⇩i⇩n⇩t (accessBalance acc' ad') ≥ 0 ∧ ReadL⇩i⇩n⇩t (accessBalance acc' ad') < 2 ^ 256"
proof (cases "ReadL⇩i⇩n⇩t val ≥ 0")
case t1: True
define v where v_def: "v = ReadL⇩i⇩n⇩t (accessBalance acc ad) - ReadL⇩i⇩n⇩t val"
with assms(2) t1 have "v < 2 ^ 256" by (smt (verit))
then show ?thesis
proof (cases "v ≥ 0")
case t2: True
with t1 v_def have "subBalance ad val acc = Some (updateBalance ad (ShowL⇩i⇩n⇩t v) acc)" by simp
with t2 `v < 2 ^ 256` show ?thesis using assms Read_ShowL_id by auto
next
case False
with t1 v_def show ?thesis using assms(1) by simp
qed
next
case False
then show ?thesis using assms(1) by simp
qed
qed
lemma subBalance_mono:
assumes "subBalance ad val acc = Some acc'"
shows "ReadL⇩i⇩n⇩t (accessBalance acc ad) ≥ ReadL⇩i⇩n⇩t (accessBalance acc' ad)"
proof -
define v where "v = ReadL⇩i⇩n⇩t (accessBalance acc ad) - ReadL⇩i⇩n⇩t val"
with assms have "acc' = updateBalance ad (ShowL⇩i⇩n⇩t v) acc" by (simp add:Let_def split:if_split_asm)
thus ?thesis using v_def Read_ShowL_id assms by (simp split:if_split_asm)
qed
lemma subBalance_eq:
assumes "subBalance ad val acc = Some acc'"
and "ad ≠ ad'"
shows "(accessBalance acc ad') = (accessBalance acc' ad')"
proof -
define v where "v = ReadL⇩i⇩n⇩t (accessBalance acc ad) - ReadL⇩i⇩n⇩t val"
with assms have "acc' = updateBalance ad (ShowL⇩i⇩n⇩t v) acc" by (simp add:Let_def split:if_split_asm)
thus ?thesis using v_def Read_ShowL_id assms by (simp split:if_split_asm)
qed
fun transfer :: "Address ⇒ Address ⇒ Valuetype ⇒ Accounts ⇒ Accounts option"
where
"transfer ads addr val acc =
(case subBalance ads val acc of
Some acc' ⇒ addBalance addr val acc'
| None ⇒ None)"
lemma transfer_val1:
assumes "transfer ads addr val acc = Some acc'"
shows "ReadL⇩i⇩n⇩t val ≥ 0"
proof -
from assms(1) obtain acc''
where *: "subBalance ads val acc = Some acc''"
and **: "addBalance addr val acc'' = Some acc'" by (simp split:if_split_asm)
then show "ReadL⇩i⇩n⇩t val ≥ 0" using subBalance_val[OF *] by simp
qed
lemma transfer_val2:
assumes "transfer ads addr val acc = Some acc'"
and "ads ≠ addr"
shows "ReadL⇩i⇩n⇩t (accessBalance acc addr) + ReadL⇩i⇩n⇩t val < 2^256"
proof -
from assms(1) obtain acc''
where *: "subBalance ads val acc = Some acc''"
and **: "addBalance addr val acc'' = Some acc'" by (simp split:if_split_asm)
then have "ReadL⇩i⇩n⇩t (accessBalance acc'' addr) + ReadL⇩i⇩n⇩t val < 2^256" using addBalance_val[OF **] by simp
with * show ?thesis using assms(2) subBalance_eq[OF *] by simp
qed
lemma transfer_add:
assumes "transfer ads addr val acc = Some acc'"
and "addr ≠ ads"
shows "ReadL⇩i⇩n⇩t (accessBalance acc' addr) = ReadL⇩i⇩n⇩t (accessBalance acc addr) + ReadL⇩i⇩n⇩t val"
proof -
from assms(1) obtain acc''
where *: "subBalance ads val acc = Some acc''"
and **: "addBalance addr val acc'' = Some acc'" by (simp split:if_split_asm)
with assms(2) have "ReadL⇩i⇩n⇩t (accessBalance acc addr) = ReadL⇩i⇩n⇩t (accessBalance acc'' addr)" using subBalance_eq[OF *] by simp
moreover have "ReadL⇩i⇩n⇩t (accessBalance acc' addr) = ReadL⇩i⇩n⇩t (accessBalance acc'' addr) + ReadL⇩i⇩n⇩t val" using addBalance_add[OF **] by simp
ultimately show ?thesis using Read_ShowL_id by simp
qed
lemma transfer_sub:
assumes "transfer ads addr val acc = Some acc'"
and "addr ≠ ads"
shows "ReadL⇩i⇩n⇩t (accessBalance acc' ads) = ReadL⇩i⇩n⇩t (accessBalance acc ads) - ReadL⇩i⇩n⇩t val"
proof -
from assms(1) obtain acc''
where *: "subBalance ads val acc = Some acc''"
and **: "addBalance addr val acc'' = Some acc'" by (simp split:if_split_asm)
then have "ReadL⇩i⇩n⇩t (accessBalance acc'' ads) = ReadL⇩i⇩n⇩t (accessBalance acc ads) - ReadL⇩i⇩n⇩t val" using subBalance_sub[OF *] by simp
moreover from assms(2) have "ReadL⇩i⇩n⇩t (accessBalance acc' ads) = ReadL⇩i⇩n⇩t (accessBalance acc'' ads)" using addBalance_eq[OF **] by simp
ultimately show ?thesis using Read_ShowL_id by simp
qed
lemma transfer_mono:
assumes "transfer ads addr val acc = Some acc'"
shows "ReadL⇩i⇩n⇩t (accessBalance acc' addr) ≥ ReadL⇩i⇩n⇩t (accessBalance acc addr)"
proof -
from assms(1) obtain acc''
where *: "subBalance ads val acc = Some acc''"
and **: "addBalance addr val acc'' = Some acc'" by (simp split:if_split_asm)
show ?thesis
proof (cases "addr = ads")
case True
with * have "acc'' = updateBalance addr (ShowL⇩i⇩n⇩t (ReadL⇩i⇩n⇩t (accessBalance acc addr) - ReadL⇩i⇩n⇩t val)) acc" by (simp add:Let_def split: if_split_asm)
moreover from ** have "acc'=updateBalance addr (ShowL⇩i⇩n⇩t (ReadL⇩i⇩n⇩t (accessBalance acc'' addr) + ReadL⇩i⇩n⇩t val)) acc''" by (simp add:Let_def split: if_split_asm)
ultimately show ?thesis using Read_ShowL_id by auto
next
case False
then have "ReadL⇩i⇩n⇩t (accessBalance acc addr) ≤ ReadL⇩i⇩n⇩t (accessBalance acc'' addr)" using subBalance_eq[OF *] by simp
also have "… ≤ ReadL⇩i⇩n⇩t (accessBalance acc' addr)" using addBalance_mono[OF **] by simp
finally show ?thesis .
qed
qed
lemma transfer_eq:
assumes "transfer ads addr val acc = Some acc'"
and "ad ≠ ads"
and "ad ≠ addr"
shows "ReadL⇩i⇩n⇩t (accessBalance acc' ad) = ReadL⇩i⇩n⇩t (accessBalance acc ad)"
proof -
from assms(1) obtain acc''
where *: "subBalance ads val acc = Some acc''"
and **: "addBalance addr val acc'' = Some acc'" by (simp split:if_split_asm)
from assms(3) have "ReadL⇩i⇩n⇩t (accessBalance acc' ad) = ReadL⇩i⇩n⇩t (accessBalance acc'' ad)" using addBalance_eq[OF **] by simp
also from assms(2) have "… = ReadL⇩i⇩n⇩t (accessBalance acc ad)" using subBalance_eq[OF *] by simp
finally show ?thesis .
qed
lemma transfer_limit:
assumes "transfer ads addr val acc = Some acc'"
and "∀ad. ReadL⇩i⇩n⇩t (accessBalance acc ad) ≥ 0 ∧ ReadL⇩i⇩n⇩t (accessBalance acc ad) < 2 ^ 256"
shows "∀ad. ReadL⇩i⇩n⇩t (accessBalance acc' ad) ≥ 0 ∧ ReadL⇩i⇩n⇩t (accessBalance acc' ad) < 2 ^ 256"
proof
fix ad'
from assms(1) obtain acc'' where "subBalance ads val acc = Some acc''" and "addBalance addr val acc'' = Some acc'" by (simp split: if_split_asm)
with subBalance_limit[OF _ assms(2)]
show "ReadL⇩i⇩n⇩t (accessBalance acc' ad') ≥ 0 ∧ ReadL⇩i⇩n⇩t (accessBalance acc' ad') < 2 ^ 256"
using addBalance_limit by presburger
qed
end