# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/bytes.src; edit the .src
import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/crypto/secp256k1/field.bend as FS
import ../../../spec/crypto/secp256k1/curve.bend as CV
import ../../../src/crypto/secp256k1/bytes.bend as B
import ../../lib/nat.bend as N
import ../../lib/logic.bend as Lg
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../math/natural/arith.bend as NR
import ../../math/typed/width.bend as WW
import ./u32and.bend as FB
import ./semiring.bend as SR
import ./limbs.bend as LV
import ./ineq.bend as I

# Octet strings (SEC 1 OS2IP / I2OSP, spec/crypto/secp256k1/curve.bend)
# and the 16-bit limbs of src/crypto/secp256k1/bytes.bend.

# the little-endian value of bytes
def le_val(bs: List<&2, U32>) -> Nat:
  match bs:
    case Nil{}: 0n
    case b <> t: Nat.add(B.byte(b), C.shift(8n, le_val(t)))

def pw8(n: Nat, +y: Nat) -> Nat:
  match n:
    case 0n: y
    case 1n+k: C.shift(8n, pw8(k, y))

def pw8_add(n: Nat, +x: Nat, +y: Nat) -> {pw8(n, Nat.add(x, y)) == Nat.add(pw8(n, x), pw8(n, y)) : Nat}:
  match n:
    case 0n:
      {==}
    case 1n+ +k:
      %Equal.sym(Nat, pw8(k, Nat.add(x, y)), Nat.add(pw8(k, x), pw8(k, y)), pw8_add(k, x, y)) : {C.shift(8n, _) == Nat.add(C.shift(8n, pw8(k, x)), C.shift(8n, pw8(k, y))) : Nat}
      %Equal.sym(Nat, C.shift(8n, Nat.add(pw8(k, x), pw8(k, y))), Nat.add(C.shift(8n, pw8(k, x)), C.shift(8n, pw8(k, y))), WW.shift_add(8n, pw8(k, x), pw8(k, y))) : {_ == Nat.add(C.shift(8n, pw8(k, x)), C.shift(8n, pw8(k, y))) : Nat}
      {==}

def pw8_zero(n: Nat) -> {pw8(n, 0n) == 0n : Nat}:
  match n:
    case 0n:
      {==}
    case 1n+ +k:
      %Equal.sym(Nat, pw8(k, 0n), 0n, pw8_zero(k)) : {C.shift(8n, _) == 0n : Nat}
      %Equal.sym(Nat, C.shift(8n, 0n), 0n, WW.shift_zero(8n)) : {_ == 0n : Nat}
      {==}

def pw8_shift(n: Nat, +y: Nat) -> {pw8(n, C.shift(8n, y)) == C.shift(8n, pw8(n, y)) : Nat}:
  match n:
    case 0n:
      {==}
    case 1n+ +k:
      %Equal.sym(Nat, pw8(k, C.shift(8n, y)), C.shift(8n, pw8(k, y)), pw8_shift(k, y)) : {C.shift(8n, _) == C.shift(8n, C.shift(8n, pw8(k, y))) : Nat}
      {==}

def le_app(xs: List<&2, U32>, +ys: List<&2, U32>) -> {le_val(List.append(&2, U32, xs, ys)) == Nat.add(le_val(xs), pw8(List.length(&2, U32, xs), le_val(ys))) : Nat}:
  match xs:
    case Nil{}:
      {==}
    case +x <> +t:
      %Equal.sym(Nat, le_val(List.append(&2, U32, t, ys)), Nat.add(le_val(t), pw8(List.length(&2, U32, t), le_val(ys))), le_app(t, ys)) : {Nat.add(B.byte(x), C.shift(8n, _)) == Nat.add(Nat.add(B.byte(x), C.shift(8n, le_val(t))), C.shift(8n, pw8(List.length(&2, U32, t), le_val(ys)))) : Nat}
      %Equal.sym(Nat, C.shift(8n, Nat.add(le_val(t), pw8(List.length(&2, U32, t), le_val(ys)))), Nat.add(C.shift(8n, le_val(t)), C.shift(8n, pw8(List.length(&2, U32, t), le_val(ys)))), WW.shift_add(8n, le_val(t), pw8(List.length(&2, U32, t), le_val(ys)))) : {Nat.add(B.byte(x), _) == Nat.add(Nat.add(B.byte(x), C.shift(8n, le_val(t))), C.shift(8n, pw8(List.length(&2, U32, t), le_val(ys)))) : Nat}
      %Equal.sym(Nat, Nat.add(Nat.add(B.byte(x), C.shift(8n, le_val(t))), C.shift(8n, pw8(List.length(&2, U32, t), le_val(ys)))), Nat.add(B.byte(x), Nat.add(C.shift(8n, le_val(t)), C.shift(8n, pw8(List.length(&2, U32, t), le_val(ys))))), NA.add_assoc(B.byte(x), C.shift(8n, le_val(t)), C.shift(8n, pw8(List.length(&2, U32, t), le_val(ys))))) : {Nat.add(B.byte(x), Nat.add(C.shift(8n, le_val(t)), C.shift(8n, pw8(List.length(&2, U32, t), le_val(ys))))) == _ : Nat}
      {==}

# ---- reverse ----

