All pull requests

Pull requests

• AArch64 X25519: the ladder step's sums and differences with one fold of the carry

  #2500·alex opened Oct 16, 2026Member·

  ·

• AArch64 Ed25519/X25519: reduce field products with one ×38 chain and a fold at bit 255

  #2499·alex opened Oct 16, 2026Member·

  ·

• ML-KEM x86-64: K-PKE.KeyGen's matrix product in one function

  #2498·alex opened Oct 16, 2026Member·

  ·
  2

• TCB: cold branches (Code.iteCold), laid out after the function's return

  #2497·alex opened Oct 16, 2026Member·

  ·
  2

• AArch64 X25519: recombine the ladder's limbs into two carry-free accumulators

  #2496·alex opened Oct 16, 2026Member·Queued

• TCB: x86-64 alignment padding (Instr.align, printed as .p2align 4/5/6)

  #2487·alex opened Oct 16, 2026Member·

  ·
  1

• WIP: Move x86-64 FFDH generation control into verified assembly

  #2437·reaperhulk opened Oct 15, 2026Member·

  ·

• ChaCha20-Poly1305 x86-64: build the data tail's padded Poly1305 block in registers

  #2422·alex opened Oct 15, 2026Member·

  ·

• ARMv7 RSA: core and key operations

  #2200·reaperhulk opened Oct 14, 2026Member·

  ·

• rustls-provider: a rustls CryptoProvider backed by verified-garbage, and benchmarks against aws-lc-rs

  #991·alex opened Oct 5, 2026Member·

  ·
  5

• Experiment: verified "no secret residue" on return (x86-64)

  #801·reaperhulk opened Oct 4, 2026Member·

  ·
  1

• Prototype: speculative store bypass (Spectre v4) semantics and taint checker for x86-64

  #773·reaperhulk opened Oct 4, 2026Member·

  ·
  1

• Prototype: speculative constant time (Spectre v1/v1.1) for x86-64 taint proofs

  #769·reaperhulk opened Oct 4, 2026Member·

  ·
  3

• SHA-384/512/512-224/512-256 on PPC64LE: verified compress/init/update/finalize

  #117·alex opened Sep 28, 2026Member·

  ·
  2

• HMAC-SHA-256 on PPC64LE: verified init/finalize

  #111·alex opened Sep 28, 2026Member·

  ·
  5

• SHA-256 on PPC64LE: verified compress/init/update/finalize

  #110·alex opened Sep 28, 2026Member·

  ·
  3

• ChaCha20 on PPC64LE: verified block function, keystream XOR and streaming API

  #109·alex opened Sep 28, 2026Member·

  ·
  2

• TCB: 64-bit little-endian PowerPC (ISA model, printer, ELFv2 target)

  #108·alex opened Sep 28, 2026Member·

  ·
  1

• CI: test on ppc64le, on a ppc64le runner as pyca/cryptography does

  #97·alex opened Sep 28, 2026Member·

  ·
  5