# Bend Bank: the proof of LAW loan
# ================================
#
# A request changes its sender's account only through the plan of its
# command: Plan.apply sets the sender's account to the plan's, and no
# gift reaches it after, since a gift to the sender fails (Self). So the
# proof follows the ops of each command (Loan): every command but Lend
# and Back runs only ops that keep the loan and the line, and Lend and
# Back are followed op by op. A join keeps every account that existed,
# with its loan and line (Keep.join, of LAW authority), and the other
# requests change no account (Web.reply_by).

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

# Self
# ----

# a bank result that does not fail has the account acct at u
def Self.R(r: Result<&2, &2, String, B.Bank>, u: B.Key(), acct: B.Acc) -> Type:
  L.Bank.If(r, b => {Some{acct} == Laws.acct(b, u) : Maybe<&2, B.Acc>})

# a gift from u to the account m at d is not to u, so it keeps u's
# account
def Self.gift_to(self: Bool, m: Maybe<&2, B.Acc>, +vault: Nat, +accts: B.Trie<B.Acc>, +u: B.Key(),
  +d: B.Key(), +g: B.Gift, -acct: B.Acc, es: {B.Key.eq(d, u) == self : Bool},
  h: {Some{acct} == B.Trie.get(B.Acc, u, accts) : Maybe<&2, B.Acc>})
  -> Self.R(B.Plan.gift.to(self, m, vault, accts, u, d, g), u, acct):
  match self m:
    case True{} _:
      Unit{}
    case False{} None{}:
      Unit{}
    case False{} Some{a}:
      +b = {Some{B.Gift.give(g, u, a)} : Maybe<&2, B.Acc>}
      %L.Trie.get_other(B.Acc, u, d, accts, b,
        L.Key.flip(d, u, False{}, es)) : {Some{acct} == _ : Maybe<&2, B.Acc>}
      h

# one more gift keeps u's account
def Self.gift(r: Result<&2, &2, String, B.Bank>, +u: B.Key(), +g: B.Gift, -acct: B.Acc,
  h: Self.R(r, u, acct))
  -> Self.R(B.Plan.gift(r, u, g), u, acct):
  match r:
    case Fail{e}:
      Unit{}
    case Done{B.Bank{vault, +accts}}:
      +d = B.Gift.dest(g)
      Self.gift_to(B.Key.eq(d, u), B.Trie.get(B.Acc, d, accts), vault, accts, u, d, g, acct, {==},
        h)

# the gifts keep u's account
def Self.gifts(gs: List<&2, B.Gift>, +u: B.Key(), +r: Result<&2, &2, String, B.Bank>, -acct: B.Acc,
  h: Self.R(r, u, acct))
  -> Self.R(B.Plan.gifts(gs, u, r), u, acct):
  match gs:
    case Nil{}:
      h
    case +g <> rest:
      Self.gifts(rest, u, B.Plan.gift(r, u, g), acct, Self.gift(r, u, g, acct, h))

# a plan of u leaves u with the plan's account
def Self.apply(+v: Nat, +t: B.Trie<B.Acc>, +u: B.Key(), +acct: B.Acc, gifts: List<&2, B.Gift>)
  -> Self.R(B.Plan.apply(B.Bank{v, t}, u, B.Plan{acct, gifts}), u, acct):
  +r = {Done{B.Bank{v, B.Trie.set(B.Acc, u, t, Some{acct})}} : Result<&2, &2, String, B.Bank>}
  Self.gifts(gifts, u, r, acct, L.Trie.get_same(B.Acc, u, t, Some{acct}))

# Loan
# ----

# a planned request that does not fail has the loan d and the line l
def Loan.Is(r: Result<&2, &2, String, B.Plan>, d: B.Loan, l: Nat) -> Type:
  match r:
    case Fail{e}:
      Unit
    case Done{B.Plan{B.Acc{pass, cash, note, line, loan, held}, gifts}}:
      {loan == d : B.Loan} & {line == l : Nat}

# a planned request that does not fail took a Step from the account a
def Loan.P(a: B.Acc, r: Result<&2, &2, String, B.Plan>, now: Nat) -> Type:
  match r:
    case Fail{e}:
      Unit
    case Done{B.Plan{b, gifts}}:
      Laws.Step(a, b, now)

