def limbs_le_v

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/bytes.bend:138

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/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
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/semiring.bend as SR
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend as LV

138def limbs_le_v(cs: List<&2, U32>) -> {LV.ev(B.limbs_le(cs)) == le_val(cs) : Nat}:
139  match cs:
140    case Nil{}:
141      {==}
142    case +b0 <> Nil{}:
143      %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}
144      %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}
145      %Equal.sym(Nat, C.shift(8n, 0n), 0n, WW.shift_zero(8n)) : {B.byte(b0) == Nat.add(B.byte(b0), _) : Nat}
146      %Equal.sym(Nat, Nat.add(B.byte(b0), 0n), B.byte(b0), NA.add_zero(B.byte(b0))) : {B.byte(b0) == _ : Nat}
147      {==}
148    case +b0 <> +b1 <> +t:
149      %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}
150      %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}
151      %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}
152      %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}
153      %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}
154      %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}
155      {==}