Search results

[Frontend] FullDef extraction failure: error[E9999]: maximum number of nodes exceeded in constant ...

frontendIssue in the Rust to JSON translationIssue in the Rust to JSON translation

Status: Open.

#2045 In cryspen/hax;

· maximebuyse opened on Jun 11, 2026

[Frontend] extraction failure with error[E0277]: the trait bound .. is not satisfied

frontendIssue in the Rust to JSON translationIssue in the Rust to JSON translation

Status: Open.

#2044 In cryspen/hax;

· maximebuyse opened on Jun 11, 2026

[Frontend] panic with assertion failed: generics.is_empty()

frontendIssue in the Rust to JSON translationIssue in the Rust to JSON translation

Status: Open.

#2043 In cryspen/hax;

· maximebuyse opened on Jun 11, 2026

[Frontend] maximum number of nodes exceeded in constant table with --experimental-full-def

frontendIssue in the Rust to JSON translationIssue in the Rust to JSON translation

Status: Open.

#2040 In cryspen/hax;

· maximebuyse opened on Jun 10, 2026

[Lean] Unknown identifier rust_primitives.hax.monomorphized_update_at.update_at_range

Status: Open.

#2036 In cryspen/hax;

· franziskuskiefer opened on Jun 9, 2026

[F*] Lean backend annotations break F* extraction

bugSomething isn't workingSomething isn't working

workaroundThis bug has a workaroundThis bug has a workaround

Status: Open.

Bug

#2026 In cryspen/hax;

· jschneider-bensch opened on May 4, 2026

Refinement types depend on std

Status: Open.

#2021 In cryspen/hax;

· fmbearmf opened on Apr 29, 2026

[Unsupported Rust] Let chains

unsupported-rustRust code rejected by hax. Unless marked wontfix, we want to support it soon.Rust code rejected by hax. Unless marked wontfix, we want to support it soon.

Status: Open.

#2018 In cryspen/hax;

· maximebuyse opened on Apr 23, 2026

[Lean] Ill-typed Lean output when unnecessarily passing a mutable reference

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.

#1984 In cryspen/hax;

· abentkamp opened on Mar 10, 2026

[Lean] Passing arrays as slices

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.

#1983 In cryspen/hax;

· abentkamp opened on Mar 10, 2026

rust_primitives.unsize omitted when argument is &mut

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.

#1977 In cryspen/hax;

· abentkamp opened on Mar 5, 2026

hax 0.3.6 crashes on RPITIT

engineIssue in the engineIssue in the engine

Status: Open.

Bug

#1965 In cryspen/hax;

· cfm opened on Feb 24, 2026