# an op that keeps the loan and the line: a calm op
def Op.Calm(op: B.Op) -> Type:
  match op:
    case B.Debt{loan}:
      Empty
    case B.Draw{cash}:
      Empty
    case B.Fund{cash}:
      Empty
    case o:
      Unit

# ops that are all calm
def Op.Calms(ops: List<&2, B.Op>) -> Type:
  match ops:
    case Nil{}:
      Unit
    case op <> rest:
      Op.Calm(op) & Op.Calms(rest)

# a need keeps the plan, or fails
def Loan.need(test: Bool, -text: String, -p: B.Plan, -d: B.Loan, -l: Nat, h: Loan.Is(Done{p}, d, l))
  -> Loan.Is(B.Op.need(test, text, p), d, l):
  match test:
    case True{}:
      h
    case False{}:
      Unit{}

# a calm op keeps the plan's loan and line
def Loan.at(op: B.Op, a: B.Acc, gifts: List<&2, B.Gift>, -d: B.Loan, -l: Nat,
  h: Loan.Is(Done{B.Plan{a, gifts}}, d, l), c: Op.Calm(op))
  -> Loan.Is(B.Op.at(op, a, gifts), d, l):
  match op a:
    case B.Need{test, text} a:
      Loan.need(test, text, B.Plan{a, gifts}, d, l, h)
    case B.Memo{t} B.Acc{pass, cash, note, line, loan, held}:
      h
    case B.Debt{x} _:
      match c:
    case B.Give{k, +x} B.Acc{pass, +cash, note, line, loan, held}:
      +p = {B.Plan{B.Acc{pass, Nat.sub(cash, x), note, line, loan, held},
        B.Pay{k, x} <> gifts} : B.Plan}
      Loan.need(Nat.is_le(x, cash), "you do not have that much", p, d, l, h)
    case B.Lock{k, +x} B.Acc{pass, +cash, note, line, loan, held}:
      +p = {B.Plan{B.Acc{pass, Nat.sub(cash, x), note, line, loan, held},
        B.Owe{k, x} <> gifts} : B.Plan}
      Loan.need(Nat.is_le(x, cash), "you do not have that much", p, d, l, h)
    case B.Open{k} B.Acc{pass, cash, note, line, loan, held}:
      h
    case B.Drop{k} B.Acc{pass, cash, note, line, loan, held}:
      h
    case B.Draw{x} _:
      match c:
    case B.Fund{x} _:
      match c:

# a calm step keeps the loan and the line
def Loan.step(r: Result<&2, &2, String, B.Plan>, op: B.Op, -d: B.Loan, -l: Nat, h: Loan.Is(r, d, l),
  c: Op.Calm(op))
  -> Loan.Is(B.Op.step(r, op), d, l):
  match r:
    case Fail{e}:
      Unit{}
    case Done{B.Plan{a, gifts}}:
      Loan.at(op, a, gifts, d, l, h, c)

# calm ops keep the loan and the line
def Loan.run(ops: List<&2, B.Op>, +r: Result<&2, &2, String, B.Plan>, -d: B.Loan, -l: Nat,
  h: Loan.Is(r, d, l), c: Op.Calms(ops))
  -> Loan.Is(B.Op.run(ops, r), d, l):
  match ops:
    case Nil{}:
      h
    case +op <> rest:
      (c1, c2) = c
      Loan.run(rest, B.Op.step(r, op), d, l, Loan.step(r, op, d, l, h, c1), c2)

# the ops of a Send are calm
def Loan.rows(rows: List<&2, B.Line>) -> Op.Calms(B.Cmd.rows(rows)):
  match rows:
    case Nil{}:
      Unit{}
    case B.Line{name, cash} <> rest:
      (Unit{}, Unit{}, Unit{}, Loan.rows(rest))

# a plan that keeps the loan and the line took a Step
def Loan.kept(r: Result<&2, &2, String, B.Plan>, -p: String, -c: Nat, -n: String, -l: Nat,
  -d: B.Loan, -h: B.Trie<Nat>, -now: Nat, e: Loan.Is(r, d, l))
  -> Loan.P(B.Acc{p, c, n, l, d, h}, r, now):
  match r:
    case Fail{x}:
      Unit{}
    case Done{B.Plan{B.Acc{p2, c2, n2, l2, d2, h2}, gifts}}:
      Inl{e}

