Bytes.os2ip_go_v: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend as Bytes
Lines 109-129 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend&start_line=109&end_line=129

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend as CV
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend as B
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW

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}
      {==}

Uses (23):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.reverse
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend&name=le_app
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend&name=le_val
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend&name=len_rev
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend&name=pw8
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend&name=pw8_add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend&name=pw8_shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend&name=rev_cons
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_comm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_swap
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend&name=shift_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=os2ip_go
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend&name=byte