~/jendhub

proofs/crypto/ed25519/top.bend

bend-collections-laws-crypto@1.0.0.0 · 263 lines · 26 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend as FS
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/x25519.bend as SX
5import bend-collections-laws-crypto@1.0.0.0/spec/crypto/ed25519.bend as SE
6import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha512.bend as SHA
7import bend-collections-laws-crypto@1.0.0.0/src/crypto/hash.bend as H
8import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend as F
9import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/x25519.bend as X
10import bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/point.bend as PT
11import bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/scalar.bend as ESC
12import bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/ed25519.bend as E
13import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
14import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
15import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM
16import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend as G
17import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/rel.bend as RL
18import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/xbits.bend as XB
19import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar.bend as SC
20import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar3.bend as S3
21import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/prel.bend as PR
22import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pcodec.bend as PC
23import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pdec.bend as PD
24import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/bytes.bend as BY
25
26# Key generation, signing and verification of src/crypto/ed25519/ed25519.bend
27# against spec/crypto/ed25519.bend, for p = 1 + pp (hP) and the curve
28# constants computed from an input xs (PT.consts(xs), related to the spec's d
29# and sqrt(-1) by pcodec.bend).
30
31def bits_eq(+one: Nat, +h1: {one == 1n : Nat}, +k: List<&2, U32>, +hk: {LM.okb(32n, k, 255n) == True{} : Bool}) -> {X.bitlen(k) == C.shift(8n, one) : Nat}:
32  Equal.trans(Nat, X.bitlen(k), 256n, C.shift(8n, one), BY.bitlen_256(k, hk), Equal.cong(Nat, Nat, z => C.shift(8n, z), 1n, one, Equal.sym(Nat, one, 1n, h1)))
33
34# [k] p, k 32 bytes: the implementation runs over bitlen(k) = 256 bits, the
35# spec over 2^8 one
36def mul_rel(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +cs: PT.Cs, +D: Nat, +rd2: RL.R(pp, PT.cs_d2(cs), FS.fadd(1n+pp, D, D)), +k: List<&2, U32>, +hk: {LM.okb(32n, k, 255n) == True{} : Bool}, +p: PT.Pt, +sp: SE.EPt, +hp: PR.Rp(pp, p, sp)) -> PR.Rp(pp, PT.mul(cs, k, p), SE.mul(one, 1n+pp, D, FS.value(k), sp)):
37  %Equal.sym(Nat, X.bitlen(k), C.shift(8n, one), bits_eq(one, h1, k, hk)) : PR.Rp(pp, PT.smul(_, cs, k, p, PT.identity()), SE.mul(one, 1n+pp, D, FS.value(k), sp))
38  PR.smul_rel(one, h1, pp, hP, C.shift(8n, one), cs, D, rd2, k, LM.okb_lea(32n, k, 255n, hk), p, sp, hp, PT.identity(), SE.identity(), PD.identity_rel(pp))
39
40# encode, the spec's byte count 2^5 one
41def enc_rel(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +p: PT.Pt, +sp: SE.EPt, +hp: PR.Rp(pp, p, sp)) -> {PT.encode(p) == SE.encode(one, 1n+pp, sp) : List<&2, U32>}:
42  L.subst(Nat, z => {PT.encode(p) == SE.encode_n(z, 1n+pp, sp) : List<&2, U32>}, 32n, C.shift(5n, one), Equal.cong(Nat, Nat, z => C.shift(5n, z), 1n, one, Equal.sym(Nat, one, 1n, h1)), PC.encode_rel(one, h1, pp, hP, p, sp, hp))
43
44# ---- scalars from digests ----
45
46def rh_val(+one: Nat, +h1: {one == 1n : Nat}, +bs: List<&2, U32>) -> {FS.value(ESC.reduce(H.sha512(bs))) == Nat.mod(FS.value(SHA.sha512_bytes(bs)), SE.ell(one)) : Nat}:
47  +M = {1n+S3.mmL(one) : Nat}
48  +hb = H.sha512(bs)
49  +sb = SHA.sha512_bytes(bs)
50  +e1 = S3.reduce_m(one, h1, hb, BY.sha_lea(bs))
51  +e2 = Equal.cong(List<&2, U32>, Nat, z => Nat.mod(FS.value(z), M), hb, sb, BY.sha_eq(bs))
52  +e3 = Equal.cong(Nat, Nat, z => Nat.mod(FS.value(sb), z), M, SE.ell(one), S3.ell_eq(one, h1))
53  Equal.trans(Nat, FS.value(ESC.reduce(hb)), Nat.mod(FS.value(hb), M), Nat.mod(FS.value(sb), SE.ell(one)), e1, Equal.trans(Nat, Nat.mod(FS.value(hb), M), Nat.mod(FS.value(sb), M), Nat.mod(FS.value(sb), SE.ell(one)), e2, e3))
54
55def rh_eq(+one: Nat, +h1: {one == 1n : Nat}, +bs: List<&2, U32>, +sbs: List<&2, U32>, +e: {bs == sbs : List<&2, U32>}) -> {FS.value(ESC.reduce(H.sha512(bs))) == Nat.mod(FS.value(SHA.sha512_bytes(sbs)), SE.ell(one)) : Nat}:
56  Equal.trans(Nat, FS.value(ESC.reduce(H.sha512(bs))), Nat.mod(FS.value(SHA.sha512_bytes(bs)), SE.ell(one)), Nat.mod(FS.value(SHA.sha512_bytes(sbs)), SE.ell(one)), rh_val(one, h1, bs), Equal.cong(List<&2, U32>, Nat, z => Nat.mod(FS.value(SHA.sha512_bytes(z)), SE.ell(one)), bs, sbs, e))
57
58def hram_s(+one: Nat, +rb: List<&2, U32>, +a: List<&2, U32>, +msg: List<&2, U32>) -> {SE.hram(one, rb, a, msg) == Nat.mod(FS.value(SHA.sha512_bytes(SE.cat(rb, SE.cat(a, msg)))), SE.ell(one)) : Nat}:
59  match rb:
60    case Nil{}:
61      {==}
62    case Con{x, xt}:
63      {==}
64
65def hram_i(+rb: List<&2, U32>, +a: List<&2, U32>, +msg: List<&2, U32>) -> {E.hram(rb, a, msg) == ESC.reduce(H.sha512(E.cat(rb, E.cat(a, msg)))) : List<&2, U32>}:
66  match rb:
67    case Nil{}:
68      {==}
69    case Con{x, xt}:
70      {==}
71
72def red_lt(+one: Nat, +h1: {one == 1n : Nat}, +bs: List<&2, U32>, +hb: {LM.lea(bs, 255n) == True{} : Bool}) -> {Nat.is_lt(FS.value(ESC.reduce(bs)), 1n+S3.mmL(one)) == True{} : Bool}:
73  +M = {1n+S3.mmL(one) : Nat}
74  L.subst(Nat, z => {Nat.is_lt(z, M) == True{} : Bool}, Nat.mod(FS.value(bs), M), FS.value(ESC.reduce(bs)), Equal.sym(Nat, FS.value(ESC.reduce(bs)), Nat.mod(FS.value(bs), M), S3.reduce_m(one, h1, bs, hb)), SC.lt_mod(S3.mmL(one), FS.value(bs)))
75
76def secret_eq(+h: List<&2, U32>) -> {FS.value(X.clamp(F.take(32n, h))) == SE.secret(h) : Nat}:
77  +t = F.take(32n, h)
78  +st = SE.first(32n, h)
79  Equal.cong(List<&2, U32>, Nat, z => FS.value(z), X.clamp(t), SX.clamp(st), Equal.trans(List<&2, U32>, X.clamp(t), SX.clamp(t), SX.clamp(st), XB.clamp_eq(t), Equal.cong(List<&2, U32>, List<&2, U32>, z => SX.clamp(z), t, st, BY.take_eq(32n, h))))
80
81def cat2_eq(+x: List<&2, U32>, +sx: List<&2, U32>, +y: List<&2, U32>, +sy: List<&2, U32>, +m: List<&2, U32>, +ex: {x == sx : List<&2, U32>}, +ey: {y == sy : List<&2, U32>}) -> {E.cat(x, E.cat(y, m)) == SE.cat(sx, SE.cat(sy, m)) : List<&2, U32>}:
82  +e1 = BY.cat_eq(x, E.cat(y, m))
83  +e2 = Equal.cong(List<&2, U32>, List<&2, U32>, z => SE.cat(x, z), E.cat(y, m), SE.cat(y, m), BY.cat_eq(y, m))
84  +e3 = Equal.cong(List<&2, U32>, List<&2, U32>, z => SE.cat(z, SE.cat(y, m)), x, sx, ex)
85  +e4 = Equal.cong(List<&2, U32>, List<&2, U32>, z => SE.cat(sx, SE.cat(z, m)), y, sy, ey)
86  Equal.trans(List<&2, U32>, E.cat(x, E.cat(y, m)), SE.cat(x, E.cat(y, m)), SE.cat(sx, SE.cat(sy, m)), e1, Equal.trans(List<&2, U32>, SE.cat(x, E.cat(y, m)), SE.cat(x, SE.cat(y, m)), SE.cat(sx, SE.cat(sy, m)), e2, Equal.trans(List<&2, U32>, SE.cat(x, SE.cat(y, m)), SE.cat(sx, SE.cat(y, m)), SE.cat(sx, SE.cat(sy, m)), e3, e4)))
87
88def hk_okb(+one: Nat, +h1: {one == 1n : Nat}, +rb: List<&2, U32>, +a: List<&2, U32>, +msg: List<&2, U32>) -> {LM.okb(32n, E.hram(rb, a, msg), 255n) == True{} : Bool}:
89  +kh = H.sha512(E.cat(rb, E.cat(a, msg)))
90  L.subst(List<&2, U32>, z => {LM.okb(32n, z, 255n) == True{} : Bool}, ESC.reduce(kh), E.hram(rb, a, msg), Equal.sym(List<&2, U32>, E.hram(rb, a, msg), ESC.reduce(kh), hram_i(rb, a, msg)), S3.reduce_okb(one, h1, kh, BY.sha_lea(E.cat(rb, E.cat(a, msg)))))
91
92def hk_val(+one: Nat, +h1: {one == 1n : Nat}, +rb: List<&2, U32>, +srb: List<&2, U32>, +erb: {rb == srb : List<&2, U32>}, +a: List<&2, U32>, +sa: List<&2, U32>, +ea: {a == sa : List<&2, U32>}, +msg: List<&2, U32>) -> {FS.value(E.hram(rb, a, msg)) == SE.hram(one, srb, sa, msg) : Nat}:
93  +KH = E.cat(rb, E.cat(a, msg))
94  +SKH = SE.cat(srb, SE.cat(sa, msg))
95  +M = Nat.mod(FS.value(SHA.sha512_bytes(SKH)), SE.ell(one))
96  +e1 = Equal.cong(List<&2, U32>, Nat, z => FS.value(z), E.hram(rb, a, msg), ESC.reduce(H.sha512(KH)), hram_i(rb, a, msg))
97  +e2 = rh_eq(one, h1, KH, SKH, cat2_eq(rb, srb, a, sa, msg, erb, ea))
98  Equal.trans(Nat, FS.value(E.hram(rb, a, msg)), FS.value(ESC.reduce(H.sha512(KH))), SE.hram(one, srb, sa, msg), e1, Equal.trans(Nat, FS.value(ESC.reduce(H.sha512(KH))), M, SE.hram(one, srb, sa, msg), e2, Equal.sym(Nat, SE.hram(one, srb, sa, msg), M, hram_s(one, srb, sa, msg))))
99
100# S = (r + k s) mod L, as 32 bytes: s reduced first (the implementation's
101# reduce(secret)), the same residue
102def ma_eq(+one: Nat, +h1: {one == 1n : Nat}, +k: List<&2, U32>, +r: List<&2, U32>, +sk: List<&2, U32>, +hk: {LM.okb(32n, k, 255n) == True{} : Bool}, +hr: {LM.okb(32n, r, 255n) == True{} : Bool}, +lr: {Nat.is_lt(FS.value(r), 1n+S3.mmL(one)) == True{} : Bool}, +hsk: {LM.okb(32n, sk, 255n) == True{} : Bool}, +Rs: Nat, +Ks: Nat, +Ss: Nat, +eR: {FS.value(r) == Rs : Nat}, +eK: {FS.value(k) == Ks : Nat}, +eS: {FS.value(sk) == Ss : Nat}) -> {ESC.mul_add(k, ESC.reduce(sk), r) == SX.le_bytes(C.shift(5n, one), Nat.mod(Nat.add(Rs, Nat.mul(Ks, Ss)), SE.ell(one))) : List<&2, U32>}:
103  +mm = S3.mmL(one)
104  +M = {1n+S3.mmL(one) : Nat}
105  +el = SE.ell(one)
106  +s = ESC.reduce(sk)
107  +hl = LM.okb_lea(32n, sk, 255n, hsk)
108  +lk = LM.okb_lea(32n, k, 255n, hk)
109  +os = S3.reduce_okb(one, h1, sk, hl)
110  +ls = red_lt(one, h1, sk, hl)
111  +MA = ESC.mul_add(k, s, r)
112  +Vr = FS.value(r)
113  +Vk = FS.value(k)
114  +Vs = FS.value(sk)
115  +T0 = FS.value(MA)
116  +T1 = Nat.mod(Nat.add(Vr, Nat.mul(Vk, FS.value(s))), M)
117  +T2 = Nat.mod(Nat.add(Vr, Nat.mul(Vk, Nat.mod(Vs, M))), M)
118  +T3 = Nat.mod(Nat.add(Vr, Nat.mul(Vk, Vs)), M)
119  +T4 = Nat.mod(Nat.add(Rs, Nat.mul(Vk, Vs)), M)
120  +T5 = Nat.mod(Nat.add(Rs, Nat.mul(Ks, Vs)), M)
121  +T6 = Nat.mod(Nat.add(Rs, Nat.mul(Ks, Ss)), M)
122  +T7 = Nat.mod(Nat.add(Rs, Nat.mul(Ks, Ss)), el)
123  +e0 = S3.mul_add_m(one, h1, k, s, r, lk, os, hr, ls, lr)
124  +e1 = Equal.cong(Nat, Nat, z => Nat.mod(Nat.add(Vr, Nat.mul(Vk, z)), M), FS.value(s), Nat.mod(Vs, M), S3.reduce_m(one, h1, sk, hl))
125  +e2 = G.c_add(mm, Vr, Vr, Nat.mul(Vk, Nat.mod(Vs, M)), Nat.mul(Vk, Vs), G.c_refl(mm, Vr), G.c_mul(mm, Vk, Vk, Nat.mod(Vs, M), Vs, G.c_refl(mm, Vk), G.c_mod(mm, Vs)))
126  +e3 = Equal.cong(Nat, Nat, z => Nat.mod(Nat.add(z, Nat.mul(Vk, Vs)), M), Vr, Rs, eR)
127  +e4 = Equal.cong(Nat, Nat, z => Nat.mod(Nat.add(Rs, Nat.mul(z, Vs)), M), Vk, Ks, eK)
128  +e5 = Equal.cong(Nat, Nat, z => Nat.mod(Nat.add(Rs, Nat.mul(Ks, z)), M), Vs, Ss, eS)
129  +e6 = Equal.cong(Nat, Nat, z => Nat.mod(Nat.add(Rs, Nat.mul(Ks, Ss)), z), M, el, S3.ell_eq(one, h1))
130  +ev = Equal.trans(Nat, T0, T1, T7, e0, Equal.trans(Nat, T1, T2, T7, e1, Equal.trans(Nat, T2, T3, T7, e2, Equal.trans(Nat, T3, T4, T7, e3, Equal.trans(Nat, T4, T5, T7, e4, Equal.trans(Nat, T5, T6, T7, e5, e6))))))
131  +eb = Equal.sym(List<&2, U32>, SX.le_bytes(32n, T0), MA, XB.bytes_le(32n, MA, S3.mul_add_lt(one, h1, k, s, r, lk, os, hr, ls, lr)))
132  +e8 = Equal.trans(List<&2, U32>, MA, SX.le_bytes(32n, T0), SX.le_bytes(32n, T7), eb, Equal.cong(Nat, List<&2, U32>, z => SX.le_bytes(32n, z), T0, T7, ev))
133  L.subst(Nat, z => {MA == SX.le_bytes(z, T7) : List<&2, U32>}, 32n, C.shift(5n, one), Equal.cong(Nat, Nat, z => C.shift(5n, z), 1n, one, Equal.sym(Nat, one, 1n, h1)), e8)
134
135# ---- key generation ----
136
137def public_body_rel(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +xs: List<&2, U32>, +D: Nat, +rd: RL.R(pp, PT.cs_d(PT.consts(xs)), D), +rd2: RL.R(pp, PT.cs_d2(PT.consts(xs)), FS.fadd(1n+pp, D, D)), +h: List<&2, U32>, +hh: {LM.okb(64n, h, 255n) == True{} : Bool}) -> {E.public_of(PT.consts(xs), xs, h) == SE.public_body(one, 1n+pp, D, h) : List<&2, U32>}:
138  +P = {1n+pp : Nat}
139  +cs = PT.consts(xs)
140  +sk = X.clamp(F.take(32n, h))
141  +hs = XB.clamp_okb(F.take(32n, h), BY.take_okb(32n, 32n, h, 255n, hh))
142  +B = PT.base(cs, xs)
143  +SB = SE.base(P, D)
144  +hB = PD.base_rel(one, h1, pp, hP, cs, D, rd, PC.r_sqm1(one, h1, pp, hP, xs), xs)
145  +rm = mul_rel(one, h1, pp, hP, cs, D, rd2, sk, hs, B, SB, hB)
146  +e1 = enc_rel(one, h1, pp, hP, PT.mul(cs, sk, B), SE.mul(one, P, D, FS.value(sk), SB), rm)
147  Equal.trans(List<&2, U32>, PT.encode(PT.mul(cs, sk, B)), SE.encode(one, P, SE.mul(one, P, D, FS.value(sk), SB)), SE.encode(one, P, SE.mul(one, P, D, SE.secret(h), SB)), e1, Equal.cong(Nat, List<&2, U32>, z => SE.encode(one, P, SE.mul(one, P, D, z, SB)), FS.value(sk), SE.secret(h), secret_eq(h)))
148
149def pub_guard(+one: Nat, +p: Nat, +d: Nat, +h: List<&2, U32>, +x: List<&2, U32>, +e: {x == SE.public_body(one, p, d, h) : List<&2, U32>}) -> {x == SE.public_of(one, p, d, h) : List<&2, U32>}:
150  match d:
151    case 0n:
152      e
153    case 1n+ +q:
154      e
155
156def public_rel(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +xs: List<&2, U32>, +D: Nat, +rd: RL.R(pp, PT.cs_d(PT.consts(xs)), D), +rd2: RL.R(pp, PT.cs_d2(PT.consts(xs)), FS.fadd(1n+pp, D, D)), +h: List<&2, U32>, +hh: {LM.okb(64n, h, 255n) == True{} : Bool}) -> {E.public_of(PT.consts(xs), xs, h) == SE.public_of(one, 1n+pp, D, h) : List<&2, U32>}:
157  pub_guard(one, 1n+pp, D, h, E.public_of(PT.consts(xs), xs, h), public_body_rel(one, h1, pp, hP, xs, D, rd, rd2, h, hh))
158
159def rb_eq(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +cs: PT.Cs, +D: Nat, +rd2: RL.R(pp, PT.cs_d2(cs), FS.fadd(1n+pp, D, D)), +B: PT.Pt, +SB: SE.EPt, +hB: PR.Rp(pp, B, SB), +r: List<&2, U32>, +okr: {LM.okb(32n, r, 255n) == True{} : Bool}, +Rs: Nat, +eR: {FS.value(r) == Rs : Nat}) -> {PT.encode(PT.mul(cs, r, B)) == SE.encode(one, 1n+pp, SE.mul(one, 1n+pp, D, Rs, SB)) : List<&2, U32>}:
160  +P = {1n+pp : Nat}
161  Equal.trans(List<&2, U32>, PT.encode(PT.mul(cs, r, B)), SE.encode(one, P, SE.mul(one, P, D, FS.value(r), SB)), SE.encode(one, P, SE.mul(one, P, D, Rs, SB)), enc_rel(one, h1, pp, hP, PT.mul(cs, r, B), SE.mul(one, P, D, FS.value(r), SB), mul_rel(one, h1, pp, hP, cs, D, rd2, r, okr, B, SB, hB)), Equal.cong(Nat, List<&2, U32>, z => SE.encode(one, P, SE.mul(one, P, D, z, SB)), FS.value(r), Rs, eR))
162
163# R || S
164def sig_eq(+one: Nat, +h1: {one == 1n : Nat}, +RB: List<&2, U32>, +SRB: List<&2, U32>, +eRB: {RB == SRB : List<&2, U32>}, +k: List<&2, U32>, +okk: {LM.okb(32n, k, 255n) == True{} : Bool}, +Ks: Nat, +eK: {FS.value(k) == Ks : Nat}, +r: List<&2, U32>, +okr: {LM.okb(32n, r, 255n) == True{} : Bool}, +lr: {Nat.is_lt(FS.value(r), 1n+S3.mmL(one)) == True{} : Bool}, +Rs: Nat, +eR: {FS.value(r) == Rs : Nat}, +sk: List<&2, U32>, +hsk: {LM.okb(32n, sk, 255n) == True{} : Bool}, +Ss: Nat, +eS: {FS.value(sk) == Ss : Nat}) -> {E.cat(RB, ESC.mul_add(k, ESC.reduce(sk), r)) == SE.cat(SRB, SX.le_bytes(C.shift(5n, one), Nat.mod(Nat.add(Rs, Nat.mul(Ks, Ss)), SE.ell(one)))) : List<&2, U32>}:
165  +MA = ESC.mul_add(k, ESC.reduce(sk), r)
166  +SMB = SX.le_bytes(C.shift(5n, one), Nat.mod(Nat.add(Rs, Nat.mul(Ks, Ss)), SE.ell(one)))
167  +eMA = ma_eq(one, h1, k, r, sk, okk, okr, lr, hsk, Rs, Ks, Ss, eR, eK, eS)
168  Equal.trans(List<&2, U32>, E.cat(RB, MA), SE.cat(RB, MA), SE.cat(SRB, SMB), BY.cat_eq(RB, MA), Equal.trans(List<&2, U32>, SE.cat(RB, MA), SE.cat(SRB, MA), SE.cat(SRB, SMB), Equal.cong(List<&2, U32>, List<&2, U32>, z => SE.cat(z, MA), RB, SRB, eRB), Equal.cong(List<&2, U32>, List<&2, U32>, z => SE.cat(SRB, z), MA, SMB, eMA)))
169
170def prefix_eq(+h: List<&2, U32>, +msg: List<&2, U32>) -> {E.cat(F.drop(32n, h), msg) == SE.cat(SE.rest(32n, h), msg) : List<&2, U32>}:
171  Equal.trans(List<&2, U32>, E.cat(F.drop(32n, h), msg), SE.cat(F.drop(32n, h), msg), SE.cat(SE.rest(32n, h), msg), BY.cat_eq(F.drop(32n, h), msg), Equal.cong(List<&2, U32>, List<&2, U32>, z => SE.cat(z, msg), F.drop(32n, h), SE.rest(32n, h), BY.drop_eq(32n, h)))
172
173def sign_body_rel(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +xs: List<&2, U32>, +D: Nat, +rd: RL.R(pp, PT.cs_d(PT.consts(xs)), D), +rd2: RL.R(pp, PT.cs_d2(PT.consts(xs)), FS.fadd(1n+pp, D, D)), +h: List<&2, U32>, +hh: {LM.okb(64n, h, 255n) == True{} : Bool}, +msg: List<&2, U32>) -> {E.sign_with(PT.consts(xs), xs, h, msg) == SE.sign_body(one, 1n+pp, D, h, msg) : List<&2, U32>}:
174  +P = {1n+pp : Nat}
175  +el = SE.ell(one)
176  +cs = PT.consts(xs)
177  +B = PT.base(cs, xs)
178  +SB = SE.base(P, D)
179  +hB = PD.base_rel(one, h1, pp, hP, cs, D, rd, PC.r_sqm1(one, h1, pp, hP, xs), xs)
180  +A = E.public_of(cs, xs, h)
181  +SA = SE.public_of(one, P, D, h)
182  +RH = E.cat(F.drop(32n, h), msg)
183  +SRH = SE.cat(SE.rest(32n, h), msg)
184  +r = ESC.reduce(H.sha512(RH))
185  +Rs = Nat.mod(FS.value(SHA.sha512_bytes(SRH)), el)
186  +eR = rh_eq(one, h1, RH, SRH, prefix_eq(h, msg))
187  +okr = S3.reduce_okb(one, h1, H.sha512(RH), BY.sha_lea(RH))
188  +RB = PT.encode(PT.mul(cs, r, B))
189  +SRB = SE.encode(one, P, SE.mul(one, P, D, Rs, SB))
190  +eRB = rb_eq(one, h1, pp, hP, cs, D, rd2, B, SB, hB, r, okr, Rs, eR)
191  +k = E.hram(RB, A, msg)
192  +Ks = SE.hram(one, SRB, SA, msg)
193  +eK = hk_val(one, h1, RB, SRB, eRB, A, SA, public_rel(one, h1, pp, hP, xs, D, rd, rd2, h, hh), msg)
194  +sk = X.clamp(F.take(32n, h))
195  +hsk = XB.clamp_okb(F.take(32n, h), BY.take_okb(32n, 32n, h, 255n, hh))
196  sig_eq(one, h1, RB, SRB, eRB, k, hk_okb(one, h1, RB, A, msg), Ks, eK, r, okr, red_lt(one, h1, H.sha512(RH), BY.sha_lea(RH)), Rs, eR, sk, hsk, SE.secret(h), secret_eq(h))
197
198def sign_guard(+one: Nat, +p: Nat, +d: Nat, +h: List<&2, U32>, +msg: List<&2, U32>, +x: List<&2, U32>, +e: {x == SE.sign_body(one, p, d, h, msg) : List<&2, U32>}) -> {x == SE.sign_with(one, p, d, h, msg) : List<&2, U32>}:
199  match d:
200    case 0n:
201      e
202    case 1n+ +q:
203      e
204
205def sign_rel(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +xs: List<&2, U32>, +D: Nat, +rd: RL.R(pp, PT.cs_d(PT.consts(xs)), D), +rd2: RL.R(pp, PT.cs_d2(PT.consts(xs)), FS.fadd(1n+pp, D, D)), +h: List<&2, U32>, +hh: {LM.okb(64n, h, 255n) == True{} : Bool}, +msg: List<&2, U32>) -> {E.sign_with(PT.consts(xs), xs, h, msg) == SE.sign_with(one, 1n+pp, D, h, msg) : List<&2, U32>}:
206  sign_guard(one, 1n+pp, D, h, msg, E.sign_with(PT.consts(xs), xs, h, msg), sign_body_rel(one, h1, pp, hP, xs, D, rd, rd2, h, hh, msg))
207
208# ---- verification ----
209
210def check_some(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +pk: List<&2, U32>, +msg: List<&2, U32>, +rb: List<&2, U32>, +sb: List<&2, U32>, +hsb: {LM.okb(32n, sb, 255n) == True{} : Bool}, +r: PT.Pt, +sr: SE.EPt, +hr: PR.Rp(pp, r, sr), +a: PT.Pt, +sa: SE.EPt, +ha: PR.Rp(pp, a, sa)) -> {E.check(PT.consts(pk), sb, rb, pk, msg, Some{r}, Some{a}) == SE.check(one, 1n+pp, SE.dconst(one, 1n+pp), FS.value(sb), rb, pk, msg, Some{sr}, Some{sa}) : Bool}:
211  +P = {1n+pp : Nat}
212  +D = SE.dconst(one, P)
213  +cs = PT.consts(pk)
214  +B = PT.base(cs, pk)
215  +SB = SE.base(P, D)
216  +hB = PD.base_rel(one, h1, pp, hP, cs, D, PC.r_d(one, h1, pp, hP, pk), PC.r_sqm1(one, h1, pp, hP, pk), pk)
217  +rd2 = PC.r_d2(one, h1, pp, hP, pk)
218  +k = E.hram(rb, pk, msg)
219  +Ks = SE.hram(one, rb, pk, msg)
220  +eK = hk_val(one, h1, rb, rb, {==}, pk, pk, {==}, msg)
221  +okk = hk_okb(one, h1, rb, pk, msg)
222  +ka = PT.mul(cs, k, a)
223  +ska = SE.mul(one, P, D, FS.value(k), sa)
224  +m1 = mul_rel(one, h1, pp, hP, cs, D, rd2, sb, hsb, B, SB, hB)
225  +m2 = mul_rel(one, h1, pp, hP, cs, D, rd2, k, okk, a, sa, ha)
226  +ad = PR.add_rel(one, h1, pp, hP, cs, D, rd2, r, ka, sr, ska, hr, m2)
227  +lhs = SE.mul(one, P, D, FS.value(sb), SB)
228  +eq = PC.equal_rel(one, h1, pp, hP, PT.mul(cs, sb, B), PT.add(cs, r, ka), lhs, SE.add(P, D, sr, ska), m1, ad)
229  Equal.trans(Bool, PT.equal(PT.mul(cs, sb, B), PT.add(cs, r, ka)), SE.equal(P, lhs, SE.add(P, D, sr, ska)), SE.equal(P, lhs, SE.add(P, D, sr, SE.mul(one, P, D, Ks, sa))), eq, Equal.cong(Nat, Bool, z => SE.equal(P, lhs, SE.add(P, D, sr, SE.mul(one, P, D, z, sa))), FS.value(k), Ks, eK))
230
231def check_a(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +pk: List<&2, U32>, +msg: List<&2, U32>, +rb: List<&2, U32>, +sb: List<&2, U32>, +hsb: {LM.okb(32n, sb, 255n) == True{} : Bool}, +r: PT.Pt, +sr: SE.EPt, +hr: PR.Rp(pp, r, sr), +aa: Maybe<&2, PT.Pt>, +saa: Maybe<&2, SE.EPt>, +haa: PC.MR(pp, aa, saa)) -> {E.check(PT.consts(pk), sb, rb, pk, msg, Some{r}, aa) == SE.check(one, 1n+pp, SE.dconst(one, 1n+pp), FS.value(sb), rb, pk, msg, Some{sr}, saa) : Bool}:
232  match aa saa:
233    case None{} None{}:
234      {==}
235    case Some{+a} Some{+sa}:
236      check_some(one, h1, pp, hP, pk, msg, rb, sb, hsb, r, sr, hr, a, sa, haa)
237    case None{} Some{+sa}:
238      Empty.absurd({E.check(PT.consts(pk), sb, rb, pk, msg, Some{r}, None{}) == SE.check(one, 1n+pp, SE.dconst(one, 1n+pp), FS.value(sb), rb, pk, msg, Some{sr}, Some{sa}) : Bool}, L.true_false(haa))
239    case Some{+a} None{}:
240      Empty.absurd({E.check(PT.consts(pk), sb, rb, pk, msg, Some{r}, Some{a}) == SE.check(one, 1n+pp, SE.dconst(one, 1n+pp), FS.value(sb), rb, pk, msg, Some{sr}, None{}) : Bool}, L.true_false(haa))
241
242def check_rel(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +pk: List<&2, U32>, +msg: List<&2, U32>, +rb: List<&2, U32>, +sb: List<&2, U32>, +hsb: {LM.okb(32n, sb, 255n) == True{} : Bool}, +ra: Maybe<&2, PT.Pt>, +sra: Maybe<&2, SE.EPt>, +hra: PC.MR(pp, ra, sra), +aa: Maybe<&2, PT.Pt>, +saa: Maybe<&2, SE.EPt>, +haa: PC.MR(pp, aa, saa)) -> {E.check(PT.consts(pk), sb, rb, pk, msg, ra, aa) == SE.check(one, 1n+pp, SE.dconst(one, 1n+pp), FS.value(sb), rb, pk, msg, sra, saa) : Bool}:
243  match ra sra:
244    case None{} None{}:
245      {==}
246    case Some{+r} Some{+sr}:
247      check_a(one, h1, pp, hP, pk, msg, rb, sb, hsb, r, sr, hra, aa, saa, haa)
248    case None{} Some{+sr}:
249      Empty.absurd({E.check(PT.consts(pk), sb, rb, pk, msg, None{}, aa) == SE.check(one, 1n+pp, SE.dconst(one, 1n+pp), FS.value(sb), rb, pk, msg, Some{sr}, saa) : Bool}, L.true_false(hra))
250    case Some{+r} None{}:
251      Empty.absurd({E.check(PT.consts(pk), sb, rb, pk, msg, Some{r}, aa) == SE.check(one, 1n+pp, SE.dconst(one, 1n+pp), FS.value(sb), rb, pk, msg, None{}, saa) : Bool}, L.true_false(hra))
252
253def verify_with_rel(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +pk: List<&2, U32>, +hpk: {LM.okb(32n, pk, 255n) == True{} : Bool}, +msg: List<&2, U32>, +rb: List<&2, U32>, +hrb: {LM.okb(32n, rb, 255n) == True{} : Bool}, +sb: List<&2, U32>, +hsb: {LM.okb(32n, sb, 255n) == True{} : Bool}, +s_ok: Bool) -> {E.verify_with(PT.consts(pk), pk, msg, rb, sb, s_ok) == SE.verify_with(one, 1n+pp, SE.dconst(one, 1n+pp), pk, msg, rb, FS.value(sb), s_ok) : Bool}:
254  match s_ok:
255    case True{}:
256      +P = {1n+pp : Nat}
257      +D = SE.dconst(one, P)
258      +cs = PT.consts(pk)
259      +rd = PC.r_d(one, h1, pp, hP, pk)
260      +rs = PC.r_sqm1(one, h1, pp, hP, pk)
261      check_rel(one, h1, pp, hP, pk, msg, rb, sb, hsb, PT.decode(cs, rb), SE.decode(P, D, rb), PD.decode_rel(one, h1, pp, hP, cs, D, rd, rs, rb, hrb), PT.decode(cs, pk), SE.decode(P, D, pk), PD.decode_rel(one, h1, pp, hP, cs, D, rd, rs, pk, hpk))
262    case False{}:
263      {==}