# a command of calm ops took a Step
def Loan.calm(+cmd: B.Cmd, a: B.Acc, +now: Nat, c: Op.Calms(B.Cmd.ops(cmd, a, now)))
  -> Loan.P(a, B.Cmd.plan(cmd, a, now), now):
  match a:
    case B.Acc{+p, +cash, +n, +l, +d, +h}:
      +a = {B.Acc{p, cash, n, l, d, h} : B.Acc}
      +r = {Done{B.Plan{a, Nil{}}} : Result<&2, &2, String, B.Plan>}
      Loan.kept(B.Cmd.plan(cmd, a, now), p, cash, n, l, d, h, now,
        Loan.run(B.Cmd.ops(cmd, a, now), r, d, l, ({==}, {==}), c))

# 0 < x gives 1 <= x
def Loan.pos(+x: Nat, e: {Nat.is_lt(0n, x) == True{} : Bool}) -> Laws.LE(1n, x):
  match x:
    case 0n:
      L.Bool.false_true(Laws.LE(1n, 0n), e)
    case 1n+q:
      L.Nat.le_add(1n, q)

# the loan of x, once its need passed: the line has x for it
def Loan.draw(t: Bool, +x: Nat, -p: String, +c: Nat, -n: String, +l: Nat, -h: B.Trie<Nat>,
  +now: Nat, -text: String, e: {Nat.is_le(x, l) == t : Bool}, e1: Laws.LE(1n, x),
  e2: Laws.LE(x, 1000n))
  -> Loan.P(B.Acc{p, c, n, l, B.Clear{}, h},
    B.Op.run([B.Debt{B.Owing{Nat.add(x, B.Loan.interest(x)), Nat.add(now, B.Loan.term())}}],
    B.Op.need(t, text, B.Plan{B.Acc{p, Nat.add(c, x), n, Nat.sub(l, x), B.Clear{}, h}, Nil{}})),
    now):
  match t:
    case True{}:
      Inr{Inl{(x, {==}, e1, e2, {==}, L.Nat.sub_add(l, x, e), {==})}}
    case False{}:
      Unit{}

# a loan of x, when nothing is owed: a positive amount up to the limit
def Loan.lend(t1: Bool, t2: Bool, +x: Nat, -p: String, +c: Nat, -n: String, +l: Nat,
  -h: B.Trie<Nat>, +now: Nat, -s1: String, -s2: String, e1: {Nat.is_lt(0n, x) == t1 : Bool},
  e2: {Nat.is_le(x, B.Loan.limit()) == t2 : Bool})
  -> Loan.P(B.Acc{p, c, n, l, B.Clear{}, h},
    B.Op.run([B.Need{t2, s2}, B.Draw{x},
    B.Debt{B.Owing{Nat.add(x, B.Loan.interest(x)), Nat.add(now, B.Loan.term())}}],
    B.Op.need(t1, s1, B.Plan{B.Acc{p, c, n, l, B.Clear{}, h}, Nil{}})), now):
  match t1 t2:
    case True{} True{}:
      Loan.draw(Nat.is_le(x, l), x, p, c, n, l, h, now, "the bank has no more credit for you", {==},
        Loan.pos(x, e1), e2)
    case True{} False{}:
      Unit{}
    case False{} _:
      Unit{}

# the repayment of x, once its needs passed: the cash has x for it
def Loan.fund(t: Bool, +x: Nat, -p: String, +c: Nat, -n: String, +l: Nat, -h: B.Trie<Nat>,
  -now: Nat, +debt: Nat, +till: Nat, -text: String, e: {Nat.is_le(x, c) == t : Bool},
  e1: Laws.LE(now, till), e2: Laws.LE(1n, x), e3: Laws.LE(x, debt))
  -> Loan.P(B.Acc{p, c, n, l, B.Owing{debt, till}, h},
    B.Op.run([B.Debt{B.Loan.rest(Nat.sub(debt, x), till)}],
    B.Op.need(t, text,
    B.Plan{B.Acc{p, Nat.sub(c, x), n, Nat.add(l, x), B.Owing{debt, till}, h}, Nil{}})), now):
  match t:
    case True{}:
      Inr{Inr{(x, e1, e2, e3, L.Nat.sub_add(c, x, e), {==}, {==})}}
    case False{}:
      Unit{}

