# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/psign.src; edit the .src
import Base
import ../../../spec/crypto/secp256k1/field.bend as FS
import ../../../spec/crypto/secp256k1/curve.bend as CV
import ../../../spec/crypto/secp256k1/ecdsa.bend as ES
import ../../../src/crypto/secp256k1/limbs.bend as L
import ../../../src/crypto/secp256k1/field.bend as F
import ../../../src/crypto/secp256k1/scalar.bend as S
import ../../../src/crypto/secp256k1/bytes.bend as B
import ../../../src/crypto/secp256k1/point.bend as P
import ../../../src/crypto/secp256k1/ecdsa.bend as E
import ../../lib/logic.bend as Lg
import ../../../spec/crypto/hmac.bend as HMS
import ../mac/hmac.bend as MH
import ./limbs.bend as LV
import ./scalarops.bend as SO
import ./scalarpow.bend as SP
import ./fwrap.bend as FW
import ./bytes.bend as BY
import ./point.bend as PT
import ./sel.bend as SL
import ./pmul.bend as PM
import ./paff.bend as PA
import ./penc.bend as PE
import ./pver.bend as PV
import ./blist.bend as BL
import ./pscal.bend as SQ

# ECDSA signing of src/crypto/secp256k1/ecdsa.bend (RFC 6979 nonces,
# low-S, recovery id) against spec/crypto/secp256k1/ecdsa.bend. The
# implementation's signature record r, s, v is the specification's
# r || s || v.

def sigb(sig: E.Signature) -> List<&2, U32>:
  match sig:
    case E.Signature{r, s, v}: List.append(&2, U32, r, List.append(&2, U32, s, [v]))

def msig(m: Maybe<&2, E.Signature>) -> Maybe<&2, List<&2, U32>>:
  match m:
    case None{}: None{}
    case Some{sig}: Some{sigb(sig)}

def matt(a: E.Attempt) -> ES.Attempt:
  match a:
    case E.ARetry{}: ES.Retry{}
    case E.ADone{sig}: ES.Sig{sigb(sig)}

def dr(g: E.Drbg) -> ES.Drbg:
  match g:
    case E.Drbg{k, v}: ES.Drbg{k, v}

# ---- r, s and the recovery id ----

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>}:
  %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>}
  %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>}
  {==}

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}:
  match lb hb q:
    case True{} True{} 0n:
      {==}
    case True{} True{} 1n:
      {==}
    case True{} False{} 0n:
      {==}
    case True{} False{} 1n:
      {==}
    case False{} True{} 0n:
      {==}
    case False{} True{} 1n:
      {==}
    case False{} False{} 0n:
      {==}
    case False{} False{} 1n:
      {==}
    case _ _ 2n+ +c:
      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))

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>}:
  match hb:
    case True{}:
      %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>}
      %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>}
      %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>}
      {==}
    case False{}:
      %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>}
      tbv(one, h1, s0, SL.sl16(one, s0, hs))

def bad_v(bad: Bool, +sig: E.Signature) -> {matt(E.finish_if(bad, sig)) == ES.finish_if(bad, sigb(sig)) : ES.Attempt}:
  match bad:
    case True{}:
      {==}
    case False{}:
      {==}

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}:
  +hr = SQ.sred_r(one, h1, x, hx)
  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)))

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}:
  +hr = SQ.sred_r(one, h1, x, hx)
  +hm = SO.mul_r(one, h1, S.reduce(x), d, hr, hd)
  %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}
  %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}
  %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}
  %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}
  %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}
  {==}

# the end of signing on scalars r, s0 of values rv, sv
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}:
  %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}
  %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}
  %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}
  %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}
  %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}
  %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}
  %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}
  %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}
  %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}
  %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}
  %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}
  %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}
  %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}
  %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}
  %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}
  %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}
  %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}
  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))))})

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}:
  +hlx = SL.l16(one, x, hx)
  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))

# ---- one attempt: k from the candidate V ----

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}:
  match a:
    case P.Affine{+x, +y}:
      fin_v(one, h1, z, hz, d, hd, k, hk, x, Lg.and_left(PT.red(one, x), PT.red(one, y), ha), y)

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}:
  match b:
    case True{}:
      +hg = PA.g_r(one, h1)
      +hm = PM.mul_r(one, h1, k, P.g(), hl, hg)
      %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}
      %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}
      %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}
      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))
    case False{}:
      {==}

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}:
  %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}
  %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}
  %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}
  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))), {==})

# ---- the candidate loop and the DRBG ----

def hm(k: List<&2, U32>, +m: List<&2, U32>) -> {E.hmac(k, m) == ES.hmac(k, m) : List<&2, U32>}:
  match k:
    case Nil{}:
      MH.sign_correct([], m)
    case +b <> +t:
      MH.sign_correct(b <> t, m)

def hlen(k: List<&2, U32>, +m: List<&2, U32>) -> {B.has_len(32n, ES.hmac(k, m)) == True{} : Bool}:
  match k:
    case Nil{}:
      %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}
      %Equal.sym(Nat, List.length(&2, U32, HMS.hmac([], m)), 32n, MH.hmac_len([], m)) : {Nat.is_eq(_, 32n) == True{} : Bool}
      {==}
    case +b <> +t:
      %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}
      %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}
      {==}

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>>}:
  match fuel att:
    case 0n E.ARetry{}:
      {==}
    case 0n E.ADone{sig}:
      {==}
    case 1n+ +f E.ARetry{}:
      %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>>}
      %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>>}
      %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>>}
      %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>>}
      %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>>}
      %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>>}
      %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>>}
      %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>>}
      %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>>}
      %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>>}
      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))))
    case 1n+f E.ADone{sig}:
      {==}

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}:
  %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}
  %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}
  %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}
  {==}

def second_v(d: E.Drbg, +seed: List<&2, U32>) -> {dr(E.drbg_second(d, seed)) == ES.update2(dr(d), seed) : ES.Drbg}:
  match d:
    case E.Drbg{+k, +v}:
      step_v(k, v, 1, seed)

def init_v(+seed: List<&2, U32>) -> {dr(E.drbg_init(seed)) == ES.drbg_init(seed) : ES.Drbg}:
  %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}
  %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}
  {==}

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>>}:
  match g:
    case E.Drbg{+k, +v}:
      %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>>}
      %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>>}
      %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>>}
      sl(16n, one, h1, z, hz, d, hd, k, ES.hmac(k, v), E.attempt(z, d, ES.hmac(k, v)))

# ---- sign ----

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>>}:
  +hz = SQ.hash_r(one, h1, h, hh)
  %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>>}
  %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>>}
  %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>>}
  %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>>}
  %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>>}
  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))))))

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>>}:
  match c:
    case True{}:
      sd(one, h1, h, hh, d, PV.ok_red(one, d, hl, hc))
    case False{}:
      {==}

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>>}:
  match b:
    case True{}:
      %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>>}
      %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>>}
      %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>>}
      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))), {==})
    case False{}:
      {==}

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>>}:
  match a:
    case True{}:
      %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>>}
      sk2(one, h1, sk, h, ha, CV.length_is(32n, sk), BL.hl_is(32n, sk))
    case False{}:
      {==}

# the signature of a 32-byte hash under a 32-byte secret key
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>>}:
  %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>>}
  sh(one, h1, sk, h, CV.length_is(32n, h), BL.hl_is(32n, h))