proofs/crypto/secp256k1/psign.bend

bend-collections-laws-crypto@1.0.0.0 · 266 lines · 27 definitions

1# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/psign.src; edit the .src
2import Base
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as FS
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend as CV
5import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend as ES
6import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend as L
7import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/field.bend as F
8import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/scalar.bend as S
9import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend as B
10import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend as P
11import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/ecdsa.bend as E
12import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as Lg
13import bend-collections-laws-crypto@1.0.0.0/spec/crypto/hmac.bend as HMS
14import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/mac/hmac.bend as MH
15import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend as LV
16import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/scalarops.bend as SO
17import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/scalarpow.bend as SP
18import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fwrap.bend as FW
19import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend as BY
20import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend as PT
21import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/sel.bend as SL
22import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pmul.bend as PM
23import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/paff.bend as PA
24import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/penc.bend as PE
25import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pver.bend as PV
26import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/blist.bend as BL
27import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pscal.bend as SQ
28
29# ECDSA signing of src/crypto/secp256k1/ecdsa.bend (RFC 6979 nonces,
30# low-S, recovery id) against spec/crypto/secp256k1/ecdsa.bend. The
31# implementation's signature record r, s, v is the specification's
32# r || s || v.
33
34def sigb(sig: E.Signature) -> List<&2, U32>:
35  match sig:
36    case E.Signature{r, s, v}: List.append(&2, U32, r, List.append(&2, U32, s, [v]))
37
38def msig(m: Maybe<&2, E.Signature>) -> Maybe<&2, List<&2, U32>>:
39  match m:
40    case None{}: None{}
41    case Some{sig}: Some{sigb(sig)}
42
43def matt(a: E.Attempt) -> ES.Attempt:
44  match a:
45    case E.ARetry{}: ES.Retry{}
46    case E.ADone{sig}: ES.Sig{sigb(sig)}
47
48def dr(g: E.Drbg) -> ES.Drbg:
49  match g:
50    case E.Drbg{k, v}: ES.Drbg{k, v}
51
52# ---- r, s and the recovery id ----
53
54def tbv(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +hx: {FS.limbs16(one, 16n, x) == True{} : Bool}) -> {B.to_be(x) == CV.i2osp(32n, FS.value(one, x)) : List<&2, U32>}:
55  %Equal.sym(List<&2, U32>, B.to_be(x), CV.i2osp(32n, LV.ev(x)), BY.to_be_v(one, h1, x, hx)) : {_ == CV.i2osp(32n, FS.value(one, x)) : List<&2, U32>}
56  %Equal.sym(Nat, FS.value(one, x), LV.ev(x), LV.ev_value(one, h1, x)) : {CV.i2osp(32n, LV.ev(x)) == CV.i2osp(32n, _) : List<&2, U32>}
57  {==}
58
59def id_v(lb: Bool, hb: Bool, q: Nat, +hq: {Nat.is_lt(q, 2n) == True{} : Bool}) -> {Nat.add(Nat.mul(E.b2n(Bool.not(lb)), 2n), Nat.sub(Nat.add(q, E.b2n(hb)), Nat.mul(Nat.mul(q, E.b2n(hb)), 2n))) == Nat.add(ES.ge2(lb), ES.flip(hb, q)) : Nat}:
60  match lb hb q:
61    case True{} True{} 0n:
62      {==}
63    case True{} True{} 1n:
64      {==}
65    case True{} False{} 0n:
66      {==}
67    case True{} False{} 1n:
68      {==}
69    case False{} True{} 0n:
70      {==}
71    case False{} True{} 1n:
72      {==}
73    case False{} False{} 0n:
74      {==}
75    case False{} False{} 1n:
76      {==}
77    case _ _ 2n+ +c:
78      Empty.absurd({Nat.add(Nat.mul(E.b2n(Bool.not(lb)), 2n), Nat.sub(Nat.add(2n+c, E.b2n(hb)), Nat.mul(Nat.mul(2n+c, E.b2n(hb)), 2n))) == Nat.add(ES.ge2(lb), ES.flip(hb, 2n+c)) : Nat}, SL.not01(c, hq))
79
80def sel_v(+one: Nat, +h1: {one == 1n : Nat}, hb: Bool, +s0: List<&2, Nat>, +hs: {FS.reduced(one, FS.order(one), s0) == True{} : Bool}) -> {B.to_be(S.select(E.b2n(hb), S.neg(s0), s0)) == CV.i2osp(32n, ES.low(hb, FS.order(one), FS.value(one, s0))) : List<&2, U32>}:
81  match hb:
82    case True{}:
83      %Equal.sym(List<&2, Nat>, L.select(1n, S.neg(s0), s0), S.neg(s0), SL.sel1(one, 16n, S.neg(s0), s0, SL.sl16(one, S.neg(s0), SO.neg_r(one, h1, s0, hs)), SL.sl16(one, s0, hs))) : {B.to_be(_) == CV.i2osp(32n, FS.mneg(FS.order(one), FS.value(one, s0))) : List<&2, U32>}
84      %Equal.sym(List<&2, U32>, B.to_be(S.neg(s0)), CV.i2osp(32n, FS.value(one, S.neg(s0))), tbv(one, h1, S.neg(s0), SL.sl16(one, S.neg(s0), SO.neg_r(one, h1, s0, hs)))) : {_ == CV.i2osp(32n, FS.mneg(FS.order(one), FS.value(one, s0))) : List<&2, U32>}
85      %Equal.sym(Nat, FS.value(one, S.neg(s0)), FS.mneg(FS.order(one), FS.value(one, s0)), SO.neg_v(one, h1, s0, hs)) : {CV.i2osp(32n, _) == CV.i2osp(32n, FS.mneg(FS.order(one), FS.value(one, s0))) : List<&2, U32>}
86      {==}
87    case False{}:
88      %Equal.sym(List<&2, Nat>, L.select(0n, S.neg(s0), s0), s0, SL.sel0(one, 16n, S.neg(s0), s0, SL.sl16(one, S.neg(s0), SO.neg_r(one, h1, s0, hs)), SL.sl16(one, s0, hs))) : {B.to_be(_) == CV.i2osp(32n, FS.value(one, s0)) : List<&2, U32>}
89      tbv(one, h1, s0, SL.sl16(one, s0, hs))
90
91def bad_v(bad: Bool, +sig: E.Signature) -> {matt(E.finish_if(bad, sig)) == ES.finish_if(bad, sigb(sig)) : ES.Attempt}:
92  match bad:
93    case True{}:
94      {==}
95    case False{}:
96      {==}
97
98def s0_r(+one: Nat, +h1: {one == 1n : Nat}, +z: List<&2, Nat>, +hz: {FS.reduced(one, FS.order(one), z) == True{} : Bool}, +d: List<&2, Nat>, +hd: {FS.reduced(one, FS.order(one), d) == True{} : Bool}, +k: List<&2, Nat>, +hk: {FS.reduced(one, FS.order(one), k) == True{} : Bool}, +x: List<&2, Nat>, +hx: {FS.limbs16(one, 16n, x) == True{} : Bool}) -> {FS.reduced(one, FS.order(one), S.mul(S.inv(k), S.add(z, S.mul(S.reduce(x), d)))) == True{} : Bool}:
99  +hr = SQ.sred_r(one, h1, x, hx)
100  SO.mul_r(one, h1, S.inv(k), S.add(z, S.mul(S.reduce(x), d)), SP.inv_r(one, h1, k, hk), SO.add_r(one, h1, z, S.mul(S.reduce(x), d), hz, SO.mul_r(one, h1, S.reduce(x), d, hr, hd)))
101
102def s0_v(+one: Nat, +h1: {one == 1n : Nat}, +z: List<&2, Nat>, +hz: {FS.reduced(one, FS.order(one), z) == True{} : Bool}, +d: List<&2, Nat>, +hd: {FS.reduced(one, FS.order(one), d) == True{} : Bool}, +k: List<&2, Nat>, +hk: {FS.reduced(one, FS.order(one), k) == True{} : Bool}, +x: List<&2, Nat>, +hx: {FS.limbs16(one, 16n, x) == True{} : Bool}) -> {FS.value(one, S.mul(S.inv(k), S.add(z, S.mul(S.reduce(x), d)))) == FS.mmul(FS.order(one), FS.minv(FS.order(one), FS.value(one, k)), FS.madd(FS.order(one), FS.value(one, z), FS.mmul(FS.order(one), Nat.mod(FS.value(one, x), FS.order(one)), FS.value(one, d)))) : Nat}:
103  +hr = SQ.sred_r(one, h1, x, hx)
104  +hm = SO.mul_r(one, h1, S.reduce(x), d, hr, hd)
105  %Equal.sym(Nat, FS.value(one, S.mul(S.inv(k), S.add(z, S.mul(S.reduce(x), d)))), FS.mmul(FS.order(one), FS.value(one, S.inv(k)), FS.value(one, S.add(z, S.mul(S.reduce(x), d)))), SO.mul_v(one, h1, S.inv(k), S.add(z, S.mul(S.reduce(x), d)), SP.inv_r(one, h1, k, hk), SO.add_r(one, h1, z, S.mul(S.reduce(x), d), hz, hm))) : {_ == FS.mmul(FS.order(one), FS.minv(FS.order(one), FS.value(one, k)), FS.madd(FS.order(one), FS.value(one, z), FS.mmul(FS.order(one), Nat.mod(FS.value(one, x), FS.order(one)), FS.value(one, d)))) : Nat}
106  %Equal.sym(Nat, FS.value(one, S.inv(k)), FS.minv(FS.order(one), FS.value(one, k)), SP.inv_v(one, h1, k, hk)) : {FS.mmul(FS.order(one), _, FS.value(one, S.add(z, S.mul(S.reduce(x), d)))) == FS.mmul(FS.order(one), FS.minv(FS.order(one), FS.value(one, k)), FS.madd(FS.order(one), FS.value(one, z), FS.mmul(FS.order(one), Nat.mod(FS.value(one, x), FS.order(one)), FS.value(one, d)))) : Nat}
107  %Equal.sym(Nat, FS.value(one, S.add(z, S.mul(S.reduce(x), d))), FS.madd(FS.order(one), FS.value(one, z), FS.value(one, S.mul(S.reduce(x), d))), SO.add_v(one, h1, z, S.mul(S.reduce(x), d), hz, hm)) : {FS.mmul(FS.order(one), FS.minv(FS.order(one), FS.value(one, k)), _) == FS.mmul(FS.order(one), FS.minv(FS.order(one), FS.value(one, k)), FS.madd(FS.order(one), FS.value(one, z), FS.mmul(FS.order(one), Nat.mod(FS.value(one, x), FS.order(one)), FS.value(one, d)))) : Nat}
108  %Equal.sym(Nat, FS.value(one, S.mul(S.reduce(x), d)), FS.mmul(FS.order(one), FS.value(one, S.reduce(x)), FS.value(one, d)), SO.mul_v(one, h1, S.reduce(x), d, hr, hd)) : {FS.mmul(FS.order(one), FS.minv(FS.order(one), FS.value(one, k)), FS.madd(FS.order(one), FS.value(one, z), _)) == FS.mmul(FS.order(one), FS.minv(FS.order(one), FS.value(one, k)), FS.madd(FS.order(one), FS.value(one, z), FS.mmul(FS.order(one), Nat.mod(FS.value(one, x), FS.order(one)), FS.value(one, d)))) : Nat}
109  %Equal.sym(Nat, FS.value(one, S.reduce(x)), Nat.mod(FS.value(one, x), FS.order(one)), SQ.sred_v(one, h1, x, hx)) : {FS.mmul(FS.order(one), FS.minv(FS.order(one), FS.value(one, k)), FS.madd(FS.order(one), FS.value(one, z), FS.mmul(FS.order(one), _, FS.value(one, d)))) == FS.mmul(FS.order(one), FS.minv(FS.order(one), FS.value(one, k)), FS.madd(FS.order(one), FS.value(one, z), FS.mmul(FS.order(one), Nat.mod(FS.value(one, x), FS.order(one)), FS.value(one, d)))) : Nat}
110  {==}
111
112# the end of signing on scalars r, s0 of values rv, sv
113def fin_g(+one: Nat, +h1: {one == 1n : Nat}, +r: List<&2, Nat>, +hr: {FS.reduced(one, FS.order(one), r) == True{} : Bool}, +s0: List<&2, Nat>, +hs: {FS.reduced(one, FS.order(one), s0) == True{} : Bool}, +x: List<&2, Nat>, +y: List<&2, Nat>, +rv: Nat, +hrv: {FS.value(one, r) == rv : Nat}, +sv: Nat, +hsv: {FS.value(one, s0) == sv : Nat}) -> {matt(E.finish_if(Bool.or(S.is_zero(r), S.is_zero(s0)), E.Signature{B.to_be(r), B.to_be(S.select(E.b2n(S.is_high(s0)), S.neg(s0), s0)), U32.from_nat(Nat.add(Nat.mul(E.b2n(Bool.not(S.lt_n(x))), 2n), Nat.sub(Nat.add(F.parity(y), E.b2n(S.is_high(s0))), Nat.mul(Nat.mul(F.parity(y), E.b2n(S.is_high(s0))), 2n))))})) == ES.finish_if(Bool.or(Nat.is_eq(rv, 0n), Nat.is_eq(sv, 0n)), List.append(&2, U32, CV.i2osp(32n, rv), List.append(&2, U32, CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(sv)), FS.order(one), sv)), [U32.from_nat(Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(sv)), Nat.mod(FS.value(one, y), 2n))))]))) : ES.Attempt}:
114  %Equal.sym(Nat, rv, FS.value(one, r), Equal.sym(Nat, FS.value(one, r), rv, hrv)) : {matt(E.finish_if(Bool.or(S.is_zero(r), S.is_zero(s0)), E.Signature{B.to_be(r), B.to_be(S.select(E.b2n(S.is_high(s0)), S.neg(s0), s0)), U32.from_nat(Nat.add(Nat.mul(E.b2n(Bool.not(S.lt_n(x))), 2n), Nat.sub(Nat.add(F.parity(y), E.b2n(S.is_high(s0))), Nat.mul(Nat.mul(F.parity(y), E.b2n(S.is_high(s0))), 2n))))})) == ES.finish_if(Bool.or(Nat.is_eq(_, 0n), Nat.is_eq(sv, 0n)), List.append(&2, U32, CV.i2osp(32n, rv), List.append(&2, U32, CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(sv)), FS.order(one), sv)), [U32.from_nat(Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(sv)), Nat.mod(FS.value(one, y), 2n))))]))) : ES.Attempt}
115  %Equal.sym(Nat, rv, FS.value(one, r), Equal.sym(Nat, FS.value(one, r), rv, hrv)) : {matt(E.finish_if(Bool.or(S.is_zero(r), S.is_zero(s0)), E.Signature{B.to_be(r), B.to_be(S.select(E.b2n(S.is_high(s0)), S.neg(s0), s0)), U32.from_nat(Nat.add(Nat.mul(E.b2n(Bool.not(S.lt_n(x))), 2n), Nat.sub(Nat.add(F.parity(y), E.b2n(S.is_high(s0))), Nat.mul(Nat.mul(F.parity(y), E.b2n(S.is_high(s0))), 2n))))})) == ES.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(sv, 0n)), List.append(&2, U32, CV.i2osp(32n, _), List.append(&2, U32, CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(sv)), FS.order(one), sv)), [U32.from_nat(Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(sv)), Nat.mod(FS.value(one, y), 2n))))]))) : ES.Attempt}
116  %Equal.sym(Nat, sv, FS.value(one, s0), Equal.sym(Nat, FS.value(one, s0), sv, hsv)) : {matt(E.finish_if(Bool.or(S.is_zero(r), S.is_zero(s0)), E.Signature{B.to_be(r), B.to_be(S.select(E.b2n(S.is_high(s0)), S.neg(s0), s0)), U32.from_nat(Nat.add(Nat.mul(E.b2n(Bool.not(S.lt_n(x))), 2n), Nat.sub(Nat.add(F.parity(y), E.b2n(S.is_high(s0))), Nat.mul(Nat.mul(F.parity(y), E.b2n(S.is_high(s0))), 2n))))})) == ES.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(_, 0n)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, r)), List.append(&2, U32, CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(sv)), FS.order(one), sv)), [U32.from_nat(Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(sv)), Nat.mod(FS.value(one, y), 2n))))]))) : ES.Attempt}
117  %Equal.sym(Nat, sv, FS.value(one, s0), Equal.sym(Nat, FS.value(one, s0), sv, hsv)) : {matt(E.finish_if(Bool.or(S.is_zero(r), S.is_zero(s0)), E.Signature{B.to_be(r), B.to_be(S.select(E.b2n(S.is_high(s0)), S.neg(s0), s0)), U32.from_nat(Nat.add(Nat.mul(E.b2n(Bool.not(S.lt_n(x))), 2n), Nat.sub(Nat.add(F.parity(y), E.b2n(S.is_high(s0))), Nat.mul(Nat.mul(F.parity(y), E.b2n(S.is_high(s0))), 2n))))})) == ES.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, r)), List.append(&2, U32, CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(_)), FS.order(one), sv)), [U32.from_nat(Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(sv)), Nat.mod(FS.value(one, y), 2n))))]))) : ES.Attempt}
118  %Equal.sym(Nat, sv, FS.value(one, s0), Equal.sym(Nat, FS.value(one, s0), sv, hsv)) : {matt(E.finish_if(Bool.or(S.is_zero(r), S.is_zero(s0)), E.Signature{B.to_be(r), B.to_be(S.select(E.b2n(S.is_high(s0)), S.neg(s0), s0)), U32.from_nat(Nat.add(Nat.mul(E.b2n(Bool.not(S.lt_n(x))), 2n), Nat.sub(Nat.add(F.parity(y), E.b2n(S.is_high(s0))), Nat.mul(Nat.mul(F.parity(y), E.b2n(S.is_high(s0))), 2n))))})) == ES.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, r)), List.append(&2, U32, CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), _)), [U32.from_nat(Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(sv)), Nat.mod(FS.value(one, y), 2n))))]))) : ES.Attempt}
119  %Equal.sym(Nat, sv, FS.value(one, s0), Equal.sym(Nat, FS.value(one, s0), sv, hsv)) : {matt(E.finish_if(Bool.or(S.is_zero(r), S.is_zero(s0)), E.Signature{B.to_be(r), B.to_be(S.select(E.b2n(S.is_high(s0)), S.neg(s0), s0)), U32.from_nat(Nat.add(Nat.mul(E.b2n(Bool.not(S.lt_n(x))), 2n), Nat.sub(Nat.add(F.parity(y), E.b2n(S.is_high(s0))), Nat.mul(Nat.mul(F.parity(y), E.b2n(S.is_high(s0))), 2n))))})) == ES.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, r)), List.append(&2, U32, CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), [U32.from_nat(Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(_)), Nat.mod(FS.value(one, y), 2n))))]))) : ES.Attempt}
120  %Equal.sym(Bool, S.is_zero(r), Nat.is_eq(FS.value(one, r), 0n), FW.is_zero_s(one, h1, r)) : {matt(E.finish_if(Bool.or(_, S.is_zero(s0)), E.Signature{B.to_be(r), B.to_be(S.select(E.b2n(S.is_high(s0)), S.neg(s0), s0)), U32.from_nat(Nat.add(Nat.mul(E.b2n(Bool.not(S.lt_n(x))), 2n), Nat.sub(Nat.add(F.parity(y), E.b2n(S.is_high(s0))), Nat.mul(Nat.mul(F.parity(y), E.b2n(S.is_high(s0))), 2n))))})) == ES.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, r)), List.append(&2, U32, CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), [U32.from_nat(Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), Nat.mod(FS.value(one, y), 2n))))]))) : ES.Attempt}
121  %Equal.sym(Bool, S.is_zero(s0), Nat.is_eq(FS.value(one, s0), 0n), FW.is_zero_s(one, h1, s0)) : {matt(E.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), _), E.Signature{B.to_be(r), B.to_be(S.select(E.b2n(S.is_high(s0)), S.neg(s0), s0)), U32.from_nat(Nat.add(Nat.mul(E.b2n(Bool.not(S.lt_n(x))), 2n), Nat.sub(Nat.add(F.parity(y), E.b2n(S.is_high(s0))), Nat.mul(Nat.mul(F.parity(y), E.b2n(S.is_high(s0))), 2n))))})) == ES.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, r)), List.append(&2, U32, CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), [U32.from_nat(Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), Nat.mod(FS.value(one, y), 2n))))]))) : ES.Attempt}
122  %Equal.sym(List<&2, U32>, B.to_be(r), CV.i2osp(32n, FS.value(one, r)), tbv(one, h1, r, SL.sl16(one, r, hr))) : {matt(E.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), E.Signature{_, B.to_be(S.select(E.b2n(S.is_high(s0)), S.neg(s0), s0)), U32.from_nat(Nat.add(Nat.mul(E.b2n(Bool.not(S.lt_n(x))), 2n), Nat.sub(Nat.add(F.parity(y), E.b2n(S.is_high(s0))), Nat.mul(Nat.mul(F.parity(y), E.b2n(S.is_high(s0))), 2n))))})) == ES.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, r)), List.append(&2, U32, CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), [U32.from_nat(Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), Nat.mod(FS.value(one, y), 2n))))]))) : ES.Attempt}
123  %Equal.sym(Bool, S.is_high(s0), Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FW.is_high_s(one, h1, s0)) : {matt(E.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), E.Signature{CV.i2osp(32n, FS.value(one, r)), B.to_be(S.select(E.b2n(_), S.neg(s0), s0)), U32.from_nat(Nat.add(Nat.mul(E.b2n(Bool.not(S.lt_n(x))), 2n), Nat.sub(Nat.add(F.parity(y), E.b2n(S.is_high(s0))), Nat.mul(Nat.mul(F.parity(y), E.b2n(S.is_high(s0))), 2n))))})) == ES.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, r)), List.append(&2, U32, CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), [U32.from_nat(Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), Nat.mod(FS.value(one, y), 2n))))]))) : ES.Attempt}
124  %Equal.sym(List<&2, U32>, B.to_be(S.select(E.b2n(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0)))), S.neg(s0), s0)), CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), sel_v(one, h1, Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), s0, hs)) : {matt(E.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), E.Signature{CV.i2osp(32n, FS.value(one, r)), _, U32.from_nat(Nat.add(Nat.mul(E.b2n(Bool.not(S.lt_n(x))), 2n), Nat.sub(Nat.add(F.parity(y), E.b2n(S.is_high(s0))), Nat.mul(Nat.mul(F.parity(y), E.b2n(S.is_high(s0))), 2n))))})) == ES.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, r)), List.append(&2, U32, CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), [U32.from_nat(Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), Nat.mod(FS.value(one, y), 2n))))]))) : ES.Attempt}
125  %Equal.sym(Bool, S.is_high(s0), Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FW.is_high_s(one, h1, s0)) : {matt(E.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), E.Signature{CV.i2osp(32n, FS.value(one, r)), CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), U32.from_nat(Nat.add(Nat.mul(E.b2n(Bool.not(S.lt_n(x))), 2n), Nat.sub(Nat.add(F.parity(y), E.b2n(_)), Nat.mul(Nat.mul(F.parity(y), E.b2n(S.is_high(s0))), 2n))))})) == ES.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, r)), List.append(&2, U32, CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), [U32.from_nat(Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), Nat.mod(FS.value(one, y), 2n))))]))) : ES.Attempt}
126  %Equal.sym(Bool, S.is_high(s0), Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FW.is_high_s(one, h1, s0)) : {matt(E.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), E.Signature{CV.i2osp(32n, FS.value(one, r)), CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), U32.from_nat(Nat.add(Nat.mul(E.b2n(Bool.not(S.lt_n(x))), 2n), Nat.sub(Nat.add(F.parity(y), E.b2n(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))))), Nat.mul(Nat.mul(F.parity(y), E.b2n(_)), 2n))))})) == ES.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, r)), List.append(&2, U32, CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), [U32.from_nat(Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), Nat.mod(FS.value(one, y), 2n))))]))) : ES.Attempt}
127  %Equal.sym(Bool, S.lt_n(x), Nat.is_lt(FS.value(one, x), FS.order(one)), FW.lt_n_s(one, h1, x)) : {matt(E.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), E.Signature{CV.i2osp(32n, FS.value(one, r)), CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), U32.from_nat(Nat.add(Nat.mul(E.b2n(Bool.not(_)), 2n), Nat.sub(Nat.add(F.parity(y), E.b2n(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))))), Nat.mul(Nat.mul(F.parity(y), E.b2n(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))))), 2n))))})) == ES.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, r)), List.append(&2, U32, CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), [U32.from_nat(Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), Nat.mod(FS.value(one, y), 2n))))]))) : ES.Attempt}
128  %Equal.sym(Nat, F.parity(y), Nat.mod(FS.value(one, y), 2n), FW.parity_f(one, h1, y)) : {matt(E.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), E.Signature{CV.i2osp(32n, FS.value(one, r)), CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), U32.from_nat(Nat.add(Nat.mul(E.b2n(Bool.not(Nat.is_lt(FS.value(one, x), FS.order(one)))), 2n), Nat.sub(Nat.add(_, E.b2n(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))))), Nat.mul(Nat.mul(F.parity(y), E.b2n(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))))), 2n))))})) == ES.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, r)), List.append(&2, U32, CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), [U32.from_nat(Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), Nat.mod(FS.value(one, y), 2n))))]))) : ES.Attempt}
129  %Equal.sym(Nat, F.parity(y), Nat.mod(FS.value(one, y), 2n), FW.parity_f(one, h1, y)) : {matt(E.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), E.Signature{CV.i2osp(32n, FS.value(one, r)), CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), U32.from_nat(Nat.add(Nat.mul(E.b2n(Bool.not(Nat.is_lt(FS.value(one, x), FS.order(one)))), 2n), Nat.sub(Nat.add(Nat.mod(FS.value(one, y), 2n), E.b2n(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))))), Nat.mul(Nat.mul(_, E.b2n(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))))), 2n))))})) == ES.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, r)), List.append(&2, U32, CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), [U32.from_nat(Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), Nat.mod(FS.value(one, y), 2n))))]))) : ES.Attempt}
130  %Equal.sym(Nat, Nat.add(Nat.mul(E.b2n(Bool.not(Nat.is_lt(FS.value(one, x), FS.order(one)))), 2n), Nat.sub(Nat.add(Nat.mod(FS.value(one, y), 2n), E.b2n(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))))), Nat.mul(Nat.mul(Nat.mod(FS.value(one, y), 2n), E.b2n(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))))), 2n))), Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), Nat.mod(FS.value(one, y), 2n))), id_v(Nat.is_lt(FS.value(one, x), FS.order(one)), Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), Nat.mod(FS.value(one, y), 2n), PE.mod2_lt(FS.value(one, y)))) : {matt(E.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), E.Signature{CV.i2osp(32n, FS.value(one, r)), CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), U32.from_nat(_)})) == ES.finish_if(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), List.append(&2, U32, CV.i2osp(32n, FS.value(one, r)), List.append(&2, U32, CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), [U32.from_nat(Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), Nat.mod(FS.value(one, y), 2n))))]))) : ES.Attempt}
131  bad_v(Bool.or(Nat.is_eq(FS.value(one, r), 0n), Nat.is_eq(FS.value(one, s0), 0n)), E.Signature{CV.i2osp(32n, FS.value(one, r)), CV.i2osp(32n, ES.low(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), FS.order(one), FS.value(one, s0))), U32.from_nat(Nat.add(ES.ge2(Nat.is_lt(FS.value(one, x), FS.order(one))), ES.flip(Nat.is_lt(FS.order(one), Nat.double(FS.value(one, s0))), Nat.mod(FS.value(one, y), 2n))))})
132
133def fin_v(+one: Nat, +h1: {one == 1n : Nat}, +z: List<&2, Nat>, +hz: {FS.reduced(one, FS.order(one), z) == True{} : Bool}, +d: List<&2, Nat>, +hd: {FS.reduced(one, FS.order(one), d) == True{} : Bool}, +k: List<&2, Nat>, +hk: {FS.reduced(one, FS.order(one), k) == True{} : Bool}, +x: List<&2, Nat>, +hx: {PT.red(one, x) == True{} : Bool}, +y: List<&2, Nat>) -> {matt(E.finish(z, d, k, x, y)) == ES.finish(one, FS.value(one, z), FS.value(one, d), FS.value(one, k), CV.SAffine{FS.value(one, x), FS.value(one, y)}) : ES.Attempt}:
134  +hlx = SL.l16(one, x, hx)
135  fin_g(one, h1, S.reduce(x), SQ.sred_r(one, h1, x, hlx), S.mul(S.inv(k), S.add(z, S.mul(S.reduce(x), d))), s0_r(one, h1, z, hz, d, hd, k, hk, x, hlx), x, y, Nat.mod(FS.value(one, x), FS.order(one)), SQ.sred_v(one, h1, x, hlx), FS.mmul(FS.order(one), FS.minv(FS.order(one), FS.value(one, k)), FS.madd(FS.order(one), FS.value(one, z), FS.mmul(FS.order(one), Nat.mod(FS.value(one, x), FS.order(one)), FS.value(one, d)))), s0_v(one, h1, z, hz, d, hd, k, hk, x, hlx))
136
137# ---- one attempt: k from the candidate V ----
138
139def aff_fin(+one: Nat, +h1: {one == 1n : Nat}, +z: List<&2, Nat>, +hz: {FS.reduced(one, FS.order(one), z) == True{} : Bool}, +d: List<&2, Nat>, +hd: {FS.reduced(one, FS.order(one), d) == True{} : Bool}, +k: List<&2, Nat>, +hk: {FS.reduced(one, FS.order(one), k) == True{} : Bool}, a: P.Affine, +ha: {PA.ared(one, a) == True{} : Bool}) -> {matt(E.attempt_aff(z, d, k, a)) == ES.finish(one, FS.value(one, z), FS.value(one, d), FS.value(one, k), PA.av(one, a)) : ES.Attempt}:
140  match a:
141    case P.Affine{+x, +y}:
142      fin_v(one, h1, z, hz, d, hd, k, hk, x, Lg.and_left(PT.red(one, x), PT.red(one, y), ha), y)
143
144def aok(+one: Nat, +h1: {one == 1n : Nat}, +z: List<&2, Nat>, +hz: {FS.reduced(one, FS.order(one), z) == True{} : Bool}, +d: List<&2, Nat>, +hd: {FS.reduced(one, FS.order(one), d) == True{} : Bool}, +k: List<&2, Nat>, +hl: {FS.limbs16(one, 16n, k) == True{} : Bool}, b: Bool, +hb: {ES.scalar_ok(one, FS.value(one, k)) == b : Bool}) -> {matt(E.attempt_ok(z, d, k, b)) == ES.attempt_ok(one, FS.value(one, z), FS.value(one, d), FS.value(one, k), b) : ES.Attempt}:
145  match b:
146    case True{}:
147      +hg = PA.g_r(one, h1)
148      +hm = PM.mul_r(one, h1, k, P.g(), hl, hg)
149      %Equal.sym(CV.SPoint, CV.g(one), PT.pv(one, P.g()), Equal.sym(CV.SPoint, PT.pv(one, P.g()), CV.g(one), PA.g_v(one, h1))) : {matt(E.attempt_aff(z, d, k, P.to_affine(P.mul(k, P.g())))) == ES.finish(one, FS.value(one, z), FS.value(one, d), FS.value(one, k), CV.to_affine(FS.prime(one), CV.pmul(FS.prime(one), FS.value(one, k), _))) : ES.Attempt}
150      %Equal.sym(CV.SPoint, CV.pmul(FS.prime(one), FS.value(one, k), PT.pv(one, P.g())), PT.pv(one, P.mul(k, P.g())), Equal.sym(CV.SPoint, PT.pv(one, P.mul(k, P.g())), CV.pmul(FS.prime(one), FS.value(one, k), PT.pv(one, P.g())), PM.mul_v(one, h1, k, P.g(), hl, hg))) : {matt(E.attempt_aff(z, d, k, P.to_affine(P.mul(k, P.g())))) == ES.finish(one, FS.value(one, z), FS.value(one, d), FS.value(one, k), CV.to_affine(FS.prime(one), _)) : ES.Attempt}
151      %Equal.sym(CV.SAffine, CV.to_affine(FS.prime(one), PT.pv(one, P.mul(k, P.g()))), PA.av(one, P.to_affine(P.mul(k, P.g()))), Equal.sym(CV.SAffine, PA.av(one, P.to_affine(P.mul(k, P.g()))), CV.to_affine(FS.prime(one), PT.pv(one, P.mul(k, P.g()))), PA.aff_v(one, h1, P.mul(k, P.g()), hm))) : {matt(E.attempt_aff(z, d, k, P.to_affine(P.mul(k, P.g())))) == ES.finish(one, FS.value(one, z), FS.value(one, d), FS.value(one, k), _) : ES.Attempt}
152      aff_fin(one, h1, z, hz, d, hd, k, PV.ok_red(one, k, hl, hb), P.to_affine(P.mul(k, P.g())), PA.aff_r(one, h1, P.mul(k, P.g()), hm))
153    case False{}:
154      {==}
155
156def att_v(+one: Nat, +h1: {one == 1n : Nat}, +z: List<&2, Nat>, +hz: {FS.reduced(one, FS.order(one), z) == True{} : Bool}, +d: List<&2, Nat>, +hd: {FS.reduced(one, FS.order(one), d) == True{} : Bool}, +v: List<&2, U32>, +hv: {B.has_len(32n, v) == True{} : Bool}) -> {matt(E.attempt(z, d, v)) == ES.attempt(one, FS.value(one, z), FS.value(one, d), v) : ES.Attempt}:
157  %Equal.sym(Bool, E.scalar_ok(B.of_be(v)), ES.scalar_ok(one, FS.value(one, B.of_be(v))), SQ.scalar_ok_v(one, h1, B.of_be(v))) : {matt(E.attempt_ok(z, d, B.of_be(v), _)) == ES.attempt_ok(one, FS.value(one, z), FS.value(one, d), CV.os2ip(v), ES.scalar_ok(one, CV.os2ip(v))) : ES.Attempt}
158  %Equal.sym(Nat, CV.os2ip(v), FS.value(one, B.of_be(v)), Equal.sym(Nat, FS.value(one, B.of_be(v)), CV.os2ip(v), BY.of_be_value(one, h1, v))) : {matt(E.attempt_ok(z, d, B.of_be(v), ES.scalar_ok(one, FS.value(one, B.of_be(v))))) == ES.attempt_ok(one, FS.value(one, z), FS.value(one, d), _, ES.scalar_ok(one, CV.os2ip(v))) : ES.Attempt}
159  %Equal.sym(Nat, CV.os2ip(v), FS.value(one, B.of_be(v)), Equal.sym(Nat, FS.value(one, B.of_be(v)), CV.os2ip(v), BY.of_be_value(one, h1, v))) : {matt(E.attempt_ok(z, d, B.of_be(v), ES.scalar_ok(one, FS.value(one, B.of_be(v))))) == ES.attempt_ok(one, FS.value(one, z), FS.value(one, d), FS.value(one, B.of_be(v)), ES.scalar_ok(one, _)) : ES.Attempt}
160  aok(one, h1, z, hz, d, hd, B.of_be(v), BY.of_be_limbs(one, h1, v, hv), ES.scalar_ok(one, FS.value(one, B.of_be(v))), {==})
161
162# ---- the candidate loop and the DRBG ----
163
164def hm(k: List<&2, U32>, +m: List<&2, U32>) -> {E.hmac(k, m) == ES.hmac(k, m) : List<&2, U32>}:
165  match k:
166    case Nil{}:
167      MH.sign_correct([], m)
168    case +b <> +t:
169      MH.sign_correct(b <> t, m)
170
171def hlen(k: List<&2, U32>, +m: List<&2, U32>) -> {B.has_len(32n, ES.hmac(k, m)) == True{} : Bool}:
172  match k:
173    case Nil{}:
174      %Equal.sym(Bool, B.has_len(32n, HMS.hmac([], m)), Nat.is_eq(List.length(&2, U32, HMS.hmac([], m)), 32n), BY.has_len_v(32n, HMS.hmac([], m))) : {_ == True{} : Bool}
175      %Equal.sym(Nat, List.length(&2, U32, HMS.hmac([], m)), 32n, MH.hmac_len([], m)) : {Nat.is_eq(_, 32n) == True{} : Bool}
176      {==}
177    case +b <> +t:
178      %Equal.sym(Bool, B.has_len(32n, HMS.hmac(b <> t, m)), Nat.is_eq(List.length(&2, U32, HMS.hmac(b <> t, m)), 32n), BY.has_len_v(32n, HMS.hmac(b <> t, m))) : {_ == True{} : Bool}
179      %Equal.sym(Nat, List.length(&2, U32, HMS.hmac(b <> t, m)), 32n, MH.hmac_len(b <> t, m)) : {Nat.is_eq(_, 32n) == True{} : Bool}
180      {==}
181
182def sl(fuel: Nat, +one: Nat, +h1: {one == 1n : Nat}, +z: List<&2, Nat>, +hz: {FS.reduced(one, FS.order(one), z) == True{} : Bool}, +d: List<&2, Nat>, +hd: {FS.reduced(one, FS.order(one), d) == True{} : Bool}, +k: List<&2, U32>, +v: List<&2, U32>, att: E.Attempt) -> {msig(E.sign_loop(fuel, z, d, k, v, att)) == ES.sign_loop(fuel, one, FS.value(one, z), FS.value(one, d), k, v, matt(att)) : Maybe<&2, List<&2, U32>>}:
183  match fuel att:
184    case 0n E.ARetry{}:
185      {==}
186    case 0n E.ADone{sig}:
187      {==}
188    case 1n+ +f E.ARetry{}:
189      %Equal.sym(List<&2, U32>, E.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(k, List.append(&2, U32, v, [0])), hm(k, List.append(&2, U32, v, [0]))) : {msig(E.sign_loop(f, z, d, _, E.hmac(E.hmac(k, List.append(&2, U32, v, [0])), E.hmac(E.hmac(k, List.append(&2, U32, v, [0])), v)), E.attempt(z, d, E.hmac(E.hmac(k, List.append(&2, U32, v, [0])), E.hmac(E.hmac(k, List.append(&2, U32, v, [0])), v))))) == ES.sign_loop(f, one, FS.value(one, z), FS.value(one, d), ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v)), ES.attempt(one, FS.value(one, z), FS.value(one, d), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v)))) : Maybe<&2, List<&2, U32>>}
190      %Equal.sym(List<&2, U32>, E.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(k, List.append(&2, U32, v, [0])), hm(k, List.append(&2, U32, v, [0]))) : {msig(E.sign_loop(f, z, d, ES.hmac(k, List.append(&2, U32, v, [0])), E.hmac(_, E.hmac(E.hmac(k, List.append(&2, U32, v, [0])), v)), E.attempt(z, d, E.hmac(E.hmac(k, List.append(&2, U32, v, [0])), E.hmac(E.hmac(k, List.append(&2, U32, v, [0])), v))))) == ES.sign_loop(f, one, FS.value(one, z), FS.value(one, d), ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v)), ES.attempt(one, FS.value(one, z), FS.value(one, d), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v)))) : Maybe<&2, List<&2, U32>>}
191      %Equal.sym(List<&2, U32>, E.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(k, List.append(&2, U32, v, [0])), hm(k, List.append(&2, U32, v, [0]))) : {msig(E.sign_loop(f, z, d, ES.hmac(k, List.append(&2, U32, v, [0])), E.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), E.hmac(_, v)), E.attempt(z, d, E.hmac(E.hmac(k, List.append(&2, U32, v, [0])), E.hmac(E.hmac(k, List.append(&2, U32, v, [0])), v))))) == ES.sign_loop(f, one, FS.value(one, z), FS.value(one, d), ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v)), ES.attempt(one, FS.value(one, z), FS.value(one, d), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v)))) : Maybe<&2, List<&2, U32>>}
192      %Equal.sym(List<&2, U32>, E.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(k, List.append(&2, U32, v, [0])), hm(k, List.append(&2, U32, v, [0]))) : {msig(E.sign_loop(f, z, d, ES.hmac(k, List.append(&2, U32, v, [0])), E.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), E.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v)), E.attempt(z, d, E.hmac(_, E.hmac(E.hmac(k, List.append(&2, U32, v, [0])), v))))) == ES.sign_loop(f, one, FS.value(one, z), FS.value(one, d), ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v)), ES.attempt(one, FS.value(one, z), FS.value(one, d), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v)))) : Maybe<&2, List<&2, U32>>}
193      %Equal.sym(List<&2, U32>, E.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(k, List.append(&2, U32, v, [0])), hm(k, List.append(&2, U32, v, [0]))) : {msig(E.sign_loop(f, z, d, ES.hmac(k, List.append(&2, U32, v, [0])), E.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), E.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v)), E.attempt(z, d, E.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), E.hmac(_, v))))) == ES.sign_loop(f, one, FS.value(one, z), FS.value(one, d), ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v)), ES.attempt(one, FS.value(one, z), FS.value(one, d), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v)))) : Maybe<&2, List<&2, U32>>}
194      %Equal.sym(List<&2, U32>, E.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v), hm(ES.hmac(k, List.append(&2, U32, v, [0])), v)) : {msig(E.sign_loop(f, z, d, ES.hmac(k, List.append(&2, U32, v, [0])), E.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), _), E.attempt(z, d, E.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), E.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v))))) == ES.sign_loop(f, one, FS.value(one, z), FS.value(one, d), ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v)), ES.attempt(one, FS.value(one, z), FS.value(one, d), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v)))) : Maybe<&2, List<&2, U32>>}
195      %Equal.sym(List<&2, U32>, E.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v), hm(ES.hmac(k, List.append(&2, U32, v, [0])), v)) : {msig(E.sign_loop(f, z, d, ES.hmac(k, List.append(&2, U32, v, [0])), E.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v)), E.attempt(z, d, E.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), _)))) == ES.sign_loop(f, one, FS.value(one, z), FS.value(one, d), ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v)), ES.attempt(one, FS.value(one, z), FS.value(one, d), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v)))) : Maybe<&2, List<&2, U32>>}
196      %Equal.sym(List<&2, U32>, E.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v)), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v)), hm(ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v))) : {msig(E.sign_loop(f, z, d, ES.hmac(k, List.append(&2, U32, v, [0])), _, E.attempt(z, d, E.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v))))) == ES.sign_loop(f, one, FS.value(one, z), FS.value(one, d), ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v)), ES.attempt(one, FS.value(one, z), FS.value(one, d), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v)))) : Maybe<&2, List<&2, U32>>}
197      %Equal.sym(List<&2, U32>, E.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v)), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v)), hm(ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v))) : {msig(E.sign_loop(f, z, d, ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v)), E.attempt(z, d, _))) == ES.sign_loop(f, one, FS.value(one, z), FS.value(one, d), ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v)), ES.attempt(one, FS.value(one, z), FS.value(one, d), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v)))) : Maybe<&2, List<&2, U32>>}
198      %Equal.sym(ES.Attempt, ES.attempt(one, FS.value(one, z), FS.value(one, d), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v))), matt(E.attempt(z, d, ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v)))), Equal.sym(ES.Attempt, matt(E.attempt(z, d, ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v)))), ES.attempt(one, FS.value(one, z), FS.value(one, d), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v))), att_v(one, h1, z, hz, d, hd, ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v)), hlen(ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v))))) : {msig(E.sign_loop(f, z, d, ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v)), E.attempt(z, d, ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v))))) == ES.sign_loop(f, one, FS.value(one, z), FS.value(one, d), ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v)), _) : Maybe<&2, List<&2, U32>>}
199      sl(f, one, h1, z, hz, d, hd, ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v)), E.attempt(z, d, ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), ES.hmac(ES.hmac(k, List.append(&2, U32, v, [0])), v))))
200    case 1n+f E.ADone{sig}:
201      {==}
202
203def step_v(+k: List<&2, U32>, +v: List<&2, U32>, +tag: U32, +seed: List<&2, U32>) -> {dr(E.drbg_step(k, v, tag, seed)) == ES.update(k, v, tag, seed) : ES.Drbg}:
204  %Equal.sym(List<&2, U32>, E.hmac(k, List.append(&2, U32, v, tag <> seed)), ES.hmac(k, List.append(&2, U32, v, tag <> seed)), hm(k, List.append(&2, U32, v, tag <> seed))) : {ES.Drbg{_, E.hmac(E.hmac(k, List.append(&2, U32, v, tag <> seed)), v)} == ES.Drbg{ES.hmac(k, List.append(&2, U32, v, tag <> seed)), ES.hmac(ES.hmac(k, List.append(&2, U32, v, tag <> seed)), v)} : ES.Drbg}
205  %Equal.sym(List<&2, U32>, E.hmac(k, List.append(&2, U32, v, tag <> seed)), ES.hmac(k, List.append(&2, U32, v, tag <> seed)), hm(k, List.append(&2, U32, v, tag <> seed))) : {ES.Drbg{ES.hmac(k, List.append(&2, U32, v, tag <> seed)), E.hmac(_, v)} == ES.Drbg{ES.hmac(k, List.append(&2, U32, v, tag <> seed)), ES.hmac(ES.hmac(k, List.append(&2, U32, v, tag <> seed)), v)} : ES.Drbg}
206  %Equal.sym(List<&2, U32>, E.hmac(ES.hmac(k, List.append(&2, U32, v, tag <> seed)), v), ES.hmac(ES.hmac(k, List.append(&2, U32, v, tag <> seed)), v), hm(ES.hmac(k, List.append(&2, U32, v, tag <> seed)), v)) : {ES.Drbg{ES.hmac(k, List.append(&2, U32, v, tag <> seed)), _} == ES.Drbg{ES.hmac(k, List.append(&2, U32, v, tag <> seed)), ES.hmac(ES.hmac(k, List.append(&2, U32, v, tag <> seed)), v)} : ES.Drbg}
207  {==}
208
209def second_v(d: E.Drbg, +seed: List<&2, U32>) -> {dr(E.drbg_second(d, seed)) == ES.update2(dr(d), seed) : ES.Drbg}:
210  match d:
211    case E.Drbg{+k, +v}:
212      step_v(k, v, 1, seed)
213
214def init_v(+seed: List<&2, U32>) -> {dr(E.drbg_init(seed)) == ES.drbg_init(seed) : ES.Drbg}:
215  %Equal.sym(ES.Drbg, dr(E.drbg_second(E.drbg_step(List.replicate(U32, 32n, 0), List.replicate(U32, 32n, 1), 0, seed), seed)), ES.update2(dr(E.drbg_step(List.replicate(U32, 32n, 0), List.replicate(U32, 32n, 1), 0, seed)), seed), second_v(E.drbg_step(List.replicate(U32, 32n, 0), List.replicate(U32, 32n, 1), 0, seed), seed)) : {_ == ES.update2(ES.update(List.replicate(U32, 32n, 0), List.replicate(U32, 32n, 1), 0, seed), seed) : ES.Drbg}
216  %Equal.sym(ES.Drbg, dr(E.drbg_step(List.replicate(U32, 32n, 0), List.replicate(U32, 32n, 1), 0, seed)), ES.update(List.replicate(U32, 32n, 0), List.replicate(U32, 32n, 1), 0, seed), step_v(List.replicate(U32, 32n, 0), List.replicate(U32, 32n, 1), 0, seed)) : {ES.update2(_, seed) == ES.update2(ES.update(List.replicate(U32, 32n, 0), List.replicate(U32, 32n, 1), 0, seed), seed) : ES.Drbg}
217  {==}
218
219def drbg_sign(+one: Nat, +h1: {one == 1n : Nat}, +z: List<&2, Nat>, +hz: {FS.reduced(one, FS.order(one), z) == True{} : Bool}, +d: List<&2, Nat>, +hd: {FS.reduced(one, FS.order(one), d) == True{} : Bool}, g: E.Drbg) -> {msig(E.sign_drbg(z, d, g)) == ES.sign_drbg(one, FS.value(one, z), FS.value(one, d), dr(g)) : Maybe<&2, List<&2, U32>>}:
220  match g:
221    case E.Drbg{+k, +v}:
222      %Equal.sym(List<&2, U32>, E.hmac(k, v), ES.hmac(k, v), hm(k, v)) : {msig(E.sign_loop(16n, z, d, k, _, E.attempt(z, d, E.hmac(k, v)))) == ES.sign_loop(16n, one, FS.value(one, z), FS.value(one, d), k, ES.hmac(k, v), ES.attempt(one, FS.value(one, z), FS.value(one, d), ES.hmac(k, v))) : Maybe<&2, List<&2, U32>>}
223      %Equal.sym(List<&2, U32>, E.hmac(k, v), ES.hmac(k, v), hm(k, v)) : {msig(E.sign_loop(16n, z, d, k, ES.hmac(k, v), E.attempt(z, d, _))) == ES.sign_loop(16n, one, FS.value(one, z), FS.value(one, d), k, ES.hmac(k, v), ES.attempt(one, FS.value(one, z), FS.value(one, d), ES.hmac(k, v))) : Maybe<&2, List<&2, U32>>}
224      %Equal.sym(ES.Attempt, ES.attempt(one, FS.value(one, z), FS.value(one, d), ES.hmac(k, v)), matt(E.attempt(z, d, ES.hmac(k, v))), Equal.sym(ES.Attempt, matt(E.attempt(z, d, ES.hmac(k, v))), ES.attempt(one, FS.value(one, z), FS.value(one, d), ES.hmac(k, v)), att_v(one, h1, z, hz, d, hd, ES.hmac(k, v), hlen(k, v)))) : {msig(E.sign_loop(16n, z, d, k, ES.hmac(k, v), E.attempt(z, d, ES.hmac(k, v)))) == ES.sign_loop(16n, one, FS.value(one, z), FS.value(one, d), k, ES.hmac(k, v), _) : Maybe<&2, List<&2, U32>>}
225      sl(16n, one, h1, z, hz, d, hd, k, ES.hmac(k, v), E.attempt(z, d, ES.hmac(k, v)))
226
227# ---- sign ----
228
229def sd(+one: Nat, +h1: {one == 1n : Nat}, +h: List<&2, U32>, +hh: {B.has_len(32n, h) == True{} : Bool}, +d: List<&2, Nat>, +hd: {FS.reduced(one, FS.order(one), d) == True{} : Bool}) -> {msig(E.sign_d(h, Some{d})) == ES.sign_d(one, h, FS.value(one, d), True{}) : Maybe<&2, List<&2, U32>>}:
230  +hz = SQ.hash_r(one, h1, h, hh)
231  %Equal.sym(List<&2, U32>, B.to_be(d), CV.i2osp(32n, FS.value(one, d)), tbv(one, h1, d, SL.sl16(one, d, hd))) : {msig(E.sign_drbg(E.hash_scalar(h), d, E.drbg_init(List.append(&2, U32, _, B.to_be(E.hash_scalar(h)))))) == ES.sign_drbg(one, ES.hash_scalar(one, h), FS.value(one, d), ES.drbg_init(List.append(&2, U32, CV.i2osp(32n, FS.value(one, d)), CV.i2osp(32n, ES.hash_scalar(one, h))))) : Maybe<&2, List<&2, U32>>}
232  %Equal.sym(List<&2, U32>, B.to_be(E.hash_scalar(h)), CV.i2osp(32n, FS.value(one, E.hash_scalar(h))), tbv(one, h1, E.hash_scalar(h), SL.sl16(one, E.hash_scalar(h), hz))) : {msig(E.sign_drbg(E.hash_scalar(h), d, E.drbg_init(List.append(&2, U32, CV.i2osp(32n, FS.value(one, d)), _)))) == ES.sign_drbg(one, ES.hash_scalar(one, h), FS.value(one, d), ES.drbg_init(List.append(&2, U32, CV.i2osp(32n, FS.value(one, d)), CV.i2osp(32n, ES.hash_scalar(one, h))))) : Maybe<&2, List<&2, U32>>}
233  %Equal.sym(Nat, ES.hash_scalar(one, h), FS.value(one, E.hash_scalar(h)), Equal.sym(Nat, FS.value(one, E.hash_scalar(h)), ES.hash_scalar(one, h), SQ.hash_v(one, h1, h, hh))) : {msig(E.sign_drbg(E.hash_scalar(h), d, E.drbg_init(List.append(&2, U32, CV.i2osp(32n, FS.value(one, d)), CV.i2osp(32n, FS.value(one, E.hash_scalar(h))))))) == ES.sign_drbg(one, _, FS.value(one, d), ES.drbg_init(List.append(&2, U32, CV.i2osp(32n, FS.value(one, d)), CV.i2osp(32n, ES.hash_scalar(one, h))))) : Maybe<&2, List<&2, U32>>}
234  %Equal.sym(Nat, ES.hash_scalar(one, h), FS.value(one, E.hash_scalar(h)), Equal.sym(Nat, FS.value(one, E.hash_scalar(h)), ES.hash_scalar(one, h), SQ.hash_v(one, h1, h, hh))) : {msig(E.sign_drbg(E.hash_scalar(h), d, E.drbg_init(List.append(&2, U32, CV.i2osp(32n, FS.value(one, d)), CV.i2osp(32n, FS.value(one, E.hash_scalar(h))))))) == ES.sign_drbg(one, FS.value(one, E.hash_scalar(h)), FS.value(one, d), ES.drbg_init(List.append(&2, U32, CV.i2osp(32n, FS.value(one, d)), CV.i2osp(32n, _)))) : Maybe<&2, List<&2, U32>>}
235  %Equal.sym(ES.Drbg, ES.drbg_init(List.append(&2, U32, CV.i2osp(32n, FS.value(one, d)), CV.i2osp(32n, FS.value(one, E.hash_scalar(h))))), dr(E.drbg_init(List.append(&2, U32, CV.i2osp(32n, FS.value(one, d)), CV.i2osp(32n, FS.value(one, E.hash_scalar(h)))))), Equal.sym(ES.Drbg, dr(E.drbg_init(List.append(&2, U32, CV.i2osp(32n, FS.value(one, d)), CV.i2osp(32n, FS.value(one, E.hash_scalar(h)))))), ES.drbg_init(List.append(&2, U32, CV.i2osp(32n, FS.value(one, d)), CV.i2osp(32n, FS.value(one, E.hash_scalar(h))))), init_v(List.append(&2, U32, CV.i2osp(32n, FS.value(one, d)), CV.i2osp(32n, FS.value(one, E.hash_scalar(h))))))) : {msig(E.sign_drbg(E.hash_scalar(h), d, E.drbg_init(List.append(&2, U32, CV.i2osp(32n, FS.value(one, d)), CV.i2osp(32n, FS.value(one, E.hash_scalar(h))))))) == ES.sign_drbg(one, FS.value(one, E.hash_scalar(h)), FS.value(one, d), _) : Maybe<&2, List<&2, U32>>}
236  drbg_sign(one, h1, E.hash_scalar(h), hz, d, hd, E.drbg_init(List.append(&2, U32, CV.i2osp(32n, FS.value(one, d)), CV.i2osp(32n, FS.value(one, E.hash_scalar(h))))))
237
238def sk3(+one: Nat, +h1: {one == 1n : Nat}, +h: List<&2, U32>, +hh: {B.has_len(32n, h) == True{} : Bool}, +d: List<&2, Nat>, +hl: {FS.limbs16(one, 16n, d) == True{} : Bool}, c: Bool, +hc: {ES.scalar_ok(one, FS.value(one, d)) == c : Bool}) -> {msig(E.sign_d(h, E.secret_if(d, c))) == ES.sign_d(one, h, FS.value(one, d), c) : Maybe<&2, List<&2, U32>>}:
239  match c:
240    case True{}:
241      sd(one, h1, h, hh, d, PV.ok_red(one, d, hl, hc))
242    case False{}:
243      {==}
244
245def sk2(+one: Nat, +h1: {one == 1n : Nat}, +sk: List<&2, U32>, +h: List<&2, U32>, +hh: {B.has_len(32n, h) == True{} : Bool}, b: Bool, +hb: {B.has_len(32n, sk) == b : Bool}) -> {msig(E.sign_d(h, E.secret_if(B.of_be(sk), Bool.and(b, E.scalar_ok(B.of_be(sk)))))) == ES.sign_d(one, h, CV.os2ip(sk), Bool.and(b, ES.scalar_ok(one, CV.os2ip(sk)))) : Maybe<&2, List<&2, U32>>}:
246  match b:
247    case True{}:
248      %Equal.sym(Bool, E.scalar_ok(B.of_be(sk)), ES.scalar_ok(one, FS.value(one, B.of_be(sk))), SQ.scalar_ok_v(one, h1, B.of_be(sk))) : {msig(E.sign_d(h, E.secret_if(B.of_be(sk), Bool.and(b, _)))) == ES.sign_d(one, h, CV.os2ip(sk), Bool.and(b, ES.scalar_ok(one, CV.os2ip(sk)))) : Maybe<&2, List<&2, U32>>}
249      %Equal.sym(Nat, CV.os2ip(sk), FS.value(one, B.of_be(sk)), Equal.sym(Nat, FS.value(one, B.of_be(sk)), CV.os2ip(sk), BY.of_be_value(one, h1, sk))) : {msig(E.sign_d(h, E.secret_if(B.of_be(sk), Bool.and(b, ES.scalar_ok(one, FS.value(one, B.of_be(sk))))))) == ES.sign_d(one, h, _, Bool.and(b, ES.scalar_ok(one, CV.os2ip(sk)))) : Maybe<&2, List<&2, U32>>}
250      %Equal.sym(Nat, CV.os2ip(sk), FS.value(one, B.of_be(sk)), Equal.sym(Nat, FS.value(one, B.of_be(sk)), CV.os2ip(sk), BY.of_be_value(one, h1, sk))) : {msig(E.sign_d(h, E.secret_if(B.of_be(sk), Bool.and(b, ES.scalar_ok(one, FS.value(one, B.of_be(sk))))))) == ES.sign_d(one, h, FS.value(one, B.of_be(sk)), Bool.and(b, ES.scalar_ok(one, _))) : Maybe<&2, List<&2, U32>>}
251      sk3(one, h1, h, hh, B.of_be(sk), BY.of_be_limbs(one, h1, sk, hb), ES.scalar_ok(one, FS.value(one, B.of_be(sk))), {==})
252    case False{}:
253      {==}
254
255def sh(+one: Nat, +h1: {one == 1n : Nat}, +sk: List<&2, U32>, +h: List<&2, U32>, a: Bool, +ha: {B.has_len(32n, h) == a : Bool}) -> {msig(E.sign_h(sk, h, a)) == ES.sign_d(one, h, CV.os2ip(sk), Bool.and(a, Bool.and(CV.length_is(32n, sk), ES.scalar_ok(one, CV.os2ip(sk))))) : Maybe<&2, List<&2, U32>>}:
256  match a:
257    case True{}:
258      %Equal.sym(Bool, B.has_len(32n, sk), CV.length_is(32n, sk), BL.hl_is(32n, sk)) : {msig(E.sign_d(h, E.secret_if(B.of_be(sk), Bool.and(_, E.scalar_ok(B.of_be(sk)))))) == ES.sign_d(one, h, CV.os2ip(sk), Bool.and(CV.length_is(32n, sk), ES.scalar_ok(one, CV.os2ip(sk)))) : Maybe<&2, List<&2, U32>>}
259      sk2(one, h1, sk, h, ha, CV.length_is(32n, sk), BL.hl_is(32n, sk))
260    case False{}:
261      {==}
262
263# the signature of a 32-byte hash under a 32-byte secret key
264def sign_v(+one: Nat, +h1: {one == 1n : Nat}, +sk: List<&2, U32>, +h: List<&2, U32>) -> {msig(E.sign(sk, h)) == ES.sign(one, sk, h) : Maybe<&2, List<&2, U32>>}:
265  %Equal.sym(Bool, B.has_len(32n, h), CV.length_is(32n, h), BL.hl_is(32n, h)) : {msig(E.sign_h(sk, h, _)) == ES.sign_d(one, h, CV.os2ip(sk), Bool.and(CV.length_is(32n, h), Bool.and(CV.length_is(32n, sk), ES.scalar_ok(one, CV.os2ip(sk))))) : Maybe<&2, List<&2, U32>>}
266  sh(one, h1, sk, h, CV.length_is(32n, h), BL.hl_is(32n, h))