src/crypto/poly1305/poly1305.bend checks

raw source on the hub · import 0xd9a2fae439ac7ff9e21e0853948f94fe/src/crypto/poly1305/poly1305.bend as Poly1305

3 imports

import Base
import ./limbs.bend as L
import ../subtle.bend as Subtle

Definitions

def mask source · line 12 · raw

@xs:List<&2, U32> -> List<&2, U32>

def clamp_mask source · line 18 · raw

@i:Nat -> U32

r &= 0x0ffffffc0ffffffc0ffffffc0fffffff, byte by byte.

def clamp source · line 29 · raw

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

def load source · line 35 · raw

@b:List<&2, U32> -> List<&2, U32>

A message block as limbs: its bytes, then the 0x01 byte.

def absorb source · line 41 · raw

@fuel:Nat -> @+msg:List<&2, U32> -> @+r:List<&2, U32> -> @h:List<&2, U32> -> List<&2, U32>

The accumulator over 16-byte blocks (the last one possibly shorter); fuel bounds the number of blocks. (A one-byte message is its own case only so that a proof about a message b <> rest with rest unknown stays small.)

def zero source · line 50 · raw

List<&2, U32>

def r_key source · line 54 · raw

@+key:List<&2, U32> -> List<&2, U32>

r = clamp(key[0..16]) and s = key[16..32], as limbs.

def s_key source · line 57 · raw

@+key:List<&2, U32> -> List<&2, U32>

def tag source · line 60 · raw

@+key:List<&2, U32> -> @+msg:List<&2, U32> -> List<&2, U32>

def mac source · line 68 · raw

@+key:List<&2, U32> -> @+msg:List<&2, U32> -> List<&2, U32>

The 16-byte tag of msg under key = r || s. (The match on msg only keeps a proof's goal small while msg is unknown; both arms are the same.)

def has_key source · line 73 · raw

@+key:List<&2, U32> -> Bool

def when source · line 76 · raw

@ok:Bool -> @x:List<&2, U32> -> Maybe<&2, List<&2, U32>>

def poly1305 source · line 82 · raw

@+key:List<&2, U32> -> @+msg:List<&2, U32> -> Maybe<&2, List<&2, U32>>

The tag, or None unless the key has 32 bytes.

def verify source · line 87 · raw

@+key:List<&2, U32> -> @+msg:List<&2, U32> -> @+tag:List<&2, U32> -> Bool

True exactly when the key has 32 bytes and tag is the tag of msg; the tags are compared in constant time (src/crypto/subtle.bend).