# a repayment of x: a positive amount, before the due time, up to the debt
def Loan.back(t1: Bool, t2: Bool, t3: Bool, +x: Nat, -p: String, +c: Nat, -n: String, +l: Nat,
  -h: B.Trie<Nat>, +now: Nat, +debt: Nat, +till: Nat, -s1: String, -s2: String, -s3: String,
  e1: {Nat.is_lt(0n, x) == t1 : Bool}, e2: {Nat.is_le(now, till) == t2 : Bool},
  e3: {Nat.is_le(x, debt) == t3 : Bool})
  -> Loan.P(B.Acc{p, c, n, l, B.Owing{debt, till}, h},
    B.Op.run([B.Need{t2, s2}, B.Need{t3, s3}, B.Fund{x},
    B.Debt{B.Loan.rest(Nat.sub(debt, x), till)}],
    B.Op.need(t1, s1, B.Plan{B.Acc{p, c, n, l, B.Owing{debt, till}, h}, Nil{}})), now):
  match t1 t2 t3:
    case True{} True{} True{}:
      Loan.fund(Nat.is_le(x, c), x, p, c, n, l, h, now, debt, till, "you do not have that much",
        {==}, e2, Loan.pos(x, e1), e3)
    case True{} True{} False{}:
      Unit{}
    case True{} False{} _:
      Unit{}
    case False{} _ _:
      Unit{}

# the plan of every command took a Step
def Loan.cmd(cmd: B.Cmd, a: B.Acc, +now: Nat) -> Loan.P(a, B.Cmd.plan(cmd, a, now), now):
  match cmd a:
    case B.Note{+text} a:
      Loan.calm(B.Note{text}, a, now, (Unit{}, Unit{}, Unit{}))
    case B.Send{+rows} a:
      Loan.calm(B.Send{rows}, a, now, (Unit{}, Loan.rows(rows)))
    case B.Lend{+x} B.Acc{p, +c, n, +l, d, h}:
      match d:
        case B.Owing{debt, till}:
          Unit{}
        case B.Clear{}:
          Loan.lend(Nat.is_lt(0n, x), Nat.is_le(x, B.Loan.limit()), x, p, c, n, l, h, now,
            B.Cmd.positive(), "the largest loan is 1,000", {==}, {==})
    case B.Back{+x} B.Acc{p, +c, n, +l, d, h}:
      match d:
        case B.Clear{}:
          Unit{}
        case B.Owing{+debt, +till}:
          Loan.back(Nat.is_lt(0n, x), Nat.is_le(now, till), Nat.is_le(x, debt), x, p, c, n, l, h,
            now, debt, till,
            B.Cmd.positive(), "your loan was written off", "you owe less than that", {==}, {==},
              {==})
    case B.Hold{+name, +x} a:
      Loan.calm(B.Hold{name, x}, a, now, (Unit{}, Unit{}, Unit{}, Unit{}))
    case B.Free{+name} a:
      Loan.calm(B.Free{name}, a, now, (Unit{}, Unit{}, Unit{}))
    case B.Void{+name} a:
      Loan.calm(B.Void{name}, a, now, (Unit{}, Unit{}, Unit{}))

# Exec
# ----

# a bank result that does not fail took a Step at k, from m0
def Loan.R(m0: Maybe<&2, B.Acc>, r: Result<&2, &2, String, B.Bank>, k: B.Key(), now: Nat) -> Type:
  L.Bank.If(r, b => Laws.Stepped(m0, Laws.acct(b, k), now))

# the sender's account after the plan of its command is the plan's
def Loan.self(r: Result<&2, &2, String, B.Bank>, -a: B.Acc, -acct: B.Acc, -u: B.Key(), -now: Nat,
  hs: Self.R(r, u, acct), h: Laws.Step(a, acct, now))
  -> Loan.R(Some{a}, r, u, now):
  match r:
    case Fail{e}:
      Unit{}
    case Done{b}:
      %hs : Laws.Stepped(Some{a}, _, now)
      h

