Skip to content

Pull requests: mit-plv/fiat-crypto

New pull request New
75 Open 1,872 Closed
75 Open 1,872 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Reviews
Filter by reviews
No reviews Review required Approved review Changes requested
Assignee
Filter by who’s assigned
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

Verify shrtz
#2424 opened Sep 4, 2026 by klinashka Contributor Loading…
chore: Update generated files for #2399
#2423 opened Sep 2, 2026 by github-actions Bot Loading…
Print Z_bneg as logical negation in Rust and Zig
#2422 opened Sep 2, 2026 by JasonGross Collaborator • Draft
Quote tabs and newlines in generated invocations
#2421 opened Sep 2, 2026 by JasonGross Collaborator Loading…
Correct generated msat postconditions
#2420 opened Sep 2, 2026 by JasonGross Collaborator • Draft
Pin wasm-feature-detect with SRI
#2419 opened Sep 2, 2026 by JasonGross Collaborator • Draft
Reject unsupported RIP-relative assembly addresses
#2418 opened Sep 2, 2026 by JasonGross Collaborator • Draft
Fix divstep_precomp postcondition
#2417 opened Sep 2, 2026 by JasonGross Collaborator • Draft
Model one-operand imul as a signed multiply in the assembly checker (scrutineer #2514)
#2415 opened Sep 2, 2026 by JasonGross Collaborator • Draft
Check assembly equivalence under output/input array aliasing (scrutineer #2521)
#2414 opened Sep 2, 2026 by JasonGross Collaborator • Draft
Fix and prove the Bernstein-Yang word-by-word Montgomery specs (scrutineer #2522, #2523, #2524)
#2413 opened Sep 2, 2026 by JasonGross Collaborator • Draft
Reject data-emitting lines and non-inert directives in checked assembly (scrutineer #2512)
#2412 opened Sep 2, 2026 by JasonGross Collaborator • Draft
Print Z_bneg as logical negation in Rust and Zig (scrutineer #2525)
#2411 opened Sep 2, 2026 by JasonGross Collaborator • Draft
Bound the assembly stack size and fix its bytes/words confusion (scrutineer #2517)
#2410 opened Sep 2, 2026 by JasonGross Collaborator Loading…
Reject RIP-relative memory operands in the assembly equivalence checker (scrutineer #2516)
#2409 opened Sep 2, 2026 by JasonGross Collaborator • Draft
Make OCaml<->Coq string conversion in the extraction drivers linear-time and stack-safe
#2408 opened Sep 2, 2026 by JasonGross Collaborator Loading…
Quote argv for the Autogenerated header with an allow-list (scrutineer #2511)
#2407 opened Sep 2, 2026 by JasonGross Collaborator • Draft
fiat-html: make the argv string encoding a faithful round trip (scrutineer #2519)
#2406 opened Sep 2, 2026 by JasonGross Collaborator • Draft
Guard bedrock2 C output against mismatched target word width
#2405 opened Sep 2, 2026 by JasonGross Collaborator • Draft
Vendor wasm-feature-detect instead of loading it unpinned from unpkg (scrutineer #2520)
#2404 opened Sep 2, 2026 by JasonGross Collaborator • Draft
Guard generated C against non-arithmetic signed right shift (scrutineer #2526)
#2403 opened Sep 2, 2026 by JasonGross Collaborator • Draft
Fix divstep postconditions in generated APIs
#2402 opened Sep 1, 2026 by JasonGross Collaborator • Draft
Make AMD64 field operations safe for in-place use
#2401 opened Sep 1, 2026 by JasonGross Collaborator • Draft
1
Fix signed semantics for one-operand IMUL
#2400 opened Sep 1, 2026 by JasonGross Collaborator • Draft
Reject Bedrock2 C outputs built for the wrong word size
#2399 opened Sep 1, 2026 by JasonGross Collaborator • Draft
1
ProTip! no:milestone will show everything without a milestone.