# Bend Bank: the proof of LAW sound
# =================================
#
# Accounts are never removed; a plan's account only drops what it held;
# a gift puts money only under its sender's name, whose account exists;
# a new account holds nothing.

import Base
import ../bank.bend as B
import ../web.bend as W
import ../LAWS.bend as Laws
import ./base.bend as L

# Tries
# -----

# the empty trie holds nothing
def Trie.get_tip(-V: Data, k: B.Key()) -> {B.Trie.get(V, k, B.Tip{}) == None{} : Maybe<&2, V>}:
  match k:
    case Nil{}:
      {==}
    case False{} <> ks:
      Trie.get_tip(V, ks)
    case True{} <> ks:
      Trie.get_tip(V, ks)

# a pick of an account or x that is nothing is x, which is nothing
def Trie.none_pick(c: Bool, -b: B.Acc, -x: Maybe<&2, B.Acc>, e: {Bool.pick(Maybe<&2, B.Acc>, c, Some{b}, x) == None{} : Maybe<&2, B.Acc>})
  -> {x == None{} : Maybe<&2, B.Acc>}:
  match c:
    case True{}:
      L.Maybe.some_none(B.Acc, b, {x == None{} : Maybe<&2, B.Acc>}, e)
    case False{}:
      e

# a key that holds nothing after a set to an account held nothing before
def Trie.none_set(+q: B.Key(), +k: B.Key(), +t: B.Trie<B.Acc>, +b: B.Acc, e: {B.Trie.get(B.Acc, q, B.Trie.set(B.Acc, k, t, Some{b})) == None{} : Maybe<&2, B.Acc>})
  -> {B.Trie.get(B.Acc, q, t) == None{} : Maybe<&2, B.Acc>}:
  +x = B.Trie.get(B.Acc, q, t)
  +p = Bool.pick(Maybe<&2, B.Acc>, B.Key.eq(q, k), Some{b}, x)
  +y = B.Trie.get(B.Acc, q, B.Trie.set(B.Acc, k, t, Some{b}))
  Trie.none_pick(B.Key.eq(q, k), b, x, Equal.trans(Maybe<&2, B.Acc>, p, y, None{}, L.Trie.pick_set(B.Acc, q, k, t, Some{b}), e))

# Sound
# -----

# every account of t holds money only under the name of an account of t
def Sound.T(t: B.Trie<B.Acc>) -> Type:
  @k: B.Key() -> @q: B.Key() -> {B.Trie.get(B.Acc, q, t) == None{} : Maybe<&2, B.Acc>} -> {B.Acc.locked(B.Trie.get(B.Acc, k, t), q) == None{} : Maybe<&2, Nat>}

# the account a holds money only under the name of an account of t
def Sound.Held(a: B.Acc, t: B.Trie<B.Acc>) -> Type:
  @q: B.Key() -> {B.Trie.get(B.Acc, q, t) == None{} : Maybe<&2, B.Acc>} -> {B.Acc.locked(Some{a}, q) == None{} : Maybe<&2, Nat>}

# the account a is sound when t is: a proof that can be used once per
# use of Sound.T(t), as proofs of functions are used at most once
def Sound.If(a: B.Acc, t: B.Trie<B.Acc>) -> Type:
  Sound.T(t) -> Sound.Held(a, t)

# t has an account at u
def Sound.Has(u: B.Key(), t: B.Trie<B.Acc>) -> Data:
  {Maybe.is_some(&2, B.Acc, B.Trie.get(B.Acc, u, t)) == True{} : Bool}

# a bank result that does not fail is sound
def Sound.R(r: Result<&2, &2, String, B.Bank>) -> Type:
  L.Bank.If(r, Laws.Sound)

# the account at k of a sound trie is sound
def Sound.at(+k: B.Key(), +t: B.Trie<B.Acc>, -a: B.Acc, +e: {Some{a} == B.Trie.get(B.Acc, k, t) : Maybe<&2, B.Acc>}) -> Sound.If(a, t):
  hs => q => hq =>
    %Equal.sym(Maybe<&2, B.Acc>, Some{a}, B.Trie.get(B.Acc, k, t), e) : {B.Acc.locked(_, q) == None{} : Maybe<&2, Nat>}
    hs(k, q, hq)

