# eukhe: the proof of LAW screen_ffi_stack

import Base
import ../../bend/ffi_screen.bend as FSc
import ../../bend/screen.bend as Sc
import ../../bend/wire.bend as Wr
import ../../laws/base.bend as LawsBase
import ../../laws/screen.bend as Screen
import ../../laws/wire.bend as Wire
import ../base/logic/bool.bend as LLogicBool
import ../base/wire.bend as LWire

def fs.rt_stack(+hs: List<&2, Nat>, +y: Nat, +rows: Nat, +f: {Bool.and(Bool.and(LawsBase.wire_fits(List.length(&2, Nat, hs)), LawsBase.wire_nats_fit(hs)), Bool.and(LawsBase.wire_fits(y), LawsBase.wire_fits(rows))) == True{} : Bool}) -> {FSc.get_req(FSc.put_req(FSc.ReqStack{hs, y, rows}, "")) == Wr.Got{FSc.ReqStack{hs, y, rows}, ""} : Wr.Dec<FSc.Req>}:
  Equal.trans(Wr.Dec<FSc.Req>, FSc.get_req(FSc.put_req(FSc.ReqStack{hs, y, rows}, "")), FSc.get_req.of(Wr.Got{2n, Wr.put_list(~Nat, ~Wr.put_nat, hs, Wr.put_nat(y, Wr.put_nat(rows, "")))}), Wr.Got{FSc.ReqStack{hs, y, rows}, ""}, Equal.cong(Wr.Dec<Nat>, Wr.Dec<FSc.Req>, zq => FSc.get_req.of(zq), Wr.get_nat(Wr.put_nat(2n, Wr.put_list(~Nat, ~Wr.put_nat, hs, Wr.put_nat(y, Wr.put_nat(rows, ""))))), Wr.Got{2n, Wr.put_list(~Nat, ~Wr.put_nat, hs, Wr.put_nat(y, Wr.put_nat(rows, "")))}, Wire.wire_nat_round_trip(2n, Wr.put_list(~Nat, ~Wr.put_nat, hs, Wr.put_nat(y, Wr.put_nat(rows, ""))), {==})), Equal.trans(Wr.Dec<FSc.Req>, FSc.get_req.of(Wr.Got{2n, Wr.put_list(~Nat, ~Wr.put_nat, hs, Wr.put_nat(y, Wr.put_nat(rows, "")))}), FSc.get_stack(Wr.Got{hs, Wr.put_nat(y, Wr.put_nat(rows, ""))}), Wr.Got{FSc.ReqStack{hs, y, rows}, ""}, Equal.cong(Wr.Dec<List<&2, Nat>>, Wr.Dec<FSc.Req>, zq => FSc.get_stack(zq), Wr.get_list(~Nat, ~Wr.get_nat, Wr.put_list(~Nat, ~Wr.put_nat, hs, Wr.put_nat(y, Wr.put_nat(rows, "")))), Wr.Got{hs, Wr.put_nat(y, Wr.put_nat(rows, ""))}, Wire.wire_list_round_trip(hs, Wr.put_nat(y, Wr.put_nat(rows, "")), LLogicBool.wr_and_l(Bool.and(LawsBase.wire_fits(List.length(&2, Nat, hs)), LawsBase.wire_nats_fit(hs)), Bool.and(LawsBase.wire_fits(y), LawsBase.wire_fits(rows)), f))), Equal.trans(Wr.Dec<FSc.Req>, FSc.get_stack(Wr.Got{hs, Wr.put_nat(y, Wr.put_nat(rows, ""))}), FSc.get_stack.y(hs, Wr.Got{y, Wr.put_nat(rows, "")}), Wr.Got{FSc.ReqStack{hs, y, rows}, ""}, Equal.cong(Wr.Dec<Nat>, Wr.Dec<FSc.Req>, zq => FSc.get_stack.y(hs, zq), Wr.get_nat(Wr.put_nat(y, Wr.put_nat(rows, ""))), Wr.Got{y, Wr.put_nat(rows, "")}, Wire.wire_nat_round_trip(y, Wr.put_nat(rows, ""), LLogicBool.wr_and_l(LawsBase.wire_fits(y), LawsBase.wire_fits(rows), LLogicBool.wr_and_r(Bool.and(LawsBase.wire_fits(List.length(&2, Nat, hs)), LawsBase.wire_nats_fit(hs)), Bool.and(LawsBase.wire_fits(y), LawsBase.wire_fits(rows)), f)))), Equal.trans(Wr.Dec<FSc.Req>, FSc.get_stack.y(hs, Wr.Got{y, Wr.put_nat(rows, "")}), FSc.get_stack.rows(hs, y, Wr.Got{rows, ""}), Wr.Got{FSc.ReqStack{hs, y, rows}, ""}, Equal.cong(Wr.Dec<Nat>, Wr.Dec<FSc.Req>, zq => FSc.get_stack.rows(hs, y, zq), Wr.get_nat(Wr.put_nat(rows, "")), Wr.Got{rows, ""}, Wire.wire_nat_round_trip(rows, "", LLogicBool.wr_and_r(LawsBase.wire_fits(y), LawsBase.wire_fits(rows), LLogicBool.wr_and_r(Bool.and(LawsBase.wire_fits(List.length(&2, Nat, hs)), LawsBase.wire_nats_fit(hs)), Bool.and(LawsBase.wire_fits(y), LawsBase.wire_fits(rows)), f)))), {==}))))

def Screen.screen_ffi_stack(hs, y, rows, f):
  Equal.trans(String, FSc.ffi(FSc.put_req(FSc.ReqStack{hs, y, rows}, "")), FSc.ffi.of(Wr.Got{FSc.ReqStack{hs, y, rows}, ""}), Wr.put_list(~Sc.Rect, ~FSc.put_rect, Sc.vstack(hs, y, rows), ""), Equal.cong(Wr.Dec<FSc.Req>, String, FSc.ffi.of, FSc.get_req(FSc.put_req(FSc.ReqStack{hs, y, rows}, "")), Wr.Got{FSc.ReqStack{hs, y, rows}, ""}, fs.rt_stack(hs, y, rows, f)), {==})