def app_assoc(xs: List<&2, U32>, +ys: List<&2, U32>, +zs: List<&2, U32>) -> {List.append(&2, U32, List.append(&2, U32, xs, ys), zs) == List.append(&2, U32, xs, List.append(&2, U32, ys, zs)) : List<&2, U32>}:
  match xs:
    case Nil{}:
      {==}
    case +x <> +t:
      Equal.cong(List<&2, U32>, List<&2, U32>, l => x <> l, List.append(&2, U32, List.append(&2, U32, t, ys), zs), List.append(&2, U32, t, List.append(&2, U32, ys, zs)), app_assoc(t, ys, zs))

def rev_go(xs: List<&2, U32>, +acc: List<&2, U32>) -> {List.reverse.go(&2, U32, xs, acc) == List.append(&2, U32, List.reverse.go(&2, U32, xs, Nil{}), acc) : List<&2, U32>}:
  match xs:
    case Nil{}:
      {==}
    case +x <> +t:
      Equal.trans(List<&2, U32>, List.reverse.go(&2, U32, t, x <> acc), List.append(&2, U32, List.reverse.go(&2, U32, t, Nil{}), x <> acc), List.append(&2, U32, List.reverse.go(&2, U32, t, [x]), acc), rev_go(t, x <> acc),
        Equal.trans(List<&2, U32>, List.append(&2, U32, List.reverse.go(&2, U32, t, Nil{}), x <> acc), List.append(&2, U32, List.append(&2, U32, List.reverse.go(&2, U32, t, Nil{}), [x]), acc), List.append(&2, U32, List.reverse.go(&2, U32, t, [x]), acc),
          Equal.sym(List<&2, U32>, List.append(&2, U32, List.append(&2, U32, List.reverse.go(&2, U32, t, Nil{}), [x]), acc), List.append(&2, U32, List.reverse.go(&2, U32, t, Nil{}), x <> acc), app_assoc(List.reverse.go(&2, U32, t, Nil{}), [x], acc)),
          Equal.cong(List<&2, U32>, List<&2, U32>, l => List.append(&2, U32, l, acc), List.append(&2, U32, List.reverse.go(&2, U32, t, Nil{}), [x]), List.reverse.go(&2, U32, t, [x]), Equal.sym(List<&2, U32>, List.reverse.go(&2, U32, t, [x]), List.append(&2, U32, List.reverse.go(&2, U32, t, Nil{}), [x]), rev_go(t, [x])))))

def rev_cons(+x: U32, +t: List<&2, U32>) -> {List.reverse(&2, U32, x <> t) == List.append(&2, U32, List.reverse(&2, U32, t), [x]) : List<&2, U32>}:
  rev_go(t, [x])

def len_app(xs: List<&2, U32>, +ys: List<&2, U32>) -> {List.length(&2, U32, List.append(&2, U32, xs, ys)) == Nat.add(List.length(&2, U32, xs), List.length(&2, U32, ys)) : Nat}:
  match xs:
    case Nil{}:
      {==}
    case +x <> +t:
      Equal.cong(Nat, Nat, n => 1n+n, List.length(&2, U32, List.append(&2, U32, t, ys)), Nat.add(List.length(&2, U32, t), List.length(&2, U32, ys)), len_app(t, ys))

def len_rev(xs: List<&2, U32>) -> {List.length(&2, U32, List.reverse(&2, U32, xs)) == List.length(&2, U32, xs) : Nat}:
  match xs:
    case Nil{}:
      {==}
    case +x <> +t:
      %Equal.sym(List<&2, U32>, List.reverse(&2, U32, x <> t), List.append(&2, U32, List.reverse(&2, U32, t), [x]), rev_cons(x, t)) : {List.length(&2, U32, _) == 1n+List.length(&2, U32, t) : Nat}
      %Equal.sym(Nat, List.length(&2, U32, List.append(&2, U32, List.reverse(&2, U32, t), [x])), Nat.add(List.length(&2, U32, List.reverse(&2, U32, t)), List.length(&2, U32, [x])), len_app(List.reverse(&2, U32, t), [x])) : {_ == 1n+List.length(&2, U32, t) : Nat}
      %Equal.sym(Nat, List.length(&2, U32, List.reverse(&2, U32, t)), List.length(&2, U32, t), len_rev(t)) : {Nat.add(_, List.length(&2, U32, [x])) == 1n+List.length(&2, U32, t) : Nat}
      %Equal.sym(Nat, 1n+List.length(&2, U32, t), Nat.add(List.length(&2, U32, t), 1n), SR.succ_add(1n, List.length(&2, U32, t))) : {Nat.add(List.length(&2, U32, t), 1n) == _ : Nat}
      {==}

# ---- OS2IP ----

