~/bend-docscommunity

src/crypto/secp256k1/point.bend checks

raw source on the hub · import 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/secp256k1/point.bend as Point

4 imports
import Base
import ./limbs.bend as L
import ./field.bend as F
import ./bytes.bend as B

Types

type Op source · line 25 · raw

Data

type Point source · line 30 · raw

Data

type Affine source · line 139 · raw

Data

Definitions

def nth source · line 33 · raw

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

def exec source · line 39 · raw

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

def run_go source · line 45 · raw

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

def run source · line 52 · raw

@prog:List<&2, Op> -> @regs:List<&2, List<&2, Nat>> -> List<&2, List<&2, Nat>>

The first register is looked at before the program runs, so that the proof checker stops at once on unknown inputs (the result is run_go's).

def add_prog source · line 60 · raw

List<&2, Op>

RCB 2016 Algorithm 7 (a = 0): registers X1 Y1 Z1 X2 Y2 Z2 b3 = 0..6; the result is X3 Y3 Z3 = registers 33, 36, 39.

def dbl_prog source · line 71 · raw

List<&2, Op>

RCB 2016 Algorithm 9 (a = 0): registers X Y Z b3 = 0..3; the result is X3 Y3 Z3 = registers 21, 18, 13.

def b3 source · line 77 · raw

List<&2, Nat>

def add_out source · line 80 · raw

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

def add source · line 83 · raw

@p:Point -> @q:Point -> Point

def dbl_out source · line 88 · raw

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

def dbl source · line 91 · raw

@p:Point -> Point

def infinity source · line 96 · raw

Point

def neg source · line 99 · raw

@p:Point -> Point

def select source · line 104 · raw

@+b:Nat -> @p:Point -> @q:Point -> Point

b ? p : q, coordinate-wise and branch-free, for b in {0, 1}

def step source · line 109 · raw

@+b:Nat -> @+p:Point -> @+d:Point -> Point

def mul_go source · line 112 · raw

@bits:List<&2, Nat> -> @+p:Point -> @+r:Point -> Point

def mul source · line 118 · raw

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

[k] p for a scalar k given by its 16 limbs (any value below 2^256)

def gx source · line 121 · raw

List<&2, Nat>

def gy source · line 125 · raw

List<&2, Nat>

def g source · line 130 · raw

Point

the generator G of SEC 2

def is_inf source · line 133 · raw

@p:Point -> Bool

def to_affine_z source · line 142 · raw

@+x:List<&2, Nat> -> @+y:List<&2, Nat> -> @+zi:List<&2, Nat> -> Affine

def to_affine source · line 146 · raw

@p:Point -> Affine

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

def aff_x source · line 150 · raw

@a:Affine -> List<&2, Nat>

def aff_y source · line 154 · raw

@a:Affine -> List<&2, Nat>

def rhs source · line 159 · raw

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

x^3 + 7

def on_curve source · line 162 · raw

@+x:List<&2, Nat> -> @+y:List<&2, Nat> -> Bool

def lift_y source · line 166 · raw

@+y:List<&2, Nat> -> @+par:Nat -> List<&2, Nat>

the square root of x^3 + 7 with the given parity, if x^3 + 7 is a square

def decompress_if source · line 169 · raw

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

def decompress source · line 174 · raw

@+x:List<&2, Nat> -> @+par:Nat -> Maybe<&2, Point>

def decode_c source · line 178 · raw

@+x:List<&2, Nat> -> @+par:Nat -> @ok:Bool -> Maybe<&2, Point>

def decode_u source · line 183 · raw

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

def decode_33 source · line 188 · raw

@+pre:U32 -> @+rest:List<&2, U32> -> Maybe<&2, Point>

def decode_65 source · line 192 · raw

@+pre:U32 -> @+rest:List<&2, U32> -> Maybe<&2, Point>

def decode_len source · line 197 · raw

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

def decode source · line 206 · raw

@+bs:List<&2, U32> -> Maybe<&2, Point>

SEC 1 section 2.3.4: a compressed (33 bytes, prefix 02/03) or uncompressed (65 bytes, prefix 04) public key, None when malformed, not below p, or not on the curve (the point at infinity, encoded 00, is refused)

def enc_c source · line 210 · raw

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

SEC 1 section 2.3.3

def encode_compressed source · line 214 · raw

@p:Point -> List<&2, U32>

def enc_u source · line 217 · raw

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

def encode_uncompressed source · line 221 · raw

@p:Point -> List<&2, U32>