def os2ip_go_v
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/bytes.bend:109
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend as Bytes
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
109def 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}:
110 match bs:
111 case Nil{}:
112 %Equal.sym(Nat, Nat.add(acc, 0n), acc, NA.add_zero(acc)) : {acc == _ : Nat}
113 {==}
114 case +b <> +t:
115 %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}
116 %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}
117 %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}
118 %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}
119 %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}
120 %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}
121 %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}
122 %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}
123 %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}
124 %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}
125 %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}
126 %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}
127 %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}
128 %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}
129 {==}