def os2ip_go_v(bs: List<&2, U32>, +acc: Nat) -> {CV.os2ip_go(bs, acc) == Nat.add(pw8(List.length(&2, U32, bs), acc), le_val(List.reverse(&2, U32, bs))) : Nat}:
  match bs:
    case Nil{}:
      %Equal.sym(Nat, Nat.add(acc, 0n), acc, NA.add_zero(acc)) : {acc == _ : Nat}
      {==}
    case +b <> +t:
      %Equal.sym(Nat, CV.os2ip_go(t, Nat.add(C.shift(8n, acc), B.byte(b))), Nat.add(pw8(List.length(&2, U32, t), Nat.add(C.shift(8n, acc), B.byte(b))), le_val(List.reverse(&2, U32, t))), os2ip_go_v(t, Nat.add(C.shift(8n, acc), B.byte(b)))) : {_ == Nat.add(C.shift(8n, pw8(List.length(&2, U32, t), acc)), le_val(List.reverse(&2, U32, b <> t))) : Nat}
      %Equal.sym(List<&2, U32>, List.reverse(&2, U32, b <> t), List.append(&2, U32, List.reverse(&2, U32, t), [b]), rev_cons(b, t)) : {Nat.add(pw8(List.length(&2, U32, t), Nat.add(C.shift(8n, acc), B.byte(b))), le_val(List.reverse(&2, U32, t))) == Nat.add(C.shift(8n, pw8(List.length(&2, U32, t), acc)), le_val(_)) : Nat}
      %Equal.sym(Nat, le_val(List.append(&2, U32, List.reverse(&2, U32, t), [b])), Nat.add(le_val(List.reverse(&2, U32, t)), pw8(List.length(&2, U32, List.reverse(&2, U32, t)), le_val([b]))), le_app(List.reverse(&2, U32, t), [b])) : {Nat.add(pw8(List.length(&2, U32, t), Nat.add(C.shift(8n, acc), B.byte(b))), le_val(List.reverse(&2, U32, t))) == Nat.add(C.shift(8n, pw8(List.length(&2, U32, t), acc)), _) : Nat}
      %Equal.sym(Nat, List.length(&2, U32, List.reverse(&2, U32, t)), List.length(&2, U32, t), len_rev(t)) : {Nat.add(pw8(List.length(&2, U32, t), Nat.add(C.shift(8n, acc), B.byte(b))), le_val(List.reverse(&2, U32, t))) == Nat.add(C.shift(8n, pw8(List.length(&2, U32, t), acc)), Nat.add(le_val(List.reverse(&2, U32, t)), pw8(_, le_val([b])))) : Nat}
      %Equal.sym(Nat, pw8(List.length(&2, U32, t), Nat.add(C.shift(8n, acc), B.byte(b))), Nat.add(pw8(List.length(&2, U32, t), C.shift(8n, acc)), pw8(List.length(&2, U32, t), B.byte(b))), pw8_add(List.length(&2, U32, t), C.shift(8n, acc), B.byte(b))) : {Nat.add(_, le_val(List.reverse(&2, U32, t))) == Nat.add(C.shift(8n, pw8(List.length(&2, U32, t), acc)), Nat.add(le_val(List.reverse(&2, U32, t)), pw8(List.length(&2, U32, t), le_val([b])))) : Nat}
      %Equal.sym(Nat, pw8(List.length(&2, U32, t), C.shift(8n, acc)), C.shift(8n, pw8(List.length(&2, U32, t), acc)), pw8_shift(List.length(&2, U32, t), acc)) : {Nat.add(Nat.add(_, pw8(List.length(&2, U32, t), B.byte(b))), le_val(List.reverse(&2, U32, t))) == Nat.add(C.shift(8n, pw8(List.length(&2, U32, t), acc)), Nat.add(le_val(List.reverse(&2, U32, t)), pw8(List.length(&2, U32, t), le_val([b])))) : Nat}
      %Equal.sym(Nat, C.shift(8n, 0n), 0n, WW.shift_zero(8n)) : {Nat.add(Nat.add(C.shift(8n, pw8(List.length(&2, U32, t), acc)), pw8(List.length(&2, U32, t), B.byte(b))), le_val(List.reverse(&2, U32, t))) == Nat.add(C.shift(8n, pw8(List.length(&2, U32, t), acc)), Nat.add(le_val(List.reverse(&2, U32, t)), pw8(List.length(&2, U32, t), Nat.add(B.byte(b), _)))) : Nat}
      %Equal.sym(Nat, Nat.add(B.byte(b), 0n), B.byte(b), NA.add_zero(B.byte(b))) : {Nat.add(Nat.add(C.shift(8n, pw8(List.length(&2, U32, t), acc)), pw8(List.length(&2, U32, t), B.byte(b))), le_val(List.reverse(&2, U32, t))) == Nat.add(C.shift(8n, pw8(List.length(&2, U32, t), acc)), Nat.add(le_val(List.reverse(&2, U32, t)), pw8(List.length(&2, U32, t), _))) : Nat}
      %Equal.sym(Nat, Nat.add(C.shift(8n, pw8(List.length(&2, U32, t), acc)), pw8(List.length(&2, U32, t), B.byte(b))), Nat.add(pw8(List.length(&2, U32, t), B.byte(b)), C.shift(8n, pw8(List.length(&2, U32, t), acc))), NA.add_comm(C.shift(8n, pw8(List.length(&2, U32, t), acc)), pw8(List.length(&2, U32, t), B.byte(b)))) : {Nat.add(_, le_val(List.reverse(&2, U32, t))) == Nat.add(C.shift(8n, pw8(List.length(&2, U32, t), acc)), Nat.add(le_val(List.reverse(&2, U32, t)), pw8(List.length(&2, U32, t), B.byte(b)))) : Nat}
      %Equal.sym(Nat, Nat.add(Nat.add(pw8(List.length(&2, U32, t), B.byte(b)), C.shift(8n, pw8(List.length(&2, U32, t), acc))), le_val(List.reverse(&2, U32, t))), Nat.add(pw8(List.length(&2, U32, t), B.byte(b)), Nat.add(C.shift(8n, pw8(List.length(&2, U32, t), acc)), le_val(List.reverse(&2, U32, t)))), NA.add_assoc(pw8(List.length(&2, U32, t), B.byte(b)), C.shift(8n, pw8(List.length(&2, U32, t), acc)), le_val(List.reverse(&2, U32, t)))) : {_ == Nat.add(C.shift(8n, pw8(List.length(&2, U32, t), acc)), Nat.add(le_val(List.reverse(&2, U32, t)), pw8(List.length(&2, U32, t), B.byte(b)))) : Nat}
      %Equal.sym(Nat, Nat.add(C.shift(8n, pw8(List.length(&2, U32, t), acc)), le_val(List.reverse(&2, U32, t))), Nat.add(le_val(List.reverse(&2, U32, t)), C.shift(8n, pw8(List.length(&2, U32, t), acc))), NA.add_comm(C.shift(8n, pw8(List.length(&2, U32, t), acc)), le_val(List.reverse(&2, U32, t)))) : {Nat.add(pw8(List.length(&2, U32, t), B.byte(b)), _) == Nat.add(C.shift(8n, pw8(List.length(&2, U32, t), acc)), Nat.add(le_val(List.reverse(&2, U32, t)), pw8(List.length(&2, U32, t), B.byte(b)))) : Nat}
      %Equal.sym(Nat, Nat.add(pw8(List.length(&2, U32, t), B.byte(b)), Nat.add(le_val(List.reverse(&2, U32, t)), C.shift(8n, pw8(List.length(&2, U32, t), acc)))), Nat.add(le_val(List.reverse(&2, U32, t)), Nat.add(pw8(List.length(&2, U32, t), B.byte(b)), C.shift(8n, pw8(List.length(&2, U32, t), acc)))), NA.add_swap(pw8(List.length(&2, U32, t), B.byte(b)), le_val(List.reverse(&2, U32, t)), C.shift(8n, pw8(List.length(&2, U32, t), acc)))) : {_ == Nat.add(C.shift(8n, pw8(List.length(&2, U32, t), acc)), Nat.add(le_val(List.reverse(&2, U32, t)), pw8(List.length(&2, U32, t), B.byte(b)))) : Nat}
      %Equal.sym(Nat, Nat.add(C.shift(8n, pw8(List.length(&2, U32, t), acc)), Nat.add(le_val(List.reverse(&2, U32, t)), pw8(List.length(&2, U32, t), B.byte(b)))), Nat.add(le_val(List.reverse(&2, U32, t)), Nat.add(C.shift(8n, pw8(List.length(&2, U32, t), acc)), pw8(List.length(&2, U32, t), B.byte(b)))), NA.add_swap(C.shift(8n, pw8(List.length(&2, U32, t), acc)), le_val(List.reverse(&2, U32, t)), pw8(List.length(&2, U32, t), B.byte(b)))) : {Nat.add(le_val(List.reverse(&2, U32, t)), Nat.add(pw8(List.length(&2, U32, t), B.byte(b)), C.shift(8n, pw8(List.length(&2, U32, t), acc)))) == _ : Nat}
      %Equal.sym(Nat, Nat.add(C.shift(8n, pw8(List.length(&2, U32, t), acc)), pw8(List.length(&2, U32, t), B.byte(b))), Nat.add(pw8(List.length(&2, U32, t), B.byte(b)), C.shift(8n, pw8(List.length(&2, U32, t), acc))), NA.add_comm(C.shift(8n, pw8(List.length(&2, U32, t), acc)), pw8(List.length(&2, U32, t), B.byte(b)))) : {Nat.add(le_val(List.reverse(&2, U32, t)), Nat.add(pw8(List.length(&2, U32, t), B.byte(b)), C.shift(8n, pw8(List.length(&2, U32, t), acc)))) == Nat.add(le_val(List.reverse(&2, U32, t)), _) : Nat}
      {==}

