All pull requests

Pull requests

• zlia: unzify preprocessing as a word-goal solver, used at most ZnWords call sites

  #587·JasonGross opened Sep 24, 2026Contributor·

  ·
  7

• Leakage specification for recvEthernet

  #586·JasonGross opened Sep 22, 2026Contributor·

  ·

• Leakage-aware specifications for the LAN9250 driver

  #585·JasonGross opened Sep 22, 2026Contributor·

  ·

• ZnWords: one list-aware closing tactic; ZnWordsL and listZnWords become aliases

  #584·JasonGross opened Sep 22, 2026Contributor·

  ·

• Leakage-aware specifications for spi_write, spi_read, spi_xchg

  #583·JasonGross opened Sep 22, 2026Contributor·

  ·

• Lift leakage specs to plain specs (plain_of_leakage, straightline_call_from_leakage)

  #582·JasonGross opened Sep 22, 2026Contributor·

  ·

• Leakage-aware specification for memmove

  #581·JasonGross opened Sep 22, 2026Contributor·

  ·

• Give memconst a leakage-aware specification

  #580·JasonGross opened Sep 22, 2026Contributor·

  ·

• memswap: leakage-aware specification and proof

  #579·JasonGross opened Sep 22, 2026Contributor·

  ·

• Bump deps/coqutil from 4c399b7 to e4d02d7

  submodules
  #578·dependabot[bot] opened Sep 22, 2026Bot·

  ·

• Keep stack frames as maps at the bedrock2 use sites (on top of #573)

  #576·JasonGross opened Sep 19, 2026Contributor·

  ·
  3

• Program logic: keep stack frames as maps on request (#477)

  #573·JasonGross opened Sep 18, 2026Contributor·

  ·
  4

• Simulate the processor regenerated from Kami's Bluespec output

  #564·JasonGross opened Sep 15, 2026Contributor·

  ·

• processor: the Kami word instance is coqutil's Naive.word (stacked on #562)

  #563·JasonGross opened Sep 12, 2026Contributor·

  ·
  2

• processor: Kami words on stdlib bits; thin KamiWord bridge (stacked on #561)

  #562·JasonGross opened Sep 12, 2026Contributor·

  ·
  1

• ToCString: emit stackalloc as 64-byte-aligned uint64_t array

  #532·spitters opened May 17, 2026·3 tasks done·

  ·

• straightline_cleanup: limit cbn [interp_binop] to goal only

  #531·spitters opened May 17, 2026·2 tasks done·

  ·

• Experiment with nonterminating programs

  #481·OwenConoly opened Aug 24, 2025Contributor·

  ·
  1

• [do not merge] Metriclightbulb

  #435·samuelgruetter opened Nov 13, 2024Contributor·

  ·
  1

• [do not merge] profiling for lia in bsearch.v

  #98·samuelgruetter opened Sep 19, 2019Contributor·

  ·
  1

• Kami2 SPI device verification

  #93·andres-erbsen-sifive opened Aug 22, 2019Contributor·

  ·

• prove memory safety for chacha20 implementation

  #72·andres-erbsen opened Apr 29, 2019Contributor·

  ·
  3

• Proposal: Globals (pre-cursor to Compilation Units)

  #30·gmalecha opened Sep 10, 2018Contributor·

  ·
  14