# a plan of u that took a Step leaves u's account Stepped
def Loan.plan(+v: Nat, +t: B.Trie<B.Acc>, +u: B.Key(), r: Result<&2, &2, String, B.Plan>, -a: B.Acc,
  -now: Nat, h: Loan.P(a, r, now))
  -> Loan.R(Some{a}, B.Bank.plan(B.Bank{v, t}, u, r), u, now):
  match r:
    case Fail{e}:
      Unit{}
    case Done{B.Plan{+acct, +gifts}}:
      +r = B.Plan.apply(B.Bank{v, t}, u, B.Plan{acct, gifts})
      Loan.self(r, a, acct, u, now, Self.apply(v, t, u, acct, gifts), h)

# the sender uk is k, the holder of a
def Loan.sent(+v: Nat, +t: B.Trie<B.Acc>, +uk: B.Key(), +a: B.Acc, +now: Nat, +cmd: B.Cmd,
  +k: B.Key(), eg: {Some{a} == B.Trie.get(B.Acc, uk, t) : Maybe<&2, B.Acc>},
  me: {B.Key.eq(uk, k) == True{} : Bool})
  -> Loan.R(B.Trie.get(B.Acc, k, t), B.Bank.plan(B.Bank{v, t}, uk, B.Cmd.plan(cmd, a, now)), k,
    now):
  +r = B.Bank.plan(B.Bank{v, t}, uk, B.Cmd.plan(cmd, a, now))
  %L.Key.eq_true(uk, k, me) : Loan.R(B.Trie.get(B.Acc, _, t), r, _, now)
  %eg : Loan.R(_, r, uk, now)
  Loan.plan(v, t, uk, B.Cmd.plan(cmd, a, now), a, now, Loan.cmd(cmd, a, now))

# a command changes its sender's loan and line only by a Step
def Loan.exec(s: B.Bank, +name: String, +pass: String, +now: Nat, +cmd: B.Cmd, +k: B.Key(),
  me: {Laws.Key.is(Laws.Bank.sender(s, name, pass), k) == True{} : Bool})
  -> Loan.R(Laws.acct(s, k), B.Bank.exec(s, name, pass, now, cmd), k, now):
  match s:
    case B.Bank{+v, +t}:
      L.Bank.exec_by(B.Key.of(name), v, t, pass, now, cmd,
        u => b => Laws.Stepped(B.Trie.get(B.Acc, k, t), Laws.acct(b, k), now),
        u => {Laws.Key.is(u, k) == True{} : Bool}, me,
        +uk => +a => eg => me => Loan.sent(v, t, uk, a, now, cmd, k, eg, me))

# Join
# ----

# a kept account took a Step: its loan and line are the same
def Loan.of_kept(m0: Maybe<&2, B.Acc>, m1: Maybe<&2, B.Acc>, -u: Maybe<&2, B.Key()>, -now: Nat,
  h: Laws.Kept(m0, m1, u)) -> Laws.Stepped(m0, m1, now):
  match m0 m1:
    case None{} _:
      Unit{}
    case Some{a} None{}:
      match h:
    case Some{B.Acc{p1, c1, n1, l1, d1, w1}} Some{B.Acc{p2, c2, n2, l2, d2, w2}}:
      (ep, en, el, ed, le, f, g) = h
      Inl{(ed, el)}

# a join keeps every account that existed (LAW authority), so it took a
# Step
def Loan.join(r: Result<&2, &2, String, B.Bank>, m0: Maybe<&2, B.Acc>, k: B.Key(), -now: Nat,
  h: A.Keep.R(m0, r, k, None{})) -> Loan.R(m0, r, k, now):
  match r:
    case Fail{e}:
      Unit{}
    case Done{b}:
      Loan.of_kept(m0, Laws.acct(b, k), None{}, now, h)

# LAW loan
def Laws.loan(s, input, k, me):
  +m0 = Laws.acct(s, k)
  +now = Laws.time(input)
  -P = {b => Laws.Stepped(m0, Laws.acct(b, k), now) : B.Bank -> Type}
  L.Web.reply_by(s, W.Req.parse(input), P,
    Loan.of_kept(m0, m0, None{}, now, A.Keep.kept_refl(m0, None{})),
    +name => Loan.join(B.Bank.join(s, name, Laws.rand(input)), m0, k, now,
      A.Keep.join(s, name, Laws.rand(input), k, None{})),
    +cmd => Loan.exec(s, Laws.user(input), Laws.key(input), now, cmd, k, me))