def os2ip_v(+bs: List<&2, U32>) -> {CV.os2ip(bs) == le_val(List.reverse(&2, U32, bs)) : Nat}:
  %Equal.sym(Nat, CV.os2ip_go(bs, 0n), Nat.add(pw8(List.length(&2, U32, bs), 0n), le_val(List.reverse(&2, U32, bs))), os2ip_go_v(bs, 0n)) : {_ == le_val(List.reverse(&2, U32, bs)) : Nat}
  %Equal.sym(Nat, pw8(List.length(&2, U32, bs), 0n), 0n, pw8_zero(List.length(&2, U32, bs))) : {Nat.add(_, le_val(List.reverse(&2, U32, bs))) == le_val(List.reverse(&2, U32, bs)) : Nat}
  {==}

# ---- limbs of bytes ----

def limbs_le_v(cs: List<&2, U32>) -> {LV.ev(B.limbs_le(cs)) == le_val(cs) : Nat}:
  match cs:
    case Nil{}:
      {==}
    case +b0 <> Nil{}:
      %Equal.sym(Nat, C.shift(16n, 0n), 0n, WW.shift_zero(16n)) : {Nat.add(B.byte(b0), _) == Nat.add(B.byte(b0), C.shift(8n, 0n)) : Nat}
      %Equal.sym(Nat, Nat.add(B.byte(b0), 0n), B.byte(b0), NA.add_zero(B.byte(b0))) : {_ == Nat.add(B.byte(b0), C.shift(8n, 0n)) : Nat}
      %Equal.sym(Nat, C.shift(8n, 0n), 0n, WW.shift_zero(8n)) : {B.byte(b0) == Nat.add(B.byte(b0), _) : Nat}
      %Equal.sym(Nat, Nat.add(B.byte(b0), 0n), B.byte(b0), NA.add_zero(B.byte(b0))) : {B.byte(b0) == _ : Nat}
      {==}
    case +b0 <> +b1 <> +t:
      %Equal.sym(Nat, LV.ev(B.limbs_le(t)), le_val(t), limbs_le_v(t)) : {Nat.add(Nat.add(Nat.mul(B.byte(b1), 256n), B.byte(b0)), C.shift(16n, _)) == Nat.add(B.byte(b0), C.shift(8n, Nat.add(B.byte(b1), C.shift(8n, le_val(t))))) : Nat}
      %Equal.sym(Nat, Nat.mul(B.byte(b1), 256n), C.shift(8n, B.byte(b1)), LV.m256(B.byte(b1))) : {Nat.add(Nat.add(_, B.byte(b0)), C.shift(16n, le_val(t))) == Nat.add(B.byte(b0), C.shift(8n, Nat.add(B.byte(b1), C.shift(8n, le_val(t))))) : Nat}
      %Equal.sym(Nat, Nat.add(C.shift(8n, B.byte(b1)), B.byte(b0)), Nat.add(B.byte(b0), C.shift(8n, B.byte(b1))), NA.add_comm(C.shift(8n, B.byte(b1)), B.byte(b0))) : {Nat.add(_, C.shift(16n, le_val(t))) == Nat.add(B.byte(b0), C.shift(8n, Nat.add(B.byte(b1), C.shift(8n, le_val(t))))) : Nat}
      %Equal.sym(Nat, Nat.add(Nat.add(B.byte(b0), C.shift(8n, B.byte(b1))), C.shift(16n, le_val(t))), Nat.add(B.byte(b0), Nat.add(C.shift(8n, B.byte(b1)), C.shift(16n, le_val(t)))), NA.add_assoc(B.byte(b0), C.shift(8n, B.byte(b1)), C.shift(16n, le_val(t)))) : {_ == Nat.add(B.byte(b0), C.shift(8n, Nat.add(B.byte(b1), C.shift(8n, le_val(t))))) : Nat}
      %Equal.sym(Nat, C.shift(8n, Nat.add(B.byte(b1), C.shift(8n, le_val(t)))), Nat.add(C.shift(8n, B.byte(b1)), C.shift(8n, C.shift(8n, le_val(t)))), WW.shift_add(8n, B.byte(b1), C.shift(8n, le_val(t)))) : {Nat.add(B.byte(b0), Nat.add(C.shift(8n, B.byte(b1)), C.shift(16n, le_val(t)))) == Nat.add(B.byte(b0), _) : Nat}
      %Equal.sym(Nat, C.shift(8n, C.shift(8n, le_val(t))), C.shift(16n, le_val(t)), SR.shift_shift(8n, 8n, le_val(t))) : {Nat.add(B.byte(b0), Nat.add(C.shift(8n, B.byte(b1)), C.shift(16n, le_val(t)))) == Nat.add(B.byte(b0), Nat.add(C.shift(8n, B.byte(b1)), _)) : Nat}
      {==}