# the account at j after a set at k is sound: the new one, or the old
def Sound.pick(c: Bool, +j: B.Key(), +q: B.Key(), -t: B.Trie<B.Acc>, -b: B.Acc, hs: Sound.T(t), hb: Sound.If(b, t),
  +hq: {B.Trie.get(B.Acc, q, t) == None{} : Maybe<&2, B.Acc>})
  -> {B.Acc.locked(Bool.pick(Maybe<&2, B.Acc>, c, Some{b}, B.Trie.get(B.Acc, j, t)), q) == None{} : Maybe<&2, Nat>}:
  match c:
    case True{}:
      hb(hs, q, hq)
    case False{}:
      hs(j, q, hq)

# setting k to a sound account keeps a trie sound
def Sound.set(+k: B.Key(), +t: B.Trie<B.Acc>, +b: B.Acc, hs: Sound.T(t), hb: Sound.If(b, t)) -> Sound.T(B.Trie.set(B.Acc, k, t, Some{b})):
  +j => +q => hq =>
    %L.Trie.pick_set(B.Acc, j, k, t, Some{b}) : {B.Acc.locked(_, q) == None{} : Maybe<&2, Nat>}
    Sound.pick(B.Key.eq(j, k), j, q, t, b, hs, hb, Trie.none_set(q, k, t, b, hq))

# a pick of an account and an account is an account
def Sound.some_pick(c: Bool, -b: B.Acc, -x: Maybe<&2, B.Acc>, h: {Maybe.is_some(&2, B.Acc, x) == True{} : Bool})
  -> {Maybe.is_some(&2, B.Acc, Bool.pick(Maybe<&2, B.Acc>, c, Some{b}, x)) == True{} : Bool}:
  match c:
    case True{}:
      {==}
    case False{}:
      h

# a set to an account keeps an account at u
def Sound.keep(+u: B.Key(), +k: B.Key(), +t: B.Trie<B.Acc>, +b: B.Acc, hu: Sound.Has(u, t)) -> Sound.Has(u, B.Trie.set(B.Acc, k, t, Some{b})):
  %L.Trie.pick_set(B.Acc, u, k, t, Some{b}) : {Maybe.is_some(&2, B.Acc, _) == True{} : Bool}
  Sound.some_pick(B.Key.eq(u, k), b, B.Trie.get(B.Acc, u, t), hu)

# Plan
# ----

# a planned request that does not fail plans a sound account
def Sound.Plan(r: Result<&2, &2, String, B.Plan>, t: B.Trie<B.Acc>) -> Type:
  match r:
    case Fail{e}:
      Unit
    case Done{B.Plan{a, gifts}}:
      Sound.If(a, t)

# a need keeps a plan sound
def Sound.need(test: Bool, -text: String, -p: B.Plan, -t: B.Trie<B.Acc>, h: Sound.Plan(Done{p}, t)) -> Sound.Plan(B.Op.need(test, text, p), t):
  match test:
    case True{}:
      h
    case False{}:
      Unit{}

# what a pick of nothing and nothing holds is nothing
def Sound.none(c: Bool, -y: Maybe<&2, Nat>, h: {y == None{} : Maybe<&2, Nat>}) -> {Bool.pick(Maybe<&2, Nat>, c, None{}, y) == None{} : Maybe<&2, Nat>}:
  match c:
    case True{}:
      {==}
    case False{}:
      h

# clearing what k held keeps an account sound
def Sound.clear(+k: B.Key(), +held: B.Trie<Nat>, -t: B.Trie<B.Acc>,
  h: @q: B.Key() -> {B.Trie.get(B.Acc, q, t) == None{} : Maybe<&2, B.Acc>} -> {B.Trie.get(Nat, q, held) == None{} : Maybe<&2, Nat>})
  -> @q: B.Key() -> {B.Trie.get(B.Acc, q, t) == None{} : Maybe<&2, B.Acc>} -> {B.Trie.get(Nat, q, B.Trie.put(k, held, 0n)) == None{} : Maybe<&2, Nat>}:
  +q => hq =>
    %L.Trie.pick_set(Nat, q, k, held, None{}) : {_ == None{} : Maybe<&2, Nat>}
    Sound.none(B.Key.eq(q, k), B.Trie.get(Nat, q, held), h(q, hq))

