1 # GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/psign.src; edit the .src 2 import Base 3 import ../../../spec/crypto/secp256k1/field.bend as FS 4 import ../../../spec/crypto/secp256k1/curve.bend as CV 5 import ../../../spec/crypto/secp256k1/ecdsa.bend as ES 6 import ../../../src/crypto/secp256k1/limbs.bend as L 7 import ../../../src/crypto/secp256k1/field.bend as F 8 import ../../../src/crypto/secp256k1/scalar.bend as S 9 import ../../../src/crypto/secp256k1/bytes.bend as B 10 import ../../../src/crypto/secp256k1/point.bend as P 11 import ../../../src/crypto/secp256k1/ecdsa.bend as E 12 import ../../lib/logic.bend as Lg 13 import ../../../spec/crypto/hmac.bend as HMS 14 import ../mac/hmac.bend as MH 15 import ./limbs.bend as LV 16 import ./scalarops.bend as SO 17 import ./scalarpow.bend as SP 18 import ./fwrap.bend as FW 19 import ./bytes.bend as BY 20 import ./point.bend as PT 21 import ./sel.bend as SL 22 import ./pmul.bend as PM 23 import ./paff.bend as PA 24 import ./penc.bend as PE 25 import ./pver.bend as PV 26 import ./blist.bend as BL 27 import ./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 34 def 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 38 def 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 43 def 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 48 def 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 54 def 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 59 def 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 80 def 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 91 def 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 98 def 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 102 def 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 113 def 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 133 def 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 139 def 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 144 def 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 156 def 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 164 def 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 171 def 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 182 def 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 203 def 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 209 def 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 214 def 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 219 def 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 229 def 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 238 def 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 245 def 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 255 def 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 264 def 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))