def of_be_v(+bs: List<&2, U32>) -> {LV.ev(B.of_be(bs)) == CV.os2ip(bs) : Nat}:
  %Equal.sym(Nat, LV.ev(B.limbs_le(List.reverse(&2, U32, bs))), le_val(List.reverse(&2, U32, bs)), limbs_le_v(List.reverse(&2, U32, bs))) : {_ == CV.os2ip(bs) : Nat}
  %Equal.sym(Nat, CV.os2ip(bs), le_val(List.reverse(&2, U32, bs)), os2ip_v(bs)) : {le_val(List.reverse(&2, U32, bs)) == _ : Nat}
  {==}

def of_be_value(+one: Nat, +h1: {one == 1n : Nat}, +bs: List<&2, U32>) -> {FS.value(one, B.of_be(bs)) == CV.os2ip(bs) : Nat}:
  %Equal.sym(Nat, FS.value(one, B.of_be(bs)), LV.ev(B.of_be(bs)), LV.ev_value(one, h1, B.of_be(bs))) : {_ == CV.os2ip(bs) : Nat}
  of_be_v(bs)

# ---- limb bounds ----

def byte_lt(+b: U32) -> {Nat.is_lt(B.byte(b), 256n) == True{} : Bool}:
  %Equal.sym(Nat, U32.to_nat(U32.and(b, 255)), C.low(8n, U32.to_nat(b)), FB.andm(b, 8n, 255, {==})) : {Nat.is_lt(_, 256n) == True{} : Bool}
  WW.low_lt(8n, U32.to_nat(b))

def byte_lt1(+one: Nat, +h1: {one == 1n : Nat}, +b: U32) -> {Nat.is_lt(B.byte(b), C.shift(8n, one)) == True{} : Bool}:
  %Equal.sym(Nat, C.shift(8n, one), 256n, LV.b8(one, h1)) : {Nat.is_lt(B.byte(b), _) == True{} : Bool}
  byte_lt(b)

