Skip to content

Issues: cryspen/hax

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

191 Open 449 Closed
191 Open 449 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
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Error with hax_lib::fstar::before on impl method lib Lib-related issue (e.g. annotations lib)
#1315 opened Feb 18, 2025 by maximebuyse
[ProVerif] Translate generic types
#1314 opened Feb 17, 2025 by jschneider-bensch
Support impl Trait in attribute name interpolation attributes workaround This bug has a workaround
#1313 opened Feb 17, 2025 by jschneider-bensch
2
Support thread locals bug Something isn't working
#1311 opened Feb 14, 2025 by Nadrieril
Trait resolution crash on coinductive goal frontend Issue in the Rust to JSON translation
#1310 opened Feb 13, 2025 by Nadrieril
1
F* backend extremely slow at one example backend Issue in one of the backends (i.e. F*, Coq, EC...) bug Something isn't working f* F* backend
#1308 opened Feb 12, 2025 by W95Psp
Cyclic dependency between trait definitions doesn't work well with F* workaround This bug has a workaround
#1297 opened Feb 6, 2025 by maximebuyse
Generic Printer: ~constructor argument to expr'_Construct_inductive is wrong for structs engine Issue in the engine
#1295 opened Feb 6, 2025 by keks
Struct constructor is difficult to use in generic printer engine Issue in the engine
#1294 opened Feb 6, 2025 by keks
Overloading arithmetic operators by implementing the corresponding traits results in incorrect F* engine Issue in the engine
#1290 opened Feb 4, 2025 by maximebuyse
1
Engine: generate doc for visitors engine Issue in the engine enhancement New feature or request
#1287 opened Feb 4, 2025 by W95Psp
Traits cannot be imported by their original module when they are part of a bundle f* F* backend
#1285 opened Feb 3, 2025 by maximebuyse
1
Improve ml-kem CI job to use the right revision for hax-lib ci
#1279 opened Jan 30, 2025 by maximebuyse
Need to refer to $self_ instead of $self in ensures lib Lib-related issue (e.g. annotations lib)
#1276 opened Jan 29, 2025 by maximebuyse
2
Missing F* implicit argument with multiple impl args engine Issue in the engine f* F* backend
#1272 opened Jan 28, 2025 by maximebuyse
F*: Remove hacl dependency f* F* backend
#1271 opened Jan 27, 2025 by W95Psp
Requires and ensures: allow multiple per function attributes backend Issue in one of the backends (i.e. F*, Coq, EC...)
#1270 opened Jan 23, 2025 by W95Psp
fstar! macro specialized for booleans attributes f* F* backend
#1269 opened Jan 23, 2025 by W95Psp
Macros: preconditions that generates an debug_assert! attributes
#1268 opened Jan 23, 2025 by W95Psp
Don't run code CI on docs ci
#1262 opened Jan 21, 2025 by franziskuskiefer
F*: bit vector library: restore implementations f* F* backend lib Lib-related issue (e.g. annotations lib)
#1242 opened Jan 20, 2025 by W95Psp
Add error message for static items
#1240 opened Jan 17, 2025 by franziskuskiefer
[Investigate] Extraction of core::convert::From
#1234 opened Jan 16, 2025 by franziskuskiefer
@W95Psp
Allow decreases classes to prove termination attributes
#1233 opened Jan 15, 2025 by karthikbhargavan
2
Loop with side effect at the end of a function gives inconsistent type
#1231 opened Jan 14, 2025 by maximebuyse
1
@maximebuyse
3
ProTip! no:milestone will show everything without a milestone.