# every op plans a sound account
def Sound.op(op: B.Op, a: B.Acc, gifts: List<&2, B.Gift>, -t: B.Trie<B.Acc>, h: Sound.If(a, t)) -> Sound.Plan(B.Op.at(op, a, gifts), t):
  match op a:
    case B.Need{test, text} a:
      Sound.need(test, text, B.Plan{a, gifts}, t, h)
    case B.Memo{x} B.Acc{pass, cash, note, line, loan, held}:
      h
    case B.Debt{d} B.Acc{pass, cash, note, line, loan, held}:
      h
    case B.Give{k, +x} B.Acc{pass, +cash, note, line, loan, held}:
      Sound.need(Nat.is_le(x, cash), "you do not have that much", B.Plan{B.Acc{pass, Nat.sub(cash, x), note, line, loan, held}, B.Pay{k, x} <> gifts}, t, h)
    case B.Lock{k, +x} B.Acc{pass, +cash, note, line, loan, held}:
      Sound.need(Nat.is_le(x, cash), "you do not have that much", B.Plan{B.Acc{pass, Nat.sub(cash, x), note, line, loan, held}, B.Owe{k, x} <> gifts}, t, h)
    case B.Open{k} a:
      h
    case B.Drop{+k} B.Acc{pass, cash, note, line, loan, +held}:
      hs => Sound.clear(k, held, t, h(hs))
    case B.Draw{+x} B.Acc{pass, cash, note, +line, loan, held}:
      Sound.need(Nat.is_le(x, line), "the bank has no more credit for you", B.Plan{B.Acc{pass, Nat.add(cash, x), note, Nat.sub(line, x), loan, held}, gifts}, t, h)
    case B.Fund{+x} B.Acc{pass, +cash, note, line, loan, held}:
      Sound.need(Nat.is_le(x, cash), "you do not have that much", B.Plan{B.Acc{pass, Nat.sub(cash, x), note, Nat.add(line, x), loan, held}, gifts}, t, h)

# a step of a plan keeps it sound
def Sound.step(r: Result<&2, &2, String, B.Plan>, +op: B.Op, -t: B.Trie<B.Acc>, h: Sound.Plan(r, t)) -> Sound.Plan(B.Op.step(r, op), t):
  match r:
    case Fail{e}:
      Unit{}
    case Done{B.Plan{a, gifts}}:
      Sound.op(op, a, gifts, t, h)

# every op of a plan keeps it sound
def Sound.run(ops: List<&2, B.Op>, +r: Result<&2, &2, String, B.Plan>, -t: B.Trie<B.Acc>, h: Sound.Plan(r, t)) -> Sound.Plan(B.Op.run(ops, r), t):
  match ops:
    case Nil{}:
      h
    case +op <> rest:
      Sound.run(rest, B.Op.step(r, op), t, Sound.step(r, op, t, h))

# Gifts
# -----

# the pick of an owe at q is nothing, as q is not u, whose account exists
def Sound.owe(c: Bool, +q: B.Key(), +u: B.Key(), +t: B.Trie<B.Acc>, -x: Maybe<&2, Nat>, -y: Maybe<&2, Nat>, e: {B.Key.eq(q, u) == c : Bool},
  hq: {B.Trie.get(B.Acc, q, t) == None{} : Maybe<&2, B.Acc>}, hu: Sound.Has(u, t), h: {y == None{} : Maybe<&2, Nat>})
  -> {Bool.pick(Maybe<&2, Nat>, c, x, y) == None{} : Maybe<&2, Nat>}:
  match c:
    case True{}:
      -M = Maybe<&2, B.Acc>
      +gq = B.Trie.get(B.Acc, q, t)
      +gu = B.Trie.get(B.Acc, u, t)
      +eq = Equal.cong(B.Key(), M, k => B.Trie.get(B.Acc, k, t), q, u, L.Key.eq_true(q, u, e))
      +eu = Equal.trans(M, None{}, gq, gu, Equal.sym(M, gq, None{}, hq), eq)
      +ef = Equal.cong(M, Bool, m => Maybe.is_some(&2, B.Acc, m), None{}, gu, eu)
      L.Bool.false_true({x == None{} : Maybe<&2, Nat>}, Equal.trans(Bool, False{}, Maybe.is_some(&2, B.Acc, gu), True{}, ef, hu))
    case False{}:
      h

