~/jendhub

spec/crypto/curve25519/field.bend

bend-collections-laws-crypto@1.0.0.0 · 169 lines · 33 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/src/crypto/curve25519/field.bend as F
4
5# GF(p), p = 2^255 - 19, over the natural numbers, and the contract of
6# src/crypto/curve25519/field.bend.
7#
8# The checker keeps every closed natural number it compares in unary, so
9# 2^255 is never written closed: it is C.shift(255n, one), with `one` a
10# variable that every clause takes together with the hypothesis
11# {one == 1n : Nat}. For one == 1 these are the usual constants; no other
12# value of `one` satisfies the hypothesis, so each clause says exactly what
13# it says with the constants written out. (The same device as the proofs of
14# spec/math/w64.bend, which keep 2^32 as a shift of a symbolic one.)
15#
16# Representation: a field element is a list of U32 limbs, little-endian in
17# radix 2^8 (value = RFC 7748's decodeLittleEndian); "tight" is 32 limbs,
18# each below 2^8, which is also a 32-byte string.
19#
20#   function          clauses
21#   add               Add.value, Add.tight
22#   sub               Sub.value, Sub.tight
23#   mul, sq           Mul.value, Mul.tight, Sq.value, Sq.tight
24#   mul_small         MulSmall.value, MulSmall.tight
25#   select            Select.zero, Select.one
26#   inv               Inv.value, Inv.tight
27#   pow_p58           PowP58.value, PowP58.tight
28#   freeze, to_bytes  Freeze.value (the canonical representative), Freeze.tight
29#   of_bytes          OfBytes.tight (its value is covered by X25519.value)
30#   eq, is_zero       Eq.value, IsZero.value
31#   parity            Parity.value
32
33# decodeLittleEndian (RFC 7748 section 5): sum of b_i 2^(8 i)
34def value(xs: List<&2, U32>) -> Nat:
35  match xs:
36    case Nil{}:
37      0n
38    case Con{h, t}:
39      Nat.add(U32.to_nat(h), C.shift(8n, value(t)))
40
41# n values, each below 2^8
42def bytes_ok(n: Nat, xs: List<&2, U32>) -> Bool:
43  match n:
44    case 0n:
45      match xs:
46        case Nil{}:
47          True{}
48        case Con{x, xt}:
49          False{}
50    case 1n+m:
51      match xs:
52        case Nil{}:
53          False{}
54        case Con{x, xt}:
55          Bool.and(Nat.is_lt(U32.to_nat(x), 256n), bytes_ok(m, xt))
56
57def tight(xs: List<&2, U32>) -> Bool:
58  bytes_ok(32n, xs)
59
60# a constant from its little-endian base-256 digits, each scaled by the
61# symbolic one (so the checker never unfolds it): digits(one, [65n, 219n, 1n])
62# is 121665 for one == 1
63def digits(+one: Nat, ds: List<&2, Nat>) -> Nat:
64  match ds:
65    case Nil{}:
66      0n
67    case Con{d, dt}:
68      Nat.add(Nat.mul(one, d), C.shift(8n, digits(one, dt)))
69
70# a constant from its little-endian bytes (U32 values), each scaled by the
71# symbolic one: uvalue(one, bs) is value(bs) for one == 1
72def uvalue(+one: Nat, xs: List<&2, U32>) -> Nat:
73  match xs:
74    case Nil{}:
75      0n
76    case Con{x, xt}:
77      Nat.add(Nat.mul(one, U32.to_nat(x)), C.shift(8n, uvalue(one, xt)))
78
79# p = 2^255 - 19
80def prime(+one: Nat) -> Nat:
81  Nat.sub(C.shift(255n, one), 19n)
82
83# arithmetic mod p (every result reduced)
84def fadd(+p: Nat, a: Nat, b: Nat) -> Nat:
85  Nat.mod(Nat.add(a, b), p)
86
87def fsub(+p: Nat, a: Nat, b: Nat) -> Nat:
88  Nat.mod(Nat.sub(Nat.add(a, p), Nat.mod(b, p)), p)
89
90def fmul(+p: Nat, a: Nat, b: Nat) -> Nat:
91  Nat.mod(Nat.mul(a, b), p)
92
93def fpow(+p: Nat, a: Nat, e: Nat) -> Nat:
94  Nat.mod(Nat.pow(a, e), p)
95
96# a^(p - 2): the inverse of a nonzero a (Fermat), 0 for 0 (RFC 7748 section 5)
97def finv(+p: Nat, a: Nat) -> Nat:
98  fpow(p, a, Nat.sub(p, 2n))
99
100# ---- clauses ----
101
102def Add.value(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +b: List<&2, U32>, +ha: {tight(a) == True{} : Bool}, +hb: {tight(b) == True{} : Bool}) -> Type:
103  {Nat.mod(value(F.add(a, b)), prime(one)) == fadd(prime(one), value(a), value(b)) : Nat}
104
105def Add.tight(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +b: List<&2, U32>, +ha: {tight(a) == True{} : Bool}, +hb: {tight(b) == True{} : Bool}) -> Type:
106  {tight(F.add(a, b)) == True{} : Bool}
107
108def Sub.value(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +b: List<&2, U32>, +ha: {tight(a) == True{} : Bool}, +hb: {tight(b) == True{} : Bool}) -> Type:
109  {Nat.mod(value(F.sub(a, b)), prime(one)) == fsub(prime(one), value(a), value(b)) : Nat}
110
111def Sub.tight(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +b: List<&2, U32>, +ha: {tight(a) == True{} : Bool}, +hb: {tight(b) == True{} : Bool}) -> Type:
112  {tight(F.sub(a, b)) == True{} : Bool}
113
114def Mul.value(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +b: List<&2, U32>, +ha: {tight(a) == True{} : Bool}, +hb: {tight(b) == True{} : Bool}) -> Type:
115  {Nat.mod(value(F.mul(a, b)), prime(one)) == fmul(prime(one), value(a), value(b)) : Nat}
116
117def Mul.tight(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +b: List<&2, U32>, +ha: {tight(a) == True{} : Bool}, +hb: {tight(b) == True{} : Bool}) -> Type:
118  {tight(F.mul(a, b)) == True{} : Bool}
119
120def Sq.value(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +ha: {tight(a) == True{} : Bool}) -> Type:
121  {Nat.mod(value(F.sq(a)), prime(one)) == fmul(prime(one), value(a), value(a)) : Nat}
122
123def Sq.tight(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +ha: {tight(a) == True{} : Bool}) -> Type:
124  {tight(F.sq(a)) == True{} : Bool}
125
126# k below 2^17
127def MulSmall.value(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +k: U32, +ha: {tight(a) == True{} : Bool}, +hk: {Nat.is_lt(U32.to_nat(k), C.shift(17n, one)) == True{} : Bool}) -> Type:
128  {Nat.mod(value(F.mul_small(a, k)), prime(one)) == fmul(prime(one), value(a), U32.to_nat(k)) : Nat}
129
130def MulSmall.tight(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +k: U32, +ha: {tight(a) == True{} : Bool}, +hk: {Nat.is_lt(U32.to_nat(k), C.shift(17n, one)) == True{} : Bool}) -> Type:
131  {tight(F.mul_small(a, k)) == True{} : Bool}
132
133def Select.zero(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +b: List<&2, U32>, +ha: {tight(a) == True{} : Bool}, +hb: {tight(b) == True{} : Bool}) -> Type:
134  {F.select(0, a, b) == a : List<&2, U32>}
135
136def Select.one(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +b: List<&2, U32>, +ha: {tight(a) == True{} : Bool}, +hb: {tight(b) == True{} : Bool}) -> Type:
137  {F.select(1, a, b) == b : List<&2, U32>}
138
139def Inv.value(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +ha: {tight(a) == True{} : Bool}) -> Type:
140  {Nat.mod(value(F.inv(a)), prime(one)) == finv(prime(one), value(a)) : Nat}
141
142def Inv.tight(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +ha: {tight(a) == True{} : Bool}) -> Type:
143  {tight(F.inv(a)) == True{} : Bool}
144
145# a^((p - 5) / 8), RFC 8032 section 5.1.3
146def PowP58.value(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +ha: {tight(a) == True{} : Bool}) -> Type:
147  {Nat.mod(value(F.pow_p58(a)), prime(one)) == fpow(prime(one), value(a), Nat.div(Nat.sub(prime(one), 5n), 8n)) : Nat}
148
149def PowP58.tight(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +ha: {tight(a) == True{} : Bool}) -> Type:
150  {tight(F.pow_p58(a)) == True{} : Bool}
151
152# the canonical representative, which is the 32-byte encoding
153def Freeze.value(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +ha: {tight(a) == True{} : Bool}) -> Type:
154  {value(F.freeze(a)) == Nat.mod(value(a), prime(one)) : Nat}
155
156def Freeze.tight(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +ha: {tight(a) == True{} : Bool}) -> Type:
157  {tight(F.freeze(a)) == True{} : Bool}
158
159def OfBytes.tight(+one: Nat, +h1: {one == 1n : Nat}, +bs: List<&2, U32>, +hb: {tight(bs) == True{} : Bool}) -> Type:
160  {tight(F.of_bytes(bs)) == True{} : Bool}
161
162def Eq.value(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +b: List<&2, U32>, +ha: {tight(a) == True{} : Bool}, +hb: {tight(b) == True{} : Bool}) -> Type:
163  {F.eq(a, b) == Nat.is_eq(Nat.mod(value(a), prime(one)), Nat.mod(value(b), prime(one))) : Bool}
164
165def IsZero.value(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +ha: {tight(a) == True{} : Bool}) -> Type:
166  {F.is_zero(a) == Nat.is_eq(Nat.mod(value(a), prime(one)), 0n) : Bool}
167
168def Parity.value(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +ha: {tight(a) == True{} : Bool}) -> Type:
169  {U32.to_nat(F.parity(a)) == Nat.mod(Nat.mod(value(a), prime(one)), 2n) : Nat}