Skip to content

Update charon #368

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

Merged
Nadrieril merged 1 commit into from
Jan 13, 2026
Merged

Update charon #368

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions flake.lock
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

51 changes: 34 additions & 17 deletions out/test-libcrux-no-const/internal/libcrux_core.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,23 @@ extern "C" {

#include "../libcrux_core.h"

#define core_option_None 0
#define core_option_Some 1

typedef uint8_t core_option_Option_08_tags;

/**
A monomorphic instance of core.option.Option
with types size_t

*/
typedef struct core_option_Option_08_s
{
core_option_Option_08_tags tag;
size_t f0;
}
core_option_Option_08;

static inline uint64_t core_num__u64__from_le_bytes(Eurydice_array_u8x8 x0);

static inline uint64_t core_num__u64__rotate_left(uint64_t x0, uint32_t x1);
Expand Down Expand Up @@ -1786,23 +1803,6 @@ with const generics
*/
Eurydice_mut_borrow_slice_u8 Eurydice_array_to_slice_mut_7d(Eurydice_arr_a0 *a);

/**
A monomorphic instance of Eurydice.array_to_subslice_mut
with types uint8_t, core_ops_range_Range size_t, Eurydice_derefed_slice uint8_t
with const generics
- N= 72
*/
Eurydice_mut_borrow_slice_u8
Eurydice_array_to_subslice_mut_36(Eurydice_arr_a0 *a, core_ops_range_Range_08 r);

/**
A monomorphic instance of Eurydice.slice_subslice_mut
with types uint8_t, core_ops_range_Range size_t, Eurydice_derefed_slice uint8_t

*/
Eurydice_mut_borrow_slice_u8
Eurydice_slice_subslice_mut_7e(Eurydice_mut_borrow_slice_u8 s, core_ops_range_Range_08 r);

/**
A monomorphic instance of core.result.Result
with types Eurydice_array_u8x8, core_array_TryFromSliceError
Expand All @@ -1829,6 +1829,23 @@ with types Eurydice_arr uint8_t[[$8size_t]], core_array_TryFromSliceError
*/
Eurydice_array_u8x8 core_result_unwrap_26_ab(core_result_Result_8e self);

/**
A monomorphic instance of Eurydice.slice_subslice_mut
with types uint8_t, core_ops_range_Range size_t, Eurydice_derefed_slice uint8_t

*/
Eurydice_mut_borrow_slice_u8
Eurydice_slice_subslice_mut_7e(Eurydice_mut_borrow_slice_u8 s, core_ops_range_Range_08 r);

/**
A monomorphic instance of Eurydice.array_to_subslice_mut
with types uint8_t, core_ops_range_Range size_t, Eurydice_derefed_slice uint8_t
with const generics
- N= 72
*/
Eurydice_mut_borrow_slice_u8
Eurydice_array_to_subslice_mut_36(Eurydice_arr_a0 *a, core_ops_range_Range_08 r);

/**
A monomorphic instance of K.
with types Eurydice_arr_600, Eurydice_arr_74
Expand Down
58 changes: 29 additions & 29 deletions out/test-libcrux-no-const/libcrux_core.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2454,21 +2454,24 @@ Eurydice_mut_borrow_slice_u8 Eurydice_array_to_slice_mut_7d(Eurydice_arr_a0 *a)
}

/**
A monomorphic instance of Eurydice.array_to_subslice_mut
with types uint8_t, core_ops_range_Range size_t, Eurydice_derefed_slice uint8_t
with const generics
- N= 72
This function found in impl {core::result::Result<T, E>[TraitClause@0, TraitClause@1]}
*/
Eurydice_mut_borrow_slice_u8
Eurydice_array_to_subslice_mut_36(Eurydice_arr_a0 *a, core_ops_range_Range_08 r)
/**
A monomorphic instance of core.result.unwrap_26
with types Eurydice_arr uint8_t[[$8size_t]], core_array_TryFromSliceError

*/
Eurydice_array_u8x8 core_result_unwrap_26_ab(core_result_Result_8e self)
{
return
(
KRML_CLITERAL(Eurydice_mut_borrow_slice_u8){
.ptr = a->data + r.start,
.meta = r.end - r.start
}
);
if (self.tag == core_result_Ok)
{
return self.val.case_Ok;
}
else
{
KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "unwrap not Ok");
KRML_HOST_EXIT(255U);
}
}

/**
Expand All @@ -2486,23 +2489,20 @@ Eurydice_slice_subslice_mut_7e(Eurydice_mut_borrow_slice_u8 s, core_ops_range_Ra
}

/**
This function found in impl {core::result::Result<T, E>[TraitClause@0, TraitClause@1]}
*/
/**
A monomorphic instance of core.result.unwrap_26
with types Eurydice_arr uint8_t[[$8size_t]], core_array_TryFromSliceError

A monomorphic instance of Eurydice.array_to_subslice_mut
with types uint8_t, core_ops_range_Range size_t, Eurydice_derefed_slice uint8_t
with const generics
- N= 72
*/
Eurydice_array_u8x8 core_result_unwrap_26_ab(core_result_Result_8e self)
Eurydice_mut_borrow_slice_u8
Eurydice_array_to_subslice_mut_36(Eurydice_arr_a0 *a, core_ops_range_Range_08 r)
{
if (self.tag == core_result_Ok)
{
return self.val.case_Ok;
}
else
{
KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "unwrap not Ok");
KRML_HOST_EXIT(255U);
}
return
(
KRML_CLITERAL(Eurydice_mut_borrow_slice_u8){
.ptr = a->data + r.start,
.meta = r.end - r.start
}
);
}

Loading
Loading