Search results

Formulate specs of integer operations using mathematical integers

leanRelated to the Lean backend or libraryRelated to the Lean backend or library

libLib-related issue (e.g. annotations lib)Lib-related issue (e.g. annotations lib)

Status: Open.

#1830 In cryspen/hax;

· abentkamp opened on Dec 23, 2025

·  

Lean backend v1.0

[Lean] Lean backend renders functions with <code>hax_lib::opaque</code> as <code>Rust_primitives.Hax.dropped_body</code>

backendIssue in one of the backends (i.e. F*, Coq, EC...)Issue in one of the backends (i.e. F*, Coq, EC...)

leanRelated to the Lean backend or libraryRelated to the Lean backend or library

Status: Open.

#1825 In cryspen/hax;

· abentkamp opened on Dec 17, 2025

[Lean] <code>hax_lib::fstar::replace</code> causes Lean backend to drop the item entirely

backendIssue in one of the backends (i.e. F*, Coq, EC...)Issue in one of the backends (i.e. F*, Coq, EC...)

bugSomething isn't workingSomething isn't working

leanRelated to the Lean backend or libraryRelated to the Lean backend or library

Status: Open.

#1824 In cryspen/hax;

· abentkamp opened on Dec 17, 2025

[Lean] Items in recursive modules do not get ordered correctly

backendIssue in one of the backends (i.e. F*, Coq, EC...)Issue in one of the backends (i.e. F*, Coq, EC...)

bugSomething isn't workingSomething isn't working

leanRelated to the Lean backend or libraryRelated to the Lean backend or library

Status: Open.

#1823 In cryspen/hax;

· abentkamp opened on Dec 17, 2025

Create a CLI command that copies generated Lean code back into Rust file or a separate file

backendIssue in one of the backends (i.e. F*, Coq, EC...)Issue in one of the backends (i.e. F*, Coq, EC...)

leanRelated to the Lean backend or libraryRelated to the Lean backend or library

Status: Open.

#1820 In cryspen/hax;

· abentkamp opened on Dec 16, 2025

·  

Lean backend v1.0

[Lean] Default proof should report a warning and be treated like <code>sorry</code> when it fails

backendIssue in one of the backends (i.e. F*, Coq, EC...)Issue in one of the backends (i.e. F*, Coq, EC...)

leanRelated to the Lean backend or libraryRelated to the Lean backend or library

P1Max priorityMax priority

Status: Open.

#1819 In cryspen/hax;

· abentkamp opened on Dec 16, 2025

·  

Lean backend v1.0

[Lean] Ensure that generated spec lemmas are communicated to mvcgen

backendIssue in one of the backends (i.e. F*, Coq, EC...)Issue in one of the backends (i.e. F*, Coq, EC...)

leanRelated to the Lean backend or libraryRelated to the Lean backend or library

P1Max priorityMax priority

Status: Open.

#1818 In cryspen/hax;

· abentkamp opened on Dec 16, 2025

·  

Lean backend v1.0

[Lean] Generate specs for functions without annotations

backendIssue in one of the backends (i.e. F*, Coq, EC...)Issue in one of the backends (i.e. F*, Coq, EC...)

leanRelated to the Lean backend or libraryRelated to the Lean backend or library

P1Max priorityMax priority

Status: Open.

#1817 In cryspen/hax;

· abentkamp opened on Dec 16, 2025

·  

Lean backend v1.0

[Lean] Disable spec-trait phase for Lean and remove pre/postcondition checks

backendIssue in one of the backends (i.e. F*, Coq, EC...)Issue in one of the backends (i.e. F*, Coq, EC...)

leanRelated to the Lean backend or libraryRelated to the Lean backend or library

Status: Open.

#1812 In cryspen/hax;

· abentkamp opened on Dec 15, 2025

Create a phase to remove items marked with <code>late_skip</code>

rust-engine

Status: Open.

#1811 In cryspen/hax;

· abentkamp opened on Dec 15, 2025

[F*] struct containing projected associated type doesn't support decidable equality

backendIssue in one of the backends (i.e. F*, Coq, EC...)Issue in one of the backends (i.e. F*, Coq, EC...)

f*F* backendF* backend

Status: Open.

Bug

#1810 In cryspen/hax;

· maximebuyse opened on Dec 12, 2025

Possible name clash between concrete parameters and trait impls (<code>i0</code>, <code>i1</code>, ..)

backendIssue in one of the backends (i.e. F*, Coq, EC...)Issue in one of the backends (i.e. F*, Coq, EC...)

f*F* backendF* backend

Status: Open.

Bug

#1809 In cryspen/hax;

· maximebuyse opened on Dec 12, 2025