diff --git a/Makefile b/Makefile index e68bf86..7969eff 100644 --- a/Makefile +++ b/Makefile @@ -3,7 +3,7 @@ KRML_HOME ?= $(dir $(abspath $(lastword $(MAKEFILE_LIST))))/../karamel EURYDICE ?= ./eurydice $(EURYDICE_FLAGS) CHARON ?= $(CHARON_HOME)/bin/charon -BROKEN_TESTS = step_by where_clauses chunks mutable_slice_range closure +BROKEN_TESTS = step_by where_clauses chunks mutable_slice_range closure issue_49 TEST_DIRS = $(filter-out $(BROKEN_TESTS),$(subst test/,,$(shell find test -maxdepth 1 -mindepth 1 -type d))) .PHONY: all diff --git a/bin/main.ml b/bin/main.ml index ab5dd6e..3f0f9b1 100644 --- a/bin/main.ml +++ b/bin/main.ml @@ -198,6 +198,7 @@ Supported options:|} fail __FILE__ __LINE__; Eurydice.Logging.log "Phase2.1" "%a" pfiles files; let files = Eurydice.Cleanup2.improve_names files in + let files = Eurydice.Cleanup2.recognize_asserts#visit_files () files in let files = Krml.Monomorphization.functions files in let files = Krml.Monomorphization.datatypes files in let files = @@ -329,6 +330,9 @@ Supported options:|} in Eurydice.Logging.log "Phase3.3" "%a" pfiles files; + let files = List.map (fun (f, ds) -> f, List.filter (fun d -> + not (Krml.Idents.LidSet.mem (Krml.Ast.lid_of_decl d) Eurydice.Builtin.skip)) + ds) files in let files = AstToCStar.mk_files files c_name_map Idents.LidSet.empty macros in let headers = CStarToC11.mk_headers c_name_map files in diff --git a/flake.lock b/flake.lock index 5d5d834..8a3800d 100644 --- a/flake.lock +++ b/flake.lock @@ -11,11 +11,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1724838996, - "narHash": "sha256-N8eoK78blhH2HRGenQbTrTxwc9W1JcSe3agcl2yj1AA=", + "lastModified": 1725287105, + "narHash": "sha256-KUxQtYXe3/BL9XwGfiTS3tjDe0nEEF9Npp5BOHCe8ig=", "owner": "aeneasverif", "repo": "charon", - "rev": "597fe150c3952fd197e37bc7b5ae2cb2f0d07c81", + "rev": "cdc1dcde447a50cbc20336c79b21b42ac977b7fd", "type": "github" }, "original": { @@ -136,11 +136,11 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1723651234, - "narHash": "sha256-u5zHiSygZhMqoc1Z5R2bP9nRwJx3JWq5xyOlcm765wE=", + "lastModified": 1724957201, + "narHash": "sha256-q8XaJiiErxDXFWhsOVN//WFSXPFmR3W8LvRL4Sov68c=", "owner": "FStarLang", "repo": "fstar", - "rev": "608c8c2cb41cc59f5a4d07fb70677c68aae8fa8a", + "rev": "d93417723d03781d0d3b4969eb7f0d6b9671ef6d", "type": "github" }, "original": { @@ -155,11 +155,11 @@ "nixpkgs": "nixpkgs_2" }, "locked": { - "lastModified": 1723651234, - "narHash": "sha256-u5zHiSygZhMqoc1Z5R2bP9nRwJx3JWq5xyOlcm765wE=", + "lastModified": 1724957201, + "narHash": "sha256-q8XaJiiErxDXFWhsOVN//WFSXPFmR3W8LvRL4Sov68c=", "owner": "fstarlang", "repo": "fstar", - "rev": "608c8c2cb41cc59f5a4d07fb70677c68aae8fa8a", + "rev": "d93417723d03781d0d3b4969eb7f0d6b9671ef6d", "type": "github" }, "original": { @@ -183,11 +183,11 @@ ] }, "locked": { - "lastModified": 1723656573, - "narHash": "sha256-sbNNlkqgBHJZwKLHbRKTKQf4tO/DhOAlC3KTzQrh92Y=", + "lastModified": 1724965512, + "narHash": "sha256-4QrNXTaIS3BxIB5XwkjC2SoOBfkqWZ66UkKPhasHIto=", "owner": "FStarLang", "repo": "karamel", - "rev": "7862fdc3899b718d39ec98568f78ec40592a622a", + "rev": "fa19d3771e6745dac67e834cd077438905ce7720", "type": "github" }, "original": { @@ -246,11 +246,11 @@ ] }, "locked": { - "lastModified": 1724811750, - "narHash": "sha256-PvhVgQ1rm3gfhK7ts4emprhh/KMkFwXogmgsQ3srR7g=", + "lastModified": 1725243956, + "narHash": "sha256-0A5ZP8uDCyBdYUzayZfy6JFdTefP79oZVAjyqA/yuSI=", "owner": "oxalica", "repo": "rust-overlay", - "rev": "6a1c4915dca7149e7258d8c7f3ac634d8c65f6c6", + "rev": "a10c8092d5f82622be79ed4dd12289f72011f850", "type": "github" }, "original": { diff --git a/include/eurydice_glue.h b/include/eurydice_glue.h index d9b08f6..f1de905 100644 --- a/include/eurydice_glue.h +++ b/include/eurydice_glue.h @@ -18,6 +18,13 @@ extern "C" { #include "krml/lowstar_endianness.h" #define LowStar_Ignore_ignore(e, t, _ret_t) ((void)e) +#define EURYDICE_ASSERT(test, msg) do { \ + if (!(test)) { \ + fprintf(stderr, \ + "assertion \"%s\" failed: file \"%s\", line %d\n", \ + msg, __FILE__, __LINE__); \ + } \ +} while (0) // SLICES, ARRAYS, ETC. @@ -130,6 +137,10 @@ static inline void core_num__u32_8__to_be_bytes(uint32_t src, uint8_t dst[4]) { memcpy(dst, &x, 4); } +static inline void core_num__u32_8__to_le_bytes(uint32_t src, uint8_t dst[4]) { + store32_le(dst, src); +} + static inline uint32_t core_num__u32_8__from_le_bytes(uint8_t buf[4]) { return load32_le(buf); } @@ -137,6 +148,7 @@ static inline uint32_t core_num__u32_8__from_le_bytes(uint8_t buf[4]) { static inline void core_num__u64_9__to_le_bytes(uint64_t v, uint8_t buf[8]) { store64_le(buf, v); } + static inline uint64_t core_num__u64_9__from_le_bytes(uint8_t buf[8]) { return load64_le(buf); } @@ -202,6 +214,9 @@ static inline uint8_t Eurydice_bitand_pv_u8(uint8_t *p, uint8_t v) { static inline uint8_t Eurydice_shr_pv_u8(uint8_t *p, int32_t v) { return (*p) >> v; } +static inline uint32_t Eurydice_min_u32(uint32_t x, uint32_t y) { + return x < y ? x : y; +} #define core_num_nonzero_private_NonZeroUsizeInner size_t static inline core_num_nonzero_private_NonZeroUsizeInner diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml index 9f99225..d8cf4f2 100644 --- a/lib/AstOfLlbc.ml +++ b/lib/AstOfLlbc.ml @@ -25,6 +25,10 @@ module K = Krml.Ast module L = Logging open Krml.PrintAst.Ops +let fail fmt = + let b = Buffer.create 256 in + Printf.kbprintf (fun b -> failwith (Buffer.contents b)) b fmt + (** Environment *) (* The various kinds of binders we insert in the expression scope. Usually come @@ -130,7 +134,7 @@ let with_any = K.(with_type TAny) let assert_slice (t : K.typ) = match t with | TApp (lid, [ t ]) when lid = Builtin.slice -> t - | _ -> Krml.Warn.fatal_error "Not a slice: %a" ptyp t + | _ -> fail "Not a slice: %a" ptyp t let string_of_path_elem (env : env) (p : Charon.Types.path_elem) : string = match p with @@ -208,6 +212,9 @@ module RustNames = struct (* bitwise & arithmetic operations *) parse_pattern "core::ops::bit::BitAnd<&'_ u8, u8>::bitand", Builtin.bitand_pv_u8; parse_pattern "core::ops::bit::Shr<&'_ u8, i32>::shr", Builtin.shr_pv_u8; + + (* misc *) + parse_pattern "core::cmp::Ord::min", Builtin.min_u32; ] [@ocamlformat "disable"] @@ -356,7 +363,7 @@ let rec typ_of_ty (env : env) (ty : Charon.Types.ty) : K.typ = failwith "Impossible -- strings always behind a pointer" | TAdt (TAssumed f, { types = args; const_generics; _ }) -> List.iter (fun x -> print_endline (C.show_const_generic x)) const_generics; - Krml.Warn.fatal_error "TODO: Adt/Assumed %s (%d) %d " (C.show_assumed_ty f) (List.length args) + fail "TODO: Adt/Assumed %s (%d) %d " (C.show_assumed_ty f) (List.length args) (List.length const_generics) | TRawPtr (t, _) -> (* Appears in some trait methods, so let's try to handle that. *) @@ -638,14 +645,14 @@ let op_of_binop (op : C.binop) : Krml.Constant.op = | C.Mul -> Mult | C.Shl -> BShiftL | C.Shr -> BShiftR - | _ -> Krml.Warn.fatal_error "unsupported operator: %s" (C.show_binop op) + | _ -> fail "unsupported operator: %s" (C.show_binop op) let mk_op_app (op : K.op) (first : K.expr) (rest : K.expr list) : K.expr = let w = match first.typ with | K.TInt w -> w | K.TBool -> Bool - | t -> Krml.Warn.fatal_error "Not an operator type: %a" ptyp t + | t -> fail "Not an operator type: %a" ptyp t in let op = if op = Not && first.typ <> K.TBool then @@ -686,6 +693,10 @@ let blocklisted_trait_decls = (* Handled primitively. *) "core::ops::function::FnMut"; "core::cmp::PartialEq"; + (* These don't have methods *) + "core::marker::Sized"; + "core::marker::Send"; + "core::marker::Sync"; (* The traits below *should* be handled properly ASAP. But for now, we have specific *instances* of those trait methods in the builtin lookup table, which we then implement by hand with macros. *) @@ -865,6 +876,8 @@ and mk_clause_binders_and_args env clause_mapping : clause_binder list = K.n_cgs = List.length signature.generics.const_generics - trait_ts.n_cgs; } in + (* TODO: figure out why this fails for e.g. Iterator.rev *) + assert (ts.n_cgs >= 0 && ts.n >= 0); { pretty_name; t; clause_id; item_name; ts }) clause_mapping @@ -920,13 +933,18 @@ let lookup_fun (env : env) depth (f : C.fn_ptr) : K.expr' * lookup_result = match f.func with | FunId (FRegular f) -> lookup_result_of_fun_id f - | FunId (FAssumed f) -> - Krml.Warn.fatal_error "unknown assumed function: %s" (C.show_assumed_fun_id f) + | FunId (FAssumed f) -> fail "unknown assumed function: %s" (C.show_assumed_fun_id f) | TraitMethod (trait_ref, method_name, _trait_opaque_signature) -> ( match trait_ref.trait_id with | TraitImpl (id, _) -> let trait = env.get_nth_trait_impl id in - let f = List.assoc method_name (trait.required_methods @ trait.provided_methods) in + let f = + try List.assoc method_name (trait.required_methods @ trait.provided_methods) + with Not_found -> + fail "Error looking trait impl: %s %s%!" + (Charon.PrintTypes.trait_ref_to_string env.format_env trait_ref) + method_name + in lookup_result_of_fun_id f | (Clause _ | ParentClause _) as tcid -> let f, t, sig_info = lookup_clause_binder env tcid method_name in @@ -940,7 +958,7 @@ let lookup_fun (env : env) depth (f : C.fn_ptr) : K.expr' * lookup_result = let cg_types, arg_types = Krml.KList.split sig_info.n_cgs arg_types in EBound f, { ts = sig_info; cg_types; arg_types; ret_type; is_known_builtin = false } | _ -> - Krml.Warn.fatal_error "Error looking trait ref: %s %s" + fail "Error looking trait ref: %s %s%!" (Charon.PrintTypes.trait_ref_to_string env.format_env trait_ref) method_name)) @@ -1163,7 +1181,7 @@ let expression_of_operand (env : env) (p : C.operand) : K.expr = let e, _, _ = expression_of_fn_ptr env fn_ptr in e | Constant _ -> - Krml.Warn.fatal_error "expression_of_operand Constant: %s" + fail "expression_of_operand Constant: %s" (Charon.PrintExpressions.operand_to_string env.format_env p) let is_str env var_id = @@ -1279,7 +1297,7 @@ let lesser t1 t2 = else if t2 = K.TAny then t2 else if t1 <> t2 then - Krml.Warn.fatal_error "lesser t1=%a t2=%a" ptyp t1 ptyp t2 + fail "lesser t1=%a t2=%a" ptyp t1 ptyp t2 else t1 @@ -1346,7 +1364,7 @@ let rec expression_of_raw_statement (env : env) (ret_var : C.var_id) (s : C.raw_ func = FnOpRegular { - func = FunId (FAssumed (ArrayIndexShared | ArrayIndexMut)); + func = FunId (FAssumed (Index { is_array = true; mutability = _; is_range = false })); generics = { types = [ ty ]; _ }; _; }; @@ -1393,7 +1411,7 @@ let rec expression_of_raw_statement (env : env) (ret_var : C.var_id) (s : C.raw_ else if matches RustNames.from_i64 || matches RustNames.into_i64 then Int64 else - Krml.Warn.fatal_error "Unknown from-cast: %s" (string_of_fn_ptr env fn_ptr) + fail "Unknown from-cast: %s" (string_of_fn_ptr env fn_ptr) in let dest, _ = expression_of_place env dest in let e = expression_of_operand env (Krml.KList.one args) in @@ -1429,15 +1447,16 @@ let rec expression_of_raw_statement (env : env) (ret_var : C.var_id) (s : C.raw_ | _ -> [] in match fn_ptr.func, fn_ptr.generics.types @ extra_types with - | ( FunId (FAssumed (SliceIndexShared | SliceIndexMut)), + | ( FunId (FAssumed (Index { is_array = false; mutability = _; is_range = false })), [ TAdt (TAssumed (TArray | TSlice), _) ] ) -> (* Will decay. See comment above maybe_addrof *) rhs - | FunId (FAssumed (SliceIndexShared | SliceIndexMut)), [ TAdt (id, generics) ] + | ( FunId (FAssumed (Index { is_array = false; mutability = _; is_range = false })), + [ TAdt (id, generics) ] ) when RustNames.is_vec env id generics -> (* Will decay. See comment above maybe_addrof *) rhs - | FunId (FAssumed (SliceIndexShared | SliceIndexMut)), _ -> + | FunId (FAssumed (Index { is_array = false; mutability = _; is_range = false })), _ -> K.(with_type (TBuf (rhs.typ, false)) (EAddrOf rhs)) | _ -> rhs in @@ -1558,7 +1577,7 @@ let flags_of_meta (meta : C.item_meta) : K.flags = let decl_of_id (env : env) (id : C.any_decl_id) : K.decl option = match id with - | IdType id -> ( + | IdType id -> begin let decl = env.get_nth_type id in let { C.item_meta; def_id; kind; generics = { types = type_params; const_generics; _ }; _ } = decl @@ -1573,7 +1592,7 @@ let decl_of_id (env : env) (id : C.any_decl_id) : K.decl option = let env = push_type_binders env type_params in match kind with - | Opaque | Error _ -> None + | Union _ | Opaque | Error _ -> None | Struct fields -> let fields = List.map @@ -1603,7 +1622,8 @@ let decl_of_id (env : env) (id : C.any_decl_id) : K.decl option = [], List.length const_generics, List.length type_params, - Abbrev (typ_of_ty env ty) ))) + Abbrev (typ_of_ty env ty) )) + end | IdFun id -> ( let decl = try Some (env.get_nth_function id) with Not_found -> None in match decl with @@ -1626,17 +1646,10 @@ let decl_of_id (env : env) (id : C.any_decl_id) : K.decl option = (* We skip those on the basis that they generate useless external prototypes, which we do not really need. *) None - | None, _ -> begin - try - (* Opaque function *) - let { K.n_cgs; n }, t = typ_of_signature env signature in - Some (K.DExternal (None, [], n_cgs, n, name, t, [])) - with e -> - L.log "AstOfLlbc" "ERROR translating %s: %s\n%s" - (string_of_name env decl.item_meta.name) - (Printexc.to_string e) (Printexc.get_backtrace ()); - None - end + | None, _ -> + (* Opaque function *) + let { K.n_cgs; n }, t = typ_of_signature env signature in + Some (K.DExternal (None, [], n_cgs, n, name, t, [])) | Some { arg_count; locals; body; _ }, _ -> if is_global_decl_body then None @@ -1715,11 +1728,19 @@ let decl_of_id (env : env) (id : C.any_decl_id) : K.decl option = Krml.Helpers.fresh_binder ~mut:true name (typ_of_ty env arg.var_ty)) args in + L.log "AstOfLlbc" "type of binders: %a" ptyps (List.map (fun o -> o.K.typ) arg_binders); let body = - with_locals env return_type (return_var :: locals) (fun env -> - expression_of_raw_statement env return_var.index body.content) + try + with_locals env return_type (return_var :: locals) (fun env -> + expression_of_raw_statement env return_var.index body.content) + with e -> + let msg = + Krml.KPrint.bsprintf "Eurydice error: %s\n%s" (Printexc.to_string e) + (Printexc.get_backtrace ()) + in + K.(with_type return_type (EAbort (None, Some msg))) in let flags = match item_meta.attr_info.inline with @@ -1769,15 +1790,32 @@ let decl_of_id (env : env) (id : C.any_decl_id) : K.decl option = end | IdTraitDecl _ | IdTraitImpl _ -> None +let name_of_id env (id : C.any_decl_id) = + match id with + | IdType id -> (env.get_nth_type id).item_meta.name + | IdFun id -> (env.get_nth_function id).item_meta.name + | IdGlobal id -> (env.get_nth_global id).item_meta.name + | _ -> failwith "unsupported" + +(* Catch-all error handler (last resort) *) +let decl_of_id env decl = + try decl_of_id env decl + with e -> + L.log "AstOfLlbc" "ERROR translating %s: %s\n%s" + (string_of_name env (name_of_id env decl)) + (Printexc.to_string e) (Printexc.get_backtrace ()); + None + let decls_of_declarations (env : env) (d : C.declaration_group) : K.decl list = incr seen; - L.log "Progress" "%d/%d" !seen !total; + L.log "Progress" "%s: %d/%d" env.crate_name !seen !total; Krml.KList.filter_some @@ List.map (decl_of_id env) @@ declaration_group_to_list d let file_of_crate (crate : Charon.LlbcAst.crate) : Krml.Ast.file = let { C.name; declarations; type_decls; fun_decls; global_decls; trait_decls; trait_impls } = crate in + seen := 0; total := List.length declarations; let get_nth_function id = C.FunDeclId.Map.find id fun_decls in let get_nth_type id = C.TypeDeclId.Map.find id type_decls in diff --git a/lib/Builtin.ml b/lib/Builtin.ml index 7265ad1..a097a14 100644 --- a/lib/Builtin.ml +++ b/lib/Builtin.ml @@ -18,6 +18,9 @@ let option : K.lident = [ "core"; "option" ], "Option" let mk_option (t : K.typ) : K.typ = K.TApp (option, [ t ]) let array_copy = [ "Eurydice" ], "array_copy" let macros = Krml.Idents.LidSet.of_list [] +(* Things that could otherwise be emitted as an extern prototype, but for some + reason ought to be skipped. *) +let skip = Krml.Idents.LidSet.of_list [ ["Eurydice"], "assert" ] let result = [ "core"; "result" ], "Result" let mk_result t1 t2 = K.TApp (result, [ t1; t2 ]) let nonzero = [ "core"; "num"; "nonzero" ], "NonZero" @@ -290,6 +293,24 @@ let shr_pv_u8 = arg_names = [ "x"; "y" ]; } +let min_u32 = + { + name = [ "Eurydice" ], "min_u32"; + typ = Krml.Helpers.fold_arrow [ TInt UInt32; TInt UInt32 ] (TInt UInt32); + n_type_args = 0; + cg_args = []; + arg_names = [ "x"; "y" ]; + } + +(* Not fully general *) +let static_assert, static_assert_ref = + let name = [ "Eurydice" ], "assert" in + let typ =Krml.Helpers.fold_arrow [ TBool; + Krml.Checker.c_string ] TUnit in + K.DExternal (None, [ Krml.Common.Private; Macro ], 0, 0, + name, typ, + [ "test"; "msg" ]), K.(with_type typ (EQualified name)) + let unwrap : K.decl = let open Krml in let open Ast in @@ -367,8 +388,9 @@ let files = replace; bitand_pv_u8; shr_pv_u8; + min_u32; ] - @ [ nonzero_def ] + @ [ nonzero_def; static_assert ] in "Eurydice", externals); ] diff --git a/lib/Cleanup1.ml b/lib/Cleanup1.ml index 935f0dd..5d218bd 100644 --- a/lib/Cleanup1.ml +++ b/lib/Cleanup1.ml @@ -56,7 +56,18 @@ let remove_assignments = List.map (fun atom -> let name, typ = AtomMap.find atom not_yet_closed in - ( { node = { atom; name; mut = true; mark = ref Krml.Mark.default; meta = None }; typ }, + ( { + node = + { + atom; + name; + mut = true; + mark = ref Krml.Mark.default; + meta = None; + attempt_inline = false; + }; + typ; + }, if typ = TUnit then Krml.Helpers.eunit else @@ -153,7 +164,15 @@ let remove_assignments = let name, typ = AtomMap.find atom not_yet_closed in let b = { - node = { atom; name; mut = true; mark = ref Krml.Mark.default; meta = None }; + node = + { + atom; + name; + mut = true; + mark = ref Krml.Mark.default; + meta = None; + attempt_inline = false; + }; typ; } in diff --git a/lib/Cleanup2.ml b/lib/Cleanup2.ml index 652c634..2bcda10 100644 --- a/lib/Cleanup2.ml +++ b/lib/Cleanup2.ml @@ -693,3 +693,18 @@ let improve_names files = end) #visit_files () files + +let recognize_asserts = + object (_self) + inherit [_] map as super + + method! visit_EIfThenElse (((), _) as env) e1 e2 e3 = + match e1.typ, e2.node, e3.node with + | TBool, EUnit, EAbort (_, msg) -> + (* if not (e1) then abort msg else () --> static_assert(e1, msg) *) + EApp (Builtin.static_assert_ref, [ e1; with_type + Krml.Checker.c_string (EString (Option.value ~default:"" msg)) ]) + | _ -> + super#visit_EIfThenElse env e1 e2 e3 + + end diff --git a/lib/Cleanup3.ml b/lib/Cleanup3.ml index 508f270..0b5189f 100644 --- a/lib/Cleanup3.ml +++ b/lib/Cleanup3.ml @@ -8,6 +8,8 @@ argument *) +module B = Builtin + open Krml open Ast diff --git a/test/issue_49/Cargo.lock b/test/issue_49/Cargo.lock new file mode 100644 index 0000000..70c7650 --- /dev/null +++ b/test/issue_49/Cargo.lock @@ -0,0 +1,7 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 3 + +[[package]] +name = "issue_49" +version = "0.1.0" diff --git a/test/issue_49/Cargo.toml b/test/issue_49/Cargo.toml new file mode 100644 index 0000000..f84f2f1 --- /dev/null +++ b/test/issue_49/Cargo.toml @@ -0,0 +1,8 @@ +[package] +name = "issue_49" +version = "0.1.0" +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] diff --git a/test/issue_49/src/main.rs b/test/issue_49/src/main.rs new file mode 100644 index 0000000..f460c04 --- /dev/null +++ b/test/issue_49/src/main.rs @@ -0,0 +1,9 @@ +pub fn f(a: usize, b: usize) -> usize { + a.min(b) +} + +fn main() { + let expected = 0; + let actual = f(0, 0); + assert_eq!(expected, actual); +} diff --git a/test/symcrust/Cargo.lock b/test/symcrust/Cargo.lock new file mode 100644 index 0000000..74fd6e7 --- /dev/null +++ b/test/symcrust/Cargo.lock @@ -0,0 +1,7 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 3 + +[[package]] +name = "symcrust" +version = "0.1.0" diff --git a/test/symcrust/Cargo.toml b/test/symcrust/Cargo.toml new file mode 100644 index 0000000..9250c33 --- /dev/null +++ b/test/symcrust/Cargo.toml @@ -0,0 +1,8 @@ +[package] +name = "symcrust" +version = "0.1.0" +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] diff --git a/test/symcrust/c.yaml b/test/symcrust/c.yaml new file mode 100644 index 0000000..48a0a35 --- /dev/null +++ b/test/symcrust/c.yaml @@ -0,0 +1,6 @@ +files: + - name: symcrust + api: + - [ symcrust, "*" ] + private: + - [ "*" ] diff --git a/test/symcrust/src/main.rs b/test/symcrust/src/main.rs new file mode 100644 index 0000000..55edee3 --- /dev/null +++ b/test/symcrust/src/main.rs @@ -0,0 +1,72 @@ +#[allow(non_snake_case)] +#[no_mangle] +pub fn SymCrustMlKemPolyElementCompressAndEncode( + coeffs: &[u16; 256], + nBitsPerCoefficient: u32, + dst: &mut [u8] ) +{ + let SYMCRYPT_MLKEM_COMPRESS_MULCONSTANT : u64 = 0x9d7dbb; + let SYMCRYPT_MLKEM_COMPRESS_SHIFTCONSTANT : u32 = 35; + let mut multiplication: u64; + let mut coefficient: u32; + let mut nBitsInCoefficient: u32; + let mut bitsToEncode: u32; + let mut nBitsToEncode: u32; + let mut cbDstWritten: usize = 0; + let mut accumulator: u32 = 0; + let mut nBitsInAccumulator: u32 = 0; + + assert!(nBitsPerCoefficient > 0); + assert!(nBitsPerCoefficient <= 12); + assert!( dst.len() as u64 == (256*u64::from(nBitsPerCoefficient) / 8) ); + + for i in 0..256 + { + nBitsInCoefficient = nBitsPerCoefficient; + coefficient = u32::from(coeffs[i]); // in range [0, Q-1] + + // first compress the coefficient + // when nBitsPerCoefficient < 12 we compress per Compress_d in draft FIPS 203; + if nBitsPerCoefficient < 12 + { + // Multiply by 2^(nBitsPerCoefficient+1) / Q by multiplying by constant and shifting right + multiplication = u64::from(coefficient) * SYMCRYPT_MLKEM_COMPRESS_MULCONSTANT; + coefficient = (multiplication >> (SYMCRYPT_MLKEM_COMPRESS_SHIFTCONSTANT-(nBitsPerCoefficient+1))) as u32; + + // add "half" to round to nearest integer + coefficient += 1; + + // final divide by two to get multiplication by 2^nBitsPerCoefficient / Q + coefficient >>= 1; // in range [0, 2^nBitsPerCoefficient] + + // modular reduction by masking + coefficient &= (1u32< 0 + { + nBitsToEncode = nBitsInCoefficient.min(32-nBitsInAccumulator); + + bitsToEncode = coefficient & ((1u32<>= nBitsToEncode; + nBitsInCoefficient -= nBitsToEncode; + + accumulator |= bitsToEncode << nBitsInAccumulator; + nBitsInAccumulator += nBitsToEncode; + if nBitsInAccumulator == 32 + { + dst[cbDstWritten..cbDstWritten+4].copy_from_slice( &accumulator.to_le_bytes() ); + cbDstWritten += 4; + accumulator = 0; + nBitsInAccumulator = 0; + } + } + } +} + +fn main() { + // let mut dst = [0; 256]; + // SymCrustMlKemPolyElementCompressAndEncode(&[0; 256], 1, &mut dst); +}