# a gift from u, whose account exists, keeps an account sound
def Sound.give(g: B.Gift, +u: B.Key(), a: B.Acc, +t: B.Trie<B.Acc>, h: Sound.Held(a, t), +hu: Sound.Has(u, t)) -> Sound.Held(B.Gift.give(g, u, a), t):
  match g a:
    case B.Pay{d, x} B.Acc{pass, cash, note, line, loan, held}:
      h
    case B.Owe{d, +x} B.Acc{pass, cash, note, line, loan, +held}:
      +q => +hq =>
        +n = B.Trie.some(Nat.add(B.Trie.num(u, held), x))
        %L.Trie.pick_set(Nat, q, u, held, n) : {_ == None{} : Maybe<&2, Nat>}
        Sound.owe(B.Key.eq(q, u), q, u, t, n, B.Trie.get(Nat, q, held), {==}, hq, hu, h(q, hq))
    case B.Rel{d} B.Acc{pass, cash, note, line, loan, +held}:
      Sound.clear(u, held, t, h)

# a bank result that does not fail is sound, with an account at u
def Sound.Gifts(r: Result<&2, &2, String, B.Bank>, u: B.Key()) -> Type:
  match r:
    case Fail{e}:
      Unit
    case Done{B.Bank{v, t}}:
      Sound.T(t) & Sound.Has(u, t)

# a gift to the account at d keeps a bank sound
def Sound.gift_to(self: Bool, m: Maybe<&2, B.Acc>, +v: Nat, +t: B.Trie<B.Acc>, +u: B.Key(), +d: B.Key(), +g: B.Gift,
  +em: {m == B.Trie.get(B.Acc, d, t) : Maybe<&2, B.Acc>}, hs: Sound.T(t), +hu: Sound.Has(u, t))
  -> Sound.Gifts(B.Plan.gift.to(self, m, v, t, u, d, g), u):
  match self m:
    case True{} _:
      Unit{}
    case False{} None{}:
      Unit{}
    case False{} Some{+a}:
      +b = B.Gift.give(g, u, a)
      hb = {hs => Sound.give(g, u, a, t, Sound.at(d, t, a, em, hs), hu) : Sound.If(b, t)}
      (Sound.set(d, t, b, hs, hb), Sound.keep(u, d, t, b, hu))

# one more gift keeps a bank result sound
def Sound.gift(r: Result<&2, &2, String, B.Bank>, +u: B.Key(), +g: B.Gift, h: Sound.Gifts(r, u)) -> Sound.Gifts(B.Plan.gift(r, u, g), u):
  match r:
    case Fail{e}:
      Unit{}
    case Done{B.Bank{v, +t}}:
      (hs, hu) = h
      +d = B.Gift.dest(g)
      Sound.gift_to(B.Key.eq(d, u), B.Trie.get(B.Acc, d, t), v, t, u, d, g, {==}, hs, hu)

# every gift of a plan keeps a bank result sound
def Sound.gifts(gs: List<&2, B.Gift>, +u: B.Key(), +r: Result<&2, &2, String, B.Bank>, h: Sound.Gifts(r, u)) -> Sound.Gifts(B.Plan.gifts(gs, u, r), u):
  match gs:
    case Nil{}:
      h
    case +g <> rest:
      Sound.gifts(rest, u, B.Plan.gift(r, u, g), Sound.gift(r, u, g, h))

# a sound bank result with an account at u is sound
def Sound.forget(r: Result<&2, &2, String, B.Bank>, -u: B.Key(), h: Sound.Gifts(r, u)) -> Sound.R(r):
  match r:
    case Fail{e}:
      Unit{}
    case Done{B.Bank{v, t}}:
      (hs, hu) = h
      hs