# y 256 + x < 2^16 for bytes x, y
def limb_lt(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +y: U32) -> {Nat.is_lt(Nat.add(Nat.mul(B.byte(y), 256n), B.byte(x)), C.shift(16n, one)) == True{} : Bool}:
  %Equal.sym(Nat, Nat.mul(B.byte(y), 256n), C.shift(8n, B.byte(y)), LV.m256(B.byte(y))) : {Nat.is_lt(Nat.add(_, B.byte(x)), C.shift(16n, one)) == True{} : Bool}
  %Equal.sym(Nat, Nat.add(C.shift(8n, B.byte(y)), B.byte(x)), Nat.add(B.byte(x), C.shift(8n, B.byte(y))), NA.add_comm(C.shift(8n, B.byte(y)), B.byte(x))) : {Nat.is_lt(_, C.shift(16n, one)) == True{} : Bool}
  %Equal.sym(Nat, C.shift(16n, one), C.shift(8n, C.shift(8n, one)), Equal.sym(Nat, C.shift(8n, C.shift(8n, one)), C.shift(16n, one), SR.shift_shift(8n, 8n, one))) : {Nat.is_lt(Nat.add(B.byte(x), C.shift(8n, B.byte(y))), _) == True{} : Bool}
  I.digit_lt(8n, one, h1, B.byte(x), B.byte(y), C.shift(8n, one), byte_lt1(one, h1, x), byte_lt1(one, h1, y))

def limbs_le_ok(+one: Nat, +h1: {one == 1n : Nat}, k: Nat, cs: List<&2, U32>, +h: {B.has_len(Nat.double(k), cs) == True{} : Bool}) -> {FS.limbs16(one, k, B.limbs_le(cs)) == True{} : Bool}:
  match k cs:
    case 0n Nil{}:
      {==}
    case 0n c <> t:
      Empty.absurd({FS.limbs16(one, 0n, B.limbs_le(c <> t)) == True{} : Bool}, Lg.false_true(h))
    case 1n+j Nil{}:
      Empty.absurd({FS.limbs16(one, 1n+j, B.limbs_le([])) == True{} : Bool}, Lg.false_true(h))
    case 1n+j b0 <> Nil{}:
      Empty.absurd({FS.limbs16(one, 1n+j, B.limbs_le([b0])) == True{} : Bool}, Lg.false_true(h))
    case 1n+ +j +b0 <> +b1 <> +t:
      Lg.and_intro(Nat.is_lt(Nat.add(Nat.mul(B.byte(b1), 256n), B.byte(b0)), C.shift(16n, one)), FS.limbs16(one, j, B.limbs_le(t)), limb_lt(one, h1, b0, b1), limbs_le_ok(one, h1, j, t, h))

def has_len_v(n: Nat, bs: List<&2, U32>) -> {B.has_len(n, bs) == Nat.is_eq(List.length(&2, U32, bs), n) : Bool}:
  match n bs:
    case 0n Nil{}:
      {==}
    case 0n b <> t:
      {==}
    case 1n+k Nil{}:
      {==}
    case 1n+ +k b <> +t:
      has_len_v(k, t)

def has_len_rev(+n: Nat, +bs: List<&2, U32>, +h: {B.has_len(n, bs) == True{} : Bool}) -> {B.has_len(n, List.reverse(&2, U32, bs)) == True{} : Bool}:
  %Equal.sym(Bool, B.has_len(n, List.reverse(&2, U32, bs)), Nat.is_eq(List.length(&2, U32, List.reverse(&2, U32, bs)), n), has_len_v(n, List.reverse(&2, U32, bs))) : {_ == True{} : Bool}
  %Equal.sym(Nat, List.length(&2, U32, List.reverse(&2, U32, bs)), List.length(&2, U32, bs), len_rev(bs)) : {Nat.is_eq(_, n) == True{} : Bool}
  %Equal.sym(Bool, Nat.is_eq(List.length(&2, U32, bs), n), B.has_len(n, bs), Equal.sym(Bool, B.has_len(n, bs), Nat.is_eq(List.length(&2, U32, bs), n), has_len_v(n, bs))) : {_ == True{} : Bool}
  h

def of_be_limbs(+one: Nat, +h1: {one == 1n : Nat}, +bs: List<&2, U32>, +h: {B.has_len(32n, bs) == True{} : Bool}) -> {FS.limbs16(one, 16n, B.of_be(bs)) == True{} : Bool}:
  limbs_le_ok(one, h1, 16n, List.reverse(&2, U32, bs), has_len_rev(32n, bs, h))

# ---- I2OSP ----

def low8(+n: Nat) -> {C.low(8n, n) == Nat.mod(n, 256n) : Nat}:
  +lo = C.low(8n, n)
  +hi = C.high(8n, n)
  +e = Equal.trans(Nat, n, Nat.add(lo, C.shift(8n, hi)), Nat.add(Nat.mul(hi, 256n), lo), WW.low_high(8n, n), Equal.trans(Nat, Nat.add(lo, C.shift(8n, hi)), Nat.add(C.shift(8n, hi), lo), Nat.add(Nat.mul(hi, 256n), lo), NA.add_comm(lo, C.shift(8n, hi)), Equal.cong(Nat, Nat, z => Nat.add(z, lo), C.shift(8n, hi), Nat.mul(hi, 256n), Equal.sym(Nat, Nat.mul(hi, 256n), C.shift(8n, hi), LV.m256(hi)))))
  %Equal.sym(Nat, n, Nat.add(Nat.mul(C.high(8n, n), 256n), C.low(8n, n)), e) : {C.low(8n, n) == Nat.mod(_, 256n) : Nat}
  Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(hi, 256n), lo), 256n), lo, NR.mod_of(hi, 255n, lo, WW.low_lt(8n, n)))

