proofs/crypto/secp256k1/bytes.bend

bend-collections-laws-crypto@1.0.0.0 · 301 lines · 33 definitions

1# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/bytes.src; edit the .src
2import Base
3import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as FS
5import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend as CV
6import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend as B
7import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
8import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as Lg
9import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
10import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
11import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW
12import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/u32and.bend as FB
13import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/semiring.bend as SR
14import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend as LV
15import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend as I
16
17# Octet strings (SEC 1 OS2IP / I2OSP, spec/crypto/secp256k1/curve.bend)
18# and the 16-bit limbs of src/crypto/secp256k1/bytes.bend.
19
20# the little-endian value of bytes
21def le_val(bs: List<&2, U32>) -> Nat:
22  match bs:
23    case Nil{}: 0n
24    case b <> t: Nat.add(B.byte(b), C.shift(8n, le_val(t)))
25
26def pw8(n: Nat, +y: Nat) -> Nat:
27  match n:
28    case 0n: y
29    case 1n+k: C.shift(8n, pw8(k, y))
30
31def pw8_add(n: Nat, +x: Nat, +y: Nat) -> {pw8(n, Nat.add(x, y)) == Nat.add(pw8(n, x), pw8(n, y)) : Nat}:
32  match n:
33    case 0n:
34      {==}
35    case 1n+ +k:
36      %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}
37      %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}
38      {==}
39
40def pw8_zero(n: Nat) -> {pw8(n, 0n) == 0n : Nat}:
41  match n:
42    case 0n:
43      {==}
44    case 1n+ +k:
45      %Equal.sym(Nat, pw8(k, 0n), 0n, pw8_zero(k)) : {C.shift(8n, _) == 0n : Nat}
46      %Equal.sym(Nat, C.shift(8n, 0n), 0n, WW.shift_zero(8n)) : {_ == 0n : Nat}
47      {==}
48
49def pw8_shift(n: Nat, +y: Nat) -> {pw8(n, C.shift(8n, y)) == C.shift(8n, pw8(n, y)) : Nat}:
50  match n:
51    case 0n:
52      {==}
53    case 1n+ +k:
54      %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}
55      {==}
56
57def 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}:
58  match xs:
59    case Nil{}:
60      {==}
61    case +x <> +t:
62      %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}
63      %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}
64      %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}
65      {==}
66
67# ---- reverse ----
68
69def 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>}:
70  match xs:
71    case Nil{}:
72      {==}
73    case +x <> +t:
74      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))
75
76def 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>}:
77  match xs:
78    case Nil{}:
79      {==}
80    case +x <> +t:
81      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),
82        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),
83          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)),
84          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])))))
85
86def 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>}:
87  rev_go(t, [x])
88
89def 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}:
90  match xs:
91    case Nil{}:
92      {==}
93    case +x <> +t:
94      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))
95
96def len_rev(xs: List<&2, U32>) -> {List.length(&2, U32, List.reverse(&2, U32, xs)) == List.length(&2, U32, xs) : Nat}:
97  match xs:
98    case Nil{}:
99      {==}
100    case +x <> +t:
101      %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}
102      %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}
103      %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}
104      %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}
105      {==}
106
107# ---- OS2IP ----
108
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      {==}
130
131def os2ip_v(+bs: List<&2, U32>) -> {CV.os2ip(bs) == le_val(List.reverse(&2, U32, bs)) : Nat}:
132  %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}
133  %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}
134  {==}
135
136# ---- limbs of bytes ----
137
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      {==}
156
157def of_be_v(+bs: List<&2, U32>) -> {LV.ev(B.of_be(bs)) == CV.os2ip(bs) : Nat}:
158  %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}
159  %Equal.sym(Nat, CV.os2ip(bs), le_val(List.reverse(&2, U32, bs)), os2ip_v(bs)) : {le_val(List.reverse(&2, U32, bs)) == _ : Nat}
160  {==}
161
162def of_be_value(+one: Nat, +h1: {one == 1n : Nat}, +bs: List<&2, U32>) -> {FS.value(one, B.of_be(bs)) == CV.os2ip(bs) : Nat}:
163  %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}
164  of_be_v(bs)
165
166# ---- limb bounds ----
167
168def byte_lt(+b: U32) -> {Nat.is_lt(B.byte(b), 256n) == True{} : Bool}:
169  %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}
170  WW.low_lt(8n, U32.to_nat(b))
171
172def byte_lt1(+one: Nat, +h1: {one == 1n : Nat}, +b: U32) -> {Nat.is_lt(B.byte(b), C.shift(8n, one)) == True{} : Bool}:
173  %Equal.sym(Nat, C.shift(8n, one), 256n, LV.b8(one, h1)) : {Nat.is_lt(B.byte(b), _) == True{} : Bool}
174  byte_lt(b)
175
176# y 256 + x < 2^16 for bytes x, y
177def 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}:
178  %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}
179  %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}
180  %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}
181  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))
182
183def 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}:
184  match k cs:
185    case 0n Nil{}:
186      {==}
187    case 0n c <> t:
188      Empty.absurd({FS.limbs16(one, 0n, B.limbs_le(c <> t)) == True{} : Bool}, Lg.false_true(h))
189    case 1n+j Nil{}:
190      Empty.absurd({FS.limbs16(one, 1n+j, B.limbs_le([])) == True{} : Bool}, Lg.false_true(h))
191    case 1n+j b0 <> Nil{}:
192      Empty.absurd({FS.limbs16(one, 1n+j, B.limbs_le([b0])) == True{} : Bool}, Lg.false_true(h))
193    case 1n+ +j +b0 <> +b1 <> +t:
194      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))
195
196def has_len_v(n: Nat, bs: List<&2, U32>) -> {B.has_len(n, bs) == Nat.is_eq(List.length(&2, U32, bs), n) : Bool}:
197  match n bs:
198    case 0n Nil{}:
199      {==}
200    case 0n b <> t:
201      {==}
202    case 1n+k Nil{}:
203      {==}
204    case 1n+ +k b <> +t:
205      has_len_v(k, t)
206
207def 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}:
208  %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}
209  %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}
210  %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}
211  h
212
213def 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}:
214  limbs_le_ok(one, h1, 16n, List.reverse(&2, U32, bs), has_len_rev(32n, bs, h))
215
216# ---- I2OSP ----
217
218def low8(+n: Nat) -> {C.low(8n, n) == Nat.mod(n, 256n) : Nat}:
219  +lo = C.low(8n, n)
220  +hi = C.high(8n, n)
221  +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)))))
222  %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}
223  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)))
224
225def high8(+n: Nat) -> {C.high(8n, n) == Nat.div(n, 256n) : Nat}:
226  +lo = C.low(8n, n)
227  +hi = C.high(8n, n)
228  +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)))))
229  %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}
230  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)))
231
232# x < 2^k (2^k with a symbolic one): x fits k bits
233def 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}:
234  match k:
235    case 0n:
236      +hx1 = I.lt_subst_r(x, one, 1n, h1, hx)
237      +e0 = N.le_antisym(x, 0n, N.lt_succ_le(x, 0n, hx1), N.zero_le(x))
238      %Equal.sym(Nat, x, 0n, e0) : {Nat.is_eq(_, 0n) == True{} : Bool}
239      {==}
240    case 1n+ +j:
241      +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)
242      fits_one(j, one, h1, C.half(x), hh)
243
244# low 8 bits of x + 2^16 r: those of x
245def low_v(+x: Nat, +r: Nat) -> {C.low(8n, Nat.add(x, C.shift(16n, r))) == Nat.mod(x, 256n) : Nat}:
246  %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}
247  %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}
248  low8(x)
249
250def fh8(+x: Nat, +f16: {C.fits(16n, x) == True{} : Bool}) -> {C.fits(8n, C.high(8n, x)) == True{} : Bool}:
251  %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}
252  f16
253
254# the next 8 bits: x div 256 (x < 2^16)
255def 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}:
256  %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}
257  %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}
258  %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}
259  %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}
260  high8(x)
261
262# the rest: r
263def 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}:
264  %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}
265  %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}
266  %Equal.sym(Nat, C.high(16n, x), 0n, N.eq_from_is_eq(C.high(16n, x), 0n, f16)) : {Nat.add(_, r) == r : Nat}
267  {==}
268
269def 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>}:
270  match k xs:
271    case 0n Nil{}:
272      {==}
273    case 0n x <> t:
274      Empty.absurd({B.bytes_le(x <> t) == CV.i2osp_le(Nat.double(0n), LV.ev(x <> t)) : List<&2, U32>}, Lg.false_true(h))
275    case 1n+j Nil{}:
276      Empty.absurd({B.bytes_le([]) == CV.i2osp_le(Nat.double(1n+j), LV.ev([])) : List<&2, U32>}, Lg.false_true(h))
277    case 1n+ +j +x <> +t:
278      +hx = Lg.and_left(Nat.is_lt(x, C.shift(16n, one)), FS.limbs16(one, j, t), h)
279      +ht = Lg.and_right(Nat.is_lt(x, C.shift(16n, one)), FS.limbs16(one, j, t), h)
280      +f16 = fits_one(16n, one, h1, x, hx)
281      +v = Nat.add(x, C.shift(16n, LV.ev(t)))
282      +e1 = low_v(x, LV.ev(t))
283      +e2 = mid_v(x, LV.ev(t), f16)
284      +e3 = top_v(x, LV.ev(t), f16)
285      %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>}
286      %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>}
287      %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>}
288      %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>}
289      {==}
290
291def i2_is(+n: Nat, x: Nat) -> {CV.i2osp(n, x) == CV.i2osp_go(n, x) : List<&2, U32>}:
292  match x:
293    case 0n:
294      {==}
295    case 1n+k:
296      {==}
297
298def 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>}:
299  %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>}
300  %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>}
301  {==}