# Requests
# --------

# a key holds an account just set at it
def Sound.has_set(+u: B.Key(), +t: B.Trie<B.Acc>, +a: B.Acc) -> Sound.Has(u, B.Trie.set(B.Acc, u, t, Some{a})):
  +m = {Some{a} : Maybe<&2, B.Acc>}
  %L.Trie.get_same(B.Acc, u, t, m) : {Maybe.is_some(&2, B.Acc, _) == True{} : Bool}
  {==}

# the plan of u, whose account is sound, keeps a trie sound
def Sound.apply(+v: Nat, +t: B.Trie<B.Acc>, +u: B.Key(), p: B.Plan, hs: Sound.T(t), hp: Sound.Plan(Done{p}, t))
  -> Sound.R(B.Plan.apply(B.Bank{v, t}, u, p)):
  match p:
    case B.Plan{+acct, +gifts}:
      +m = {Some{acct} : Maybe<&2, B.Acc>}
      +t1 = B.Trie.set(B.Acc, u, t, m)
      +hu = Sound.has_set(u, t, acct)
      +r = {Done{B.Bank{v, t1}} : Result<&2, &2, String, B.Bank>}
      Sound.forget(B.Plan.gifts(gifts, u, r), u, Sound.gifts(gifts, u, r, (Sound.set(u, t, acct, hs, hp), hu)))

# a planned request keeps a bank sound
def Sound.plan(+v: Nat, +t: B.Trie<B.Acc>, +u: B.Key(), r: Result<&2, &2, String, B.Plan>, hs: Sound.T(t), hp: Sound.Plan(r, t))
  -> Sound.R(B.Bank.plan(B.Bank{v, t}, u, r)):
  match r:
    case Fail{e}:
      Unit{}
    case Done{p}:
      Sound.apply(v, t, u, p, hs, hp)

# a command keeps a bank sound
def Sound.exec(s: B.Bank, +user: String, +key: String, +now: Nat, +cmd: B.Cmd, h: Laws.Sound(s)) -> Sound.R(B.Bank.exec(s, user, key, now, cmd)):
  match s:
    case B.Bank{+v, +t}:
      L.Bank.exec_by(B.Key.of(user), v, t, key, now, cmd, u => Laws.Sound, u => Unit, Unit{},
        +u => +a => eg => r => Sound.plan(v, t, u, B.Cmd.plan(cmd, a, now), h,
          Sound.run(B.Cmd.ops(cmd, a, now), Done{B.Plan{a, Nil{}}}, t, Sound.at(u, t, a, eg))))

# a join keeps a bank sound
def Sound.join(s: B.Bank, +name: String, +pass: String, h: Laws.Sound(s)) -> Sound.R(B.Bank.join(s, name, pass)):
  match s:
    case B.Bank{+v, +t}:
      L.Bank.join_by(B.Key.of(name), v, t, pass, Laws.Sound,
        +k => em => o => Sound.set(k, t, B.Acc.new(pass), h, hs => q => hq => Trie.get_tip(Nat, q)))

# Web
# ---

# a result that is sound when s is: its bank is sound when s is
def Sound.imp(r: Result<&2, &2, String, B.Bank>, -s: B.Bank, h: Laws.Sound(s) -> Sound.R(r))
  -> L.Bank.If(r, b => Laws.Sound(s) -> Laws.Sound(b)):
  match r:
    case Fail{e}:
      Unit{}
    case Done{b}:
      h

# LAW sound
def Laws.sound(s, input, ok):
  +rand = Laws.rand(input)
  +user = Laws.user(input)
  +key = Laws.key(input)
  +time = Laws.time(input)
  -P = {b => Laws.Sound(s) -> Laws.Sound(b) : B.Bank -> Type}
  h = L.Web.reply_by(s, W.Req.parse(input), P, h => h,
    +name => Sound.imp(B.Bank.join(s, name, rand), s, h => Sound.join(s, name, rand, h)),
    +cmd => Sound.imp(B.Bank.exec(s, user, key, time, cmd), s, h => Sound.exec(s, user, key, time, cmd, h)))
  h(ok)