def high8(+n: Nat) -> {C.high(8n, n) == Nat.div(n, 256n) : Nat}:
  +lo = C.low(8n, n)
  +hi = C.high(8n, n)
  +e = Equal.trans(Nat, n, Nat.add(lo, C.shift(8n, hi)), Nat.add(Nat.mul(hi, 256n), lo), WW.low_high(8n, n), Equal.trans(Nat, Nat.add(lo, C.shift(8n, hi)), Nat.add(C.shift(8n, hi), lo), Nat.add(Nat.mul(hi, 256n), lo), NA.add_comm(lo, C.shift(8n, hi)), Equal.cong(Nat, Nat, z => Nat.add(z, lo), C.shift(8n, hi), Nat.mul(hi, 256n), Equal.sym(Nat, Nat.mul(hi, 256n), C.shift(8n, hi), LV.m256(hi)))))
  %Equal.sym(Nat, n, Nat.add(Nat.mul(C.high(8n, n), 256n), C.low(8n, n)), e) : {C.high(8n, n) == Nat.div(_, 256n) : Nat}
  Equal.sym(Nat, Nat.div(Nat.add(Nat.mul(hi, 256n), lo), 256n), hi, NR.div_of(hi, 255n, lo, WW.low_lt(8n, n)))

# x < 2^k (2^k with a symbolic one): x fits k bits
def fits_one(k: Nat, +one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +hx: {Nat.is_lt(x, C.shift(k, one)) == True{} : Bool}) -> {C.fits(k, x) == True{} : Bool}:
  match k:
    case 0n:
      +hx1 = I.lt_subst_r(x, one, 1n, h1, hx)
      +e0 = N.le_antisym(x, 0n, N.lt_succ_le(x, 0n, hx1), N.zero_le(x))
      %Equal.sym(Nat, x, 0n, e0) : {Nat.is_eq(_, 0n) == True{} : Bool}
      {==}
    case 1n+ +j:
      +hh = Equal.trans(Bool, Nat.is_lt(C.half(x), C.shift(j, one)), Nat.is_lt(x, Nat.double(C.shift(j, one))), True{}, WW.lt_half(x, C.shift(j, one)), hx)
      fits_one(j, one, h1, C.half(x), hh)

# low 8 bits of x + 2^16 r: those of x
def low_v(+x: Nat, +r: Nat) -> {C.low(8n, Nat.add(x, C.shift(16n, r))) == Nat.mod(x, 256n) : Nat}:
  %Equal.sym(Nat, C.shift(16n, r), C.shift(8n, C.shift(8n, r)), Equal.sym(Nat, C.shift(8n, C.shift(8n, r)), C.shift(16n, r), SR.shift_shift(8n, 8n, r))) : {C.low(8n, Nat.add(x, _)) == Nat.mod(x, 256n) : Nat}
  %Equal.sym(Nat, C.low(8n, Nat.add(x, C.shift(8n, C.shift(8n, r)))), C.low(8n, x), WW.low_add_shift(8n, x, C.shift(8n, r))) : {_ == Nat.mod(x, 256n) : Nat}
  low8(x)

def fh8(+x: Nat, +f16: {C.fits(16n, x) == True{} : Bool}) -> {C.fits(8n, C.high(8n, x)) == True{} : Bool}:
  %Equal.sym(Nat, C.high(8n, C.high(8n, x)), C.high(16n, x), Equal.sym(Nat, C.high(16n, x), C.high(8n, C.high(8n, x)), WW.high_comp(8n, 8n, x))) : {Nat.is_eq(_, 0n) == True{} : Bool}
  f16

# the next 8 bits: x div 256 (x < 2^16)
def mid_v(+x: Nat, +r: Nat, +f16: {C.fits(16n, x) == True{} : Bool}) -> {C.low(8n, C.high(8n, Nat.add(x, C.shift(16n, r)))) == Nat.div(x, 256n) : Nat}:
  %Equal.sym(Nat, C.shift(16n, r), C.shift(8n, C.shift(8n, r)), Equal.sym(Nat, C.shift(8n, C.shift(8n, r)), C.shift(16n, r), SR.shift_shift(8n, 8n, r))) : {C.low(8n, C.high(8n, Nat.add(x, _))) == Nat.div(x, 256n) : Nat}
  %Equal.sym(Nat, C.high(8n, Nat.add(x, C.shift(8n, C.shift(8n, r)))), Nat.add(C.high(8n, x), C.shift(8n, r)), WW.high_add_shift(8n, x, C.shift(8n, r))) : {C.low(8n, _) == Nat.div(x, 256n) : Nat}
  %Equal.sym(Nat, C.low(8n, Nat.add(C.high(8n, x), C.shift(8n, r))), C.low(8n, C.high(8n, x)), WW.low_add_shift(8n, C.high(8n, x), r)) : {_ == Nat.div(x, 256n) : Nat}
  %Equal.sym(Nat, C.low(8n, C.high(8n, x)), C.high(8n, x), WW.low_fit(8n, C.high(8n, x), fh8(x, f16))) : {_ == Nat.div(x, 256n) : Nat}
  high8(x)

