Theory Accounts

section‹Accounts›
theory Accounts
imports Valuetypes
begin

type_synonym Balance = Valuetype
 
type_synonym Accounts = "Address ⇒ Balance"

fun emptyAccount :: "Accounts"
where
  "emptyAccount _ = ShowLint 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 ReadLint val ≥ 0
      then (let v = ReadLint (accessBalance acc ad) + ReadLint val
         in if (v < 2^256)
           then Some (updateBalance ad (ShowLint v) acc)
           else None)
      else None)"

lemma addBalance_val:
  assumes "addBalance ad val acc = Some acc'"
    shows "ReadLint (accessBalance acc ad) + ReadLint 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. ReadLint (accessBalance acc ad) ≥ 0 ∧ ReadLint (accessBalance acc ad) < 2 ^ 256"
   shows "∀ad. ReadLint (accessBalance acc' ad) ≥ 0 ∧ ReadLint (accessBalance acc' ad) < 2 ^ 256"
proof
  fix ad'
  show "ReadLint (accessBalance acc' ad') ≥ 0 ∧ ReadLint (accessBalance acc' ad') < 2 ^ 256"
  proof (cases "ReadLint val ≥ 0")
    case t1: True
    define v where v_def: "v = ReadLint (accessBalance acc ad) + ReadLint 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 (ShowLint 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 "ReadLint (accessBalance acc' ad) = ReadLint (accessBalance acc ad) + ReadLint val"
proof -
  define v where "v = ReadLint (accessBalance acc ad) + ReadLint val"
  with assms have "acc' = updateBalance ad (ShowLint 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 "ReadLint (accessBalance acc' ad) ≥ ReadLint (accessBalance acc ad)"
proof -
  define v where "v = ReadLint (accessBalance acc ad) + ReadLint val"
  with assms have "acc' = updateBalance ad (ShowLint 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 = ReadLint (accessBalance acc ad) + ReadLint val"
  with assms have "acc' = updateBalance ad (ShowLint 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 ReadLint val ≥ 0
      then (let v = ReadLint (accessBalance acc ad) - ReadLint val
         in if (v ≥ 0)
           then Some (updateBalance ad (ShowLint v) acc)
           else None)
      else None)"

lemma subBalance_val:
  assumes "subBalance ad val acc = Some acc'"
    shows "ReadLint val ≥ 0"
using assms by (simp split:if_split_asm)

lemma subBalance_sub:
  assumes "subBalance ad val acc = Some acc'"
    shows "ReadLint (accessBalance acc' ad) = ReadLint (accessBalance acc ad) - ReadLint val"
proof -
  define v where "v = ReadLint (accessBalance acc ad) - ReadLint val"
  with assms have "acc' = updateBalance ad (ShowLint 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. ReadLint (accessBalance acc ad) ≥ 0 ∧ ReadLint (accessBalance acc ad) < 2 ^ 256"
   shows "∀ad. ReadLint (accessBalance acc' ad) ≥ 0 ∧ ReadLint (accessBalance acc' ad) < 2 ^ 256"
proof
  fix ad'
  show "ReadLint (accessBalance acc' ad') ≥ 0 ∧ ReadLint (accessBalance acc' ad') < 2 ^ 256"
  proof (cases "ReadLint val ≥ 0")
    case t1: True
    define v where v_def: "v = ReadLint (accessBalance acc ad) - ReadLint 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 (ShowLint 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 "ReadLint (accessBalance acc ad) ≥ ReadLint (accessBalance acc' ad)"
proof -
  define v where "v = ReadLint (accessBalance acc ad) - ReadLint val"
  with assms have "acc' = updateBalance ad (ShowLint 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 = ReadLint (accessBalance acc ad) - ReadLint val"
  with assms have "acc' = updateBalance ad (ShowLint 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 "ReadLint 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 "ReadLint val ≥ 0" using subBalance_val[OF *] by simp
qed

lemma transfer_val2:
  assumes "transfer ads addr val acc = Some acc'"
      and "ads ≠ addr"
    shows "ReadLint (accessBalance acc addr) + ReadLint 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 "ReadLint (accessBalance acc'' addr) + ReadLint 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 "ReadLint (accessBalance acc' addr) = ReadLint (accessBalance acc addr) + ReadLint 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 "ReadLint (accessBalance acc addr) = ReadLint (accessBalance acc'' addr)" using subBalance_eq[OF *] by simp
  moreover have "ReadLint (accessBalance acc' addr) = ReadLint (accessBalance acc'' addr) + ReadLint 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 "ReadLint (accessBalance acc' ads) = ReadLint (accessBalance acc ads) - ReadLint 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 "ReadLint (accessBalance acc'' ads) = ReadLint (accessBalance acc ads) - ReadLint val" using subBalance_sub[OF *] by simp
  moreover from assms(2) have "ReadLint (accessBalance acc' ads) = ReadLint (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 "ReadLint (accessBalance acc' addr) ≥ ReadLint (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 (ShowLint (ReadLint (accessBalance acc addr) - ReadLint val)) acc" by (simp add:Let_def split: if_split_asm)
    moreover from ** have "acc'=updateBalance addr (ShowLint (ReadLint (accessBalance acc'' addr) + ReadLint 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 "ReadLint (accessBalance acc addr) ≤ ReadLint (accessBalance acc'' addr)" using subBalance_eq[OF *] by simp
    also have "… ≤ ReadLint (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 "ReadLint (accessBalance acc' ad) = ReadLint (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 "ReadLint (accessBalance acc' ad) = ReadLint (accessBalance acc'' ad)" using addBalance_eq[OF **] by simp
  also from assms(2) have "… = ReadLint (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. ReadLint (accessBalance acc ad) ≥ 0 ∧ ReadLint (accessBalance acc ad) < 2 ^ 256"
   shows "∀ad. ReadLint (accessBalance acc' ad) ≥ 0 ∧ ReadLint (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 "ReadLint (accessBalance acc' ad') ≥ 0 ∧ ReadLint (accessBalance acc' ad') < 2 ^ 256"
    using addBalance_limit by presburger
qed

end