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