# the rest: r
def top_v(+x: Nat, +r: Nat, +f16: {C.fits(16n, x) == True{} : Bool}) -> {C.high(8n, C.high(8n, Nat.add(x, C.shift(16n, r)))) == r : Nat}:
  %Equal.sym(Nat, C.high(8n, C.high(8n, Nat.add(x, C.shift(16n, r)))), C.high(16n, Nat.add(x, C.shift(16n, r))), Equal.sym(Nat, C.high(16n, Nat.add(x, C.shift(16n, r))), C.high(8n, C.high(8n, Nat.add(x, C.shift(16n, r)))), WW.high_comp(8n, 8n, Nat.add(x, C.shift(16n, r))))) : {_ == r : Nat}
  %Equal.sym(Nat, C.high(16n, Nat.add(x, C.shift(16n, r))), Nat.add(C.high(16n, x), r), WW.high_add_shift(16n, x, r)) : {_ == r : Nat}
  %Equal.sym(Nat, C.high(16n, x), 0n, N.eq_from_is_eq(C.high(16n, x), 0n, f16)) : {Nat.add(_, r) == r : Nat}
  {==}

def bytes_le_v(+one: Nat, +h1: {one == 1n : Nat}, k: Nat, xs: List<&2, Nat>, +h: {FS.limbs16(one, k, xs) == True{} : Bool}) -> {B.bytes_le(xs) == CV.i2osp_le(Nat.double(k), LV.ev(xs)) : List<&2, U32>}:
  match k xs:
    case 0n Nil{}:
      {==}
    case 0n x <> t:
      Empty.absurd({B.bytes_le(x <> t) == CV.i2osp_le(Nat.double(0n), LV.ev(x <> t)) : List<&2, U32>}, Lg.false_true(h))
    case 1n+j Nil{}:
      Empty.absurd({B.bytes_le([]) == CV.i2osp_le(Nat.double(1n+j), LV.ev([])) : List<&2, U32>}, Lg.false_true(h))
    case 1n+ +j +x <> +t:
      +hx = Lg.and_left(Nat.is_lt(x, C.shift(16n, one)), FS.limbs16(one, j, t), h)
      +ht = Lg.and_right(Nat.is_lt(x, C.shift(16n, one)), FS.limbs16(one, j, t), h)
      +f16 = fits_one(16n, one, h1, x, hx)
      +v = Nat.add(x, C.shift(16n, LV.ev(t)))
      +e1 = low_v(x, LV.ev(t))
      +e2 = mid_v(x, LV.ev(t), f16)
      +e3 = top_v(x, LV.ev(t), f16)
      %Equal.sym(Nat, C.low(8n, Nat.add(x, C.shift(16n, LV.ev(t)))), Nat.mod(x, 256n), e1) : {U32.from_nat(Nat.mod(x, 256n)) <> U32.from_nat(Nat.div(x, 256n)) <> B.bytes_le(t) == U32.from_nat(_) <> U32.from_nat(C.low(8n, C.high(8n, Nat.add(x, C.shift(16n, LV.ev(t)))))) <> CV.i2osp_le(Nat.double(j), C.high(8n, C.high(8n, Nat.add(x, C.shift(16n, LV.ev(t)))))) : List<&2, U32>}
      %Equal.sym(Nat, C.low(8n, C.high(8n, Nat.add(x, C.shift(16n, LV.ev(t))))), Nat.div(x, 256n), e2) : {U32.from_nat(Nat.mod(x, 256n)) <> U32.from_nat(Nat.div(x, 256n)) <> B.bytes_le(t) == U32.from_nat(Nat.mod(x, 256n)) <> U32.from_nat(_) <> CV.i2osp_le(Nat.double(j), C.high(8n, C.high(8n, Nat.add(x, C.shift(16n, LV.ev(t)))))) : List<&2, U32>}
      %Equal.sym(Nat, C.high(8n, C.high(8n, Nat.add(x, C.shift(16n, LV.ev(t))))), LV.ev(t), e3) : {U32.from_nat(Nat.mod(x, 256n)) <> U32.from_nat(Nat.div(x, 256n)) <> B.bytes_le(t) == U32.from_nat(Nat.mod(x, 256n)) <> U32.from_nat(Nat.div(x, 256n)) <> CV.i2osp_le(Nat.double(j), _) : List<&2, U32>}
      %Equal.sym(List<&2, U32>, B.bytes_le(t), CV.i2osp_le(Nat.double(j), LV.ev(t)), bytes_le_v(one, h1, j, t, ht)) : {U32.from_nat(Nat.mod(x, 256n)) <> U32.from_nat(Nat.div(x, 256n)) <> _ == U32.from_nat(Nat.mod(x, 256n)) <> U32.from_nat(Nat.div(x, 256n)) <> CV.i2osp_le(Nat.double(j), LV.ev(t)) : List<&2, U32>}
      {==}

def i2_is(+n: Nat, x: Nat) -> {CV.i2osp(n, x) == CV.i2osp_go(n, x) : List<&2, U32>}:
  match x:
    case 0n:
      {==}
    case 1n+k:
      {==}

def to_be_v(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, Nat>, +h: {FS.limbs16(one, 16n, xs) == True{} : Bool}) -> {B.to_be(xs) == CV.i2osp(32n, LV.ev(xs)) : List<&2, U32>}:
  %Equal.sym(List<&2, U32>, CV.i2osp(32n, LV.ev(xs)), CV.i2osp_go(32n, LV.ev(xs)), i2_is(32n, LV.ev(xs))) : {B.to_be(xs) == _ : List<&2, U32>}
  %Equal.sym(List<&2, U32>, B.bytes_le(xs), CV.i2osp_le(Nat.double(16n), LV.ev(xs)), bytes_le_v(one, h1, 16n, xs, h)) : {List.reverse(&2, U32, _) == List.reverse(&2, U32, CV.i2osp_le(32n, LV.ev(xs))) : List<&2, U32>}
  {==}