~/bend-docscommunity

spec/crypto/secp256k1/curve.bend checks

raw source on the hub · import 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/secp256k1/curve.bend as Curve

3 imports
import Base
import ../../lib/common.bend as C
import ./field.bend as FS

Types

type SPoint source · line 24 · raw

Data

type SOp source · line 27 · raw

Data

type SAffine source · line 163 · raw

Data

Definitions

def nth source · line 32 · raw

@i:Nat -> @regs:List<&2, Nat> -> Nat

def exec source · line 38 · raw

@+p:Nat -> @op:SOp -> @+regs:List<&2, Nat> -> Nat

def run_go source · line 45 · raw

@+p:Nat -> @prog:List<&2, SOp> -> @+regs:List<&2, Nat> -> List<&2, Nat>

run a program: each instruction appends its result as a new register

def run source · line 51 · raw

@+p:Nat -> @prog:List<&2, SOp> -> @regs:List<&2, Nat> -> List<&2, Nat>

(the first register is looked at first; the result is run_go's)

def add_prog source · line 71 · raw

List<&2, SOp>

RCB Algorithm 7 (a = 0). Registers: 0 X1, 1 Y1, 2 Z1, 3 X2, 4 Y2, 5 Z2, 6 b3; the paper's lines, in order, write registers 7..39: t0 = X1 X2 (7) t1 = Y1 Y2 (8) t2 = Z1 Z2 (9) t3 = X1 + Y1 (10) t4 = X2 + Y2 (11) t3 = t3 t4 (12) t4 = t0 + t1 (13) t3 = t3 - t4 (14) t4 = Y1 + Z1 (15) X3 = Y2 + Z2 (16) t4 = t4 X3 (17) X3 = t1 + t2 (18) t4 = t4 - X3 (19) X3 = X1 + Z1 (20) Y3 = X2 + Z2 (21) X3 = X3 Y3 (22) Y3 = t0 + t2 (23) Y3 = X3 - Y3 (24) X3 = t0 + t0 (25) t0 = X3 + t0 (26) t2 = b3 t2 (27) Z3 = t1 + t2 (28) t1 = t1 - t2 (29) Y3 = b3 Y3 (30) X3 = t4 Y3 (31) t2 = t3 t1 (32) X3 = t2 - X3 (33) Y3 = Y3 t0 (34) t1 = t1 Z3 (35) Y3 = t1 + Y3 (36) t0 = t0 t3 (37) Z3 = Z3 t4 (38) Z3 = Z3 + t0 (39) and the result is (X3 : Y3 : Z3) = registers (33 : 36 : 39).

def dbl_prog source · line 89 · raw

List<&2, SOp>

RCB Algorithm 9 (a = 0). Registers: 0 X, 1 Y, 2 Z, 3 b3; lines write registers 4..21: t0 = Y Y (4) Z3 = t0 + t0 (5) Z3 = Z3 + Z3 (6) Z3 = Z3 + Z3 (7) t1 = Y Z (8) t2 = Z Z (9) t2 = b3 t2 (10) X3 = t2 Z3 (11) Y3 = t0 + t2 (12) Z3 = t1 Z3 (13) t1 = t2 + t2 (14) t2 = t1 + t2 (15) t0 = t0 - t2 (16) Y3 = t0 Y3 (17) Y3 = X3 + Y3 (18) t1 = X Y (19) X3 = t0 t1 (20) X3 = X3 + X3 (21) and the result is (X3 : Y3 : Z3) = registers (21 : 18 : 13).

def b3 source · line 95 · raw

Nat

def add_out source · line 98 · raw

@+r:List<&2, Nat> -> SPoint

def padd source · line 101 · raw

@+p:Nat -> @a:SPoint -> @b:SPoint -> SPoint

def dbl_out source · line 106 · raw

@+r:List<&2, Nat> -> SPoint

def pdbl source · line 109 · raw

@+p:Nat -> @a:SPoint -> SPoint

def infinity source · line 114 · raw

SPoint

def is_inf source · line 117 · raw

@a:SPoint -> Bool

def bit source · line 122 · raw

@+i:Nat -> @+k:Nat -> Nat

bit i of k

def step source · line 125 · raw

@b:Nat -> @+p:Nat -> @+a:SPoint -> @+d:SPoint -> SPoint

def bits_go source · line 132 · raw

@i:Nat -> @+k:Nat -> List<&2, Nat>

bits i - 1, ..., 0 of k, most significant first (k is looked at first, so that on an unknown k nothing is unfolded)

def bits source · line 137 · raw

@+i:Nat -> @k:Nat -> List<&2, Nat>

def lmul source · line 144 · raw

@+p:Nat -> @bs:List<&2, Nat> -> @+a:SPoint -> @r:SPoint -> SPoint

left-to-right double-and-add: for each bit b, R = 2 R, then R = R + A when b is set

def pmul source · line 150 · raw

@+p:Nat -> @+k:Nat -> @+a:SPoint -> SPoint

[k] A for 0 <= k < 2^256

def g source · line 154 · raw

@+one:Nat -> SPoint

G (SEC 2), with z = 1

def aff_z source · line 166 · raw

@+p:Nat -> @+x:Nat -> @+y:Nat -> @+zi:Nat -> SAffine

def to_affine source · line 170 · raw

@+p:Nat -> @a:SPoint -> SAffine

(X / Z, Y / Z), (0, 0) for the point at infinity

def aff_x source · line 174 · raw

@a:SAffine -> Nat

def aff_y source · line 178 · raw

@a:SAffine -> Nat

def rhs source · line 183 · raw

@+p:Nat -> @+x:Nat -> Nat

x^3 + 7

def on_curve source · line 186 · raw

@+p:Nat -> @+x:Nat -> @+y:Nat -> Bool

def byte source · line 191 · raw

@+b:U32 -> Nat

def os2ip_go source · line 195 · raw

@bs:List<&2, U32> -> @acc:Nat -> Nat

OS2IP (big-endian)

def os2ip source · line 200 · raw

@bs:List<&2, U32> -> Nat

def i2osp_le source · line 204 · raw

@n:Nat -> @+x:Nat -> List<&2, U32>

I2OSP: the n low bytes of x, big-endian

def i2osp_go source · line 209 · raw

@n:Nat -> @+x:Nat -> List<&2, U32>

def i2osp source · line 213 · raw

@+n:Nat -> @x:Nat -> List<&2, U32>

(x is looked at first, so that on an unknown x nothing is unfolded)

def length_is source · line 218 · raw

@n:Nat -> @bs:List<&2, U32> -> Bool

def first source · line 221 · raw

@n:Nat -> @bs:List<&2, U32> -> List<&2, U32>

def after source · line 227 · raw

@n:Nat -> @bs:List<&2, U32> -> List<&2, U32>

def enc_c source · line 240 · raw

@a:SAffine -> List<&2, U32>

def encode_compressed source · line 245 · raw

@+p:Nat -> @a:SPoint -> List<&2, U32>

compressed: 02 or 03 (the parity of y), then x

def enc_u source · line 248 · raw

@a:SAffine -> List<&2, U32>

def encode_uncompressed source · line 253 · raw

@+p:Nat -> @a:SPoint -> List<&2, U32>

uncompressed: 04, x, y

def pick_if source · line 258 · raw

@+p:Nat -> @+y:Nat -> @same:Bool -> Nat

y = (x^3 + 7)^((p + 1) / 4), then y or p - y to get the wanted parity; no point when that y does not square to x^3 + 7

def pick_parity source · line 263 · raw

@+p:Nat -> @+y:Nat -> @+par:Nat -> Nat

def decompress_if source · line 266 · raw

@+x:Nat -> @+y:Nat -> @ok:Bool -> Maybe<&2, SPoint>

def decompress_y source · line 271 · raw

@+p:Nat -> @+x:Nat -> @+par:Nat -> @+y:Nat -> Maybe<&2, SPoint>

def decompress source · line 274 · raw

@+p:Nat -> @+x:Nat -> @+par:Nat -> Maybe<&2, SPoint>

def decode_c_if source · line 277 · raw

@+p:Nat -> @+pre:U32 -> @+x:Nat -> @ok:Bool -> Maybe<&2, SPoint>

def decode_c source · line 282 · raw

@+p:Nat -> @+pre:U32 -> @+x:Nat -> Maybe<&2, SPoint>

def decode_u source · line 285 · raw

@+p:Nat -> @+pre:U32 -> @+x:Nat -> @+y:Nat -> Maybe<&2, SPoint>

def decode_len source · line 290 · raw

@+p:Nat -> @+bs:List<&2, U32> -> @c33:Bool -> @c65:Bool -> Maybe<&2, SPoint>

a compressed (33 bytes) or uncompressed (65 bytes) public key; None when malformed, a coordinate is not below p, or the point is not on the curve

def decode source · line 296 · raw

@+p:Nat -> @+bs:List<&2, U32> -> Maybe<&2, SPoint>