diff --git a/.github/workflows/extract_and_run_coq.yml b/.github/workflows/extract_and_run_coq.yml new file mode 100644 index 000000000..e5bd83514 --- /dev/null +++ b/.github/workflows/extract_and_run_coq.yml @@ -0,0 +1,50 @@ +name: Extract and Run - Coq + +on: [pull_request] +jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: DeterminateSystems/nix-installer-action@main + - uses: DeterminateSystems/magic-nix-cache-action@main + + - name: ⤵ Install hax + run: | + nix build .\#coq-coverage-example + + # - name: build coverage example + # working-directory: hax/examples/coverage + # run: | + # nix run . into coq + + # - name: install annotated core for coq + # working-directory: hax/proof-libs/coq/coq/generated-core + # run: | + # nix-shell --packages coq coqPackages.coq-record-update --run "coq_makefile -f _CoqProject -o Makefile" && \ + # nix-shell --packages coq coqPackages.coq-record-update --run "make" && \ + # nix-shell --packages coq coqPackages.coq-record-update --run "sudo make install" + + # - name: run coq - coverage + # working-directory: hax/examples/coverage/proofs/coq/extraction + # run: | + # sed 's/_impl_f_/_f_/' < Coverage_Test_instance.v > Coverage_Test_instance.v # TODO: this is a hotfix, should be solved in backend and removed from here. + # nix-shell --packages coq coqPackages.coq-record-update --run "coq_makefile -f _CoqProject -o Makefile" + # nix-shell --packages coq coqPackages.coq-record-update --run "make" + + # - name: build and run coq on tests + # env: + # FILES: assert attribute-opaque enum-struct-variant + # NOT_SUPPORTED_FILES: attributes cli conditional-match constructor-as-closure cyclic-modules enum-repr even dyn functions + # run: | + # for f in $FILES; do \ + # cd hax/tests/$f && \ + # nix run . into coq && \ + # cd ../../.. + # done + # for f in $FILES; do \ + # cd hax/tests/$f/proofs/coq/extraction && \ + # nix-shell --packages coq coqPackages.coq-record-update --run "coq_makefile -f _CoqProject -o Makefile" && \ + # nix-shell --packages coq coqPackages.coq-record-update --run "make" && \ + # cd ../../../../../../ + # done diff --git a/engine/backends/coq/coq/coq_backend.ml b/engine/backends/coq/coq/coq_backend.ml index 0e03029fc..6862028d7 100644 --- a/engine/backends/coq/coq/coq_backend.ml +++ b/engine/backends/coq/coq/coq_backend.ml @@ -64,10 +64,43 @@ struct let metadata = Phase_utils.Metadata.make (Reject (NotInBackendLang backend)) end +(* module CoqNamePolicy = Concrete_ident.DefaultNamePolicy *) +module CoqNamePolicy = struct + (* include Concrete_ident.DefaultNamePolicy *) + + (** List of all words that have a special meaning in the target + language, and that should thus be escaped. *) + let reserved_words : string Hash_set.t = + Hash_set.of_list + (module String) + [ + "Definition"; + "Inductive"; + "match"; + "if"; + "then"; + "else"; + "as"; + "into"; + "end"; + "Record"; + "Arguments"; + "Type"; + ] + (* TODO: Make complete *) + + (** Transformation applied to indexes fields name (i.e. [x.1]) *) + let index_field_transform x = x + + let field_name_transform ~struct_name x = struct_name ^ "_" ^ x + let enum_constructor_name_transform ~enum_name x = x + let struct_constructor_name_transform x : string = "Build_t_" ^ x + let constructor_prefix = "" +end + module AST = Ast.Make (InputLanguage) module BackendOptions = Backend.UnitBackendOptions open Ast -module CoqNamePolicy = Concrete_ident.DefaultNamePolicy module U = Ast_utils.MakeWithNamePolicy (InputLanguage) (CoqNamePolicy) open AST @@ -82,7 +115,56 @@ let hardcoded_coq_headers = Require Import String.\n\ Require Import Coq.Floats.Floats.\n\ From RecordUpdate Require Import RecordSet.\n\ - Import RecordSetNotations.\n" + Import RecordSetNotations.\n\ + From Core Require Import Core.\n\n" + +let dummy_lib = + "(* TODO: Replace this dummy lib with core lib *)\n\ + Class t_Sized (T : Type) := { }.\n\ + Definition t_u8 := Z.\n\ + Definition t_u16 := Z.\n\ + Definition t_u32 := Z.\n\ + Definition t_u64 := Z.\n\ + Definition t_u128 := Z.\n\ + Definition t_usize := Z.\n\ + Definition t_i8 := Z.\n\ + Definition t_i16 := Z.\n\ + Definition t_i32 := Z.\n\ + Definition t_i64 := Z.\n\ + Definition t_i128 := Z.\n\ + Definition t_isize := Z.\n\ + Definition t_Array T (x : t_usize) := list T.\n\ + Definition t_String := string.\n\ + Definition ToString_f_to_string (x : string) := x.\n\ + Instance Sized_any : forall {t_A}, t_Sized t_A := {}.\n\ + Class t_Clone (T : Type) := { Clone_f_clone : T -> T }.\n\ + Instance Clone_any : forall {t_A}, t_Clone t_A := {Clone_f_clone := fun x \ + => x}.\n\ + Definition t_Slice (T : Type) := list T.\n\ + Definition unsize {T : Type} : list T -> t_Slice T := id.\n\ + Definition t_PartialEq_f_eq x y := x =? y.\n\ + Definition t_Rem_f_rem (x y : Z) := x mod y.\n\ + Definition assert (b : bool) (* `{H_assert : b = true} *) : unit := tt.\n\ + Inductive globality := | t_Global.\n\ + Definition t_Vec T (_ : globality) : Type := list T.\n\ + Definition impl_1__append {T} l1 l2 : list T * list T := (app l1 l2, l2).\n\ + Definition impl_1__len {A} (l : list A) := Z.of_nat (List.length l).\n\ + Definition impl__new {A} (_ : Datatypes.unit) : list A := nil.\n\ + Definition impl__with_capacity {A} (_ : Z) : list A := nil.\n\ + Definition impl_1__push {A} l (x : A) := cons x l.\n\ + Class t_From (A B : Type) := { From_f_from : B -> A }.\n\ + Definition impl__to_vec {T} (x : t_Slice T) : t_Vec T t_Global := x.\n\ + Class t_Into (A B : Type) := { Into_f_into : A -> B }.\n\ + Instance t_Into_from_t_From {A B : Type} `{H : t_From B A} : t_Into A B := \ + { Into_f_into x := @From_f_from B A H x }.\n\ + Definition from_elem {A} (x : A) (l : Z) := repeat x (Z.to_nat l).\n\ + Definition t_Option := option.\n\ + Definition impl__map {A B} (x : t_Option A) (f : A -> B) : t_Option B := \ + match x with | Some x => Some (f x) | None => None end.\n\ + Definition t_Add_f_add x y := x + y.\n\ + Class Cast A B := { cast : A -> B }.\n\ + Instance cast_t_u8_t_u32 : Cast t_u8 t_u32 := {| cast x := x |}.\n\ + (* / dummy lib *)\n" module BasePrinter = Generic_printer.Make (InputLanguage) @@ -97,17 +179,25 @@ struct let default_string_for s = "TODO: please implement the method `" ^ s ^ "`" let default_document_for = default_string_for >> string + let concat_with ?(pre = empty) ?(post = empty) l = + concat_map (fun x -> pre ^^ x ^^ post) l + + let concat_map_with ?(pre = empty) ?(post = empty) f l = + concat_map (fun x -> pre ^^ f x ^^ post) l + + let concat_spaced_doc l = concat_map_with ~pre:space (fun x -> x#p) l + module CoqNotation = struct let definition_struct keyword n name generics params typ body = keyword ^^ space ^^ name ^^ generics - ^^ concat_map (fun x -> space ^^ x) params + ^^ concat_with ~pre:space params ^^ space ^^ colon ^^ space ^^ typ ^^ space ^^ string ":=" ^^ nest n (break 1 ^^ body) ^^ dot let proof_struct keyword name generics params statement = keyword ^^ space ^^ name ^^ generics - ^^ concat_map (fun x -> space ^^ x) params + ^^ concat_with ~pre:space params ^^ space ^^ colon ^^ nest 2 (break 1 ^^ statement ^^ dot) ^^ break 1 ^^ string "Proof" ^^ dot ^^ space ^^ string "Admitted" ^^ dot @@ -119,6 +209,20 @@ struct let instance = definition_struct (string "Instance") 2 let class_ = definition_struct (string "Class") 2 let lemma = proof_struct (string "Lemma") + + let arguments name (explicivity : bool list) = + !^"Arguments" ^^ space ^^ name + ^^ concat_map_with ~pre:space + (function true -> string "(_)" | false -> string "{_}") + explicivity + ^^ dot + + let notation pattern value = + !^"Notation" ^^ space ^^ string "\"" ^^ pattern ^^ string "\"" ^^ space + ^^ !^":=" ^^ space ^^ value ^^ dot + + let notation_name name value = + notation (string "'" ^^ name ^^ string "'") value end type ('get_span_data, 'a) object_type = @@ -128,6 +232,9 @@ struct object (self) inherit BasePrinter.base + val concrete_ident_view : (module Concrete_ident.VIEW_API) = + (module U.Concrete_ident_view) + method private primitive_to_string (id : primitive_ident) : document = match id with | Deref -> default_document_for "(TODO: Deref)" @@ -163,15 +270,27 @@ struct match witness with _ -> . method expr'_App_application ~super:_ ~f ~args ~generics:_ = - f#p ^^ concat_map (fun x -> space ^^ parens x#p) args + f#p ^^ concat_map_with ~pre:space (fun x -> parens x#p) args method expr'_App_constant ~super:_ ~constant ~generics:_ = constant#p method expr'_App_field_projection ~super:_ ~field ~e = field#p ^^ space ^^ e#p - method expr'_App_tuple_projection ~super:_ ~size:_ ~nth:_ ~e:_ = - default_document_for "expr'_App_tuple_projection" + method expr'_App_tuple_projection ~super:_ ~size ~nth ~e = + let size = + match e#v.e with + | Construct { constructor; is_record; is_struct; fields; base } -> + List.length fields + | _ -> size (* TODO: Size argument incorrect? *) + in + List.fold_right ~init:e#p + ~f:(fun x y -> parens (x ^^ y)) + ((if Stdlib.(nth != 0) then [ string "snd" ] else []) + @ + if size - 1 - nth > 0 then + List.init (size - 1 - nth) ~f:(fun _ -> string "fst") + else []) method expr'_Ascription ~super:_ ~e ~typ = e#p ^^ space ^^ colon ^^ space ^^ typ#p @@ -189,9 +308,7 @@ struct match witness with _ -> . method expr'_Closure ~super:_ ~params ~body ~captures:_ = - !^"fun" - ^^ concat_map (fun x -> space ^^ x#p) params - ^^ space ^^ !^"=>" ^^ space + !^"fun" ^^ concat_spaced_doc params ^^ space ^^ !^"=>" ^^ space ^^ nest 2 (break 1 ^^ body#p) method expr'_Construct_inductive ~super:_ ~constructor ~is_record @@ -199,22 +316,29 @@ struct let fields_or_empty add_space = if List.is_empty fields then empty else - add_space - ^^ parens - (separate_map (comma ^^ space) (fun x -> (snd x)#p) fields) + add_space ^^ separate_map space (fun x -> parens (snd x)#p) fields in if is_record && is_struct then match base with - | Some x -> string "Build_" ^^ x#p ^^ fields_or_empty space - | None -> string "Build_t_" ^^ constructor#p ^^ fields_or_empty space + | Some x -> + (* Update fields *) + x#p + ^^ concat_map_with ~pre:space + (fun x -> + string "<|" ^^ (fst x)#p ^^ space ^^ !^":=" ^^ space + ^^ (snd x)#p ^^ space ^^ string "|>") + fields + | None -> constructor#p ^^ fields_or_empty space else if not is_record then - if is_struct then - string "Build_t_" ^^ constructor#p ^^ fields_or_empty space + if is_struct then constructor#p ^^ fields_or_empty space else constructor#p ^^ fields_or_empty space else - default_document_for - "expr'_Construct_inductive [is_record=true, is_struct = false] \ - todo record" + constructor#p ^^ space ^^ string "{|" ^^ space + ^^ separate_map (semi ^^ space) + (fun (ident, exp) -> + ident#p ^^ space ^^ string ":=" ^^ space ^^ parens exp#p) + fields + ^^ space ^^ string "|}" method expr'_Construct_tuple ~super:_ ~components = if List.length components == 0 then !^"tt" @@ -242,7 +366,12 @@ struct string "let" ^^ space ^^ lhs#p ^^ space ^^ string ":=" ^^ space ^^ rhs#p ^^ space ^^ string "in" ^^ break 1 ^^ body#p - method expr'_Literal ~super:_ x2 = x2#p + method expr'_Literal ~super x2 = + parens + (x2#p ^^ space ^^ colon ^^ space + ^^ (self#_do_not_override_lazy_of_ty AstPos_expr'_Literal_x0 super.typ) + #p) + method expr'_LocalVar ~super:_ x2 = x2#p method expr'_Loop ~super:_ ~body ~kind ~state ~control_flow ~label:_ @@ -262,7 +391,11 @@ struct method expr'_Match ~super:_ ~scrutinee ~arms = string "match" ^^ space ^^ scrutinee#p ^^ space ^^ string "with" ^^ break 1 - ^^ concat_map (fun x -> string "|" ^^ space ^^ x#p ^^ break 1) arms + ^^ concat_map_with + ~pre:(string "|" ^^ space) + ~post:(break 1) + (fun x -> x#p) + arms ^^ string "end" method expr'_QuestionMark ~super:_ ~e:_ ~return_typ:_ ~witness = @@ -284,7 +417,7 @@ struct method generic_constraint_GCType x1 = string "`" ^^ braces x1#p method generic_param ~ident ~span:_ ~attrs:_ ~kind = - string "`" ^^ braces (ident#p ^^ space ^^ colon ^^ space ^^ kind#p) + ident#p ^^ space ^^ colon ^^ space ^^ kind#p method generic_param_kind_GPConst ~typ = typ#p @@ -300,10 +433,10 @@ struct method generic_value_GType x1 = parens x1#p method generics ~params ~constraints = - let params_document = concat_map (fun x -> space ^^ x#p) params in - let constraints_document = - concat_map (fun x -> space ^^ x#p) constraints + let params_document = + concat_map_with ~pre:space (fun x -> string "`" ^^ braces x#p) params in + let constraints_document = concat_spaced_doc constraints in params_document ^^ constraints_document method guard ~guard:_ ~span:_ = default_document_for "guard" @@ -342,17 +475,14 @@ struct method impl_item'_IIFn ~body ~params = if List.length params == 0 then body#p else - string "fun" ^^ space - ^^ concat_map (fun x -> x#p ^^ space) params - ^^ string "=>" + string "fun" ^^ space ^^ concat_spaced_doc params ^^ string "=>" ^^ nest 2 (break 1 ^^ body#p) method impl_item'_IIType ~typ ~parent_bounds:_ = typ#p method item ~v ~span:_ ~ident:_ ~attrs:_ = v#p ^^ break 1 method item'_Alias ~super:_ ~name ~item = - string "Notation" ^^ space ^^ string "\"'" ^^ name#p ^^ string "'\"" - ^^ space ^^ string ":=" ^^ space ^^ parens item#p ^^ dot + CoqNotation.notation_name name#p (parens item#p) method item'_Fn ~super ~name ~generics ~body ~params ~safety:_ = (* TODO: Why is type not available here ? *) @@ -365,6 +495,26 @@ struct self#_do_not_override_lazy_of_ty AstPos_item'_Fn_body body#v.typ in + let params = + List.map + ~f:(fun x -> + match x#v with + | { + pat = + { + p = PBinding { mut; mode; var; typ = _; subpat }; + span : span; + typ = _; + }; + typ; + typ_span; + attrs; + } -> + x#p + | _ -> string "'" ^^ x#p) + params + in + let get_expr_of kind f : document option = Attrs.associated_expr kind super.attrs |> Option.map ~f:(self#entrypoint_expr >> f) @@ -377,23 +527,21 @@ struct get_expr_of Ensures (fun x -> x ^^ space ^^ string "=" ^^ space ^^ string "true") in - let is_lemma = Attrs.lemma super.attrs in if is_lemma then - CoqNotation.lemma name#p generics#p - (List.map ~f:(fun x -> x#p) params) + CoqNotation.lemma name#p generics#p params (Option.value ~default:empty requires ^^ space ^^ !^"->" ^^ break 1 ^^ Option.value ~default:empty ensures) else if is_rec then CoqNotation.fixpoint name#p generics#p - (List.map ~f:(fun x -> x#p) params + (params @ Option.value ~default:[] (Option.map ~f:(fun x -> [ string "`" ^^ braces x ]) requires)) typ#p body#p (* ^^ TODO: ensures? *) else CoqNotation.definition name#p generics#p - (List.map ~f:(fun x -> x#p) params + (params @ Option.value ~default:[] (Option.map ~f:(fun x -> [ string "`" ^^ braces x ]) requires)) typ#p body#p (* ^^ TODO: ensures? *) @@ -410,10 +558,19 @@ struct CoqNotation.instance (name#p ^^ string "_" ^^ string (Int.to_string ([%hash: item] super))) generics#p [] - (name#p ^^ concat_map (fun x -> space ^^ parens x#p) args) + (name#p ^^ concat_map_with ~pre:space (fun x -> parens x#p) args) (braces (nest 2 - (concat_map (fun x -> break 1 ^^ name#p ^^ !^"_" ^^ x#p) items) + (concat_map_with + ~pre: + (break 1 + ^^ string + (String.drop_prefix + (U.Concrete_ident_view.to_definition_name name#v) + 2) + ^^ !^"_") + (fun x -> x#p) + items) ^^ break 1)) method item'_NotImplementedYet = string "(* NotImplementedYet *)" @@ -423,23 +580,39 @@ struct method item'_Trait ~super:_ ~name ~generics ~items ~safety:_ = let _, params, constraints = generics#v in - CoqNotation.class_ name#p generics#p [] !^"Type" + CoqNotation.class_ name#p + (concat_map_with ~pre:space (fun x -> parens x#p) params + ^^ concat_map_with ~pre:space (fun x -> x#p) constraints) + [] !^"Type" (braces - (nest 2 (concat_map (fun x -> break 1 ^^ x#p) items) ^^ break 1)) - ^^ break 1 ^^ !^"Arguments" ^^ space ^^ name#p ^^ colon - ^^ !^"clear implicits" ^^ dot ^^ break 1 ^^ !^"Arguments" ^^ space - ^^ name#p - ^^ concat_map (fun _ -> space ^^ !^"(_)") params - ^^ concat_map (fun _ -> space ^^ !^"{_}") constraints - ^^ dot + (nest 2 (concat_map_with ~pre:(break 1) (fun x -> x#p) items) + ^^ break 1)) + ^^ break 1 + ^^ CoqNotation.arguments name#p + (List.map ~f:(fun _ -> true) params + @ List.map ~f:(fun _ -> false) constraints) method item'_TyAlias ~super:_ ~name ~generics:_ ~ty = - string "Notation" ^^ space ^^ string "\"'" ^^ name#p ^^ string "'\"" - ^^ space ^^ string ":=" ^^ space ^^ ty#p ^^ dot + CoqNotation.notation_name name#p ty#p - method item'_Type_struct ~super:_ ~name ~generics ~tuple_struct:_ - ~arguments = - CoqNotation.record name#p generics#p [] (string "Type") + method item'_Type_struct ~super:_ ~name ~generics ~tuple_struct ~arguments + = + let arguments_explicity_with_ty = + List.map ~f:(fun _ -> true) generics#v.params + @ List.map ~f:(fun _ -> false) generics#v.constraints + in + let arguments_explicity_without_ty = + List.map ~f:(fun _ -> false) generics#v.params + @ List.map ~f:(fun _ -> false) generics#v.constraints + in + CoqNotation.record name#p + (concat_map_with ~pre:space + (fun x -> parens (self#entrypoint_generic_param x)) + generics#v.params + ^^ concat_map_with ~pre:space + (fun x -> self#entrypoint_generic_constraint x) + generics#v.constraints) + [] (string "Type") (braces (nest 2 (concat_map @@ -448,38 +621,115 @@ struct ^^ semi) arguments) ^^ break 1)) - ^^ break 1 ^^ !^"Arguments" ^^ space ^^ name#p ^^ colon - ^^ !^"clear implicits" ^^ dot ^^ break 1 ^^ !^"Arguments" ^^ space - ^^ name#p - ^^ concat_map (fun _ -> space ^^ !^"(_)") generics#v.params - ^^ concat_map (fun _ -> space ^^ !^"{_}") generics#v.constraints - ^^ dot ^^ break 1 ^^ !^"Arguments" ^^ space ^^ !^"Build_" ^^ name#p - ^^ concat_map (fun _ -> space ^^ !^"{_}") generics#v.params - ^^ concat_map (fun _ -> space ^^ !^"{_}") generics#v.constraints - ^^ dot ^^ break 1 ^^ !^"#[export]" ^^ space - ^^ CoqNotation.instance - (string "settable" ^^ string "_" ^^ name#p) - generics#p [] - (!^"Settable" ^^ space ^^ !^"_") - (string "settable!" ^^ space - ^^ parens (!^"@" ^^ !^"Build_" ^^ name#p ^^ generics#p) - ^^ space ^^ string "<" - ^^ separate_map (semi ^^ space) - (fun (ident, typ, attr) -> ident#p) - arguments - ^^ string ">") - - method item'_Type_enum ~super:_ ~name ~generics ~variants = - CoqNotation.inductive name#p generics#p [] (string "Type") - (separate_map (break 1) - (fun x -> string "|" ^^ space ^^ x#p) - variants) - ^^ break 1 ^^ !^"Arguments" ^^ space ^^ name#p ^^ colon - ^^ !^"clear implicits" ^^ dot ^^ break 1 ^^ !^"Arguments" ^^ space - ^^ name#p - ^^ concat_map (fun _ -> space ^^ !^"(_)") generics#v.params - ^^ concat_map (fun _ -> space ^^ !^"{_}") generics#v.constraints - ^^ dot + ^^ break 1 + ^^ CoqNotation.arguments (!^"Build_" ^^ name#p) + arguments_explicity_without_ty (* arguments_explicity_with_ty *) + ^^ concat_map_with ~pre:(break 1) + (fun (ident, typ, attr) -> + CoqNotation.arguments ident#p arguments_explicity_without_ty) + arguments + ^^ break 1 ^^ !^"#[export]" ^^ space + ^^ (if List.is_empty arguments then empty + else + CoqNotation.instance + (string "settable" ^^ string "_" ^^ name#p) + generics#p [] + (!^"Settable" ^^ space ^^ !^"_") + (string "settable!" ^^ space + ^^ parens + (!^"Build_" ^^ name#p + ^^ concat_map_with ~pre:space + (fun (x : generic_param) -> + match x with + | { ident; _ } -> + let idx = + (self#_do_not_override_lazy_of_local_ident + AstPos_item'_Type_generics ident) + #p + in + parens (idx ^^ space ^^ !^":=" ^^ space ^^ idx)) + generics#v.params) + ^^ space ^^ string "<" + ^^ separate_map (semi ^^ space) + (fun (ident, typ, attr) -> ident#p) + arguments + ^^ string ">")) + ^^ + if tuple_struct then + break 1 + ^^ CoqNotation.notation_name + (string + (String.drop_prefix + (U.Concrete_ident_view.to_definition_name name#v) + 2)) + (!^"Build_" ^^ name#p) + else empty + + (* map_def_path_item_string (fun x -> x) x#v.name *) + + method item'_Type_enum ~super ~name ~generics ~variants = + let arguments_explicity_without_ty = + List.map ~f:(fun _ -> false) generics#v.params + @ List.map ~f:(fun _ -> false) generics#v.constraints + in + + concat_map_with ~post:(break 1) + (fun x -> + self#item'_Type_struct ~super + ~name: + (self#_do_not_override_lazy_of_concrete_ident + AstPos_variant__arguments + (Concrete_ident.Create.map_last + ~f:(fun x -> x ^ "_record") + x#v.name)) + ~generics ~tuple_struct:false + ~arguments: + (List.map + ~f:(fun (ident, typ, attrs) -> + ( self#_do_not_override_lazy_of_concrete_ident + AstPos_variant__arguments ident, + self#_do_not_override_lazy_of_ty + AstPos_variant__arguments typ, + self#_do_not_override_lazy_of_attrs AstPos_variant__attrs + attrs )) + x#v.arguments)) + (List.filter ~f:(fun x -> x#v.is_record) variants) + ^^ CoqNotation.inductive name#p + (concat_map_with ~pre:space + (fun x -> parens (self#entrypoint_generic_param x)) + generics#v.params + ^^ concat_map_with ~pre:space + (fun x -> self#entrypoint_generic_constraint x) + generics#v.constraints) + [] (string "Type") + (separate_map (break 1) + (fun x -> + string "|" ^^ space ^^ x#p + ^^ + if x#v.is_record then + concat_map_with ~pre:space + (fun (x : generic_param) -> + (self#_do_not_override_lazy_of_local_ident + AstPos_item'_Type_generics x.ident) + #p) + generics#v.params + ^^ space ^^ !^"->" ^^ space ^^ !^"_" + else empty) + variants) + ^^ concat_map_with ~pre:(break 1) + (fun v -> + CoqNotation.arguments + (self#_do_not_override_lazy_of_concrete_ident + AstPos_variant__arguments v#v.name) + #p + arguments_explicity_without_ty) + variants + (* ^^ break 1 ^^ !^"Arguments" ^^ space ^^ name#p ^^ colon *) + (* ^^ !^"clear implicits" ^^ dot ^^ break 1 ^^ !^"Arguments" ^^ space *) + (* ^^ name#p *) + (* ^^ concat_map (fun _ -> space ^^ !^"(_)") generics#v.params *) + (* ^^ concat_map (fun _ -> space ^^ !^"{_}") generics#v.constraints *) + (* ^^ dot *) method item'_Use ~super:_ ~path ~is_external ~rename:_ = if List.length path == 0 || is_external then empty @@ -535,9 +785,10 @@ struct string "\"" ^^ string (Char.escaped x1) ^^ string "\"" ^^ string "%char" method literal_Float ~value ~negative ~kind:_ = - (if negative then !^"-" else empty) ^^ string value ^^ string "%float" + (if negative then parens (!^"-" ^^ string value) else string value) + ^^ string "%float" - method literal_Int ~value ~negative ~kind:_ = + method literal_Int ~value ~negative ~kind = (if negative then !^"-" else empty) ^^ string value method literal_String x1 = string "\"" ^^ string x1 ^^ string "\"%string" @@ -579,10 +830,19 @@ struct (separate_map (comma ^^ space) (fun field_pat -> (snd field_pat)#p) fields) + else if is_record then + (* constructor#p ^^ *) + string "{|" + ^^ separate_map (semi ^^ space) + (fun (ident, exp) -> + ident#p ^^ space ^^ string ":=" ^^ space ^^ parens exp#p) + fields + ^^ string "|}" else - (if is_struct then string "Build_t_" else empty) - ^^ constructor#p - ^^ concat_map (fun (ident, exp) -> space ^^ parens exp#p) fields + constructor#p + ^^ concat_map_with ~pre:space + (fun (ident, exp) -> parens exp#p) + fields method pat'_PConstruct_tuple ~super:_ ~components = (* TODO: Only add `'` if you are a top-level pattern *) @@ -706,11 +966,11 @@ struct method item'_Enum_Variant ~name ~arguments ~is_record ~attrs:_ = if is_record then - concat_map - (fun (ident, typ, attr) -> - ident#p ^^ space ^^ colon ^^ space ^^ typ#p) - arguments - ^^ semi + name#p ^^ space ^^ colon ^^ space ^^ name#p ^^ !^"_record" ^^ space + (* concat_map *) + (* (fun (ident, typ, attr) -> *) + (* ident#p ^^ space ^^ colon ^^ space ^^ typ#p) *) + (* arguments *) else if List.length arguments == 0 then name#p else name#p ^^ space ^^ colon ^^ space @@ -720,21 +980,24 @@ struct arguments ^^ space ^^ string "->" ^^ space ^^ string "_" + method quote (quote : quote) : document = empty method module_path_separator = "." method concrete_ident ~local:_ id : document = string (match id.definition with | "not" -> "negb" - | "eq" -> "t_PartialEq_f_eq" - | "lt" -> "t_PartialOrd_f_lt" - | "gt" -> "t_PartialOrd_f_gt" - | "le" -> "t_PartialOrd_f_le" - | "ge" -> "t_PartialOrd_f_ge" - | "rem" -> "t_Rem_f_rem" - | "add" -> "t_Add_f_add" - | "mul" -> "t_Mul_f_mul" - | "div" -> "t_Div_f_div" + | "eq" -> "PartialEq_f_eq" + | "lt" -> "PartialOrd_f_lt" + | "gt" -> "PartialOrd_f_gt" + | "le" -> "PartialOrd_f_le" + | "ge" -> "PartialOrd_f_ge" + | "rem" -> "Rem_f_rem" + | "add" -> "Add_f_add" + | "sub" -> "Sub_f_sub" + | "mul" -> "Mul_f_mul" + | "div" -> "Div_f_div" + | "index" -> "Index_f_index" | x -> x) end @@ -758,7 +1021,7 @@ let make (module M : Attrs.WITH_ITEMS) = let translate m _ ~bundles:_ (items : AST.item list) : Types.file list = let my_printer = make m in - U.group_items_by_namespace items + (U.group_items_by_namespace items |> Map.to_alist |> List.map ~f:(fun (ns, items) -> let mod_name = @@ -770,13 +1033,34 @@ let translate m _ ~bundles:_ (items : AST.item list) : Types.file list = let sourcemap, contents = let annotated = my_printer#entrypoint_modul items in let open Generic_printer.AnnotatedString in - let header = pure (hardcoded_coq_headers ^ "\n") in + let header = pure hardcoded_coq_headers in let annotated = concat header annotated in (to_sourcemap annotated, to_string annotated) in let sourcemap = Some sourcemap in let path = mod_name ^ ".v" in - Types.{ path; contents; sourcemap }) + Types.{ path; contents; sourcemap })) + @ [ + Types. + { + path = "_CoqProject"; + contents = + "-R ./ " ^ "TODO" ^ "\n-arg -w\n-arg all\n\n" + ^ String.concat ~sep:"\n" + (List.rev + (U.group_items_by_namespace items + |> Map.to_alist + |> List.map ~f:(fun (ns, items) -> + let mod_name = + String.concat ~sep:"_" + (List.map + ~f:(map_first_letter String.uppercase) + (fst ns :: snd ns)) + in + mod_name ^ ".v"))); + sourcemap = None; + }; + ] open Phase_utils diff --git a/engine/lib/concrete_ident/concrete_ident.ml b/engine/lib/concrete_ident/concrete_ident.ml index b0d0cc160..0a2b4918f 100644 --- a/engine/lib/concrete_ident/concrete_ident.ml +++ b/engine/lib/concrete_ident/concrete_ident.ml @@ -473,7 +473,8 @@ module MakeViewAPI (NP : NAME_POLICY) : VIEW_API = struct else escape name | Constructor { is_struct } -> let name = - if start_lowercase name || is_reserved_word name then "C_" ^ name + if start_lowercase name || is_reserved_word name then + NP.constructor_prefix ^ name else escape name in if is_struct then NP.struct_constructor_name_transform name @@ -565,6 +566,7 @@ module DefaultNamePolicy = struct let field_name_transform ~struct_name:_ = Fn.id let enum_constructor_name_transform ~enum_name:_ = Fn.id let struct_constructor_name_transform = Fn.id + let constructor_prefix = "C_" end let matches_namespace (ns : Types.namespace) (did : t) : bool = diff --git a/engine/lib/concrete_ident/concrete_ident_sig.ml b/engine/lib/concrete_ident/concrete_ident_sig.ml index 09af4797a..13df71853 100644 --- a/engine/lib/concrete_ident/concrete_ident_sig.ml +++ b/engine/lib/concrete_ident/concrete_ident_sig.ml @@ -18,6 +18,7 @@ struct val field_name_transform : struct_name:string -> string -> string val enum_constructor_name_transform : enum_name:string -> string -> string val struct_constructor_name_transform : string -> string + val constructor_prefix : string end module type VIEW_API = sig diff --git a/engine/lib/generic_printer/generic_printer.ml b/engine/lib/generic_printer/generic_printer.ml index 811051c0e..ee5f7079f 100644 --- a/engine/lib/generic_printer/generic_printer.ml +++ b/engine/lib/generic_printer/generic_printer.ml @@ -618,7 +618,7 @@ module Make (F : Features.T) = struct lazy_doc (fun (id : global_ident) -> match id with - | `Concrete cid -> + | `Concrete cid | `Projector (`Concrete cid) -> (self#_do_not_override_lazy_of_concrete_ident ast_position cid) #p | _ -> diff --git a/examples/Cargo.lock b/examples/Cargo.lock index af90ddc48..1160deeab 100644 --- a/examples/Cargo.lock +++ b/examples/Cargo.lock @@ -151,6 +151,10 @@ dependencies = [ "hax-lib", ] +[[package]] +name = "coverage" +version = "0.1.0" + [[package]] name = "cpufeatures" version = "0.2.11" @@ -385,7 +389,6 @@ name = "kyber_compress" version = "0.1.0" dependencies = [ "hax-lib", - "hax-lib-macros", ] [[package]] @@ -733,7 +736,7 @@ dependencies = [ name = "sha256" version = "0.1.0" dependencies = [ - "hax-lib-macros", + "hax-lib", ] [[package]] diff --git a/examples/Cargo.toml b/examples/Cargo.toml index 9b7eceb41..4aea4b684 100644 --- a/examples/Cargo.toml +++ b/examples/Cargo.toml @@ -6,7 +6,8 @@ members = [ "barrett", "kyber_compress", "proverif-psk", - "coq-example"] + "coq-example", + "coverage"] resolver = "2" [workspace.dependencies] diff --git a/examples/commonArgs.nix b/examples/commonArgs.nix new file mode 100644 index 000000000..6238f52ea --- /dev/null +++ b/examples/commonArgs.nix @@ -0,0 +1,26 @@ +{ + craneLib, + lib, +}: +let + matches = re: path: !builtins.isNull (builtins.match re path); +in +{ + version = "0.0.1"; + src = lib.cleanSourceWith { + src = craneLib.path ./..; + filter = path: type: + # We include only certain files. FStar files under the example + # directory are listed out. Same for proverif (*.pvl) files. + ( matches ".*(Makefile|.*[.](rs|toml|lock|diff|fsti?|pv))$" path + && !matches ".*examples/.*[.]fsti?$" path + ) || ("directory" == type); + }; + doCheck = false; + cargoVendorDir = craneLib.vendorMultipleCargoDeps { + cargoLockList = [ + ./Cargo.lock + ../Cargo.lock + ]; + }; +} diff --git a/examples/coverage/Cargo.toml b/examples/coverage/Cargo.toml new file mode 100644 index 000000000..055dab5dd --- /dev/null +++ b/examples/coverage/Cargo.toml @@ -0,0 +1,6 @@ +[package] +name = "coverage" +version = "0.1.0" +edition = "2021" + +[dependencies] diff --git a/examples/coverage/default.nix b/examples/coverage/default.nix new file mode 100644 index 000000000..abc457c6a --- /dev/null +++ b/examples/coverage/default.nix @@ -0,0 +1,38 @@ +{ + stdenv, + lib, + hax, + coqPackages, + gnused, + craneLib, + bat, + coqGeneratedCore ? import ../../proof-libs/coq/coq {inherit stdenv coqPackages;}, +}: +let + commonArgs = import ../commonArgs.nix {inherit craneLib lib;}; + cargoArtifacts = craneLib.buildDepsOnly commonArgs; +in + craneLib.mkCargoDerivation (commonArgs + // { + inherit cargoArtifacts; + pname = "coverage"; + doCheck = false; + buildPhaseCargoCommand = '' + cd examples/coverage + cargo hax into coq + + cd proofs/coq/extraction + echo -e "-R ${coqGeneratedCore}/lib/coq/user-contrib/Core Core\n$(cat _CoqProject)" > _CoqProject + coq_makefile -f _CoqProject -o Makefile + make + ''; + buildInputs = [ + hax + coqPackages.coq-record-update + coqPackages.coq + gnused + ]; + }) + + + # COQLIB diff --git a/examples/coverage/src/lib.rs b/examples/coverage/src/lib.rs new file mode 100644 index 000000000..2b5521210 --- /dev/null +++ b/examples/coverage/src/lib.rs @@ -0,0 +1,15 @@ +// https://doc.rust-lang.org/reference/types.html +mod test_primitives; +mod test_sequence; + +mod test_enum; +mod test_struct; + +mod test_closures; +mod test_functions; + +mod test_instance; + +mod test_trait; + +mod test_arrays; diff --git a/examples/coverage/src/test_arrays.rs b/examples/coverage/src/test_arrays.rs new file mode 100644 index 000000000..939f85f73 --- /dev/null +++ b/examples/coverage/src/test_arrays.rs @@ -0,0 +1,34 @@ +// // This function borrows a slice. +// fn analyze_slice(slice: &[i32]) { +// let _ = slice[0]; +// let _ = slice.len(); +// } + +// fn test(){ +// // Fixed-size array (type signature is superfluous). +// let xs: [i32; 5] = [1, 2, 3, 4, 5]; + +// // All elements can be initialized to the same value. +// let ys: [i32; 500] = [0; 500]; + +// // Indexing starts at 0. +// let _ = xs[0]; +// let _ = xs[1]; + +// // `len` returns the count of elements in the array. +// let _ = xs.len(); + +// // Arrays can be automatically borrowed as slices. +// analyze_slice(&xs); + +// // Slices can point to a section of an array. +// // They are of the form [starting_index..ending_index]. +// // `starting_index` is the first position in the slice. +// // `ending_index` is one more than the last position in the slice. +// analyze_slice(&ys[1 .. 4]); + +// // Example of empty slice `&[]`: +// let empty_array: [u32; 0] = []; +// assert_eq!(&empty_array, &[]); +// assert_eq!(&empty_array, &[][..]); // Same but more verbose +// } diff --git a/examples/coverage/src/test_closures.rs b/examples/coverage/src/test_closures.rs new file mode 100644 index 000000000..f761be221 --- /dev/null +++ b/examples/coverage/src/test_closures.rs @@ -0,0 +1,14 @@ +// TODO: +// fn test() { +// let add : fn(i32, i32) -> i32 = |x, y| x + y; +// let _ = (|x : &u8| { x + x })(&2); + +// fn f u8> (g: F) -> u8 { +// g() + 2 +// } + +// f(|| { +// 23 +// }); +// // Prints "foobar". +// } diff --git a/examples/coverage/src/test_enum.rs b/examples/coverage/src/test_enum.rs new file mode 100644 index 000000000..27c18b69f --- /dev/null +++ b/examples/coverage/src/test_enum.rs @@ -0,0 +1,56 @@ +fn test() { + { + enum Foo<'a, T, const N: usize> { + Bar(u8), + Baz, + Qux { x: &'a T, y: [T; N], z: u8 }, + } + + let x: Foo = Foo::Baz; + } + + { + enum AnimalA { + Dog, + Cat, + } + + let mut a: AnimalA = AnimalA::Dog; + a = AnimalA::Cat; + } + + { + enum AnimalB { + Dog(String, f64), + Cat { name: String, weight: f64 }, + } + + let mut a: AnimalB = AnimalB::Dog("Cocoa".to_string(), 37.2); + a = AnimalB::Cat { + name: "Spotty".to_string(), + weight: 2.7, + }; + } + { + enum Examples { + UnitLike, + TupleLike(i32), + StructLike { value: i32 }, + } + + // use Examples::*; // Creates aliases to all variants. + let x = Examples::UnitLike; // Path expression of the const item. + let x = Examples::UnitLike {}; // Struct expression. + let y = Examples::TupleLike(123); // Call expression. + let y = Examples::TupleLike { 0: 123 }; // Struct expression using integer field names. + let z = Examples::StructLike { value: 123 }; // Struct expression. + } + { + #[repr(u8)] + enum Enum { + Unit = 3, + Tuple(u16), + Struct { a: u8, b: u16 } = 1, + } + } +} diff --git a/examples/coverage/src/test_functions.rs b/examples/coverage/src/test_functions.rs new file mode 100644 index 000000000..7db88a867 --- /dev/null +++ b/examples/coverage/src/test_functions.rs @@ -0,0 +1,32 @@ +fn first((value, _): (A, i32), y: B) -> A +where + B: Clone, +{ + value +} + +// foo is generic over A and B + +fn foo1(x: A, y: B) {} + +fn foo2(x: &[T], y: &[T; 1]) +where + T: Clone, +{ + // details elided +} + +fn test() { + let x = [1u8]; + foo2(&x, &x); + foo2(&[1, 2], &x); +} + +extern "Rust" fn foo3() {} + +// async fn regular_example() { } // TODO: Not yet supported + +// Requires std::fmt; +// fn documented() { +// #![doc = "Example"] +// } diff --git a/examples/coverage/src/test_instance.rs b/examples/coverage/src/test_instance.rs new file mode 100644 index 000000000..81f8d1204 --- /dev/null +++ b/examples/coverage/src/test_instance.rs @@ -0,0 +1,21 @@ +// enum SomeEnum { +// None, +// Some(T), +// } + +// trait SomeTrait { +// fn some_fun(&self) -> Self; +// } + +// impl SomeTrait for SomeEnum +// where +// T: SomeTrait, +// { +// #[inline] +// fn some_fun(&self) -> Self { +// match self { +// SomeEnum::Some(x) => SomeEnum::Some(x.some_fun()), +// SomeEnum::None => SomeEnum::None, +// } +// } +// } diff --git a/examples/coverage/src/test_primitives.rs b/examples/coverage/src/test_primitives.rs new file mode 100644 index 000000000..6980f480b --- /dev/null +++ b/examples/coverage/src/test_primitives.rs @@ -0,0 +1,30 @@ +fn test_primtives() { + // bool + let _: bool = false; + let _: bool = true; + + // Numerics + let _: u8 = 12u8; + let _: u16 = 123u16; + let _: u32 = 1234u32; + let _: u64 = 12345u64; + let _: u128 = 123456u128; + let _: usize = 32usize; + + let _: i8 = -12i8; + let _: i16 = 123i16; + let _: i32 = -1234i32; + let _: i64 = 12345i64; + let _: i128 = 123456i128; + let _: isize = -32isize; + + let _: f32 = 1.2f32; + let _: f64 = -1.23f64; + + // Textual + let _: char = 'c'; + let _: &str = "hello world"; + + // Never + // cannot be built +} diff --git a/examples/coverage/src/test_sequence.rs b/examples/coverage/src/test_sequence.rs new file mode 100644 index 000000000..d1539ecae --- /dev/null +++ b/examples/coverage/src/test_sequence.rs @@ -0,0 +1,17 @@ +fn test() { + // Tuple + let _: () = (); + let _: (u8, u16, i8) = (1, 2, 3); + let _: u8 = (1, 2).0; + let _: u8 = (1,).0; + let _: u8 = (1, 2, 3, 4, 5).3; + + // Array + let _: [u8; 0] = []; + let _: [&str; 3] = ["23", "a", "hllo"]; + let _: [u8; 14] = [2; 14]; + + // Slice + let _: &[u8] = &[1, 2, 3, 4]; + let _: &[&str] = &[]; +} diff --git a/examples/coverage/src/test_struct.rs b/examples/coverage/src/test_struct.rs new file mode 100644 index 000000000..a3ba8c7db --- /dev/null +++ b/examples/coverage/src/test_struct.rs @@ -0,0 +1,64 @@ +struct foo<'a, T, const N: usize> { + bar: &'a T, + baz: [T; N], + qux: u8, +} + +// Point {x: 10.0, y: 20.0}; +// NothingInMe {}; +// TuplePoint(10.0, 20.0); +// TuplePoint { 0: 10.0, 1: 20.0 }; // Results in the same value as the above line +// let u = game::User {name: "Joe", age: 35, score: 100_000}; +// some_fn::(Cookie); + +fn test() { + { + struct Gamma; + let a = Gamma; // Gamma unit value. + let b = Gamma {}; // Exact same value as `a`. + } + { + struct Position(i32, i32, i32); + Position(0, 0, 0); // Typical way of creating a tuple struct. + let c = Position; // `c` is a function that takes 3 arguments. + let pos = c(8, 6, 7); // Creates a `Position` value. + } + { + struct Color(u8, u8, u8); + let c1 = Color(0, 0, 0); // Typical way of creating a tuple struct. + let c2 = Color { + 0: 255, + 1: 127, + 2: 0, + }; // Specifying fields by index. + let c3 = Color { 1: 0, ..c2 }; // Fill out all other fields using a base struct. + } + { + struct PointA { + x: i32, + y: i32, + } + let p = PointA { x: 10, y: 11 }; + let px: i32 = p.x; + + let mut p2 = PointA { x: 10, y: 11 }; + p2.x = 10; + p2.y = 14; + } + { + struct PointB(i32, i32); + let p = PointB(10, 11); + let px: i32 = match p { + PointB(x, _) => x, + }; + } + { + struct CookieA; + let c = [CookieA, CookieA {}, CookieA, CookieA {}]; + } + { + struct Cookie {} + const Cookie: Cookie = Cookie {}; + let c = [Cookie, Cookie {}, Cookie, Cookie {}]; + } +} diff --git a/examples/coverage/src/test_trait.rs b/examples/coverage/src/test_trait.rs new file mode 100644 index 000000000..421715775 --- /dev/null +++ b/examples/coverage/src/test_trait.rs @@ -0,0 +1,11 @@ +// Broken.. + +// // Co-inductive trait +// trait TraitA { +// type B : TraitB; +// } + +// trait TraitB { +// fn test(other : U) -> U +// where U: TraitA; +// } diff --git a/examples/default.nix b/examples/default.nix index bd602e515..29f68c404 100644 --- a/examples/default.nix +++ b/examples/default.nix @@ -9,26 +9,7 @@ jq, proverif, }: let - matches = re: path: !builtins.isNull (builtins.match re path); - commonArgs = { - version = "0.0.1"; - src = lib.cleanSourceWith { - src = craneLib.path ./..; - filter = path: type: - # We include only certain files. FStar files under the example - # directory are listed out. Same for proverif (*.pvl) files. - ( matches ".*(Makefile|.*[.](rs|toml|lock|diff|fsti?|pv))$" path - && !matches ".*examples/.*[.]fsti?$" path - ) || ("directory" == type); - }; - doCheck = false; - cargoVendorDir = craneLib.vendorMultipleCargoDeps { - cargoLockList = [ - ./Cargo.lock - ../Cargo.lock - ]; - }; - }; + commonArgs = import ./commonArgs.nix {inherit craneLib lib;}; cargoArtifacts = craneLib.buildDepsOnly commonArgs; in craneLib.mkCargoDerivation (commonArgs diff --git a/flake.nix b/flake.nix index 168556d28..cf7f1e499 100644 --- a/flake.nix +++ b/flake.nix @@ -91,6 +91,12 @@ check-examples = checks.examples; check-readme-coherency = checks.readme-coherency; + coq-coverage-example = pkgs.callPackage ./examples/coverage { + inherit (packages) hax; + inherit (pkgs) coqPackages; + inherit craneLib; + }; + rust-by-example-hax-extraction = pkgs.stdenv.mkDerivation { name = "rust-by-example-hax-extraction"; phases = ["installPhase"]; diff --git a/proof-libs/coq/coq/default.nix b/proof-libs/coq/coq/default.nix new file mode 100644 index 000000000..d0ccfd8f0 --- /dev/null +++ b/proof-libs/coq/coq/default.nix @@ -0,0 +1,22 @@ +{ + stdenv ? (import {}).stdenv, + coqPackages ? (import {}).coqPackages, +}: +stdenv.mkDerivation { + name = "hax-coq-generated-core"; + src = ./generated-core; + buildPhase = '' + coq_makefile -f _CoqProject -o Makefile + make + ''; + installPhase = '' + export DESTDIR=$out + make install + mv $out/nix/store/*/lib $out + rm -rf $out/nix + ''; + buildInputs = [ + coqPackages.coq-record-update + coqPackages.coq + ]; +} diff --git a/proof-libs/coq/coq/generated-core/src/Core_Base_interface_Int.v b/proof-libs/coq/coq/generated-core/src/Core_Base_interface_Int.v index 0fa9edfaf..de6d3af4d 100644 --- a/proof-libs/coq/coq/generated-core/src/Core_Base_interface_Int.v +++ b/proof-libs/coq/coq/generated-core/src/Core_Base_interface_Int.v @@ -441,19 +441,19 @@ Definition impl_219__WORDSIZE : t_HaxInt := Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I16) (Abstraction_f_lift (x) : t_Z); }. -#[globa] Instance t_From_106548803 : t_From ((t_I32)) ((t_I128)) := +#[global] Instance t_From_106548803 : t_From ((t_I32)) ((t_I128)) := { From_f_from := fun (x : t_I128)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I32) (Abstraction_f_lift (x) : t_Z); }. -#[globa] Instance t_From_237552649 : t_From ((t_I64)) ((t_I128)) := +#[global] Instance t_From_237552649 : t_From ((t_I64)) ((t_I128)) := { From_f_from := fun (x : t_I128)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I64) (Abstraction_f_lift (x) : t_Z); }. -#[globa] Instance t_PartialEq_488790252 : t_PartialEq ((t_I128)) ((t_I128)) := +#[global] Instance t_PartialEq_488790252 : t_PartialEq ((t_I128)) ((t_I128)) := { PartialEq_f_eq := fun (self : t_I128) (rhs : t_I128)=> PartialEq_f_eq (z_cmp (Abstraction_f_lift (Clone_f_clone (self))) (Abstraction_f_lift (Clone_f_clone (rhs)))) (Ordering_Equal); @@ -461,7 +461,7 @@ Definition impl_219__WORDSIZE : t_HaxInt := PartialEq_f_ne (z_cmp (Abstraction_f_lift (Clone_f_clone (self))) (Abstraction_f_lift (Clone_f_clone (rhs)))) (Ordering_Equal); }. -#[globa] Instance t_PartialOrd_387128921 : t_PartialOrd ((t_I128)) ((t_I128)) := +#[global] Instance t_PartialOrd_387128921 : t_PartialOrd ((t_I128)) ((t_I128)) := { PartialOrd_f_partial_cmp := fun (self : t_I128) (rhs : t_I128)=> Option_Some (z_cmp (Abstraction_f_lift (Clone_f_clone (self))) (Abstraction_f_lift (Clone_f_clone (rhs)))); @@ -497,38 +497,38 @@ Definition impl_219__WORDSIZE : t_HaxInt := end; }. -#[globa] Instance t_Abstraction_692501606 : t_Abstraction ((t_I64)) := +#[global] Instance t_Abstraction_692501606 : t_Abstraction ((t_I64)) := { Abstraction_f_AbstractType := t_Z; Abstraction_f_lift := fun (self : t_I64)=> I64_f_v self; }. -#[globa] Instance t_From_318313768 : t_From ((t_I8)) ((t_I64)) := +#[global] Instance t_From_318313768 : t_From ((t_I8)) ((t_I64)) := { From_f_from := fun (x : t_I64)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I8) (Abstraction_f_lift (x)); }. -#[globa] Instance t_From_215423074 : t_From ((t_I16)) ((t_I64)) := +#[global] Instance t_From_215423074 : t_From ((t_I16)) ((t_I64)) := { From_f_from := fun (x : t_I64)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I16) (Abstraction_f_lift (x)); }. -#[globa] Instance t_From_221659723 : t_From ((t_I32)) ((t_I64)) := +#[global] Instance t_From_221659723 : t_From ((t_I32)) ((t_I64)) := { From_f_from := fun (x : t_I64)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I32) (Abstraction_f_lift (x)); }. -#[globa] Instance t_From_927453474 : t_From ((t_I128)) ((t_I64)) := +#[global] Instance t_From_927453474 : t_From ((t_I128)) ((t_I64)) := { From_f_from := fun (x : t_I64)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I128) (Abstraction_f_lift (x)); }. -#[globa] Instance t_PartialEq_474861724 : t_PartialEq ((t_I64)) ((t_I64)) := +#[global] Instance t_PartialEq_474861724 : t_PartialEq ((t_I64)) ((t_I64)) := { PartialEq_f_eq := fun (self : t_I64) (rhs : t_I64)=> PartialEq_f_eq (t_PartialEq := _ : t_PartialEq t_Ordering t_Ordering) (z_cmp (Abstraction_f_lift (Clone_f_clone (self))) (Abstraction_f_lift (Clone_f_clone (rhs)))) (Ordering_Equal); @@ -536,7 +536,7 @@ Definition impl_219__WORDSIZE : t_HaxInt := PartialEq_f_ne (t_PartialEq := _ : t_PartialEq t_Ordering t_Ordering) (z_cmp (Abstraction_f_lift (Clone_f_clone (self))) (Abstraction_f_lift (Clone_f_clone (rhs)))) (Ordering_Equal); }. -#[globa] Instance t_PartialOrd_552634265 : t_PartialOrd ((t_I64)) ((t_I64)) := +#[global] Instance t_PartialOrd_552634265 : t_PartialOrd ((t_I64)) ((t_I64)) := { PartialOrd_f_partial_cmp := fun (self : t_I64) (rhs : t_I64)=> Option_Some (z_cmp (Abstraction_f_lift (Clone_f_clone (self))) (Abstraction_f_lift (Clone_f_clone (rhs)))); @@ -572,38 +572,38 @@ Definition impl_219__WORDSIZE : t_HaxInt := end; }. -#[globa] Instance t_Abstraction_493183574 : t_Abstraction ((t_I32)) := +#[global] Instance t_Abstraction_493183574 : t_Abstraction ((t_I32)) := { Abstraction_f_AbstractType := t_Z; Abstraction_f_lift := fun (self : t_I32)=> I32_f_v self; }. -#[globa] Instance t_From_573287156 : t_From ((t_I8)) ((t_I32)) := +#[global] Instance t_From_573287156 : t_From ((t_I8)) ((t_I32)) := { From_f_from := fun (x : t_I32)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I8) (Abstraction_f_lift (x)); }. -#[globa] Instance t_From_278670998 : t_From ((t_I16)) ((t_I32)) := +#[global] Instance t_From_278670998 : t_From ((t_I16)) ((t_I32)) := { From_f_from := fun (x : t_I32)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I16) (Abstraction_f_lift (x)); }. -#[globa] Instance t_From_697572388 : t_From ((t_I64)) ((t_I32)) := +#[global] Instance t_From_697572388 : t_From ((t_I64)) ((t_I32)) := { From_f_from := fun (x : t_I32)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I64) (Abstraction_f_lift (x)); }. -#[globa] Instance t_From_30146175 : t_From ((t_I128)) ((t_I32)) := +#[global] Instance t_From_30146175 : t_From ((t_I128)) ((t_I32)) := { From_f_from := fun (x : t_I32)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I128) (Abstraction_f_lift (x)); }. -#[globa] Instance t_PartialEq_795859780 : t_PartialEq ((t_I32)) ((t_I32)) := +#[global] Instance t_PartialEq_795859780 : t_PartialEq ((t_I32)) ((t_I32)) := { PartialEq_f_eq := fun (self : t_I32) (rhs : t_I32)=> PartialEq_f_eq (t_PartialEq := _ : t_PartialEq t_Ordering t_Ordering) (z_cmp (Abstraction_f_lift (Clone_f_clone (self))) (Abstraction_f_lift (Clone_f_clone (rhs)))) (Ordering_Equal); @@ -611,7 +611,7 @@ Definition impl_219__WORDSIZE : t_HaxInt := PartialEq_f_ne (t_PartialEq := _ : t_PartialEq t_Ordering t_Ordering) (z_cmp (Abstraction_f_lift (Clone_f_clone (self))) (Abstraction_f_lift (Clone_f_clone (rhs)))) (Ordering_Equal); }. -#[globa] Instance t_PartialOrd_126468614 : t_PartialOrd ((t_I32)) ((t_I32)) := +#[global] Instance t_PartialOrd_126468614 : t_PartialOrd ((t_I32)) ((t_I32)) := { PartialOrd_f_partial_cmp := fun (self : t_I32) (rhs : t_I32)=> Option_Some (z_cmp (Abstraction_f_lift (Clone_f_clone (self))) (Abstraction_f_lift (Clone_f_clone (rhs)))); @@ -647,38 +647,38 @@ Definition impl_219__WORDSIZE : t_HaxInt := end; }. -#[globa] Instance t_Abstraction_8671741 : t_Abstraction ((t_I16)) := +#[global] Instance t_Abstraction_8671741 : t_Abstraction ((t_I16)) := { Abstraction_f_AbstractType := t_Z; Abstraction_f_lift := fun (self : t_I16)=> I16_f_v self; }. -#[globa] Instance t_From_767089390 : t_From ((t_I8)) ((t_I16)) := +#[global] Instance t_From_767089390 : t_From ((t_I8)) ((t_I16)) := { From_f_from := fun (x : t_I16)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I8) (Abstraction_f_lift (x)); }. -#[globa] Instance t_From_339600325 : t_From ((t_I32)) ((t_I16)) := +#[global] Instance t_From_339600325 : t_From ((t_I32)) ((t_I16)) := { From_f_from := fun (x : t_I16)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I32) (Abstraction_f_lift (x)); }. -#[globa] Instance t_From_929749154 : t_From ((t_I64)) ((t_I16)) := +#[global] Instance t_From_929749154 : t_From ((t_I64)) ((t_I16)) := { From_f_from := fun (x : t_I16)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I64) (Abstraction_f_lift (x)); }. -#[globa] Instance t_From_366897745 : t_From ((t_I128)) ((t_I16)) := +#[global] Instance t_From_366897745 : t_From ((t_I128)) ((t_I16)) := { From_f_from := fun (x : t_I16)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I128) (Abstraction_f_lift (x)); }. -#[globa] Instance t_PartialEq_359538097 : t_PartialEq ((t_I16)) ((t_I16)) := +#[global] Instance t_PartialEq_359538097 : t_PartialEq ((t_I16)) ((t_I16)) := { PartialEq_f_eq := fun (self : t_I16) (rhs : t_I16)=> PartialEq_f_eq (t_PartialEq := _ : t_PartialEq t_Ordering t_Ordering) (z_cmp (Abstraction_f_lift (Clone_f_clone (self))) (Abstraction_f_lift (Clone_f_clone (rhs)))) (Ordering_Equal); @@ -686,7 +686,7 @@ Definition impl_219__WORDSIZE : t_HaxInt := PartialEq_f_ne (t_PartialEq := _ : t_PartialEq t_Ordering t_Ordering) (z_cmp (Abstraction_f_lift (Clone_f_clone (self))) (Abstraction_f_lift (Clone_f_clone (rhs)))) (Ordering_Equal); }. -#[globa] Instance t_PartialOrd_524872806 : t_PartialOrd ((t_I16)) ((t_I16)) := +#[global] Instance t_PartialOrd_524872806 : t_PartialOrd ((t_I16)) ((t_I16)) := { PartialOrd_f_partial_cmp := fun (self : t_I16) (rhs : t_I16)=> Option_Some (z_cmp (Abstraction_f_lift (Clone_f_clone (self))) (Abstraction_f_lift (Clone_f_clone (rhs)))); @@ -722,38 +722,38 @@ Definition impl_219__WORDSIZE : t_HaxInt := end; }. -#[globa] Instance t_Abstraction_78490685 : t_Abstraction ((t_I8)) := +#[global] Instance t_Abstraction_78490685 : t_Abstraction ((t_I8)) := { Abstraction_f_AbstractType := t_Z; Abstraction_f_lift := fun (self : t_I8)=> I8_f_v self; }. -#[globa] Instance t_From_995744130 : t_From ((t_I16)) ((t_I8)) := +#[global] Instance t_From_995744130 : t_From ((t_I16)) ((t_I8)) := { From_f_from := fun (x : t_I8)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I16) (Abstraction_f_lift (x)); }. -#[globa] Instance t_From_513826093 : t_From ((t_I32)) ((t_I8)) := +#[global] Instance t_From_513826093 : t_From ((t_I32)) ((t_I8)) := { From_f_from := fun (x : t_I8)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I32) (Abstraction_f_lift (x)); }. -#[globa] Instance t_From_843443999 : t_From ((t_I64)) ((t_I8)) := +#[global] Instance t_From_843443999 : t_From ((t_I64)) ((t_I8)) := { From_f_from := fun (x : t_I8)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I64) (Abstraction_f_lift (x)); }. -#[globa] Instance t_From_532428771 : t_From ((t_I128)) ((t_I8)) := +#[global] Instance t_From_532428771 : t_From ((t_I128)) ((t_I8)) := { From_f_from := fun (x : t_I8)=> Concretization_f_concretize(t_Concretization := _ : t_Concretization t_Z t_I128) (Abstraction_f_lift (x)); }. -#[globa] Instance t_PartialEq_594648758 : t_PartialEq ((t_I8)) ((t_I8)) := +#[global] Instance t_PartialEq_594648758 : t_PartialEq ((t_I8)) ((t_I8)) := { PartialEq_f_eq := fun (self : t_I8) (rhs : t_I8)=> PartialEq_f_eq (t_PartialEq := _ : t_PartialEq t_Ordering t_Ordering) (z_cmp (Abstraction_f_lift (Clone_f_clone (self))) (Abstraction_f_lift (Clone_f_clone (rhs)))) (Ordering_Equal); @@ -761,7 +761,7 @@ Definition impl_219__WORDSIZE : t_HaxInt := PartialEq_f_ne (t_PartialEq := _ : t_PartialEq t_Ordering t_Ordering) (z_cmp (Abstraction_f_lift (Clone_f_clone (self))) (Abstraction_f_lift (Clone_f_clone (rhs)))) (Ordering_Equal); }. -#[globa] Instance t_PartialOrd_221919414 : t_PartialOrd ((t_I8)) ((t_I8)) := +#[global] Instance t_PartialOrd_221919414 : t_PartialOrd ((t_I8)) ((t_I8)) := { PartialOrd_f_partial_cmp := fun (self : t_I8) (rhs : t_I8)=> Option_Some (z_cmp (Abstraction_f_lift (Clone_f_clone (self))) (Abstraction_f_lift (Clone_f_clone (rhs)))); @@ -797,14 +797,14 @@ Definition impl_219__WORDSIZE : t_HaxInt := end; }. -#[globa] Instance t_Abstraction_133243863 : t_Abstraction ((t_U128)) := +#[global] Instance t_Abstraction_133243863 : t_Abstraction ((t_U128)) := { Abstraction_f_AbstractType := t_HaxInt; Abstraction_f_lift := fun (self : t_U128)=> U128_f_v self; }. -#[globa] Instance t_PartialEq_792968920 : t_PartialEq ((t_U128)) ((t_U128)) := +#[global] Instance t_PartialEq_792968920 : t_PartialEq ((t_U128)) ((t_U128)) := { PartialEq_f_eq := fun (self : t_U128) (rhs : t_U128)=> PartialEq_f_eq (t_PartialEq := _ : t_PartialEq t_Ordering t_Ordering) (haxint_cmp (Abstraction_f_lift (Clone_f_clone (self))) (Abstraction_f_lift (Clone_f_clone (rhs)))) (Ordering_Equal); @@ -812,7 +812,7 @@ Definition impl_219__WORDSIZE : t_HaxInt := PartialEq_f_ne (t_PartialEq := _ : t_PartialEq t_Ordering t_Ordering) (haxint_cmp (Abstraction_f_lift (Clone_f_clone (self))) (Abstraction_f_lift (Clone_f_clone (rhs)))) (Ordering_Equal); }. -#[globa] Instance t_PartialOrd_168269581 : t_PartialOrd ((t_U128)) ((t_U128)) := +#[global] Instance t_PartialOrd_168269581 : t_PartialOrd ((t_U128)) ((t_U128)) := { PartialOrd_f_partial_cmp := fun (self : t_U128) (rhs : t_U128)=> Option_Some (haxint_cmp (Abstraction_f_lift (Clone_f_clone (self))) (Abstraction_f_lift (Clone_f_clone (rhs)))); @@ -848,14 +848,14 @@ Definition impl_219__WORDSIZE : t_HaxInt := end; }. -#[globa] Instance t_Abstraction_219241396 : t_Abstraction ((t_U64)) := +#[global] Instance t_Abstraction_219241396 : t_Abstraction ((t_U64)) := { Abstraction_f_AbstractType := t_HaxInt; Abstraction_f_lift := fun (self : t_U64)=> U64_f_v self; }. -#[globa] Instance t_PartialEq_162514109 : t_PartialEq ((t_U64)) ((t_U64)) := +#[global] Instance t_PartialEq_162514109 : t_PartialEq ((t_U64)) ((t_U64)) := { PartialEq_f_eq := fun (self : t_U64) (rhs : t_U64)=> PartialEq_f_eq (t_PartialEq := _ : t_PartialEq t_Ordering t_Ordering) (haxint_cmp (Abstraction_f_lift (Clone_f_clone (self))) (Abstraction_f_lift (Clone_f_clone (rhs)))) (Ordering_Equal); @@ -863,7 +863,7 @@ Definition impl_219__WORDSIZE : t_HaxInt := PartialEq_f_ne (t_PartialEq := _ : t_PartialEq t_Ordering t_Ordering) (haxint_cmp (Abstraction_f_lift (Clone_f_clone (self))) (Abstraction_f_lift (Clone_f_clone (rhs)))) (Ordering_Equal); }. -#[globa] Instance t_PartialOrd_210240032 : t_PartialOrd ((t_U64)) ((t_U64)) := +#[global] Instance t_PartialOrd_210240032 : t_PartialOrd ((t_U64)) ((t_U64)) := { PartialOrd_f_partial_cmp := fun (self : t_U64) (rhs : t_U64)=> Option_Some (haxint_cmp (Abstraction_f_lift (Clone_f_clone (self))) (Abstraction_f_lift (Clone_f_clone (rhs)))); @@ -899,14 +899,14 @@ Definition impl_219__WORDSIZE : t_HaxInt := end; }. -#[globa] Instance t_Abstraction_517050128 : t_Abstraction ((t_U32)) := +#[global] Instance t_Abstraction_517050128 : t_Abstraction ((t_U32)) := { Abstraction_f_AbstractType := t_HaxInt; Abstraction_f_lift := fun (self : t_U32)=> U32_f_v self; }. -#[globa] Instance t_PartialEq_894496962 : t_PartialEq ((t_U32)) ((t_U32)) := +#[global] Instance t_PartialEq_894496962 : t_PartialEq ((t_U32)) ((t_U32)) := { PartialEq_f_eq := fun (self : t_U32) (rhs : t_U32)=> PartialEq_f_eq (t_PartialEq := _ : t_PartialEq t_Ordering t_Ordering) (haxint_cmp (Abstraction_f_lift (Clone_f_clone (self))) (Abstraction_f_lift (Clone_f_clone (rhs)))) (Ordering_Equal); @@ -914,7 +914,7 @@ Definition impl_219__WORDSIZE : t_HaxInt := PartialEq_f_ne (t_PartialEq := _ : t_PartialEq t_Ordering t_Ordering) (haxint_cmp (Abstraction_f_lift (Clone_f_clone (self))) (Abstraction_f_lift (Clone_f_clone (rhs)))) (Ordering_Equal); }. -#[globa] Instance t_PartialOrd_534404445 : t_PartialOrd ((t_U32)) ((t_U32)) := +#[global] Instance t_PartialOrd_534404445 : t_PartialOrd ((t_U32)) ((t_U32)) := { PartialOrd_f_partial_cmp := fun (self : t_U32) (rhs : t_U32)=> Option_Some (haxint_cmp (Abstraction_f_lift (Clone_f_clone (self))) (Abstraction_f_lift (Clone_f_clone (rhs)))); @@ -950,14 +950,14 @@ Definition impl_219__WORDSIZE : t_HaxInt := end; }. -#[globa] Instance t_Abstraction_994821584 : t_Abstraction ((t_U16)) := +#[global] Instance t_Abstraction_994821584 : t_Abstraction ((t_U16)) := { Abstraction_f_AbstractType := t_HaxInt; Abstraction_f_lift := fun (self : t_U16)=> U16_f_v self; }. -#[globa] Instance t_PartialEq_603208302 : t_PartialEq ((t_U16)) ((t_U16)) := +#[global] Instance t_PartialEq_603208302 : t_PartialEq ((t_U16)) ((t_U16)) := { PartialEq_f_eq := fun (self : t_U16) (rhs : t_U16)=> PartialEq_f_eq (t_PartialEq := _ : t_PartialEq t_Ordering t_Ordering) (haxint_cmp (Abstraction_f_lift (Clone_f_clone (self))) (Abstraction_f_lift (Clone_f_clone (rhs)))) (Ordering_Equal); @@ -965,7 +965,7 @@ Definition impl_219__WORDSIZE : t_HaxInt := PartialEq_f_ne (t_PartialEq := _ : t_PartialEq t_Ordering t_Ordering) (haxint_cmp (Abstraction_f_lift (Clone_f_clone (self))) (Abstraction_f_lift (Clone_f_clone (rhs)))) (Ordering_Equal); }. -#[globa] Instance t_PartialOrd_595325431 : t_PartialOrd ((t_U16)) ((t_U16)) := +#[global] Instance t_PartialOrd_595325431 : t_PartialOrd ((t_U16)) ((t_U16)) := { PartialOrd_f_partial_cmp := fun (self : t_U16) (rhs : t_U16)=> Option_Some (haxint_cmp (Abstraction_f_lift (Clone_f_clone (self))) (Abstraction_f_lift (Clone_f_clone (rhs)))); @@ -1001,14 +1001,14 @@ Definition impl_219__WORDSIZE : t_HaxInt := end; }. -#[globa] Instance t_Abstraction_789996186 : t_Abstraction ((t_U8)) := +#[global] Instance t_Abstraction_789996186 : t_Abstraction ((t_U8)) := { Abstraction_f_AbstractType := t_HaxInt; Abstraction_f_lift := fun (self : t_U8)=> U8_f_v self; }. -#[globa] Instance t_PartialEq_774173636 : t_PartialEq ((t_U8)) ((t_U8)) := +#[global] Instance t_PartialEq_774173636 : t_PartialEq ((t_U8)) ((t_U8)) := { PartialEq_f_eq := fun (self : t_U8) (rhs : t_U8)=> PartialEq_f_eq (t_PartialEq := _ : t_PartialEq t_Ordering t_Ordering) (haxint_cmp (Abstraction_f_lift (Clone_f_clone (self))) (Abstraction_f_lift (Clone_f_clone (rhs)))) (Ordering_Equal); @@ -1016,7 +1016,7 @@ Definition impl_219__WORDSIZE : t_HaxInt := PartialEq_f_ne (t_PartialEq := _ : t_PartialEq t_Ordering t_Ordering) (haxint_cmp (Abstraction_f_lift (Clone_f_clone (self))) (Abstraction_f_lift (Clone_f_clone (rhs)))) (Ordering_Equal); }. -#[globa] Instance t_PartialOrd_577399304 : t_PartialOrd ((t_U8)) ((t_U8)) := +#[global] Instance t_PartialOrd_577399304 : t_PartialOrd ((t_U8)) ((t_U8)) := { PartialOrd_f_partial_cmp := fun (self : t_U8) (rhs : t_U8)=> Option_Some (haxint_cmp (Abstraction_f_lift (Clone_f_clone (self))) (Abstraction_f_lift (Clone_f_clone (rhs)))); @@ -1052,1095 +1052,1095 @@ Definition impl_219__WORDSIZE : t_HaxInt := end; }. -#[globa] Instance t_Neg_375517228 : t_Neg ((t_I128)) := +#[global] Instance t_Neg_375517228 : t_Neg ((t_I128)) := { Neg_f_Output := t_I128; Neg_f_neg := fun (self : t_I128)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I128) (z_neg (Abstraction_f_lift (self))); }. -#[globa] Instance t_BitOr_938342430 : t_BitOr ((t_I128)) ((t_I128)) := +#[global] Instance t_BitOr_938342430 : t_BitOr ((t_I128)) ((t_I128)) := { BitOr_f_Output := t_I128; BitOr_f_bitor := fun (self : t_I128) (rhs : t_I128)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I128) (z_bitor (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Neg_210530286 : t_Neg ((t_I64)) := +#[global] Instance t_Neg_210530286 : t_Neg ((t_I64)) := { Neg_f_Output := t_I64; Neg_f_neg := fun (self : t_I64)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I64) (z_neg (Abstraction_f_lift (self))); }. -#[globa] Instance t_BitOr_329754853 : t_BitOr ((t_I64)) ((t_I64)) := +#[global] Instance t_BitOr_329754853 : t_BitOr ((t_I64)) ((t_I64)) := { BitOr_f_Output := t_I64; BitOr_f_bitor := fun (self : t_I64) (rhs : t_I64)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I64) (z_bitor (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Neg_104016941 : t_Neg ((t_I32)) := +#[global] Instance t_Neg_104016941 : t_Neg ((t_I32)) := { Neg_f_Output := t_I32; Neg_f_neg := fun (self : t_I32)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I32) (z_neg (Abstraction_f_lift (self))); }. -#[globa] Instance t_BitOr_840483685 : t_BitOr ((t_I32)) ((t_I32)) := +#[global] Instance t_BitOr_840483685 : t_BitOr ((t_I32)) ((t_I32)) := { BitOr_f_Output := t_I32; BitOr_f_bitor := fun (self : t_I32) (rhs : t_I32)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I32) (z_bitor (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Neg_1063990797 : t_Neg ((t_I16)) := +#[global] Instance t_Neg_1063990797 : t_Neg ((t_I16)) := { Neg_f_Output := t_I16; Neg_f_neg := fun (self : t_I16)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I16) (z_neg (Abstraction_f_lift (self))); }. -#[globa] Instance t_BitOr_450806124 : t_BitOr ((t_I16)) ((t_I16)) := +#[global] Instance t_BitOr_450806124 : t_BitOr ((t_I16)) ((t_I16)) := { BitOr_f_Output := t_I16; BitOr_f_bitor := fun (self : t_I16) (rhs : t_I16)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I16) (z_bitor (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Neg_979719905 : t_Neg ((t_I8)) := +#[global] Instance t_Neg_979719905 : t_Neg ((t_I8)) := { Neg_f_Output := t_I8; Neg_f_neg := fun (self : t_I8)=> Concretization_f_concretize (z_neg (Abstraction_f_lift (self))); }. -#[globa] Instance t_BitOr_828862178 : t_BitOr ((t_I8)) ((t_I8)) := +#[global] Instance t_BitOr_828862178 : t_BitOr ((t_I8)) ((t_I8)) := { BitOr_f_Output := t_I8; BitOr_f_bitor := fun (self : t_I8) (rhs : t_I8)=> Concretization_f_concretize (z_bitor (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Add_749575336 : t_Add ((t_I128)) ((t_I128)) := +#[global] Instance t_Add_749575336 : t_Add ((t_I128)) ((t_I128)) := { Add_f_Output := t_I128; Add_f_add := fun (self : t_I128) (rhs : t_I128)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I128) (z_add (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Sub_800692471 : t_Sub ((t_I128)) ((t_I128)) := +#[global] Instance t_Sub_800692471 : t_Sub ((t_I128)) ((t_I128)) := { Sub_f_Output := t_I128; Sub_f_sub := fun (self : t_I128) (rhs : t_I128)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I128) (z_sub (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Add_87367909 : t_Add ((t_I64)) ((t_I64)) := +#[global] Instance t_Add_87367909 : t_Add ((t_I64)) ((t_I64)) := { Add_f_Output := t_I64; Add_f_add := fun (self : t_I64) (rhs : t_I64)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I64) (z_add (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Sub_741383133 : t_Sub ((t_I64)) ((t_I64)) := +#[global] Instance t_Sub_741383133 : t_Sub ((t_I64)) ((t_I64)) := { Sub_f_Output := t_I64; Sub_f_sub := fun (self : t_I64) (rhs : t_I64)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I64) (z_sub (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Add_574043038 : t_Add ((t_I32)) ((t_I32)) := +#[global] Instance t_Add_574043038 : t_Add ((t_I32)) ((t_I32)) := { Add_f_Output := t_I32; Add_f_add := fun (self : t_I32) (rhs : t_I32)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I32) (z_add (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Sub_699874712 : t_Sub ((t_I32)) ((t_I32)) := +#[global] Instance t_Sub_699874712 : t_Sub ((t_I32)) ((t_I32)) := { Sub_f_Output := t_I32; Sub_f_sub := fun (self : t_I32) (rhs : t_I32)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I32) (z_sub (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Add_413164706 : t_Add ((t_I16)) ((t_I16)) := +#[global] Instance t_Add_413164706 : t_Add ((t_I16)) ((t_I16)) := { Add_f_Output := t_I16; Add_f_add := fun (self : t_I16) (rhs : t_I16)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I16) (z_add (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Sub_544358249 : t_Sub ((t_I16)) ((t_I16)) := +#[global] Instance t_Sub_544358249 : t_Sub ((t_I16)) ((t_I16)) := { Sub_f_Output := t_I16; Sub_f_sub := fun (self : t_I16) (rhs : t_I16)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I16) (z_sub (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Add_335735231 : t_Add ((t_I8)) ((t_I8)) := +#[global] Instance t_Add_335735231 : t_Add ((t_I8)) ((t_I8)) := { Add_f_Output := t_I8; Add_f_add := fun (self : t_I8) (rhs : t_I8)=> Concretization_f_concretize (z_add (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Sub_257575332 : t_Sub ((t_I8)) ((t_I8)) := +#[global] Instance t_Sub_257575332 : t_Sub ((t_I8)) ((t_I8)) := { Sub_f_Output := t_I8; Sub_f_sub := fun (self : t_I8) (rhs : t_I8)=> Concretization_f_concretize (z_sub (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Concretization_943450188 : t_Concretization ((t_HaxInt)) ((t_U128)) := +#[global] Instance t_Concretization_943450188 : t_Concretization ((t_HaxInt)) ((t_U128)) := { Concretization_f_concretize := fun (self : t_HaxInt)=> Build_t_U128 (haxint_rem (self) (v_WORDSIZE_128_)); }. -#[globa] Instance t_From_355161674 : t_From ((t_U128)) ((t_U8)) := +#[global] Instance t_From_355161674 : t_From ((t_U128)) ((t_U8)) := { From_f_from := fun (x : t_U8)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U128) (Abstraction_f_lift (x)); }. -#[globa] Instance t_From_739905379 : t_From ((t_U128)) ((t_U16)) := +#[global] Instance t_From_739905379 : t_From ((t_U128)) ((t_U16)) := { From_f_from := fun (x : t_U16)=> Concretization_f_concretize(t_Concretization := _ : t_Concretization t_HaxInt t_U128) (Abstraction_f_lift (x)); }. -#[globa] Instance t_From_487010006 : t_From ((t_U128)) ((t_U32)) := +#[global] Instance t_From_487010006 : t_From ((t_U128)) ((t_U32)) := { From_f_from := fun (x : t_U32)=> Concretization_f_concretize(t_Concretization := _ : t_Concretization t_HaxInt t_U128) (Abstraction_f_lift (x)); }. -#[globa] Instance t_From_665417617 : t_From ((t_U128)) ((t_U64)) := +#[global] Instance t_From_665417617 : t_From ((t_U128)) ((t_U64)) := { From_f_from := fun (x : t_U64)=> Concretization_f_concretize(t_Concretization := _ : t_Concretization t_HaxInt t_U128) (Abstraction_f_lift (x)); }. -#[globa] Instance t_Concretization_10977439 : t_Concretization ((t_HaxInt)) ((t_U64)) := +#[global] Instance t_Concretization_10977439 : t_Concretization ((t_HaxInt)) ((t_U64)) := { Concretization_f_concretize := fun (self : t_HaxInt)=> Build_t_U64 (haxint_rem (self) (v_WORDSIZE_64_)); }. -#[globa] Instance t_From_746191059 : t_From ((t_U64)) ((t_U8)) := +#[global] Instance t_From_746191059 : t_From ((t_U64)) ((t_U8)) := { From_f_from := fun (x : t_U8)=> Concretization_f_concretize(t_Concretization := _ : t_Concretization t_HaxInt t_U64) (Abstraction_f_lift (x)); }. -#[globa] Instance t_From_598353876 : t_From ((t_U64)) ((t_U16)) := +#[global] Instance t_From_598353876 : t_From ((t_U64)) ((t_U16)) := { From_f_from := fun (x : t_U16)=> Concretization_f_concretize(t_Concretization := _ : t_Concretization t_HaxInt t_U64) (Abstraction_f_lift (x)); }. -#[globa] Instance t_From_293255347 : t_From ((t_U64)) ((t_U32)) := +#[global] Instance t_From_293255347 : t_From ((t_U64)) ((t_U32)) := { From_f_from := fun (x : t_U32)=> Concretization_f_concretize(t_Concretization := _ : t_Concretization t_HaxInt t_U64) (Abstraction_f_lift (x)); }. -#[globa] Instance t_From_478031507 : t_From ((t_U64)) ((t_U128)) := +#[global] Instance t_From_478031507 : t_From ((t_U64)) ((t_U128)) := { From_f_from := fun (x : t_U128)=> Concretization_f_concretize(t_Concretization := _ : t_Concretization t_HaxInt t_U64) (Abstraction_f_lift (x)); }. -#[globa] Instance t_Concretization_264065114 : t_Concretization ((t_HaxInt)) ((t_U32)) := +#[global] Instance t_Concretization_264065114 : t_Concretization ((t_HaxInt)) ((t_U32)) := { Concretization_f_concretize := fun (self : t_HaxInt)=> Build_t_U32 (haxint_rem (self) (v_WORDSIZE_32_)); }. -#[globa] Instance t_From_675834555 : t_From ((t_U32)) ((t_U8)) := +#[global] Instance t_From_675834555 : t_From ((t_U32)) ((t_U8)) := { From_f_from := fun (x : t_U8)=> Concretization_f_concretize(t_Concretization := _ : t_Concretization t_HaxInt t_U32) (Abstraction_f_lift (x)); }. -#[globa] Instance t_From_410569540 : t_From ((t_U32)) ((t_U16)) := +#[global] Instance t_From_410569540 : t_From ((t_U32)) ((t_U16)) := { From_f_from := fun (x : t_U16)=> Concretization_f_concretize(t_Concretization := _ : t_Concretization t_HaxInt t_U32) (Abstraction_f_lift (x)); }. -#[globa] Instance t_From_616913228 : t_From ((t_U32)) ((t_U64)) := +#[global] Instance t_From_616913228 : t_From ((t_U32)) ((t_U64)) := { From_f_from := fun (x : t_U64)=> Concretization_f_concretize(t_Concretization := _ : t_Concretization t_HaxInt t_U32) (Abstraction_f_lift (x)); }. -#[globa] Instance t_From_376625380 : t_From ((t_U32)) ((t_U128)) := +#[global] Instance t_From_376625380 : t_From ((t_U32)) ((t_U128)) := { From_f_from := fun (x : t_U128)=> Concretization_f_concretize(t_Concretization := _ : t_Concretization t_HaxInt t_U32) (Abstraction_f_lift (x)); }. -#[globa] Instance t_Concretization_656994795 : t_Concretization ((t_HaxInt)) ((t_U16)) := +#[global] Instance t_Concretization_656994795 : t_Concretization ((t_HaxInt)) ((t_U16)) := { Concretization_f_concretize := fun (self : t_HaxInt)=> Build_t_U16 (haxint_rem (self) (v_WORDSIZE_16_)); }. -#[globa] Instance t_From_352276566 : t_From ((t_U16)) ((t_U8)) := +#[global] Instance t_From_352276566 : t_From ((t_U16)) ((t_U8)) := { From_f_from := fun (x : t_U8)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U16) (Abstraction_f_lift (x)); }. -#[globa] Instance t_From_699842532 : t_From ((t_U16)) ((t_U32)) := +#[global] Instance t_From_699842532 : t_From ((t_U16)) ((t_U32)) := { From_f_from := fun (x : t_U32)=> Concretization_f_concretize(t_Concretization := _ : t_Concretization t_HaxInt t_U16) (Abstraction_f_lift (x)); }. -#[globa] Instance t_From_326646767 : t_From ((t_U16)) ((t_U64)) := +#[global] Instance t_From_326646767 : t_From ((t_U16)) ((t_U64)) := { From_f_from := fun (x : t_U64)=> Concretization_f_concretize(t_Concretization := _ : t_Concretization t_HaxInt t_U16) (Abstraction_f_lift (x)); }. -#[globa] Instance t_From_604186294 : t_From ((t_U16)) ((t_U128)) := +#[global] Instance t_From_604186294 : t_From ((t_U16)) ((t_U128)) := { From_f_from := fun (x : t_U128)=> Concretization_f_concretize(t_Concretization := _ : t_Concretization t_HaxInt t_U16) (Abstraction_f_lift (x)); }. -#[globa] Instance t_Concretization_492312374 : t_Concretization ((t_HaxInt)) ((t_U8)) := +#[global] Instance t_Concretization_492312374 : t_Concretization ((t_HaxInt)) ((t_U8)) := { Concretization_f_concretize := fun (self : t_HaxInt)=> Build_t_U8 (haxint_rem (self) (v_WORDSIZE_8_)); }. -#[globa] Instance t_From_374313775 : t_From ((t_U8)) ((t_U16)) := +#[global] Instance t_From_374313775 : t_From ((t_U8)) ((t_U16)) := { From_f_from := fun (x : t_U16)=> Concretization_f_concretize(t_Concretization := _ : t_Concretization t_HaxInt t_U8) (Abstraction_f_lift (x)); }. -#[globa] Instance t_From_42776580 : t_From ((t_U8)) ((t_U32)) := +#[global] Instance t_From_42776580 : t_From ((t_U8)) ((t_U32)) := { From_f_from := fun (x : t_U32)=> Concretization_f_concretize(t_Concretization := _ : t_Concretization t_HaxInt t_U8) (Abstraction_f_lift (x)); }. -#[globa] Instance t_From_480314375 : t_From ((t_U8)) ((t_U64)) := +#[global] Instance t_From_480314375 : t_From ((t_U8)) ((t_U64)) := { From_f_from := fun (x : t_U64)=> Concretization_f_concretize(t_Concretization := _ : t_Concretization t_HaxInt t_U8) (Abstraction_f_lift (x)); }. -#[globa] Instance t_From_135782329 : t_From ((t_U8)) ((t_U128)) := +#[global] Instance t_From_135782329 : t_From ((t_U8)) ((t_U128)) := { From_f_from := fun (x : t_U128)=> Concretization_f_concretize(t_Concretization := _ : t_Concretization t_HaxInt t_U8) (Abstraction_f_lift (x)); }. -#[globa] Instance t_Mul_180009375 : t_Mul ((t_I128)) ((t_I128)) := +#[global] Instance t_Mul_180009375 : t_Mul ((t_I128)) ((t_I128)) := { Mul_f_Output := t_I128; Mul_f_mul := fun (self : t_I128) (rhs : t_I128)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I128) (z_mul (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Mul_1051209688 : t_Mul ((t_I64)) ((t_I64)) := +#[global] Instance t_Mul_1051209688 : t_Mul ((t_I64)) ((t_I64)) := { Mul_f_Output := t_I64; Mul_f_mul := fun (self : t_I64) (rhs : t_I64)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I64) (z_mul (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Mul_481497752 : t_Mul ((t_I32)) ((t_I32)) := +#[global] Instance t_Mul_481497752 : t_Mul ((t_I32)) ((t_I32)) := { Mul_f_Output := t_I32; Mul_f_mul := fun (self : t_I32) (rhs : t_I32)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I32) (z_mul (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Mul_768005208 : t_Mul ((t_I16)) ((t_I16)) := +#[global] Instance t_Mul_768005208 : t_Mul ((t_I16)) ((t_I16)) := { Mul_f_Output := t_I16; Mul_f_mul := fun (self : t_I16) (rhs : t_I16)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I16) (z_mul (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Mul_1057691929 : t_Mul ((t_I8)) ((t_I8)) := +#[global] Instance t_Mul_1057691929 : t_Mul ((t_I8)) ((t_I8)) := { Mul_f_Output := t_I8; Mul_f_mul := fun (self : t_I8) (rhs : t_I8)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I8) (z_mul (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Neg_200638412 : t_Neg ((t_U128)) := +#[global] Instance t_Neg_200638412 : t_Neg ((t_U128)) := { Neg_f_Output := t_U128; Neg_f_neg := fun (self : t_U128)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U128) (haxint_sub (v_WORDSIZE_128_) (haxint_rem (Abstraction_f_lift (self)) (v_WORDSIZE_128_))); }. -#[globa] Instance t_Mul_508073751 : t_Mul ((t_U128)) ((t_U128)) := +#[global] Instance t_Mul_508073751 : t_Mul ((t_U128)) ((t_U128)) := { Mul_f_Output := t_U128; Mul_f_mul := fun (self : t_U128) (rhs : t_U128)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U128) (haxint_mul (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Rem_184769952 : t_Rem ((t_U128)) ((t_U128)) := +#[global] Instance t_Rem_184769952 : t_Rem ((t_U128)) ((t_U128)) := { Rem_f_Output := t_U128; Rem_f_rem := fun (self : t_U128) (rhs : t_U128)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U128) (haxint_rem (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Add_74062568 : t_Add ((t_U128)) ((t_U128)) := +#[global] Instance t_Add_74062568 : t_Add ((t_U128)) ((t_U128)) := { Add_f_Output := t_U128; Add_f_add := fun (self : t_U128) (rhs : t_U128)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U128) (haxint_add (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Div_697142148 : t_Div ((t_U128)) ((t_U128)) := +#[global] Instance t_Div_697142148 : t_Div ((t_U128)) ((t_U128)) := { Div_f_Output := t_U128; Div_f_div := fun (self : t_U128) (rhs : t_U128)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U128) (haxint_div (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shl_912131656 : t_Shl ((t_U128)) ((t_U8)) := +#[global] Instance t_Shl_912131656 : t_Shl ((t_U128)) ((t_U8)) := { Shl_f_Output := t_U128; Shl_f_shl := fun (self : t_U128) (rhs : t_U8)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U128) (haxint_shl (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shl_188720840 : t_Shl ((t_U128)) ((t_U16)) := +#[global] Instance t_Shl_188720840 : t_Shl ((t_U128)) ((t_U16)) := { Shl_f_Output := t_U128; Shl_f_shl := fun (self : t_U128) (rhs : t_U16)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U128) (haxint_shl (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shl_674581806 : t_Shl ((t_U128)) ((t_U32)) := +#[global] Instance t_Shl_674581806 : t_Shl ((t_U128)) ((t_U32)) := { Shl_f_Output := t_U128; Shl_f_shl := fun (self : t_U128) (rhs : t_U32)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U128) (haxint_shl (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shl_230523808 : t_Shl ((t_U128)) ((t_U64)) := +#[global] Instance t_Shl_230523808 : t_Shl ((t_U128)) ((t_U64)) := { Shl_f_Output := t_U128; Shl_f_shl := fun (self : t_U128) (rhs : t_U64)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U128) (haxint_shl (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shl_304350501 : t_Shl ((t_U128)) ((t_U128)) := +#[global] Instance t_Shl_304350501 : t_Shl ((t_U128)) ((t_U128)) := { Shl_f_Output := t_U128; Shl_f_shl := fun (self : t_U128) (rhs : t_U128)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U128) (haxint_shl (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shr_584068908 : t_Shr ((t_U128)) ((t_U8)) := +#[global] Instance t_Shr_584068908 : t_Shr ((t_U128)) ((t_U8)) := { Shr_f_Output := t_U128; Shr_f_shr := fun (self : t_U128) (rhs : t_U8)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U128) (haxint_shr (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shr_73833277 : t_Shr ((t_U128)) ((t_U16)) := +#[global] Instance t_Shr_73833277 : t_Shr ((t_U128)) ((t_U16)) := { Shr_f_Output := t_U128; Shr_f_shr := fun (self : t_U128) (rhs : t_U16)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U128) (haxint_shr (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shr_50912121 : t_Shr ((t_U128)) ((t_U32)) := +#[global] Instance t_Shr_50912121 : t_Shr ((t_U128)) ((t_U32)) := { Shr_f_Output := t_U128; Shr_f_shr := fun (self : t_U128) (rhs : t_U32)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U128) (haxint_shr (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shr_282345299 : t_Shr ((t_U128)) ((t_U64)) := +#[global] Instance t_Shr_282345299 : t_Shr ((t_U128)) ((t_U64)) := { Shr_f_Output := t_U128; Shr_f_shr := fun (self : t_U128) (rhs : t_U64)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U128) (haxint_shr (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shr_354892033 : t_Shr ((t_U128)) ((t_U128)) := +#[global] Instance t_Shr_354892033 : t_Shr ((t_U128)) ((t_U128)) := { Shr_f_Output := t_U128; Shr_f_shr := fun (self : t_U128) (rhs : t_U128)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U128) (haxint_shr (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_BitXor_457452962 : t_BitXor ((t_U128)) ((t_U128)) := +#[global] Instance t_BitXor_457452962 : t_BitXor ((t_U128)) ((t_U128)) := { BitXor_f_Output := t_U128; BitXor_f_bitxor := fun (self : t_U128) (rhs : t_U128)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U128) (haxint_bitxor (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_BitAnd_499214249 : t_BitAnd ((t_U128)) ((t_U128)) := +#[global] Instance t_BitAnd_499214249 : t_BitAnd ((t_U128)) ((t_U128)) := { BitAnd_f_Output := t_U128; BitAnd_f_bitand := fun (self : t_U128) (rhs : t_U128)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U128) (haxint_bitand (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_BitOr_579754702 : t_BitOr ((t_U128)) ((t_U128)) := +#[global] Instance t_BitOr_579754702 : t_BitOr ((t_U128)) ((t_U128)) := { BitOr_f_Output := t_U128; BitOr_f_bitor := fun (self : t_U128) (rhs : t_U128)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U128) (haxint_bitor (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Neg_338880159 : t_Neg ((t_U64)) := +#[global] Instance t_Neg_338880159 : t_Neg ((t_U64)) := { Neg_f_Output := t_U64; Neg_f_neg := fun (self : t_U64)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U64) (haxint_sub (v_WORDSIZE_64_) (haxint_rem (Abstraction_f_lift (self)) (v_WORDSIZE_64_))); }. -#[globa] Instance t_Mul_785129859 : t_Mul ((t_U64)) ((t_U64)) := +#[global] Instance t_Mul_785129859 : t_Mul ((t_U64)) ((t_U64)) := { Mul_f_Output := t_U64; Mul_f_mul := fun (self : t_U64) (rhs : t_U64)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U64) (haxint_mul (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Rem_450198244 : t_Rem ((t_U64)) ((t_U64)) := +#[global] Instance t_Rem_450198244 : t_Rem ((t_U64)) ((t_U64)) := { Rem_f_Output := t_U64; Rem_f_rem := fun (self : t_U64) (rhs : t_U64)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U64) (haxint_rem (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Add_880469818 : t_Add ((t_U64)) ((t_U64)) := +#[global] Instance t_Add_880469818 : t_Add ((t_U64)) ((t_U64)) := { Add_f_Output := t_U64; Add_f_add := fun (self : t_U64) (rhs : t_U64)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U64) (haxint_add (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Div_1065913959 : t_Div ((t_U64)) ((t_U64)) := +#[global] Instance t_Div_1065913959 : t_Div ((t_U64)) ((t_U64)) := { Div_f_Output := t_U64; Div_f_div := fun (self : t_U64) (rhs : t_U64)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U64) (haxint_div (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shl_307107617 : t_Shl ((t_U64)) ((t_U8)) := +#[global] Instance t_Shl_307107617 : t_Shl ((t_U64)) ((t_U8)) := { Shl_f_Output := t_U64; Shl_f_shl := fun (self : t_U64) (rhs : t_U8)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U64 )(haxint_shl (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shl_521831749 : t_Shl ((t_U64)) ((t_U16)) := +#[global] Instance t_Shl_521831749 : t_Shl ((t_U64)) ((t_U16)) := { Shl_f_Output := t_U64; Shl_f_shl := fun (self : t_U64) (rhs : t_U16)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U64) (haxint_shl (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shl_243646433 : t_Shl ((t_U64)) ((t_U32)) := +#[global] Instance t_Shl_243646433 : t_Shl ((t_U64)) ((t_U32)) := { Shl_f_Output := t_U64; Shl_f_shl := fun (self : t_U64) (rhs : t_U32)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U64) (haxint_shl (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shl_732371970 : t_Shl ((t_U64)) ((t_U64)) := +#[global] Instance t_Shl_732371970 : t_Shl ((t_U64)) ((t_U64)) := { Shl_f_Output := t_U64; Shl_f_shl := fun (self : t_U64) (rhs : t_U64)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U64) (haxint_shl (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shl_362455113 : t_Shl ((t_U64)) ((t_U128)) := +#[global] Instance t_Shl_362455113 : t_Shl ((t_U64)) ((t_U128)) := { Shl_f_Output := t_U64; Shl_f_shl := fun (self : t_U64) (rhs : t_U128)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U64) (haxint_shl (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shr_675607391 : t_Shr ((t_U64)) ((t_U8)) := +#[global] Instance t_Shr_675607391 : t_Shr ((t_U64)) ((t_U8)) := { Shr_f_Output := t_U64; Shr_f_shr := fun (self : t_U64) (rhs : t_U8)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U64) (haxint_shr (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shr_163042579 : t_Shr ((t_U64)) ((t_U16)) := +#[global] Instance t_Shr_163042579 : t_Shr ((t_U64)) ((t_U16)) := { Shr_f_Output := t_U64; Shr_f_shr := fun (self : t_U64) (rhs : t_U16)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U64) (haxint_shr (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shr_329072619 : t_Shr ((t_U64)) ((t_U32)) := +#[global] Instance t_Shr_329072619 : t_Shr ((t_U64)) ((t_U32)) := { Shr_f_Output := t_U64; Shr_f_shr := fun (self : t_U64) (rhs : t_U32)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U64) (haxint_shr (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shr_1046321056 : t_Shr ((t_U64)) ((t_U64)) := +#[global] Instance t_Shr_1046321056 : t_Shr ((t_U64)) ((t_U64)) := { Shr_f_Output := t_U64; Shr_f_shr := fun (self : t_U64) (rhs : t_U64)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U64) (haxint_shr (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shr_1027159812 : t_Shr ((t_U64)) ((t_U128)) := +#[global] Instance t_Shr_1027159812 : t_Shr ((t_U64)) ((t_U128)) := { Shr_f_Output := t_U64; Shr_f_shr := fun (self : t_U64) (rhs : t_U128)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U64) (haxint_shr (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_BitXor_771705591 : t_BitXor ((t_U64)) ((t_U64)) := +#[global] Instance t_BitXor_771705591 : t_BitXor ((t_U64)) ((t_U64)) := { BitXor_f_Output := t_U64; BitXor_f_bitxor := fun (self : t_U64) (rhs : t_U64)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U64) (haxint_bitxor (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_BitAnd_61309855 : t_BitAnd ((t_U64)) ((t_U64)) := +#[global] Instance t_BitAnd_61309855 : t_BitAnd ((t_U64)) ((t_U64)) := { BitAnd_f_Output := t_U64; BitAnd_f_bitand := fun (self : t_U64) (rhs : t_U64)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U64) (haxint_bitand (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_BitOr_584478327 : t_BitOr ((t_U64)) ((t_U64)) := +#[global] Instance t_BitOr_584478327 : t_BitOr ((t_U64)) ((t_U64)) := { BitOr_f_Output := t_U64; BitOr_f_bitor := fun (self : t_U64) (rhs : t_U64)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U64) (haxint_bitor (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Neg_660092460 : t_Neg ((t_U32)) := +#[global] Instance t_Neg_660092460 : t_Neg ((t_U32)) := { Neg_f_Output := t_U32; Neg_f_neg := fun (self : t_U32)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U32) (haxint_sub (v_WORDSIZE_32_) (haxint_rem (Abstraction_f_lift (self)) (v_WORDSIZE_32_))); }. -#[globa] Instance t_Mul_907086750 : t_Mul ((t_U32)) ((t_U32)) := +#[global] Instance t_Mul_907086750 : t_Mul ((t_U32)) ((t_U32)) := { Mul_f_Output := t_U32; Mul_f_mul := fun (self : t_U32) (rhs : t_U32)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U32) (haxint_mul (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Rem_754047547 : t_Rem ((t_U32)) ((t_U32)) := +#[global] Instance t_Rem_754047547 : t_Rem ((t_U32)) ((t_U32)) := { Rem_f_Output := t_U32; Rem_f_rem := fun (self : t_U32) (rhs : t_U32)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U32) (haxint_rem (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Add_62760194 : t_Add ((t_U32)) ((t_U32)) := +#[global] Instance t_Add_62760194 : t_Add ((t_U32)) ((t_U32)) := { Add_f_Output := t_U32; Add_f_add := fun (self : t_U32) (rhs : t_U32)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U32) (haxint_add (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Div_1036065219 : t_Div ((t_U32)) ((t_U32)) := +#[global] Instance t_Div_1036065219 : t_Div ((t_U32)) ((t_U32)) := { Div_f_Output := t_U32; Div_f_div := fun (self : t_U32) (rhs : t_U32)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U32) (haxint_div (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shl_940272829 : t_Shl ((t_U32)) ((t_U8)) := +#[global] Instance t_Shl_940272829 : t_Shl ((t_U32)) ((t_U8)) := { Shl_f_Output := t_U32; Shl_f_shl := fun (self : t_U32) (rhs : t_U8)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U32) (haxint_shl (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shl_184065944 : t_Shl ((t_U32)) ((t_U16)) := +#[global] Instance t_Shl_184065944 : t_Shl ((t_U32)) ((t_U16)) := { Shl_f_Output := t_U32; Shl_f_shl := fun (self : t_U32) (rhs : t_U16)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U32) (haxint_shl (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shl_512141775 : t_Shl ((t_U32)) ((t_U32)) := +#[global] Instance t_Shl_512141775 : t_Shl ((t_U32)) ((t_U32)) := { Shl_f_Output := t_U32; Shl_f_shl := fun (self : t_U32) (rhs : t_U32)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U32) (haxint_shl (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shl_760382167 : t_Shl ((t_U32)) ((t_U64)) := +#[global] Instance t_Shl_760382167 : t_Shl ((t_U32)) ((t_U64)) := { Shl_f_Output := t_U32; Shl_f_shl := fun (self : t_U32) (rhs : t_U64)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U32) (haxint_shl (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shl_938844716 : t_Shl ((t_U32)) ((t_U128)) := +#[global] Instance t_Shl_938844716 : t_Shl ((t_U32)) ((t_U128)) := { Shl_f_Output := t_U32; Shl_f_shl := fun (self : t_U32) (rhs : t_U128)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U32) (haxint_shl (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shr_376401556 : t_Shr ((t_U32)) ((t_U8)) := +#[global] Instance t_Shr_376401556 : t_Shr ((t_U32)) ((t_U8)) := { Shr_f_Output := t_U32; Shr_f_shr := fun (self : t_U32) (rhs : t_U8)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U32) (haxint_shr (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shr_816225657 : t_Shr ((t_U32)) ((t_U16)) := +#[global] Instance t_Shr_816225657 : t_Shr ((t_U32)) ((t_U16)) := { Shr_f_Output := t_U32; Shr_f_shr := fun (self : t_U32) (rhs : t_U16)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U32) (haxint_shr (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shr_131570199 : t_Shr ((t_U32)) ((t_U32)) := +#[global] Instance t_Shr_131570199 : t_Shr ((t_U32)) ((t_U32)) := { Shr_f_Output := t_U32; Shr_f_shr := fun (self : t_U32) (rhs : t_U32)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U32) (haxint_shr (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shr_643141508 : t_Shr ((t_U32)) ((t_U64)) := +#[global] Instance t_Shr_643141508 : t_Shr ((t_U32)) ((t_U64)) := { Shr_f_Output := t_U32; Shr_f_shr := fun (self : t_U32) (rhs : t_U64)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U32) (haxint_shr (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shr_472576920 : t_Shr ((t_U32)) ((t_U128)) := +#[global] Instance t_Shr_472576920 : t_Shr ((t_U32)) ((t_U128)) := { Shr_f_Output := t_U32; Shr_f_shr := fun (self : t_U32) (rhs : t_U128)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U32) (haxint_shr (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_BitXor_568575701 : t_BitXor ((t_U32)) ((t_U32)) := +#[global] Instance t_BitXor_568575701 : t_BitXor ((t_U32)) ((t_U32)) := { BitXor_f_Output := t_U32; BitXor_f_bitxor := fun (self : t_U32) (rhs : t_U32)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U32) (haxint_bitxor (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_BitAnd_188629984 : t_BitAnd ((t_U32)) ((t_U32)) := +#[global] Instance t_BitAnd_188629984 : t_BitAnd ((t_U32)) ((t_U32)) := { BitAnd_f_Output := t_U32; BitAnd_f_bitand := fun (self : t_U32) (rhs : t_U32)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U32) (haxint_bitand (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_BitOr_727300711 : t_BitOr ((t_U32)) ((t_U32)) := +#[global] Instance t_BitOr_727300711 : t_BitOr ((t_U32)) ((t_U32)) := { BitOr_f_Output := t_U32; BitOr_f_bitor := fun (self : t_U32) (rhs : t_U32)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U32) (haxint_bitor (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Neg_524209972 : t_Neg ((t_U16)) := +#[global] Instance t_Neg_524209972 : t_Neg ((t_U16)) := { Neg_f_Output := t_U16; Neg_f_neg := fun (self : t_U16)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U16) (haxint_sub (v_WORDSIZE_16_) (haxint_rem (Abstraction_f_lift (self)) (v_WORDSIZE_16_))); }. -#[globa] Instance t_Mul_813798593 : t_Mul ((t_U16)) ((t_U16)) := +#[global] Instance t_Mul_813798593 : t_Mul ((t_U16)) ((t_U16)) := { Mul_f_Output := t_U16; Mul_f_mul := fun (self : t_U16) (rhs : t_U16)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U16) (haxint_mul (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Rem_1023129312 : t_Rem ((t_U16)) ((t_U16)) := +#[global] Instance t_Rem_1023129312 : t_Rem ((t_U16)) ((t_U16)) := { Rem_f_Output := t_U16; Rem_f_rem := fun (self : t_U16) (rhs : t_U16)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U16) (haxint_rem (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Add_669194837 : t_Add ((t_U16)) ((t_U16)) := +#[global] Instance t_Add_669194837 : t_Add ((t_U16)) ((t_U16)) := { Add_f_Output := t_U16; Add_f_add := fun (self : t_U16) (rhs : t_U16)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U16) (haxint_add (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Div_599727096 : t_Div ((t_U16)) ((t_U16)) := +#[global] Instance t_Div_599727096 : t_Div ((t_U16)) ((t_U16)) := { Div_f_Output := t_U16; Div_f_div := fun (self : t_U16) (rhs : t_U16)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U16) (haxint_div (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shl_254354835 : t_Shl ((t_U16)) ((t_U8)) := +#[global] Instance t_Shl_254354835 : t_Shl ((t_U16)) ((t_U8)) := { Shl_f_Output := t_U16; Shl_f_shl := fun (self : t_U16) (rhs : t_U8)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U16) (haxint_shl (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shl_786190756 : t_Shl ((t_U16)) ((t_U16)) := +#[global] Instance t_Shl_786190756 : t_Shl ((t_U16)) ((t_U16)) := { Shl_f_Output := t_U16; Shl_f_shl := fun (self : t_U16) (rhs : t_U16)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U16) (haxint_shl (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shl_961613024 : t_Shl ((t_U16)) ((t_U32)) := +#[global] Instance t_Shl_961613024 : t_Shl ((t_U16)) ((t_U32)) := { Shl_f_Output := t_U16; Shl_f_shl := fun (self : t_U16) (rhs : t_U32)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U16) (haxint_shl (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shl_699049796 : t_Shl ((t_U16)) ((t_U64)) := +#[global] Instance t_Shl_699049796 : t_Shl ((t_U16)) ((t_U64)) := { Shl_f_Output := t_U16; Shl_f_shl := fun (self : t_U16) (rhs : t_U64)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U16) (haxint_shl (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shl_98667823 : t_Shl ((t_U16)) ((t_U128)) := +#[global] Instance t_Shl_98667823 : t_Shl ((t_U16)) ((t_U128)) := { Shl_f_Output := t_U16; Shl_f_shl := fun (self : t_U16) (rhs : t_U128)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U16) (haxint_shl (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shr_116990915 : t_Shr ((t_U16)) ((t_U8)) := +#[global] Instance t_Shr_116990915 : t_Shr ((t_U16)) ((t_U8)) := { Shr_f_Output := t_U16; Shr_f_shr := fun (self : t_U16) (rhs : t_U8)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U16) (haxint_shr (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shr_53270962 : t_Shr ((t_U16)) ((t_U16)) := +#[global] Instance t_Shr_53270962 : t_Shr ((t_U16)) ((t_U16)) := { Shr_f_Output := t_U16; Shr_f_shr := fun (self : t_U16) (rhs : t_U16)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U16) (haxint_shr (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shr_622272332 : t_Shr ((t_U16)) ((t_U32)) := +#[global] Instance t_Shr_622272332 : t_Shr ((t_U16)) ((t_U32)) := { Shr_f_Output := t_U16; Shr_f_shr := fun (self : t_U16) (rhs : t_U32)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U16) (haxint_shr (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shr_1061476863 : t_Shr ((t_U16)) ((t_U64)) := +#[global] Instance t_Shr_1061476863 : t_Shr ((t_U16)) ((t_U64)) := { Shr_f_Output := t_U16; Shr_f_shr := fun (self : t_U16) (rhs : t_U64)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U16) (haxint_shr (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shr_148349277 : t_Shr ((t_U16)) ((t_U128)) := +#[global] Instance t_Shr_148349277 : t_Shr ((t_U16)) ((t_U128)) := { Shr_f_Output := t_U16; Shr_f_shr := fun (self : t_U16) (rhs : t_U128)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U16) (haxint_shr (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_BitXor_39308972 : t_BitXor ((t_U16)) ((t_U16)) := +#[global] Instance t_BitXor_39308972 : t_BitXor ((t_U16)) ((t_U16)) := { BitXor_f_Output := t_U16; BitXor_f_bitxor := fun (self : t_U16) (rhs : t_U16)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U16) (haxint_bitxor (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_BitAnd_100986953 : t_BitAnd ((t_U16)) ((t_U16)) := +#[global] Instance t_BitAnd_100986953 : t_BitAnd ((t_U16)) ((t_U16)) := { BitAnd_f_Output := t_U16; BitAnd_f_bitand := fun (self : t_U16) (rhs : t_U16)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U16) (haxint_bitand (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_BitOr_321212552 : t_BitOr ((t_U16)) ((t_U16)) := +#[global] Instance t_BitOr_321212552 : t_BitOr ((t_U16)) ((t_U16)) := { BitOr_f_Output := t_U16; BitOr_f_bitor := fun (self : t_U16) (rhs : t_U16)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_HaxInt t_U16) (haxint_bitor (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Neg_410091205 : t_Neg ((t_U8)) := +#[global] Instance t_Neg_410091205 : t_Neg ((t_U8)) := { Neg_f_Output := t_U8; Neg_f_neg := fun (self : t_U8)=> Concretization_f_concretize (haxint_sub (v_WORDSIZE_8_) (haxint_rem (Abstraction_f_lift (self)) (v_WORDSIZE_8_))); }. -#[globa] Instance t_Mul_116494850 : t_Mul ((t_U8)) ((t_U8)) := +#[global] Instance t_Mul_116494850 : t_Mul ((t_U8)) ((t_U8)) := { Mul_f_Output := t_U8; Mul_f_mul := fun (self : t_U8) (rhs : t_U8)=> Concretization_f_concretize (haxint_mul (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Rem_674469245 : t_Rem ((t_U8)) ((t_U8)) := +#[global] Instance t_Rem_674469245 : t_Rem ((t_U8)) ((t_U8)) := { Rem_f_Output := t_U8; Rem_f_rem := fun (self : t_U8) (rhs : t_U8)=> Concretization_f_concretize (haxint_rem (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Add_886374338 : t_Add ((t_U8)) ((t_U8)) := +#[global] Instance t_Add_886374338 : t_Add ((t_U8)) ((t_U8)) := { Add_f_Output := t_U8; Add_f_add := fun (self : t_U8) (rhs : t_U8)=> Concretization_f_concretize (haxint_add (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Div_7559770 : t_Div ((t_U8)) ((t_U8)) := +#[global] Instance t_Div_7559770 : t_Div ((t_U8)) ((t_U8)) := { Div_f_Output := t_U8; Div_f_div := fun (self : t_U8) (rhs : t_U8)=> Concretization_f_concretize (haxint_div (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shl_889664521 : t_Shl ((t_U8)) ((t_U8)) := +#[global] Instance t_Shl_889664521 : t_Shl ((t_U8)) ((t_U8)) := { Shl_f_Output := t_U8; Shl_f_shl := fun (self : t_U8) (rhs : t_U8)=> Concretization_f_concretize (haxint_shl (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shl_268581730 : t_Shl ((t_U8)) ((t_U16)) := +#[global] Instance t_Shl_268581730 : t_Shl ((t_U8)) ((t_U16)) := { Shl_f_Output := t_U8; Shl_f_shl := fun (self : t_U8) (rhs : t_U16)=> Concretization_f_concretize (haxint_shl (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shl_833473770 : t_Shl ((t_U8)) ((t_U32)) := +#[global] Instance t_Shl_833473770 : t_Shl ((t_U8)) ((t_U32)) := { Shl_f_Output := t_U8; Shl_f_shl := fun (self : t_U8) (rhs : t_U32)=> Concretization_f_concretize (haxint_shl (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shl_896563459 : t_Shl ((t_U8)) ((t_U64)) := +#[global] Instance t_Shl_896563459 : t_Shl ((t_U8)) ((t_U64)) := { Shl_f_Output := t_U8; Shl_f_shl := fun (self : t_U8) (rhs : t_U64)=> Concretization_f_concretize (haxint_shl (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shl_595294021 : t_Shl ((t_U8)) ((t_U128)) := +#[global] Instance t_Shl_595294021 : t_Shl ((t_U8)) ((t_U128)) := { Shl_f_Output := t_U8; Shl_f_shl := fun (self : t_U8) (rhs : t_U128)=> Concretization_f_concretize (haxint_shl (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shr_467626732 : t_Shr ((t_U8)) ((t_U8)) := +#[global] Instance t_Shr_467626732 : t_Shr ((t_U8)) ((t_U8)) := { Shr_f_Output := t_U8; Shr_f_shr := fun (self : t_U8) (rhs : t_U8)=> Concretization_f_concretize (haxint_shr (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shr_985367369 : t_Shr ((t_U8)) ((t_U16)) := +#[global] Instance t_Shr_985367369 : t_Shr ((t_U8)) ((t_U16)) := { Shr_f_Output := t_U8; Shr_f_shr := fun (self : t_U8) (rhs : t_U16)=> Concretization_f_concretize (haxint_shr (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shr_868101800 : t_Shr ((t_U8)) ((t_U32)) := +#[global] Instance t_Shr_868101800 : t_Shr ((t_U8)) ((t_U32)) := { Shr_f_Output := t_U8; Shr_f_shr := fun (self : t_U8) (rhs : t_U32)=> Concretization_f_concretize (haxint_shr (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shr_300023283 : t_Shr ((t_U8)) ((t_U64)) := +#[global] Instance t_Shr_300023283 : t_Shr ((t_U8)) ((t_U64)) := { Shr_f_Output := t_U8; Shr_f_shr := fun (self : t_U8) (rhs : t_U64)=> Concretization_f_concretize (haxint_shr (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Shr_794091640 : t_Shr ((t_U8)) ((t_U128)) := +#[global] Instance t_Shr_794091640 : t_Shr ((t_U8)) ((t_U128)) := { Shr_f_Output := t_U8; Shr_f_shr := fun (self : t_U8) (rhs : t_U128)=> Concretization_f_concretize (haxint_shr (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_BitXor_24738444 : t_BitXor ((t_U8)) ((t_U8)) := +#[global] Instance t_BitXor_24738444 : t_BitXor ((t_U8)) ((t_U8)) := { BitXor_f_Output := t_U8; BitXor_f_bitxor := fun (self : t_U8) (rhs : t_U8)=> Concretization_f_concretize (haxint_bitxor (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_BitAnd_358790390 : t_BitAnd ((t_U8)) ((t_U8)) := +#[global] Instance t_BitAnd_358790390 : t_BitAnd ((t_U8)) ((t_U8)) := { BitAnd_f_Output := t_U8; BitAnd_f_bitand := fun (self : t_U8) (rhs : t_U8)=> Concretization_f_concretize (haxint_bitand (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_BitOr_349401480 : t_BitOr ((t_U8)) ((t_U8)) := +#[global] Instance t_BitOr_349401480 : t_BitOr ((t_U8)) ((t_U8)) := { BitOr_f_Output := t_U8; BitOr_f_bitor := fun (self : t_U8) (rhs : t_U8)=> Concretization_f_concretize (haxint_bitor (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Rem_998027599 : t_Rem ((t_I128)) ((t_I128)) := +#[global] Instance t_Rem_998027599 : t_Rem ((t_I128)) ((t_I128)) := { Rem_f_Output := t_I128; Rem_f_rem := fun (self : t_I128) (rhs : t_I128)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I128) (z_rem (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Div_865866956 : t_Div ((t_I128)) ((t_I128)) := +#[global] Instance t_Div_865866956 : t_Div ((t_I128)) ((t_I128)) := { Div_f_Output := t_I128; Div_f_div := fun (self : t_I128) (rhs : t_I128)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I128) (z_div (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Rem_957489424 : t_Rem ((t_I64)) ((t_I64)) := +#[global] Instance t_Rem_957489424 : t_Rem ((t_I64)) ((t_I64)) := { Rem_f_Output := t_I64; Rem_f_rem := fun (self : t_I64) (rhs : t_I64)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I64) (z_rem (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Div_611785525 : t_Div ((t_I64)) ((t_I64)) := +#[global] Instance t_Div_611785525 : t_Div ((t_I64)) ((t_I64)) := { Div_f_Output := t_I64; Div_f_div := fun (self : t_I64) (rhs : t_I64)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I64) (z_div (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Rem_219303214 : t_Rem ((t_I32)) ((t_I32)) := +#[global] Instance t_Rem_219303214 : t_Rem ((t_I32)) ((t_I32)) := { Rem_f_Output := t_I32; Rem_f_rem := fun (self : t_I32) (rhs : t_I32)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I32) (z_rem (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Div_1002924104 : t_Div ((t_I32)) ((t_I32)) := +#[global] Instance t_Div_1002924104 : t_Div ((t_I32)) ((t_I32)) := { Div_f_Output := t_I32; Div_f_div := fun (self : t_I32) (rhs : t_I32)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I32) (z_div (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Rem_948867246 : t_Rem ((t_I16)) ((t_I16)) := +#[global] Instance t_Rem_948867246 : t_Rem ((t_I16)) ((t_I16)) := { Rem_f_Output := t_I16; Rem_f_rem := fun (self : t_I16) (rhs : t_I16)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I16) (z_rem (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Div_357493436 : t_Div ((t_I16)) ((t_I16)) := +#[global] Instance t_Div_357493436 : t_Div ((t_I16)) ((t_I16)) := { Div_f_Output := t_I16; Div_f_div := fun (self : t_I16) (rhs : t_I16)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I16) (z_div (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Rem_228000167 : t_Rem ((t_I8)) ((t_I8)) := +#[global] Instance t_Rem_228000167 : t_Rem ((t_I8)) ((t_I8)) := { Rem_f_Output := t_I8; Rem_f_rem := fun (self : t_I8) (rhs : t_I8)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I8) (z_rem (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Div_470010025 : t_Div ((t_I8)) ((t_I8)) := +#[global] Instance t_Div_470010025 : t_Div ((t_I8)) ((t_I8)) := { Div_f_Output := t_I8; Div_f_div := fun (self : t_I8) (rhs : t_I8)=> Concretization_f_concretize (t_Concretization := _ : t_Concretization t_Z t_I8) (z_div (Abstraction_f_lift (self)) (Abstraction_f_lift (rhs))); }. -#[globa] Instance t_Sub_1018502693 : t_Sub ((t_U128)) ((t_U128)) := +#[global] Instance t_Sub_1018502693 : t_Sub ((t_U128)) ((t_U128)) := { Sub_f_Output := t_U128; Sub_f_sub := fun (self : t_U128) (rhs : t_U128)=> Add_f_add (t_Add := _ : t_Add t_U128 t_U128) (self) (Neg_f_neg (rhs)); }. -#[globa] Instance t_Not_758360759 : t_Not ((t_U128)) := +#[global] Instance t_Not_758360759 : t_Not ((t_U128)) := { Not_f_Output := t_U128; Not_f_not := fun (self : t_U128)=> BitXor_f_bitxor (self) (Constants_f_MAX); }. -#[globa] Instance t_Sub_919216830 : t_Sub ((t_U64)) ((t_U64)) := +#[global] Instance t_Sub_919216830 : t_Sub ((t_U64)) ((t_U64)) := { Sub_f_Output := t_U64; Sub_f_sub := fun (self : t_U64) (rhs : t_U64)=> Add_f_add (t_Add := _ : t_Add _ t_U64) (self) (Neg_f_neg (rhs)); }. -#[globa] Instance t_Not_693249901 : t_Not ((t_U64)) := +#[global] Instance t_Not_693249901 : t_Not ((t_U64)) := { Not_f_Output := t_U64; Not_f_not := fun (self : t_U64)=> BitXor_f_bitxor (self) (Constants_f_MAX); }. -#[globa] Instance t_Sub_22623594 : t_Sub ((t_U32)) ((t_U32)) := +#[global] Instance t_Sub_22623594 : t_Sub ((t_U32)) ((t_U32)) := { Sub_f_Output := t_U32; Sub_f_sub := fun (self : t_U32) (rhs : t_U32)=> Add_f_add (t_Add := _ : t_Add _ t_U32) (self) (Neg_f_neg (rhs)); }. -#[globa] Instance t_Not_183316157 : t_Not ((t_U32)) := +#[global] Instance t_Not_183316157 : t_Not ((t_U32)) := { Not_f_Output := t_U32; Not_f_not := fun (self : t_U32)=> BitXor_f_bitxor (self) (Constants_f_MAX); }. -#[globa] Instance t_Sub_502320750 : t_Sub ((t_U16)) ((t_U16)) := +#[global] Instance t_Sub_502320750 : t_Sub ((t_U16)) ((t_U16)) := { Sub_f_Output := t_U16; Sub_f_sub := fun (self : t_U16) (rhs : t_U16)=> Add_f_add (t_Add := _ : t_Add _ t_U16) (self) (Neg_f_neg (rhs)); }. -#[globa] Instance t_Not_669226601 : t_Not ((t_U16)) := +#[global] Instance t_Not_669226601 : t_Not ((t_U16)) := { Not_f_Output := t_U16; Not_f_not := fun (self : t_U16)=> BitXor_f_bitxor (self) (Constants_f_MAX); }. -#[globa] Instance t_Sub_299023787 : t_Sub ((t_U8)) ((t_U8)) := +#[global] Instance t_Sub_299023787 : t_Sub ((t_U8)) ((t_U8)) := { Sub_f_Output := t_U8; Sub_f_sub := fun (self : t_U8) (rhs : t_U8)=> Add_f_add (t_Add := _ : t_Add _ t_U8) (self) (Neg_f_neg (rhs)); }. -#[globa] Instance t_Not_761019181 : t_Not ((t_U8)) := +#[global] Instance t_Not_761019181 : t_Not ((t_U8)) := { Not_f_Output := t_U8; Not_f_not := fun (self : t_U8)=> diff --git a/test-harness/src/snapshots/toolchain__assert into-coq.snap b/test-harness/src/snapshots/toolchain__assert into-coq.snap index a000cc9f9..6f94866e0 100644 --- a/test-harness/src/snapshots/toolchain__assert into-coq.snap +++ b/test-harness/src/snapshots/toolchain__assert into-coq.snap @@ -38,21 +38,28 @@ Require Import String. Require Import Coq.Floats.Floats. From RecordUpdate Require Import RecordSet. Import RecordSetNotations. +From Core Require Import Core. (* NotImplementedYet *) -Definition asserts (_ : unit) : unit := - let _ := assert (true) in - let _ := assert (t_PartialEq_f_eq (1) (1)) in - let _ := match (2,2) with +Definition asserts '(_ : unit) : unit := + let _ := assert ((true : bool)) in + let _ := assert (PartialEq_f_eq ((1 : t_i32)) ((1 : t_i32))) in + let _ := match ((2 : t_i32),(2 : t_i32)) with | (left_val,right_val) => - assert (t_PartialEq_f_eq (left_val) (right_val)) + assert (PartialEq_f_eq (left_val) (right_val)) end in - let _ := match (1,2) with + let _ := match ((1 : t_i32),(2 : t_i32)) with | (left_val,right_val) => - assert (negb (t_PartialEq_f_eq (left_val) (right_val))) + assert (negb (PartialEq_f_eq (left_val) (right_val))) end in tt. ''' +_CoqProject = ''' +-R ./ TODO +-arg -w +-arg all + +Assert.v''' diff --git a/test-harness/src/snapshots/toolchain__enum-repr into-coq.snap b/test-harness/src/snapshots/toolchain__enum-repr into-coq.snap index bfe3bcc0a..7293ed72f 100644 --- a/test-harness/src/snapshots/toolchain__enum-repr into-coq.snap +++ b/test-harness/src/snapshots/toolchain__enum-repr into-coq.snap @@ -39,22 +39,25 @@ Require Import String. Require Import Coq.Floats.Floats. From RecordUpdate Require Import RecordSet. Import RecordSetNotations. +From Core Require Import Core. Definition discriminant_EnumWithRepr_ExplicitDiscr1 : t_u16 := - 1. + (1 : t_u16). Definition discriminant_EnumWithRepr_ExplicitDiscr2 : t_u16 := - 5. + (5 : t_u16). Inductive t_EnumWithRepr : Type := | EnumWithRepr_ExplicitDiscr1 | EnumWithRepr_ExplicitDiscr2 | EnumWithRepr_ImplicitDiscrEmptyTuple | EnumWithRepr_ImplicitDiscrEmptyStruct. -Arguments t_EnumWithRepr:clear implicits. -Arguments t_EnumWithRepr. +Arguments EnumWithRepr_ExplicitDiscr1. +Arguments EnumWithRepr_ExplicitDiscr2. +Arguments EnumWithRepr_ImplicitDiscrEmptyTuple. +Arguments EnumWithRepr_ImplicitDiscrEmptyStruct. Definition t_EnumWithRepr_cast_to_repr (x : t_EnumWithRepr) : t_u16 := match x with @@ -63,19 +66,19 @@ Definition t_EnumWithRepr_cast_to_repr (x : t_EnumWithRepr) : t_u16 := | EnumWithRepr_ExplicitDiscr2 => discriminant_EnumWithRepr_ExplicitDiscr2 | EnumWithRepr_ImplicitDiscrEmptyTuple => - t_Add_f_add (discriminant_EnumWithRepr_ExplicitDiscr2) (1) + Add_f_add (discriminant_EnumWithRepr_ExplicitDiscr2) ((1 : t_u16)) | EnumWithRepr_ImplicitDiscrEmptyStruct => - t_Add_f_add (discriminant_EnumWithRepr_ExplicitDiscr2) (2) + Add_f_add (discriminant_EnumWithRepr_ExplicitDiscr2) ((2 : t_u16)) end. (* NotImplementedYet *) -Definition f (_ : unit) : t_u32 := - let v__x := cast (t_Add_f_add (discriminant_EnumWithRepr_ExplicitDiscr2) (0)) in - t_Add_f_add (cast (t_EnumWithRepr_cast_to_repr (EnumWithRepr_ImplicitDiscrEmptyTuple))) (cast (t_EnumWithRepr_cast_to_repr (EnumWithRepr_ImplicitDiscrEmptyStruct))). +Definition f '(_ : unit) : t_u32 := + let v__x := cast (Add_f_add (discriminant_EnumWithRepr_ExplicitDiscr2) ((0 : t_u16))) in + Add_f_add (cast (t_EnumWithRepr_cast_to_repr (EnumWithRepr_ImplicitDiscrEmptyTuple))) (cast (t_EnumWithRepr_cast_to_repr (EnumWithRepr_ImplicitDiscrEmptyStruct))). Definition ff__CONST : t_u16 := - cast (t_Add_f_add (discriminant_EnumWithRepr_ExplicitDiscr1) (0)). + cast (Add_f_add (discriminant_EnumWithRepr_ExplicitDiscr1) ((0 : t_u16))). Definition get_casted_repr (x : t_EnumWithRepr) : t_u64 := cast (t_EnumWithRepr_cast_to_repr (x)). @@ -83,3 +86,9 @@ Definition get_casted_repr (x : t_EnumWithRepr) : t_u64 := Definition get_repr (x : t_EnumWithRepr) : t_u16 := t_EnumWithRepr_cast_to_repr (x). ''' +_CoqProject = ''' +-R ./ TODO +-arg -w +-arg all + +Enum_repr.v''' diff --git a/test-harness/src/snapshots/toolchain__guards into-coq.snap b/test-harness/src/snapshots/toolchain__guards into-coq.snap index abd2a3274..739f6efe8 100644 --- a/test-harness/src/snapshots/toolchain__guards into-coq.snap +++ b/test-harness/src/snapshots/toolchain__guards into-coq.snap @@ -38,6 +38,7 @@ Require Import String. Require Import Coq.Floats.Floats. From RecordUpdate Require Import RecordSet. Import RecordSetNotations. +From Core Require Import Core. @@ -46,7 +47,7 @@ Import RecordSetNotations. Definition equivalent (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i32 := match x with | Option_None => - 0 + (0 : t_i32) | _ => match match x with | Option_Some (v) => @@ -66,7 +67,7 @@ Definition equivalent (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i32 := | Option_Some (Result_Err (y)) => y | _ => - 1 + (1 : t_i32) end end end. @@ -74,7 +75,7 @@ Definition equivalent (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i32 := Definition if_guard (x : t_Option ((t_i32))) : t_i32 := match match x with | Option_Some (v) => - match t_PartialOrd_f_gt (v) (0) with + match PartialOrd_f_gt (v) ((0 : t_i32)) with | true => Option_Some (v) | _ => @@ -86,13 +87,13 @@ Definition if_guard (x : t_Option ((t_i32))) : t_i32 := | Option_Some (x) => x | Option_None => - 0 + (0 : t_i32) end. Definition if_let_guard (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i32 := match x with | Option_None => - 0 + (0 : t_i32) | _ => match match x with | Option_Some (v) => @@ -112,7 +113,7 @@ Definition if_let_guard (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i32 | Option_Some (Result_Err (y)) => y | _ => - 1 + (1 : t_i32) end end end. @@ -120,13 +121,13 @@ Definition if_let_guard (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i32 Definition multiple_guards (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i32 := match x with | Option_None => - 0 + (0 : t_i32) | _ => match match x with | Option_Some (Result_Ok (v)) => - match Option_Some (t_Add_f_add (v) (1)) with + match Option_Some (Add_f_add (v) ((1 : t_i32))) with | Option_Some (1) => - Option_Some (0) + Option_Some ((0 : t_i32)) | _ => Option_None end @@ -154,9 +155,15 @@ Definition multiple_guards (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i | Option_Some (Result_Err (y)) => y | _ => - 1 + (1 : t_i32) end end end end. ''' +_CoqProject = ''' +-R ./ TODO +-arg -w +-arg all + +Guards.v''' diff --git a/test-harness/src/snapshots/toolchain__include-flag into-coq.snap b/test-harness/src/snapshots/toolchain__include-flag into-coq.snap index c86f3b275..4e449530c 100644 --- a/test-harness/src/snapshots/toolchain__include-flag into-coq.snap +++ b/test-harness/src/snapshots/toolchain__include-flag into-coq.snap @@ -38,22 +38,20 @@ Require Import String. Require Import Coq.Floats.Floats. From RecordUpdate Require Import RecordSet. Import RecordSetNotations. +From Core Require Import Core. Record t_Foo : Type := { }. -Arguments t_Foo:clear implicits. -Arguments t_Foo. Arguments Build_t_Foo. -#[export] Instance settable_t_Foo : Settable _ := - settable! (@Build_t_Foo) <>. +#[export] +Notation "'Foo'" := Build_t_Foo. -Class t_Trait `{v_Self : Type} : Type := +Class t_Trait (v_Self : Type) : Type := { }. -Arguments t_Trait:clear implicits. Arguments t_Trait (_). Instance t_Trait_254780795 : t_Trait ((t_Foo)) := @@ -62,13 +60,13 @@ Instance t_Trait_254780795 : t_Trait ((t_Foo)) := (* NotImplementedYet *) -Definition main_a_a (_ : unit) : unit := +Definition main_a_a '(_ : unit) : unit := tt. -Definition main_a_b (_ : unit) : unit := +Definition main_a_b '(_ : unit) : unit := tt. -Definition main_a_c (_ : unit) : unit := +Definition main_a_c '(_ : unit) : unit := tt. Definition main_a `{v_T : Type} `{t_Sized (v_T)} `{t_Trait (v_T)} (x : v_T) : unit := @@ -77,39 +75,45 @@ Definition main_a `{v_T : Type} `{t_Sized (v_T)} `{t_Trait (v_T)} (x : v_T) : un let _ := main_a_c (tt) in tt. -Definition main_b_a (_ : unit) : unit := +Definition main_b_a '(_ : unit) : unit := tt. -Definition main_b_b (_ : unit) : unit := +Definition main_b_b '(_ : unit) : unit := tt. -Definition main_b_c (_ : unit) : unit := +Definition main_b_c '(_ : unit) : unit := tt. -Definition main_b (_ : unit) : unit := +Definition main_b '(_ : unit) : unit := let _ := main_b_a (tt) in let _ := main_b_b (tt) in let _ := main_b_c (tt) in tt. -Definition main_c_a (_ : unit) : unit := +Definition main_c_a '(_ : unit) : unit := tt. -Definition main_c_b (_ : unit) : unit := +Definition main_c_b '(_ : unit) : unit := tt. -Definition main_c_c (_ : unit) : unit := +Definition main_c_c '(_ : unit) : unit := tt. -Definition main_c (_ : unit) : unit := +Definition main_c '(_ : unit) : unit := let _ := main_c_a (tt) in let _ := main_c_b (tt) in let _ := main_c_c (tt) in tt. -Definition main (_ : unit) : unit := +Definition main '(_ : unit) : unit := let _ := main_a (Build_t_Foo) in let _ := main_b (tt) in let _ := main_c (tt) in tt. ''' +_CoqProject = ''' +-R ./ TODO +-arg -w +-arg all + +Include_flag.v''' diff --git a/test-harness/src/snapshots/toolchain__let-else into-coq.snap b/test-harness/src/snapshots/toolchain__let-else into-coq.snap index 330c601b3..1f3aeb359 100644 --- a/test-harness/src/snapshots/toolchain__let-else into-coq.snap +++ b/test-harness/src/snapshots/toolchain__let-else into-coq.snap @@ -38,6 +38,7 @@ Require Import String. Require Import Coq.Floats.Floats. From RecordUpdate Require Import RecordSet. Import RecordSetNotations. +From Core Require Import Core. @@ -46,17 +47,23 @@ Import RecordSetNotations. Definition let_else (opt : t_Option ((t_u32))) : bool := run (match opt with | Option_Some (x) => - ControlFlow_Continue (true) + ControlFlow_Continue ((true : bool)) | _ => - ControlFlow_Break (false) + ControlFlow_Break ((false : bool)) end). Definition let_else_different_type (opt : t_Option ((t_u32))) : bool := run (let hoist1 := match opt with | Option_Some (x) => - ControlFlow_Continue (Option_Some (t_Add_f_add (x) (1))) + ControlFlow_Continue (Option_Some (Add_f_add (x) ((1 : t_u32)))) | _ => - ControlFlow_Break (false) + ControlFlow_Break ((false : bool)) end in ControlFlow_Continue (let_else (hoist1))). ''' +_CoqProject = ''' +-R ./ TODO +-arg -w +-arg all + +Let_else.v''' diff --git a/test-harness/src/snapshots/toolchain__literals into-coq.snap b/test-harness/src/snapshots/toolchain__literals into-coq.snap index f2da7be00..c9fa99b7d 100644 --- a/test-harness/src/snapshots/toolchain__literals into-coq.snap +++ b/test-harness/src/snapshots/toolchain__literals into-coq.snap @@ -39,6 +39,7 @@ Require Import String. Require Import Coq.Floats.Floats. From RecordUpdate Require Import RecordSet. Import RecordSetNotations. +From Core Require Import Core. @@ -47,47 +48,46 @@ Export Hax_lib (t_int). Record t_Foo : Type := { - f_field : t_u8; + Foo_f_field : t_u8; }. -Arguments t_Foo:clear implicits. -Arguments t_Foo. Arguments Build_t_Foo. +Arguments Foo_f_field. #[export] Instance settable_t_Foo : Settable _ := - settable! (@Build_t_Foo) . + settable! (Build_t_Foo) . (* NotImplementedYet *) Definition v_CONSTANT : t_Foo := - Build_t_Foo (3). + Build_t_Foo ((3 : t_u8)). Definition casts (x8 : t_u8) (x16 : t_u16) (x32 : t_u32) (x64 : t_u64) (xs : t_usize) : unit := - let _ : t_u64 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (x64)) (cast (xs)) in - let _ : t_u32 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (x32)) (cast (x64))) (cast (xs)) in - let _ : t_u16 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (x16)) (cast (x32))) (cast (x64))) (cast (xs)) in - let _ : t_u8 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (x8) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in - let _ : t_i64 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in - let _ : t_i32 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in - let _ : t_i16 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in - let _ : t_i8 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in + let _ : t_u64 := Add_f_add (Add_f_add (Add_f_add (Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (x64)) (cast (xs)) in + let _ : t_u32 := Add_f_add (Add_f_add (Add_f_add (Add_f_add (cast (x8)) (cast (x16))) (x32)) (cast (x64))) (cast (xs)) in + let _ : t_u16 := Add_f_add (Add_f_add (Add_f_add (Add_f_add (cast (x8)) (x16)) (cast (x32))) (cast (x64))) (cast (xs)) in + let _ : t_u8 := Add_f_add (Add_f_add (Add_f_add (Add_f_add (x8) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in + let _ : t_i64 := Add_f_add (Add_f_add (Add_f_add (Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in + let _ : t_i32 := Add_f_add (Add_f_add (Add_f_add (Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in + let _ : t_i16 := Add_f_add (Add_f_add (Add_f_add (Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in + let _ : t_i8 := Add_f_add (Add_f_add (Add_f_add (Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in tt. -Definition fn_pointer_cast (_ : unit) : unit := +Definition fn_pointer_cast '(_ : unit) : unit := let f : t_u32 -> t_u32 := fun x => x in tt. -Definition math_integers (x : t_Int) `{andb (f_gt (x) (impl__Int___unsafe_from_str ("0"%string))) (f_lt (x) (impl__Int___unsafe_from_str ("16"%string))) = true} : t_u8 := - let _ : t_Int := f_lift (3) in - let _ := f_gt (impl__Int___unsafe_from_str ("-340282366920938463463374607431768211455000"%string)) (impl__Int___unsafe_from_str ("340282366920938463463374607431768211455000"%string)) in - let _ := f_lt (x) (x) in - let _ := f_ge (x) (x) in - let _ := f_le (x) (x) in - let _ := f_ne (x) (x) in - let _ := f_eq (x) (x) in - let _ := f_add (x) (x) in - let _ := f_sub (x) (x) in - let _ := f_mul (x) (x) in - let _ := f_div (x) (x) in +Definition math_integers (x : t_Int) `{andb (PartialOrd_f_gt (x) (impl__Int___unsafe_from_str (("0"%string : string)))) (PartialOrd_f_lt (x) (impl__Int___unsafe_from_str (("16"%string : string)))) = true} : t_u8 := + let _ : t_Int := Abstraction_f_lift ((3 : t_usize)) in + let _ := PartialOrd_f_gt (impl__Int___unsafe_from_str (("-340282366920938463463374607431768211455000"%string : string))) (impl__Int___unsafe_from_str (("340282366920938463463374607431768211455000"%string : string))) in + let _ := PartialOrd_f_lt (x) (x) in + let _ := PartialOrd_f_ge (x) (x) in + let _ := PartialOrd_f_le (x) (x) in + let _ := PartialEq_f_ne (x) (x) in + let _ := PartialEq_f_eq (x) (x) in + let _ := Add_f_add (x) (x) in + let _ := Sub_f_sub (x) (x) in + let _ := Mul_f_mul (x) (x) in + let _ := Div_f_div (x) (x) in let _ : t_i16 := impl__Int__to_i16 (x) in let _ : t_i32 := impl__Int__to_i32 (x) in let _ : t_i64 := impl__Int__to_i64 (x) in @@ -98,44 +98,50 @@ Definition math_integers (x : t_Int) `{andb (f_gt (x) (impl__Int___unsafe_from_s let _ : t_u64 := impl__Int__to_u64 (x) in let _ : t_u128 := impl__Int__to_u128 (x) in let _ : t_usize := impl__Int__to_usize (x) in - impl__Int__to_u8 (f_add (x) (f_mul (x) (x))). + impl__Int__to_u8 (Add_f_add (x) (Mul_f_mul (x) (x))). Definition null : ascii := - "\000"%char. - -Definition numeric (_ : unit) : unit := - let _ : t_usize := 123 in - let _ : t_isize := -42 in - let _ : t_isize := 42 in - let _ : t_i32 := -42 in - let _ : t_u128 := 22222222222222222222 in + ("\000"%char : ascii). + +Definition numeric '(_ : unit) : unit := + let _ : t_usize := (123 : t_usize) in + let _ : t_isize := (-42 : t_isize) in + let _ : t_isize := (42 : t_isize) in + let _ : t_i32 := (-42 : t_i32) in + let _ : t_u128 := (22222222222222222222 : t_u128) in tt. -Definition patterns (_ : unit) : unit := - let _ := match 1 with +Definition patterns '(_ : unit) : unit := + let _ := match (1 : t_u8) with | 2 => tt | _ => tt end in - let _ := match ("hello"%string,(123,["a"%string; "b"%string])) with + let _ := match (("hello"%string : string),((123 : t_i32),[("a"%string : string); ("b"%string : string)])) with | ("hello"%string,(123,v__todo)) => tt | _ => tt end in - let _ := match Build_t_Foo (4) with - | Foo (3) => + let _ := match Build_t_Foo ((4 : t_u8)) with + | Build_t_Foo (3) => tt | _ => tt end in tt. -Definition panic_with_msg (_ : unit) : unit := - never_to_any (panic_fmt (impl_2__new_const (["with msg"%string]))). +Definition panic_with_msg '(_ : unit) : unit := + never_to_any (panic_fmt (impl_2__new_const ([("with msg"%string : string)]))). -Definition empty_array (_ : unit) : unit := +Definition empty_array '(_ : unit) : unit := let _ : t_Slice t_u8 := unsize ([]) in tt. ''' +_CoqProject = ''' +-R ./ TODO +-arg -w +-arg all + +Literals.v''' diff --git a/test-harness/src/snapshots/toolchain__pattern-or into-coq.snap b/test-harness/src/snapshots/toolchain__pattern-or into-coq.snap index f4b3cbfe0..10ed9a1f3 100644 --- a/test-harness/src/snapshots/toolchain__pattern-or into-coq.snap +++ b/test-harness/src/snapshots/toolchain__pattern-or into-coq.snap @@ -39,21 +39,22 @@ Require Import String. Require Import Coq.Floats.Floats. From RecordUpdate Require Import RecordSet. Import RecordSetNotations. +From Core Require Import Core. Inductive t_E : Type := | E_A | E_B. -Arguments t_E:clear implicits. -Arguments t_E. +Arguments E_A. +Arguments E_B. Definition t_E_cast_to_repr (x : t_E) : t_isize := match x with | E_A => - 0 + (0 : t_isize) | E_B => - 1 + (1 : t_isize) end. (* NotImplementedYet *) @@ -70,7 +71,7 @@ Definition deep (x : (t_i32*t_Option ((t_i32)))) : t_i32 := | (1 | 2,Option_Some (3 | 4)) => - 0 + (0 : t_i32) | (x,_) => x end. @@ -93,7 +94,7 @@ Definition equivalent (x : (t_i32*t_Option ((t_i32)))) : t_i32 := | (1,Option_Some (4)) | (2,Option_Some (3)) | (2,Option_Some (4)) => - 0 + (0 : t_i32) | (x,_) => x end. @@ -102,10 +103,16 @@ Definition nested (x : t_Option ((t_i32))) : t_i32 := match x with | Option_Some (1 | 2) => - 1 + (1 : t_i32) | Option_Some (x) => x | Option_None => - 0 + (0 : t_i32) end. ''' +_CoqProject = ''' +-R ./ TODO +-arg -w +-arg all + +Pattern_or.v''' diff --git a/test-harness/src/snapshots/toolchain__reordering into-coq.snap b/test-harness/src/snapshots/toolchain__reordering into-coq.snap index d3b0567d8..648f01f46 100644 --- a/test-harness/src/snapshots/toolchain__reordering into-coq.snap +++ b/test-harness/src/snapshots/toolchain__reordering into-coq.snap @@ -38,44 +38,51 @@ Require Import String. Require Import Coq.Floats.Floats. From RecordUpdate Require Import RecordSet. Import RecordSetNotations. +From Core Require Import Core. Inductive t_Foo : Type := | Foo_A | Foo_B. -Arguments t_Foo:clear implicits. -Arguments t_Foo. +Arguments Foo_A. +Arguments Foo_B. Record t_Bar : Type := { - 0 : t_Foo; + Bar_0 : t_Foo; }. -Arguments t_Bar:clear implicits. -Arguments t_Bar. Arguments Build_t_Bar. +Arguments Bar_0. #[export] Instance settable_t_Bar : Settable _ := - settable! (@Build_t_Bar) <0>. + settable! (Build_t_Bar) . +Notation "'Bar'" := Build_t_Bar. Definition t_Foo_cast_to_repr (x : t_Foo) : t_isize := match x with | Foo_A => - 0 + (0 : t_isize) | Foo_B => - 1 + (1 : t_isize) end. (* NotImplementedYet *) -Definition f (_ : t_u32) : t_Foo := +Definition f '(_ : t_u32) : t_Foo := Foo_A. -Definition g (_ : unit) : t_Bar := - Build_t_Bar (f (32)). +Definition g '(_ : unit) : t_Bar := + Build_t_Bar (f ((32 : t_u32))). -Definition no_dependency_1_ (_ : unit) : unit := +Definition no_dependency_1_ '(_ : unit) : unit := tt. -Definition no_dependency_2_ (_ : unit) : unit := +Definition no_dependency_2_ '(_ : unit) : unit := tt. ''' +_CoqProject = ''' +-R ./ TODO +-arg -w +-arg all + +Reordering.v''' diff --git a/test-harness/src/snapshots/toolchain__slices into-coq.snap b/test-harness/src/snapshots/toolchain__slices into-coq.snap index 93fa425b0..80cde0df4 100644 --- a/test-harness/src/snapshots/toolchain__slices into-coq.snap +++ b/test-harness/src/snapshots/toolchain__slices into-coq.snap @@ -39,20 +39,27 @@ Require Import String. Require Import Coq.Floats.Floats. From RecordUpdate Require Import RecordSet. Import RecordSetNotations. +From Core Require Import Core. (* NotImplementedYet *) Definition v_VERSION : t_Slice t_u8 := - unsize ([118; 49]). + unsize ([(118 : t_u8); (49 : t_u8)]). -Definition do_something (_ : t_Slice t_u8) : unit := +Definition do_something '(_ : t_Slice t_u8) : unit := tt. -Definition r#unsized (_ : t_Array (t_Slice t_u8) (1)) : unit := +Definition r#unsized '(_ : t_Array (t_Slice t_u8) ((1 : t_usize))) : unit := tt. -Definition sized (x : t_Array (t_Array (t_u8) (4)) (1)) : unit := - r#unsized ([unsize (index (x) (0))]). +Definition sized (x : t_Array (t_Array (t_u8) ((4 : t_usize))) ((1 : t_usize))) : unit := + r#unsized ([unsize (Index_f_index (x) ((0 : t_usize)))]). ''' +_CoqProject = ''' +-R ./ TODO +-arg -w +-arg all + +Slices.v'''