All issues

Search results

Set Kernel Conversion Dep Heuristic in lightbulb

Status: Open.

#516 In mit-plv/bedrock2;

· JasonGross opened on Feb 27, 2026

investigate straightline slowdowns for resolving Loops.enforce

Status: Open.

#507 In mit-plv/bedrock2;

· miriampolzer opened on Jan 26, 2026

Build fails on master, blocking Coq bench

Status: Open.

#499 In mit-plv/bedrock2;

· JasonGross opened on Nov 3, 2025

FR: Sign-extending load1/load2/load4

Status: Open.

#496 In mit-plv/bedrock2;

· andres-erbsen opened on Oct 7, 2025

Improve program_logic_goal_for error messages

Status: Open.

#492 In mit-plv/bedrock2;

· miriampolzer opened on Sep 16, 2025

Preserve variable names in ProgramLogic proofs

Status: Open.

#478 In mit-plv/bedrock2;

· andres-erbsen opened on Jul 24, 2025

supporting $@ (map.of_list_word_at) for stackalloc/stackdealloc

Status: Open.

#477 In mit-plv/bedrock2;

· andres-erbsen opened on Jul 16, 2025

bytedump test seems to no longer work on Windows

Status: Open.

#454 In mit-plv/bedrock2;

· JasonGross opened on Apr 24, 2025

README should link relevant papers written on / on top of bedrock2

Status: Open.

#448 In mit-plv/bedrock2;

· JasonGross opened on Feb 18, 2025

build fails on 32-bit

Status: Open.

#434 In mit-plv/bedrock2;

· JasonGross opened on Oct 26, 2024

design: core functionality of RecordPredicates?

Status: Open.

#370 In mit-plv/bedrock2;

· andres-erbsen opened on Aug 25, 2023

design: outputting bitwidth-generic code?

Status: Open.

#368 In mit-plv/bedrock2;

· andres-erbsen opened on Aug 23, 2023