src/crypto/poly1305/limbs.bend checks
raw source on the hub · import 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/poly1305/limbs.bend as Limbs
1 import
import Base
Definitions
def hd0 source · line 15 · raw
@xs:List<&2, U32> -> U32
The first limb (0 for the empty list) and the rest.
def tl source · line 20 · raw
@xs:List<&2, U32> -> List<&2, U32>
def add source · line 26 · raw
@a:List<&2, U32> -> @b:List<&2, U32> -> List<&2, U32>
Limb-wise sum (the shorter list is padded with zeros), no carries.
def scale source · line 33 · raw
@+c:U32 -> @a:List<&2, U32> -> List<&2, U32>
Every limb times c, no carries.
def mul source · line 39 · raw
@+x:List<&2, U32> -> @r:List<&2, U32> -> List<&2, U32>
Schoolbook product, no carries: x r0 + 2^8 (x r1 + 2^8 (...)).
def take source · line 44 · raw
@n:Nat -> @xs:List<&2, U32> -> List<&2, U32>
def skip source · line 50 · raw
@n:Nat -> @xs:List<&2, U32> -> List<&2, U32>
def fit source · line 57 · raw
@n:Nat -> @+xs:List<&2, U32> -> List<&2, U32>
The first n limbs, padded with zeros to exactly n.
def fold source · line 63 · raw
@+z:List<&2, U32> -> List<&2, U32>
2^136 = 64 p + 320: limbs 17.. are folded onto limbs 0.. times 320.
def carry source · line 68 · raw
@n:Nat -> @+ds:List<&2, U32> -> @u:U32 -> List<&2, U32>
A carry pass over n limbs, each kept to 8 bits; the carry u and all limbs from n on (one, on the Poly1305 path) are summed into the top limb.
def split source · line 77 · raw
@n:Nat -> @+xs:List<&2, U32> -> List<&2, U32>
Limb n (the top one) reduced to its low 2 bits, i.e. the value below 2^130 when n = 16; quot is the rest of limb n, the multiple of 2^130.
def quot source · line 82 · raw
@n:Nat -> @+xs:List<&2, U32> -> U32
def reduce source · line 90 · raw
@+d:List<&2, U32> -> List<&2, U32>
Partial reduction of 17 limbs: carry, then 2^130 q = p q + 5 q, so q is folded back as 5 q on limb 0 and carried again. The result has limbs 0..15 below 2^8 and a value below 5 * 2^128 < 2p.
def block source · line 95 · raw
@+r:List<&2, U32> -> @h:List<&2, U32> -> @c:List<&2, U32> -> List<&2, U32>
One Poly1305 block: h = (h + c) r, partially reduced mod p.
def pick source · line 99 · raw
@+m:U32 -> @+a:U32 -> @b:U32 -> U32
a when m is all zeros, b when m is all ones.
def select source · line 102 · raw
@+m:U32 -> @a:List<&2, U32> -> @b:List<&2, U32> -> List<&2, U32>
def freeze source · line 109 · raw
@+h:List<&2, U32> -> List<&2, U32>
The low 16 limbs of h mod p, for h below 2p: g = h + 5 has bit 130 set exactly when h >= p, and then its low 128 bits are those of h - p.
def bytes source · line 115 · raw
@n:Nat -> @+ds:List<&2, U32> -> @u:U32 -> List<&2, U32>
n bytes of the value of ds + u (mod 2^(8n)).
def fin source · line 125 · raw
@+h:List<&2, U32> -> @s:List<&2, U32> -> List<&2, U32>
The tag bytes: the low 128 bits of (h mod p) + s. (Entered through a match on s, both arms the same: while s is unknown a proof's goal stays one call instead of sixteen unfolded byte steps.)