Repository navigation

All pull requests

Fix x86 AT&T assembly for Windows COFF targets
#497pps83 opened Nov 11, 2026
RV: Extend RV32-IM support to full architecture
#493hanno-becker opened Nov 6, 2026Collaborator
[DRAFT] Prove equivalence between Sail and s2n-bignum instruction models
#492hanno-becker opened Nov 6, 2026Collaborator
Tidy all the AES-GCM proofs
#490jargh opened Nov 5, 2026Contributor
[WIP] Improve performance of symbolic execution to support larger unrolled workloads
#481hanno-becker opened Oct 19, 2026Collaborator
Clean up NTT proofs
#480jargh opened Oct 17, 2026Contributor
Add safety proofs for all remaining functions
#478jargh opened Oct 16, 2026Contributor
Modulus / remainder operation
#477jargh opened Oct 15, 2026Contributor
Arm: Add DUP (element), scalar form
#476BenKnill opened Oct 14, 2026Contributor
CI: cosimulate x86 under Intel SDE instead of QEMU for AVX-512 support
#474awl-compsci opened Oct 8, 2026Contributor
Prove BIGNUM_EMONTREDC_8N_CDIFF_SUBROUTINE_SAFE
#471BenKnill opened Oct 5, 2026Contributor
Widen cosimulation to 512-bit and migrate all vector proofs to the ZMM operand view
#468awl-compsci opened Sep 28, 2026Contributor
[WIP -- Alternative] Speed up cosimulation by removing unnecessary reliance on large frame idempotence- #460
#464hanno-becker opened Sep 23, 2026Collaborator
x86: AVX-512 Foundation + Decoder
#462awl-compsci opened Sep 22, 2026Contributor
36
Speed up cosimulation by removing unnecessary reliance on large frame idempotence
#460hanno-becker opened Sep 20, 2026Collaborator
AES-XTS encrypt: prove the len<0x20 memory-safety lemma
#451sgmenda opened Sep 8, 2026Contributor
13
x86_64 sha256 block compression implementation with sha-specific instructions + functional proof + safety proof + Windows
#450torben-hansen opened Sep 8, 2026Contributor
ARM: gcm_ghash_v8 correctness proof for all lengths
#448nebeid opened Aug 26, 2026Contributor
Align x86 timing events with DOIT policy
#444namtran1812 opened Aug 19, 2026
13
Arm: Add sub-word loads and extended register offsets
#441ckocaogullar opened Aug 17, 2026Contributor
x86: Add SIMD instruction models for PCLMULQDQ/PSLLDQ/PSRLDQ, VPSHUFD/LEAVE, VPCMPEQW
#439jakemas opened Aug 9, 2026Contributor
Arm: Model SIMD LD1/ST1, LD2/ST2, LDR/STR, and LDUR/STUR forms
#437ckocaogullar opened Jul 30, 2026Contributor
3
x86_64 sha512 block compression implementation without SIMD and without sha-specific instructions + functional proof + safety proof + Windows
#420torben-hansen opened Jul 1, 2026Contributor
x86 Keccak safety proofs
#418manastasova opened Jun 30, 2026Contributor
10
x86_64 sha256 block compression implementation without SIMD and without sha-specific instructions + functional proof + safety proof + Windows
#415torben-hansen opened Jun 23, 2026Contributor

Pull requests