diff --git a/.github/coq-errors.json b/.github/coq-errors.json new file mode 100644 index 000000000..a52d73e5e --- /dev/null +++ b/.github/coq-errors.json @@ -0,0 +1,20 @@ +{ + "problemMatcher": [ + { + "owner": "coq", + "pattern": [ + { + "regexp": "^File \"([^\"].*)\", line (\\d+), characters (\\d+)-(\\d+):$", + "file": 1, + "line": 2, + "column": 3 + }, + { + "regexp": "^(Error|Warning): (.*)$", + "severity": 1, + "message": 2 + } + ] + } + ] +} diff --git a/.github/workflows/coq-hacspec-lib.yml b/.github/workflows/coq-hacspec-lib.yml new file mode 100644 index 000000000..87caa29e2 --- /dev/null +++ b/.github/workflows/coq-hacspec-lib.yml @@ -0,0 +1,100 @@ + +name: Hacspec - Coq Lib + +on: + push: + branches: + - master + pull_request: + branches: + - '**' + +jobs: + build: + # the OS must be GNU/Linux to be able to use the docker-coq-action + runs-on: ubuntu-latest + strategy: + matrix: + image: + - 'coqorg/coq:8.18' + fail-fast: false + steps: + - uses: actions/checkout@v3 + - uses: DeterminateSystems/nix-installer-action@main + - uses: DeterminateSystems/magic-nix-cache-action@main + - name: Build + run: nix build -L + + - name: Install the toolchain + run: | + nix profile install nixpkgs#yq + nix profile install .#rustc + nix profile install . + - name: Install tomlq + run: cargo install --git https://github.com/Techcable/tomlq + + - name: Set up environment + run: | + echo "::group::Setting up problem matcher" + echo "::add-matcher::./.github/coq-errors.json" + echo "::endgroup::" + - name: Build Coq-Hacspec lib + uses: coq-community/docker-coq-action@v1 + with: + opam_file: 'opam/coq-hacspec.opam' + custom_image: ${{ matrix.image }} + + - name: Run Coq on Tests + working-directory: tests + run: | + paths=$(tomlq -r '.workspace.members | .[]' Cargo.toml) + for cratePath in $paths; do + crate=$(tomlq -r '.package.name' "$cratePath/Cargo.toml") + for skip in $SKIPLIST; do + if [[ "$skip" == "$crate" || "$skip" == "$crate-$backend" ]]; then + echo "⛔ $crate [$backend] (skipping)" + continue 2 + fi + done + for backend in coq; do + echo "::group::$crate [$backend]" + cargo hax -C -p "$crate" \; into "$backend" + coqc $cratePath/proofs/coq/extraction/*.v + echo "::endgroup::" + done + done + env: + SKIPLIST: | + enum-struct-variant + literals + slices + naming + if-let + enum-repr + pattern-or + side-effects + v1-lib + mut_arg + fnmut + mut-ref-functionalization + generics + loops + even + odd + never-type + attributes + attribute-opaque + raw-attributes + traits + reordering + nested-derefs + minimal + basic-structs + ping-pong + noise-kkpsk0 + fn-to-letfun + include-flag + recursion +# See also: +# https://github.com/coq-community/docker-coq-action#readme +# https://github.com/erikmd/docker-coq-github-action-demo diff --git a/dune-project b/dune-project new file mode 100644 index 000000000..2c8058a98 --- /dev/null +++ b/dune-project @@ -0,0 +1,24 @@ +(lang dune 3.8) +(using coq 0.8) +(generate_opam_files true) +(name coq-hacspec) +(opam_file_location inside_opam_directory) + +(package + (name coq-hacspec) + (synopsis "A short synopsis") + (description "A longer description") + (maintainers "Lasse Letager Hansen") + (authors "Lasse Letager Hansen") + (depends + ocaml + dune + (base (>= "0.16.2")) + (coq (>= "8.18.0")) + coq-compcert + coq-coqprime + coq-quickchick + ) + (tags + (topics "to describe" your project))) + diff --git a/engine/backends/coq/coq/coq_backend.ml b/engine/backends/coq/coq/coq_backend.ml index 5e04b85cc..64ca727fd 100644 --- a/engine/backends/coq/coq/coq_backend.ml +++ b/engine/backends/coq/coq/coq_backend.ml @@ -73,7 +73,7 @@ open AST module CoqLibrary : Library = struct module Notation = struct let int_repr (x : string) (i : string) : string = - "(@repr" ^ " " ^ "WORDSIZE" ^ x ^ " " ^ i ^ ")" + "(Int" ^ x ^ ".repr" ^ " " ^ i ^ ")" let type_str : string = "Type" let bool_str : string = "bool" @@ -106,17 +106,17 @@ struct id.definition else (* id.crate ^ "_" ^ *) - (* List.fold_left ~init:"" ~f:(fun x y -> x ^ "_" ^ y) *) + (* List.fold_left ~init:"" ~f:(fun x y -> x ^ "_" ^ y) id.path ^ *) id.definition let pglobal_ident (id : global_ident) : string = match id with - | `Projector (`Concrete cid) | `Concrete cid -> pconcrete_ident cid + | `Concrete cid -> pconcrete_ident cid + | `Projector (`Concrete cid) -> pconcrete_ident cid ^ "_ci" | `Primitive p_id -> primitive_to_string p_id | `TupleType _i -> "TODO (global ident) tuple type" | `TupleCons _i -> "TODO (global ident) tuple cons" - | `Projector (`TupleField _) | `TupleField _ -> - "TODO (global ident) tuple field" + | `Projector (`TupleField _) | `TupleField _ -> "TODO (global ident) tuple field" | _ -> . module TODOs_debug = struct @@ -167,14 +167,13 @@ struct | TBool -> C.AST.Bool | TChar -> __TODO_ty__ span "char" | TInt k -> C.AST.Int (pint_kind k) - | TStr -> __TODO_ty__ span "str" + | TStr -> C.AST.NameTy "string" | TApp { ident = `TupleType 0; args = [] } -> C.AST.Unit | TApp { ident = `TupleType 1; args = [ GType ty ] } -> pty span ty | TApp { ident = `TupleType n; args } when n >= 2 -> C.AST.Product (args_ty span args) | TApp { ident; args } -> - C.AST.AppTy - (C.AST.NameTy (pglobal_ident ident ^ "_t"), args_ty span args) + C.AST.AppTy (C.AST.NameTy (pglobal_ident ident), args_ty span args) | TArrow (inputs, output) -> List.fold_right ~init:(pty span output) ~f:(fun x y -> C.AST.Arrow (x, y)) @@ -184,7 +183,11 @@ struct C.AST.ArrayTy (pty span typ, "TODO: Int.to_string length") | TSlice { ty; _ } -> C.AST.SliceTy (pty span ty) | TParam i -> C.AST.NameTy i.name - | TAssociatedType _ -> C.AST.WildTy + | TAssociatedType { impl = Self; item } -> C.AST.NameTy (U.Concrete_ident_view.to_definition_name item) + | TAssociatedType { impl = Dyn; item } -> __TODO_ty__ span "pty: Dyn" + | TAssociatedType { impl = Concrete _; item } -> __TODO_ty__ span "pty: Concrete" + | TAssociatedType { impl = LocalBound _; item } -> __TODO_ty__ span "pty: LocalBound" + | TAssociatedType { impl = goal; item } -> __TODO_ty__ span "pty: LocalBound" | TOpaque _ -> __TODO_ty__ span "pty: TAssociatedType/TOpaque" | _ -> . @@ -195,7 +198,7 @@ struct (match arg with | GLifetime _ -> __TODO_ty__ span "lifetime" | GType x -> pty span x - | GConst _ -> __TODO_ty__ span "const") + | GConst { typ } -> pty span typ) :: args_ty span xs | [] -> [] @@ -255,6 +258,7 @@ struct (c Core__ops__arith__Rem__rem, (2, [ ""; ".%"; "" ])); (c Core__ops__bit__Shl__shl, (2, [ ""; " shift_left "; "" ])); (c Core__ops__bit__Shr__shr, (2, [ ""; " shift_right "; "" ])); + (c Core__ops__bit__Not__not, (1, [ " negb "; "" ])); (* TODO: those two are not notations/operators at all, right? *) (* (c "secret_integers::rotate_left", (2, [ "rol "; " "; "" ])); *) (* (c "hacspec::lib::foldi", (4, [ "foldi "; " "; " "; " "; "" ])); *) @@ -276,7 +280,7 @@ struct let span = e.span in match e.e with | Literal l -> C.AST.Const (pliteral e.span l) - | LocalVar local_ident -> C.AST.NameTerm local_ident.name + | LocalVar local_ident -> C.AST.NameTerm (local_ident.name) | GlobalVar (`TupleCons 0) | Construct { constructor = `TupleCons 0; fields = []; _ } -> C.AST.UnitTerm @@ -298,8 +302,8 @@ struct (* __TODO_term__ span "GLOBAL APP?" *) | App { f; args; _ } -> let base = pexpr f in - let args = List.map ~f:pexpr args in - C.AST.App (base, args) + let args = List.map ~f:(fun x -> C.AST.TypedTerm (pexpr x, pty span x.typ)) args in + C.AST.TypedTerm (C.AST.App (base, args), pty span e.typ) | If { cond; then_; else_ } -> C.AST.If ( pexpr cond, @@ -341,8 +345,8 @@ struct | Construct { is_record = true; constructor; fields; _ } -> (* TODO: handle base *) C.AST.RecordConstructor - ( pglobal_ident constructor, - List.map ~f:(fun (f, e) -> (pglobal_ident f, pexpr e)) fields ) + ( "t_" ^ pglobal_ident constructor, + List.map ~f:(fun (f, e) -> (pglobal_ident constructor, pexpr e)) fields ) | Construct { is_record = false; constructor; fields = [ (_f, e) ]; _ } -> C.AST.App (C.AST.Var (pglobal_ident constructor), [ pexpr e ]) | Construct { constructor; _ } -> @@ -390,20 +394,16 @@ struct | TyAlias { name; ty; _ } -> [ C.AST.Notation - ( "'" ^ pconcrete_ident name ^ "_t" ^ "'", - C.AST.Type (pty span ty), - None ); + ("'" ^ pconcrete_ident name ^ "'", C.AST.Type (pty span ty), None); ] (* record *) - | Type { name; generics; variants = [ v ]; is_struct = true } -> + | Type { name; generics; variants = [ { arguments; is_record = true; _ } ]; is_struct = true } -> [ (* TODO: generics *) C.AST.Record ( U.Concrete_ident_view.to_definition_name name, List.map ~f:(pgeneric_param_as_argument span) generics.params, - List.map - ~f:(fun (x, y) -> C.AST.Named (x, y)) - (p_record_record span v.arguments) ); + List.map ~f:(fun (x, y) -> C.AST.Named (U.Concrete_ident_view.to_definition_name name ^ "_" ^ x, y)) (p_record_record span arguments) ); ] (* enum *) | Type { name; generics; variants; _ } -> @@ -442,7 +442,7 @@ struct in [ C.AST.Notation - ( "'" ^ o.type_name ^ "_t" ^ "'", + ( "'" ^ o.type_name ^ "'", C.AST.Type (C.AST.NatMod ( o.type_of_canvas, @@ -454,8 +454,7 @@ struct [], C.AST.Var "id", C.AST.Arrow - ( C.AST.NameTy (o.type_name ^ "_t"), - C.AST.NameTy (o.type_name ^ "_t") ) ); + (C.AST.NameTy o.type_name, C.AST.NameTy o.type_name) ); ] | "bytes" -> let open Hacspeclib_macro_parser in @@ -464,7 +463,7 @@ struct in [ C.AST.Notation - ( "'" ^ o.bytes_name ^ "_t" ^ "'", + ( "'" ^ o.bytes_name ^ "'", C.AST.Type (C.AST.ArrayTy ( C.AST.Int { size = C.AST.U8; signed = false }, @@ -475,8 +474,8 @@ struct [], C.AST.Var "id", C.AST.Arrow - ( C.AST.NameTy (o.bytes_name ^ "_t"), - C.AST.NameTy (o.bytes_name ^ "_t") ) ); + (C.AST.NameTy o.bytes_name, C.AST.NameTy o.bytes_name) + ); ] | "unsigned_public_integer" -> let open Hacspeclib_macro_parser in @@ -485,7 +484,7 @@ struct in [ C.AST.Notation - ( "'" ^ o.integer_name ^ "_t" ^ "'", + ( "'" ^ o.integer_name ^ "'", C.AST.Type (C.AST.ArrayTy ( C.AST.Int { size = C.AST.U8; signed = false }, @@ -496,8 +495,8 @@ struct [], C.AST.Var "id", C.AST.Arrow - ( C.AST.NameTy (o.integer_name ^ "_t"), - C.AST.NameTy (o.integer_name ^ "_t") ) ); + ( C.AST.NameTy o.integer_name, + C.AST.NameTy o.integer_name ) ); ] | "public_bytes" -> let open Hacspeclib_macro_parser in @@ -510,15 +509,14 @@ struct (* int_of_string *) o.size ) in [ - C.AST.Notation - ("'" ^ o.bytes_name ^ "_t" ^ "'", C.AST.Type typ, None); + C.AST.Notation ("'" ^ o.bytes_name ^ "'", C.AST.Type typ, None); C.AST.Definition ( o.bytes_name, [], C.AST.Var "id", C.AST.Arrow - ( C.AST.NameTy (o.bytes_name ^ "_t"), - C.AST.NameTy (o.bytes_name ^ "_t") ) ); + (C.AST.NameTy o.bytes_name, C.AST.NameTy o.bytes_name) + ); ] | "array" -> let open Hacspeclib_macro_parser in @@ -541,7 +539,7 @@ struct in [ C.AST.Notation - ( "'" ^ o.array_name ^ "_t" ^ "'", + ( "'" ^ o.array_name ^ "'", C.AST.Type (C.AST.ArrayTy ( C.AST.Int { size = typ; signed = false }, @@ -552,8 +550,8 @@ struct [], C.AST.Var "id", C.AST.Arrow - ( C.AST.NameTy (o.array_name ^ "_t"), - C.AST.NameTy (o.array_name ^ "_t") ) ); + (C.AST.NameTy o.array_name, C.AST.NameTy o.array_name) + ); ] | _ -> unsupported ()) | _ -> unsupported ()) @@ -578,7 +576,13 @@ struct match x.ti_v with | TIFn fn_ty -> pty span fn_ty | TIDefault _ -> . - | _ -> __TODO_ty__ span "field_ty" )) + | TIType impl_list -> + C.AST.TypeTy + (* C.AST.Product *) + (* (List.map *) + (* ~f:(fun { goal = { trait; args }; name } -> C.AST.NameTy (U.Concrete_ident_view.to_definition_name trait)) *) + (* impl_list) *) + )) items ); ] | Impl { generics; self_ty; of_trait = name, gen_vals; items } -> @@ -588,26 +592,24 @@ struct List.map ~f:(pgeneric_param_as_argument span) generics.params, pty span self_ty, args_ty span gen_vals, - List.map - ~f:(fun x -> - match x.ii_v with + List.fold_left ~init:[] + ~f:(fun y x -> + y @ (match x.ii_v with | IIFn { body; params } -> - ( U.Concrete_ident_view.to_definition_name x.ii_ident, + [( U.Concrete_ident_view.to_definition_name x.ii_ident, List.map ~f:(fun { pat; typ; _ } -> C.AST.Explicit (ppat pat, pty span typ)) params, pexpr body, - pty span body.typ ) - | _ -> - ( "todo_name", - [], - __TODO_term__ span "body", - __TODO_ty__ span "typ" )) + pty span body.typ )] + | IIType { typ; parent_bounds } -> + [] (* TODO: Is this just Self? *))) items ); ] + | _ -> . - and p_inductive span variants _parrent_name : C.AST.inductive_case list = + and p_inductive span variants parrent_name : C.AST.inductive_case list = List.map variants ~f:(fun { name; arguments; is_record; _ } -> if is_record then C.AST.InductiveCase @@ -673,11 +675,13 @@ let string_of_items : AST.item list -> string = let hardcoded_coq_headers = "(* File automatically generated by Hacspec *)\n\ - From Hacspec Require Import Hacspec_Lib MachineIntegers.\n\ + From Hacspec Require Import Hacspec_Lib.\n\ From Coq Require Import ZArith.\n\ Import List.ListNotations.\n\ + Require Import Coq.Strings.String.\n\ Open Scope Z_scope.\n\ - Open Scope bool_scope.\n" + Open Scope bool_scope.\n\ + Open Scope hacspec_scope.\n" let translate _ (_bo : BackendOptions.t) (items : AST.item list) : Types.file list = diff --git a/engine/backends/coq/coq_ast.ml b/engine/backends/coq/coq_ast.ml index 1fd848982..5e0b8f7e4 100644 --- a/engine/backends/coq/coq_ast.ml +++ b/engine/backends/coq/coq_ast.ml @@ -163,15 +163,15 @@ functor | AST.Product [] | AST.Unit -> (Lib.Notation.unit_str, false (* TODO: might need paren *)) | AST.TypeTy -> (Lib.Notation.type_str, false (* TODO: might need paren *)) - | AST.Int { size = AST.USize; _ } -> ("uint_size", false) - | AST.Int { size; _ } -> ("int" ^ int_size_to_string size, false) + | AST.Int { size = AST.USize; _ } -> ("t_usize", false) + | AST.Int { size; _ } -> ("t_u" ^ int_size_to_string size, false) | AST.NameTy s -> (s, false) | AST.RecordTy (name, _fields) -> (* [ AST.Record (name, fields) ] *) (name, false) | AST.Product l -> let ty_str = String.concat - ~sep:(" " ^ "×" ^ " ") + ~sep:(" " ^ "*" ^ " ") (* TODO, notations differ for SSProve '×' *) (List.map ~f:ty_to_string_without_paren l) in (ty_str, true) @@ -256,7 +256,7 @@ functor let literal_to_string (x : AST.literal) : string = match x with - | Const_string s -> s + | Const_string s -> "\"" ^ s ^ "\"%string" | Const_char c -> Int.to_string c (* TODO *) | Const_int (i, { size; _ }) -> Lib.Notation.int_repr (int_size_to_string size) i @@ -297,15 +297,21 @@ functor ^ ")" (* TODO: Should this be true of false? *) | AST.DisjunctivePat pats -> let f pat = pat_to_string pat true depth in - String.concat ~sep:" | " @@ List.map ~f pats + "(" ^ (String.concat ~sep:" | " @@ List.map ~f pats) ^ ")" and tick_if is_top_expr = if is_top_expr then "'" else "" let rec term_to_string (x : AST.term) depth : string * bool = match x with | AST.UnitTerm -> ("tt", false) - | AST.Let { pattern = pat; value = bind; value_typ = typ; body = term; _ } - -> + | AST.Let + { + pattern = AST.AscriptionPat (pat, _) | pat; + value = bind; + value_typ = typ; + body = term; + _; + } -> (* TODO: propegate type definition *) let var_str = pat_to_string pat true depth in let expr_str = term_to_string_without_paren bind (depth + 1) in @@ -364,8 +370,8 @@ functor ^ (if List.length args > 0 then " " else "") ^ String.concat ~sep:" " (List.map - ~f:(fun (n, t) -> - "(" ^ n ^ " " ^ ":=" ^ " " + ~f:(fun (_n, t) -> + "(" (* ^ n ^ " " ^ ":=" *) ^ " " ^ term_to_string_without_paren t depth ^ ")") args), @@ -417,6 +423,7 @@ functor ^ "]", true ) | AST.Array [] -> ("!TODO empty array!", false) + | AST.TypedTerm (AST.TypedTerm (e, t), _) -> term_to_string (AST.TypedTerm (e, t)) depth | AST.TypedTerm (e, t) -> ( term_to_string_without_paren e depth ^ " " ^ ":" ^ " " ^ ty_to_string_with_paren t, diff --git a/hax-lib-macros/src/lib.rs b/hax-lib-macros/src/lib.rs index 22261bf84..e81913c09 100644 --- a/hax-lib-macros/src/lib.rs +++ b/hax-lib-macros/src/lib.rs @@ -382,6 +382,27 @@ pub fn ensures(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream .into() } +/// Exclude this item from the Hax translation. +#[proc_macro_error] +#[proc_macro_attribute] +pub fn interface(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream { + let item: ItemFn = parse_macro_input!(item); + let ItemFn { + // The function signature + sig, + // The visibility specifier of this function + vis, + // The function block or body + block, + // Other attributes applied to this function + attrs, + } = item.clone(); + + quote! { + #(#attrs)* #vis #sig { todo!() } + }.into() +} + mod kw { syn::custom_keyword!(hax_lib); syn::custom_keyword!(decreases); diff --git a/hax-lib/src/proc_macros.rs b/hax-lib/src/proc_macros.rs index 866c7cfda..e5cf39666 100644 --- a/hax-lib/src/proc_macros.rs +++ b/hax-lib/src/proc_macros.rs @@ -2,7 +2,7 @@ //! proc-macro crate cannot export anything but procedural macros. pub use hax_lib_macros::{ - attributes, ensures, exclude, impl_fn_decoration, include, lemma, loop_invariant, opaque_type, + attributes, ensures, exclude, impl_fn_decoration, include, interface, lemma, loop_invariant, opaque_type, refinement_type, requires, trait_fn_decoration, }; diff --git a/opam/coq-hacspec.opam b/opam/coq-hacspec.opam new file mode 100644 index 000000000..ef220caae --- /dev/null +++ b/opam/coq-hacspec.opam @@ -0,0 +1,31 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +synopsis: "A short synopsis" +description: "A longer description" +maintainer: ["Lasse Letager Hansen"] +authors: ["Lasse Letager Hansen"] +tags: ["topics" "to describe" "your" "project"] +depends: [ + "ocaml" + "dune" {>= "3.8"} + "base" {>= "0.16.2"} + "coq" {>= "8.18.0"} + "coq-compcert" + "coq-coqprime" + "coq-quickchick" + "odoc" {with-doc} +] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] diff --git a/proof-libs/coq/coq/.gitignore b/proof-libs/coq/coq/.gitignore new file mode 100644 index 000000000..0b7287c5c --- /dev/null +++ b/proof-libs/coq/coq/.gitignore @@ -0,0 +1,7 @@ +*.vo* +*.aux +*.glob +*.cache +.Makefile.d +Makefile +Makefile.conf diff --git a/proof-libs/coq/coq/README.md b/proof-libs/coq/coq/README.md new file mode 100644 index 000000000..62587eca1 --- /dev/null +++ b/proof-libs/coq/coq/README.md @@ -0,0 +1,21 @@ +## Dependencies + +The coq libraries uses `compcert` for machine signed and unsigned integer modulo arithmetic, and `coqprime` for finite field arithmetic on prime modulus (to support hacspec's `nat_mod p` type). +These requires the following repository: + +``` +opam repo add coq-released https://coq.inria.fr/opam/released --all-switches +``` + +Then one can install the dependencies through `opam`: + +``` +opam install coq-compcert coq-coqprime +``` +(assuming you have coq installed through opam). + +## Compiling the coq files + +In folder `/coq`, type `make`. This compiles the coq libraries and the compiled examples, as defined in `_CoqProject`. This requires the coq compiler to be installed. + +If you want to add a new example to `_CoqProject`, such that it is compiled through `make`, you should run `coq_makefile -f _CoqProject -o Makefile` in `/coq` to update the makefile. diff --git a/proof-libs/coq/coq/_CoqProject b/proof-libs/coq/coq/_CoqProject new file mode 100644 index 000000000..c9279aeb1 --- /dev/null +++ b/proof-libs/coq/coq/_CoqProject @@ -0,0 +1,10 @@ +-R src/ Hacspec +-arg -w +-arg all + +src/Hacspec_Types.v +src/Hacspec_Integers.v +src/Hacspec_TODO.v +src/Hacspec_Lib.v +src/Hacspec_lib.v +src/QuickChickLib.v diff --git a/proof-libs/coq/coq/docker_build/Dockerfile b/proof-libs/coq/coq/docker_build/Dockerfile new file mode 100644 index 000000000..2892719e2 --- /dev/null +++ b/proof-libs/coq/coq/docker_build/Dockerfile @@ -0,0 +1,12 @@ +FROM coqorg/coq:8.16 +RUN curl https://sh.rustup.rs -sSf | sh -s -- -y +ENV PATH $HOME/.cargo/bin:$PATH +RUN rustup update +RUN rustup toolchain install nightly-2022-07-04 +RUN rustup component add --toolchain nightly-2022-07-04 rustc-dev llvm-tools-preview rust-analysis rust-src +RUN rustc --version +RUN cargo --version +RUN opam config list; opam repo list; opam list +RUN opam repo add coq-released https://coq.inria.fr/opam/released --all-switches +RUN opam update +RUN opam install coq-compcert coq-coqprime coq-quickchick --yes diff --git a/proof-libs/coq/coq/src/Hacspec_Integers.v b/proof-libs/coq/coq/src/Hacspec_Integers.v new file mode 100644 index 000000000..17ae34a86 --- /dev/null +++ b/proof-libs/coq/coq/src/Hacspec_Integers.v @@ -0,0 +1,363 @@ +Global Set Warnings "-ambiguous-paths". +Global Set Warnings "-uniform-inheritance". +Global Set Warnings "-auto-template". +Global Set Warnings "-disj-pattern-notation". +(*** Integers *) +From Coq Require Import ZArith List. +Import ListNotations. +(* Require Import IntTypes. *) + +(* Require Import MachineIntegers. *) From compcert Require Import Integers. +From Coqprime Require GZnZ. + +Require Import Lia. + +Declare Scope hacspec_scope. + +Set Default Goal Selector "!". + +(*** Positive util *) + +Fixpoint binary_representation_pre (n : nat) {struct n}: positive := + match n with + | O => 1 + | S O => 1 + | S n => Pos.succ (binary_representation_pre n) + end%positive. +Definition binary_representation (n : nat) `(n <> O) := binary_representation_pre n. + +Theorem positive_is_succs : forall n, forall (H : n <> O) (K : S n <> O), + @binary_representation (S n) K = Pos.succ (@binary_representation n H). +Proof. induction n ; [contradiction | reflexivity]. Qed. + +(* Conversion of positive to binary Int8.representation *) +Theorem positive_to_positive_succs : forall p, binary_representation (Pos.to_nat p) (Nat.neq_sym _ _ (Nat.lt_neq _ _ (Pos2Nat.is_pos p))) = p. +Proof. + intros p. + generalize dependent (Nat.neq_sym 0 (Pos.to_nat p) (Nat.lt_neq 0 (Pos.to_nat p) (Pos2Nat.is_pos p))). + + destruct Pos.to_nat eqn:ptno. + - contradiction. + - generalize dependent p. + induction n ; intros. + + cbn. + apply Pos2Nat.inj. + symmetry. + apply ptno. + + rewrite positive_is_succs with (H := Nat.neq_succ_0 n). + rewrite IHn with (p := Pos.of_nat (S n)). + * rewrite <- Nat2Pos.inj_succ by apply Nat.neq_succ_0. + rewrite <- ptno. + apply Pos2Nat.id. + * apply Nat2Pos.id. + apply Nat.neq_succ_0. +Qed. + +(*** Hacspec Integers *) + +Class MyAdd (A : Type) := myadd : A -> A -> A. +Infix ".+" := (myadd) (at level 77) : hacspec_scope. + +Module HacspecIntegers (WS : WORDSIZE). + Include (Make WS). + (**** Public integers *) + + Definition pub (n : Z) : int := repr n. + + (**** Operations *) + + (* Should maybe use size of s instead? *) + Definition rotate_left (u: int) (s: int) : int := rol u s. + + Definition pub_uint_wrapping_add (x y: int) : int := add x y. + + Definition shift_left_ (i : int) (j : int) := + shl i j. + + Definition shift_right_ (i : int) (j : int) := + shr i j. + + Infix "shift_left" := (shift_left_) (at level 77) : hacspec_scope. + Infix "shift_right" := (shift_right_) (at level 77) : hacspec_scope. + + Instance MyAddInstance : MyAdd int := add. + + Infix "%%" := Z.rem (at level 40, left associativity) : Z_scope. + (* Infix ".+" := (add) (at level 77) : hacspec_scope. *) + Infix ".-" := (sub) (at level 77) : hacspec_scope. + Notation "-" := (neg) (at level 77) : hacspec_scope. + Infix ".*" := (mul) (at level 77) : hacspec_scope. + Infix "./" := (divs) (at level 77) : hacspec_scope. + Infix ".%" := (mods) (at level 77) : hacspec_scope. + Infix ".^" := (xor) (at level 77) : hacspec_scope. + Infix ".&" := (and) (at level 77) : hacspec_scope. + Infix ".|" := (or) (at level 77) : hacspec_scope. + Infix "==" := (eq) (at level 32) : hacspec_scope. + (* Definition one := (@one WORDSIZE32). *) + (* Definition zero := (@zero WORDSIZE32). *) + Notation "A × B" := (prod A B) (at level 79, left associativity) : hacspec_scope. + + (*** Uint size util *) + + (* If a natural number is in bound then a smaller natural number is still in bound *) + Lemma range_of_nat_succ : + forall i, (Z.pred 0 < Z.of_nat (S i) < modulus)%Z -> (Z.pred 0 < Z.of_nat i < modulus)%Z. + Proof. lia. Qed. + + (* Conversion to equivalent bound *) + Lemma modulus_range_helper : + forall i, (Z.pred 0 < i < modulus)%Z -> (0 <= i <= max_unsigned)%Z. + Proof. unfold max_unsigned. lia. Qed. + + Definition unsigned_repr_alt (a : Z) `((Z.pred 0 < a < modulus)%Z) : unsigned (repr a) = a := + unsigned_repr a (modulus_range_helper a H). + + Theorem zero_always_modulus : (Z.pred 0 < 0 < modulus)%Z. + Proof. easy. Qed. + + (* any uint_size can be .represented as a natural number and a bound *) + (* this is easier for proofs, however less efficient for computation *) + (* as Z uses a binary .representation *) + Theorem int_as_nat : + forall (us: int), + { n : nat | + us = repr (Z.of_nat n) /\ (Z.pred 0 < Z.of_nat n < modulus)%Z}. + Proof. + destruct us as [intval intrange]. + exists (Z.to_nat intval). + rewrite Z2Nat.id by (apply Z.lt_pred_le ; apply intrange). + + split. + - apply mkint_eq. + rewrite Z_mod_modulus_eq. + rewrite Z.mod_small. + + reflexivity. + + lia. + - apply intrange. + Qed. + + (* destruct int as you would a natural number *) + Definition destruct_int_as_nat (a : int) : forall (P : int -> Prop), + forall (zero_case : P (repr 0)), + forall (succ_case : forall (n : nat), (Z.pred 0 < Z.of_nat n < modulus)%Z -> P (repr (Z.of_nat n))), + P a. + Proof. + intros. + destruct (int_as_nat a) as [ n y ] ; destruct y as [ya yb] ; subst. + destruct n. + - apply zero_case. + - apply succ_case. + apply yb. + Qed. + + Ltac destruct_int_as_nat a := + generalize dependent a ; + intros a ; + apply (destruct_int_as_nat a) ; [ pose proof (@unsigned_repr_alt 0 zero_always_modulus) | let n := fresh in let H := fresh in intros n H ; pose proof (@unsigned_repr_alt _ H)] ; intros. + + (* induction for int as you would do for a natural number *) + Definition induction_int_as_nat : + forall (P : int -> Prop), + (P (repr 0)) -> + (forall n, + (Z.pred 0 < Z.succ (Z.of_nat n) < @modulus)%Z -> + P (repr (Z.of_nat n)) -> + P (repr (Z.succ (Z.of_nat n)))) -> + forall (a : int), P a. + Proof. + intros P H_zero H_ind a. + destruct (int_as_nat a) as [ n y ] ; destruct y as [ya yb] ; subst. + induction n. + - apply H_zero. + - rewrite Nat2Z.inj_succ. + apply H_ind. + + rewrite <- Nat2Z.inj_succ. + apply yb. + + apply IHn. + lia. + Qed. + + Ltac induction_int_as_nat var := + generalize dependent var ; + intros var ; + apply induction_int_as_nat with (a := var) ; [ pose proof (@unsigned_repr_alt 0 zero_always_modulus) | let n := fresh in let IH := fresh in intros n IH ; pose proof (@unsigned_repr_alt _ IH)] ; intros. + + (* conversion of usize to positive or zero and the respective bound *) + Theorem int_as_positive : + forall (us: int), + { pu : unit + positive | + match pu with inl u => us = repr Z0 | inr p => us = repr (Z.pos p) /\ (Z.pred 0 < Z.pos p < @modulus)%Z end + }. + Proof. + destruct us as [intval intrange]. + destruct intval. + - exists (inl tt). apply mkint_eq. reflexivity. + - exists (inr p). + split. + + apply mkint_eq. + rewrite Z_mod_modulus_eq. + symmetry. + apply Zmod_small. + lia. + + apply intrange. + - exfalso. + lia. + Defined. + + (* destruction of int as positive *) + Definition destruct_int_as_positive (a : int) : forall (P : int -> Prop), + (P (repr 0)) -> + (forall b, (Z.pred 0 < Z.pos b < @modulus)%Z -> P (repr (Z.pos b))) -> + P a. + Proof. + intros P H_zero H_succ. + destruct (int_as_positive a) as [ [ _ | b ] y ] ; [ subst | destruct y as [ya yb] ; subst ]. + - apply H_zero. + - apply H_succ. + apply yb. + Qed. + + Ltac destruct_int_as_positive a := + generalize dependent a ; + intros a ; + apply (destruct_int_as_positive a) ; intros. + + (* induction of int as positive *) + Definition induction_int_as_positive : + forall (P : int -> Prop), + (P (repr 0)) -> + (P (repr 1)) -> + (forall b, + (Z.pred 0 < Z.succ (Z.pos b) < @modulus)%Z -> + P (repr (Z.pos b)) -> + P (repr (Z.succ (Z.pos b)))) -> + forall (a : int), P a. + Proof. + intros P H_zero H_one H_ind a. + + destruct (int_as_positive a) as [ [ _ | b ] y ] ; [ subst | destruct y as [ya yb] ; subst ]. + - apply H_zero. + - pose proof (pos_succ_b := positive_to_positive_succs b) + ; symmetry in pos_succ_b + ; rewrite pos_succ_b in * + ; clear pos_succ_b. + + generalize dependent (Nat.neq_sym 0 (Pos.to_nat b) (Nat.lt_neq 0 (Pos.to_nat b) (Pos2Nat.is_pos b))). + + induction (Pos.to_nat b). + + contradiction. + + intros n_neq yb. + destruct n. + * apply H_one. + * rewrite (positive_is_succs _ (Nat.neq_succ_0 n) n_neq) in *. + rewrite Pos2Z.inj_succ in *. + apply H_ind. + -- apply yb. + -- apply IHn. + lia. + Qed. + + Ltac induction_int_as_positive var := + generalize dependent var ; + intros var ; + apply induction_int_as_positive with (a := var) ; intros ; [ | | ]. + +End HacspecIntegers. + +Module Wordsize_16 : WORDSIZE. + Definition wordsize := 16. + Theorem wordsize_not_zero : wordsize <> 0%nat. easy. Qed. +End Wordsize_16. + +Module Wordsize_128 : WORDSIZE. + Definition wordsize := 128. + Theorem wordsize_not_zero : wordsize <> 0%nat. easy. Qed. +End Wordsize_128. + +Module Int8 := HacspecIntegers Wordsize_8. +Module Int16 := HacspecIntegers Wordsize_16. +Module Int32 := HacspecIntegers Wordsize_32. +Module Int64 := HacspecIntegers Wordsize_64. +Module Int128 := HacspecIntegers Wordsize_128. + +Import Int128. Export Int128. +Import Int64. Export Int64. +Import Int32. Export Int32. +Import Int16. Export Int16. +Import Int8. Export Int8. + +Definition int8 := Int8.int. +Definition int16 := Int16.int. +Definition int32 := Int32.int. +Definition int64 := Int64.int. +Definition int128 := Int128.int. + +(* Instance int8_add : MyAdd int8 := Int8.add. *) +(* Instance int16_add : MyAdd int16 := Int16.add. *) +(* Instance int32_add : MyAdd int32 := Int32.add. *) +(* Instance int64_add : MyAdd int64 := Int64.add. *) +(* Instance int128_add : MyAdd int128 := Int128.add. *) + +(* CompCert integers' signedness is only interpreted through 'signed' and 'unsigned', + and not in the representation. Therefore, uints are just names for their respective ints. + *) +Definition uint8 := int8. +Definition uint16 := int16. +Definition uint32 := int32. +Definition uint64 := int64. +Definition uint128 := int128. + +Definition uint_size := int32. +Definition int_size := int32. + +Axiom declassify_usize_from_uint8 : uint8 -> uint_size. + +(* Represents any type that can be converted to uint_size and back *) +Class UInt_sizable (A : Type) := { + usize : A -> uint_size; + from_uint_size : uint_size -> A; +}. +Arguments usize {_} {_}. +Arguments from_uint_size {_} {_}. + +Global Instance nat_uint_sizable : UInt_sizable nat := { + usize n := Int32.repr (Z.of_nat n); + from_uint_size n := Z.to_nat (Int32.unsigned n); +}. + +Global Instance N_uint_sizable : UInt_sizable N := { + usize n := Int32.repr (Z.of_N n); + from_uint_size n := Z.to_N (Int32.unsigned n); +}. + +Global Instance Z_uint_sizable : UInt_sizable Z := { + usize n := Int32.repr n; + from_uint_size n := Int32.unsigned n; +}. + + +(* Same, but for int_size *) +Class Int_sizable (A : Type) := { + isize : A -> int_size; + from_int_size : int_size -> A; +}. + +Arguments isize {_} {_}. +Arguments from_int_size {_} {_}. + +Global Instance nat_Int_sizable : Int_sizable nat := { + isize n := Int32.repr (Z.of_nat n); + from_int_size n := Z.to_nat (Int32.signed n); +}. + +Global Instance N_Int_sizable : Int_sizable N := { + isize n := Int32.repr (Z.of_N n); + from_int_size n := Z.to_N (Int32.signed n); +}. + +Global Instance Z_Int_sizable : Int_sizable Z := { + isize n := Int32.repr n; + from_int_size n := Int32.signed n; +}. + +Notation secret := id. diff --git a/proof-libs/coq/coq/src/Hacspec_Lib.v b/proof-libs/coq/coq/src/Hacspec_Lib.v new file mode 100644 index 000000000..277174a92 --- /dev/null +++ b/proof-libs/coq/coq/src/Hacspec_Lib.v @@ -0,0 +1,1475 @@ +Global Set Warnings "-ambiguous-paths". +Global Set Warnings "-uniform-inheritance". +Global Set Warnings "-auto-template". +Global Set Warnings "-disj-pattern-notation". +(*** Integers *) +From Coq Require Import ZArith List. +Import ListNotations. +(* Require Import IntTypes. *) + +(* Require Import MachineIntegers. *) From compcert Require Import Integers. +From Coqprime Require GZnZ. + +Require Import Lia. + +Declare Scope hacspec_scope. + +From Hacspec Require Import Hacspec_Types. Export Hacspec_Types. +From Hacspec Require Import Hacspec_Integers. Export Hacspec_Integers. +From Hacspec Require Import Hacspec_TODO. Export Hacspec_TODO. + +(* Notation *) + +Infix "'×" := prod (at level 100) : hacspec_scope. + +(*** Loops *) + +Open Scope nat_scope. +Fixpoint foldi_ + {acc : Type} + (fuel : nat) + (i : uint_size) + (f : uint_size -> acc -> acc) + (cur : acc) : acc := + match fuel with + | 0 => cur + | S n' => foldi_ n' (Int32.add i Int32.one) f (f i cur) + end. +Close Scope nat_scope. +Definition foldi + {acc: Type} + (lo: uint_size) + (hi: uint_size) (* {lo <= hi} *) + (f: (uint_size) -> acc -> acc) (* {i < hi} *) + (init: acc) : acc := + match Z.sub (Int32.unsigned hi) (Int32.unsigned lo) with + | Z0 => init + | Zneg p => init + | Zpos p => foldi_ (Pos.to_nat p) lo f init + end. + +(* Fold done using natural numbers for bounds *) +Fixpoint foldi_nat_ + {acc : Type} + (fuel : nat) + (i : nat) + (f : nat -> acc -> acc) + (cur : acc) : acc := + match fuel with + | O => cur + | S n' => foldi_nat_ n' (S i) f (f i cur) + end. +Definition foldi_nat + {acc: Type} + (lo: nat) + (hi: nat) (* {lo <= hi} *) + (f: nat -> acc -> acc) (* {i < hi} *) + (init: acc) : acc := + match Nat.sub hi lo with + | O => init + | S n' => foldi_nat_ (S n') lo f init + end. + +Lemma foldi__move_S : + forall {acc: Type} + (fuel : nat) + (i : uint_size) + (f : uint_size -> acc -> acc) + (cur : acc), + foldi_ fuel (Int32.add i Int32.one) f (f i cur) = foldi_ (S fuel) i f cur. +Proof. reflexivity. Qed. + +Lemma foldi__nat_move_S : + forall {acc: Type} + (fuel : nat) + (i : nat) + (f : nat -> acc -> acc) + (cur : acc), + foldi_nat_ fuel (S i) f (f i cur) = foldi_nat_ (S fuel) i f cur. +Proof. reflexivity. Qed. + +(* You can do one iteration of the fold by burning a unit of fuel *) +Lemma foldi__move_S_fuel : + forall {acc: Type} + (fuel : nat) + (i : uint_size) + (f : uint_size -> acc -> acc) + (cur : acc), + (0 <= Z.of_nat fuel <= Int32.max_unsigned)%Z -> + f (Int32.add (Int32.repr (Z.of_nat fuel)) i) (foldi_ (fuel) i f cur) = foldi_ (S (fuel)) i f cur. +Proof. + intros acc fuel. + induction fuel ; intros. + - cbn. + replace (Int32.repr 0) with (Int32.zero) by reflexivity. + rewrite Int32.add_zero_l. + reflexivity. + - do 2 rewrite <- foldi__move_S. + replace (Int32.add (Int32.repr (Z.of_nat (S fuel))) i) + with (Int32.add (Int32.repr (Z.of_nat fuel)) (Int32.add i Int32.one)). + 2 : { + rewrite <- (Int32.add_commut Int32.one). + rewrite <- Int32.add_assoc. + f_equal. + unfold Int32.add. + f_equal. + rewrite Int32.unsigned_one. + rewrite Z.add_1_r. + rewrite Nat2Z.inj_succ. + f_equal. + apply Int32.unsigned_repr. + lia. + } + rewrite IHfuel. + reflexivity. + lia. +Qed. + +(* You can do one iteration of the fold by burning a unit of fuel *) +Lemma foldi__nat_move_S_fuel : + forall {acc: Type} + (fuel : nat) + (i : nat) + (f : nat -> acc -> acc) + (cur : acc), + (0 <= Z.of_nat fuel <= @Int32.max_unsigned)%Z -> + f (fuel + i)%nat (foldi_nat_ fuel i f cur) = foldi_nat_ (S fuel) i f cur. +Proof. + induction fuel ; intros. + - reflexivity. + - do 2 rewrite <- foldi__nat_move_S. + + Require Import PeanoNat. + replace (S fuel + i)%nat with (fuel + (S i))%nat by (symmetry ; apply plus_n_Sm). + rewrite IHfuel. + + reflexivity. + + lia. +Qed. + +(* folds and natural number folds compute the same thing *) +Lemma foldi_to_foldi_nat : + forall {acc: Type} + (lo: uint_size) (* {lo <= hi} *) + (hi: uint_size) (* {lo <= hi} *) + (f: (uint_size) -> acc -> acc) (* {i < hi} *) + (init: acc), + (Int32.unsigned lo <= Int32.unsigned hi)%Z -> + foldi lo hi f init = foldi_nat (Z.to_nat (Int32.unsigned lo)) (Z.to_nat (Int32.unsigned hi)) (fun x => f (Int32.repr (Z.of_nat x))) init. +Proof. + intros. + + unfold foldi. + unfold foldi_nat. + + destruct (Int32.int_as_nat hi) as [ hi_n [ hi_eq hi_H ] ] ; subst. + rewrite (Int32.unsigned_repr_alt _ hi_H) in *. + rewrite Nat2Z.id. + + destruct (Int32.int_as_nat lo) as [ lo_n [ lo_eq lo_H ] ] ; subst. + rewrite (Int32.unsigned_repr_alt _ lo_H) in *. + rewrite Nat2Z.id. + + remember (hi_n - lo_n)%nat as n. + apply f_equal with (f := Z.of_nat) in Heqn. + rewrite (Nat2Z.inj_sub) in Heqn by (apply Nat2Z.inj_le ; apply H). + rewrite <- Heqn. + + assert (H_bound : (Z.pred 0 < Z.of_nat n < Int32.modulus)%Z) by lia. + + clear Heqn. + induction n. + - reflexivity. + - pose proof (H_max_bound := Int32.modulus_range_helper _ (Int32.range_of_nat_succ _ H_bound)). + rewrite <- foldi__nat_move_S_fuel by apply H_max_bound. + cbn. + rewrite SuccNat2Pos.id_succ. + rewrite <- foldi__move_S_fuel by apply H_max_bound. + + destruct n. + + cbn. + replace (Int32.repr 0) with (Int32.zero) by reflexivity. + rewrite Int32.add_zero_l. + reflexivity. + + cbn in *. + assert (H_bound_pred: (Z.pred 0 < Z.pos (Pos.of_succ_nat n) < @Int32.modulus)%Z) by lia. + rewrite <- (IHn H_bound_pred) ; clear IHn. + f_equal. + * unfold Int32.add. + f_equal. + rewrite (Int32.unsigned_repr_alt _ lo_H) in *. + rewrite (Int32.unsigned_repr_alt _ H_bound_pred). + do 2 rewrite Zpos_P_of_succ_nat. + rewrite Z.add_succ_l. + f_equal. + rewrite Nat2Z.inj_add. + reflexivity. + * rewrite SuccNat2Pos.id_succ. + rewrite foldi__move_S. + reflexivity. +Qed. + +(* folds can be computed by doing one iteration and incrementing the lower bound *) +Lemma foldi_nat_split_S : + forall {acc: Type} + (lo: nat) + (hi: nat) (* {lo <= hi} *) + (f: nat -> acc -> acc) (* {i < hi} *) + (init: acc), + (lo < hi)%nat -> + foldi_nat lo hi f init = foldi_nat (S lo) hi f (foldi_nat lo (S lo) f init). +Proof. + unfold foldi_nat. + intros. + + assert (succ_sub_diag : forall n, (S n - n = 1)%nat) by lia. + rewrite (succ_sub_diag lo). + + induction hi ; [ lia | ]. + destruct (S hi =? S lo)%nat eqn:hi_eq_lo. + - apply Nat.eqb_eq in hi_eq_lo ; rewrite hi_eq_lo in *. + rewrite (succ_sub_diag lo). + rewrite Nat.sub_diag. + reflexivity. + - apply Nat.eqb_neq in hi_eq_lo. + apply Nat.lt_gt_cases in hi_eq_lo. + destruct hi_eq_lo. + + lia. + + rewrite (Nat.sub_succ_l (S lo)) by apply (Nat.lt_le_pred _ _ H0). + rewrite Nat.sub_succ_l by apply (Nat.lt_le_pred _ _ H). + replace ((S (hi - S lo))) with (hi - lo)%nat by lia. + reflexivity. +Qed. + +(* folds can be split at some valid offset from lower bound *) +Lemma foldi_nat_split_add : + forall (k : nat), + forall {acc: Type} + (lo: nat) + (hi: nat) (* {lo <= hi} *) + (f: nat -> acc -> acc) (* {i < hi} *) + (init: acc), + forall {guarantee: (lo + k <= hi)%nat}, + foldi_nat lo hi f init = foldi_nat (k + lo) hi f (foldi_nat lo (k + lo) f init). +Proof. + induction k ; intros. + - cbn. + unfold foldi_nat. + rewrite Nat.sub_diag. + reflexivity. + - rewrite foldi_nat_split_S by lia. + replace (S k + lo)%nat with (k + S lo)%nat by lia. + specialize (IHk acc (S lo) hi f (foldi_nat lo (S lo) f init)). + rewrite IHk by lia. + f_equal. + rewrite <- foldi_nat_split_S by lia. + reflexivity. +Qed. + +(* folds can be split at some midpoint *) +Lemma foldi_nat_split : + forall (mid : nat), (* {lo <= mid <= hi} *) + forall {acc: Type} + (lo: nat) + (hi: nat) (* {lo <= hi} *) + (f: nat -> acc -> acc) (* {i < hi} *) + (init: acc), + forall {guarantee: (lo <= mid <= hi)%nat}, + foldi_nat lo hi f init = foldi_nat mid hi f (foldi_nat lo mid f init). +Proof. + intros. + assert (mid_is_low_plus_constant : {k : nat | (mid = lo + k)%nat}) by (exists (mid - lo)%nat ; lia). + destruct mid_is_low_plus_constant ; subst. + rewrite Nat.add_comm. + apply foldi_nat_split_add. + apply guarantee. +Qed. + +(* folds can be split at some midpoint *) +Lemma foldi_split : + forall (mid : uint_size), (* {lo <= mid <= hi} *) + forall {acc: Type} + (lo: uint_size) + (hi: uint_size) (* {lo <= hi} *) + (f: uint_size -> acc -> acc) (* {i < hi} *) + (init: acc), + forall {guarantee: (Int32.unsigned lo <= Int32.unsigned mid <= Int32.unsigned hi)%Z}, + foldi lo hi f init = foldi mid hi f (foldi lo mid f init). +Proof. + intros. + do 3 rewrite foldi_to_foldi_nat by lia. + apply foldi_nat_split ; lia. +Qed. + +(*** Default *) + +(* Typeclass handling of default elements, for use in sequences/arrays. + We provide instances for the library integer types *) +Class Default (A : Type) := { + default : A +}. +Global Arguments default {_} {_}. + +(*** Seq *) + +Definition public_byte_seq := seq int8. +Definition byte_seq := seq int8. +Definition list_len := length. + +Definition seq_index {A: Type} `{Default A} (s: seq A) (i : nat) := + List.nth i s default. + +Definition seq_len {A: Type} (s: seq A) : N := N.of_nat (length s). + +Definition seq_new_ {A: Type} (init : A) (len: nat) : seq A := + Vector.to_list (VectorDef.const init len). + +Definition seq_new {A: Type} `{Default A} (len: nat) : seq A := + seq_new_ default len. + +Fixpoint array_from_list {A: Type} (l: list A) : nseq A (length l) := + match l return (nseq A (length l)) with + | [] => VectorDef.nil A + | x :: xs => VectorDef.cons A x (length xs) (array_from_list xs) + end. + + (* match l, length l with *) +(* | [], O => VectorDef.nil A *) +(* | (x :: xs), S n => VectorDef.cons A x (length xs) (array_from_list A xs) *) +(* end. *) +(* - apply (VectorDef.cons A a (length l) (array_from_list A l)). *) +(* Defined. *) + + (* match l with *) + (* | [] => VectorDef.nil *) + (* | (x :: xs) => VectorDef.cons A x (length xs) (array_from_list xs) *) + (* end. *) + +(* Definition array_from_list (A: Type) (l: list A) : nseq A (length l) := *) + (* VectorDef.of_list l. *) +(* Proof. *) +(* induction l. *) +(* - apply (VectorDef.nil A). *) +(* - apply (VectorDef.cons A a (length l) IHl). *) +(* Defined. *) + +(* automatic conversion from list to array *) +(* Global Coercion array_from_list : list >-> nseq. *) + + +(**** Array manipulation *) + + +Definition array_new_ {A: Type} (init:A) (len: nat) : nseq A len := + VectorDef.const init len. + +Open Scope nat_scope. +Definition array_index {A: Type} `{Default A} {len : nat} (s: nseq A len) (i: nat) : A. +Proof. + destruct (i nat -> nat -> seq A -> t A len. *) +Definition update_sub {A len slen} `{Default A} (v : nseq A len) (i : nat) (n : nat) (sub : nseq A slen) : nseq A len := + let fix rec x acc := + match x with + | 0 => acc + (* | 0 => array_upd acc 0 (array_index sub 0) *) + | S x => rec x (array_upd acc (i+x) (array_index sub x)) + end in + rec (n - i + 1) v. + +(* Sanity check *) +(* Compute (to_list (update_sub [1;2;3;4;5] 0 4 (of_list [9;8;7;6;12]))). *) + +Definition array_to_seq + {a: Type} + {out_len:nat} + (input: nseq a out_len) + (* {H : List.length input = out_len} *) + : seq a := VectorDef.to_list input. + +Definition array_from_seq + {a: Type} + `{Default a} + (out_len:nat) + (input: seq a) + : nseq a out_len := + let out := VectorDef.const default out_len in + update_sub out 0 (out_len - 1) (Vector.of_list input). + +(* Global Coercion array_from_seq : seq >-> nseq. *) + +Definition slice {A} (l : seq A) (i j : nat) : seq A := + if j <=? i then [] else firstn (j-i+1) (skipn i l). + +Definition lseq_slice {A n} (l : nseq A n) (i j : nat) : nseq A _ := + VectorDef.of_list (slice (VectorDef.to_list l) i j). + +Definition array_from_slice + {a: Type} + `{Default a} + (default_value: a) + (out_len: nat) + (input: seq a) + (start: nat) + (slice_len: nat) + : nseq a out_len := + let out := VectorDef.const default_value out_len in + update_sub out 0 slice_len (lseq_slice (VectorDef.of_list input) start (start + slice_len)). + + +Definition array_slice + {a: Type} + `{Default a} + {len : nat} + (input: nseq a len) + (start: nat) + (slice_len: nat) + : seq a := + slice (array_to_seq input) start (start + slice_len). + + +Definition array_from_slice_range + {a: Type} + `{Default a} + (default_value: a) + (out_len: nat) + (input: seq a) + (start_fin: (uint_size * uint_size)) + : nseq a out_len := + let out := array_new_ default_value out_len in + let (start, fin) := start_fin in + update_sub out 0 ((from_uint_size fin) - (from_uint_size start)) (VectorDef.of_list (slice input (from_uint_size start) (from_uint_size fin))). + + +Definition array_slice_range + {a: Type} + {len : nat} + (input: nseq a len) + (start_fin:(uint_size * uint_size)) + : nseq a _ := + lseq_slice input (from_uint_size (fst start_fin)) (from_uint_size (snd start_fin)). + +Definition array_update + {a: Type} + `{Default a} + {len: nat} + (s: nseq a len) + (start : nat) + (start_s: seq a) + : nseq a len := + update_sub (s) start (length start_s) (VectorDef.of_list start_s). + +Definition array_update_start + {a: Type} + `{Default a} + {len: nat} + (s: nseq a len) + (start_s: seq a) + : nseq a len := + update_sub (s) 0 (length start_s) (VectorDef.of_list start_s). + +Definition array_len {a: Type} {len: nat} (s: nseq a len) := len. +(* May also come up as 'length' instead of 'len' *) +Definition array_length {a: Type} {len: nat} (s: nseq a len) := len. + +(**** Seq manipulation *) + +Definition seq_slice + {a: Type} + `{Default a} + (s: seq a) + (start: nat) + (len: nat) + : seq a := + (slice s start (start + len)). + +Definition seq_slice_range + {a: Type} + `{Default a} + (input: seq a) + (start_fin:(uint_size * uint_size)) + : seq a := + seq_slice input (from_uint_size (fst start_fin)) (from_uint_size (snd start_fin)). + +(* updating a subsequence in a sequence *) +Definition seq_update + {a: Type} + `{Default a} + (s: seq a) + (start: nat) + (input: seq a) + : seq a := + array_to_seq (update_sub (VectorDef.of_list s) start (length input) (VectorDef.of_list input)). + +(* updating only a single value in a sequence*) +Definition seq_upd + {a: Type} + `{Default a} + (s: seq a) + (start: nat) + (v: a) + : seq a := + array_to_seq (update_sub (VectorDef.of_list s) start 1 (VectorDef.of_list [v])). + +Definition sub {a} (s : list a) start n := + slice s start (start + n). + +Definition seq_update_start + {a: Type} + `{Default a} + (s: seq a) + (start_s: seq a) + : seq a := + array_to_seq (update_sub (VectorDef.of_list s) 0 (length start_s) (VectorDef.of_list start_s)). + +Definition array_update_slice + {a : Type} + `{Default a} + {l : nat} + (out: nseq a l) + (start_out: nat) + (input: seq a) + (start_in: nat) + (len: nat) + : nseq a (array_length out) + := + update_sub (out) start_out len + (VectorDef.of_list (sub input start_in len)). + +Definition seq_update_slice + {a : Type} + `{Default a} + (out: seq a) + (start_out: nat) + (input: seq a) + (start_in: nat) + (len: nat) + : nseq a (length out) + := + update_sub (VectorDef.of_list out) start_out len + (VectorDef.of_list (sub input start_in len)). + +Definition seq_concat + {a : Type} + (s1 :seq a) + (s2: seq a) + : seq a := + (s1 ++ s2). + +Definition seq_push + {a : Type} + (s1 :seq a) + (s2: a) + : seq a := + (s1 ++ [s2]). + +Definition seq_from_slice_range + {a: Type} + `{Default a} + (input: seq a) + (start_fin: (uint_size * uint_size)) + : seq a := + let out := array_new_ (default) (length input) in + let (start, fin) := start_fin in + array_to_seq (update_sub out 0 ((from_uint_size fin) - (from_uint_size start)) (VectorDef.of_list (slice input (from_uint_size start) (from_uint_size fin)))). + +Definition seq_from_seq {A} (l : seq A) := l. + + +(**** Chunking *) + +Definition seq_num_chunks {a: Type} (s: seq a) (chunk_len: nat) : nat := + ((length s) + chunk_len - 1) / chunk_len. + +Definition seq_chunk_len + {a: Type} + (s: seq a) + (chunk_len: nat) + (chunk_num: nat) + : nat := + let idx_start := chunk_len * chunk_num in + if (length s) + out_len := seq_chunk_len s chunk_len chunk_num /\ LSeq.length chunk := out_len + )) *) + := + let idx_start := chunk_len * chunk_num in + let out_len := seq_chunk_len s chunk_len chunk_num in + (usize out_len, slice + s idx_start (idx_start + seq_chunk_len s chunk_len chunk_num)). + +Definition seq_set_chunk + {a: Type} + `{Default a} + (s: seq a) + (chunk_len: nat) + (chunk_num: nat) + (chunk: seq a ) : seq a := + let idx_start := chunk_len * chunk_num in + let out_len := seq_chunk_len s chunk_len chunk_num in + VectorDef.to_list (update_sub (VectorDef.of_list s) idx_start out_len (VectorDef.of_list chunk)). + + +Definition seq_num_exact_chunks {a} (l : seq a) (chunk_size : uint_size) : uint_size := + Int32.divs (Int32.repr (Z.of_nat (length l))) chunk_size. + +(* Until #84 is fixed this returns an empty sequence if not enough *) +Definition seq_get_exact_chunk {a} (l : seq a) (chunk_size chunk_num: uint_size) : seq a := + let '(len, chunk) := seq_get_chunk l (from_uint_size chunk_size) (from_uint_size chunk_num) in + if Int32.eq len chunk_size then [] else chunk. + +Definition seq_set_exact_chunk {a} `{H : Default a} := @seq_set_chunk a H. + +Definition seq_get_remainder_chunk : forall {a}, seq a -> uint_size -> seq a := + fun _ l chunk_size => + let chunks := seq_num_chunks l (from_uint_size chunk_size) in + let last_chunk := if 0 [] + | [], _ => [] + | (x :: xs), S n' => x :: (seq_truncate xs n') + end. + +(**** Numeric operations *) + +(* takes two nseq's and joins them using a function op : a -> a -> a *) +Definition array_join_map + {a: Type} + `{Default a} + {len: nat} + (op: a -> a -> a) + (s1: nseq a len) + (s2 : nseq a len) := + let out := s1 in + foldi (usize 0) (usize len) (fun i out => + let i := from_uint_size i in + array_upd out i (op (array_index s1 i) (array_index s2 i)) + ) out. + +Module ArrayJoint (WS : WORDSIZE). + Include (HacspecIntegers WS). + Import Int. + Infix "array_xor" := (array_join_map xor) (at level 33) : hacspec_scope. + Infix "array_add" := (array_join_map add) (at level 33) : hacspec_scope. + Infix "array_minus" := (array_join_map sub) (at level 33) : hacspec_scope. + Infix "array_mul" := (array_join_map mul) (at level 33) : hacspec_scope. + Infix "array_div" := (array_join_map divs) (at level 33) : hacspec_scope. + Infix "array_or" := (array_join_map or) (at level 33) : hacspec_scope. + Infix "array_and" := (array_join_map and) (at level 33) : hacspec_scope. +End ArrayJoint. + +Definition array_eq_ + {a: Type} + {len: nat} + (eq: a -> a -> bool) + (s1: nseq a len) + (s2 : nseq a len) + : bool := Vector.eqb _ eq s1 s2. + +Infix "array_eq" := (array_eq_ eq) (at level 33) : hacspec_scope. +Infix "array_neq" := (fun s1 s2 => negb (array_eq_ eq s1 s2)) (at level 33) : hacspec_scope. + + +(**** Integers to arrays *) +Axiom uint32_to_le_bytes : int32 -> nseq int8 4. +Axiom uint32_to_be_bytes : int32 -> nseq int8 4. +Axiom uint32_from_le_bytes : nseq int8 4 -> int32. +Axiom uint32_from_be_bytes : nseq int8 4 -> int32. +Axiom uint64_to_le_bytes : int64 -> nseq int8 8. +Axiom uint64_to_be_bytes : int64 -> nseq int8 8. +Axiom uint64_from_le_bytes : nseq int8 8 -> int64. +Axiom uint64_from_be_bytes : nseq int8 8 -> int64. +Axiom uint128_to_le_bytes : int128 -> nseq int8 16. +Axiom uint128_to_be_bytes : int128 -> nseq int8 16. +Axiom uint128_from_le_bytes : nseq int8 16 -> int128. +Axiom uint128_from_be_bytes : nseq int8 16 -> int128. +Axiom u32_to_le_bytes : int32 -> nseq int8 4. +Axiom u32_to_be_bytes : int32 -> nseq int8 4. +Axiom u32_from_le_bytes : nseq int8 4 -> int32. +Axiom u32_from_be_bytes : nseq int8 4 -> int32. +Axiom u64_to_le_bytes : int64 -> nseq int8 8. +Axiom u64_from_le_bytes : nseq int8 8 -> int64. +Axiom u128_to_le_bytes : int128 -> nseq int8 16. +Axiom u128_to_be_bytes : int128 -> nseq int8 16. +Axiom u128_from_le_bytes : nseq int8 16 -> int128. +Axiom u128_from_be_bytes : nseq int8 16 -> int128. + +(*** Nats *) + + +Definition nat_mod (p : Z) : Set := GZnZ.znz p. + + +Definition nat_mod_equal {p} (a b : nat_mod p) : bool := + Z.eqb (GZnZ.val p a) (GZnZ.val p b). + +Definition nat_mod_zero {p} : nat_mod p := GZnZ.zero p. +Definition nat_mod_one {p} : nat_mod p := GZnZ.one p. +Definition nat_mod_two {p} : nat_mod p := GZnZ.mkznz p _ (GZnZ.modz p 2). + + +(* convenience coercions from nat_mod to Z and N *) +(* Coercion Z.of_N : N >-> Z. *) + +Definition nat_mod_add {n : Z} (a : nat_mod n) (b : nat_mod n) : nat_mod n := GZnZ.add n a b. + +Infix "+%" := nat_mod_add (at level 33) : hacspec_scope. + +Definition nat_mod_mul {n : Z} (a:nat_mod n) (b:nat_mod n) : nat_mod n := GZnZ.mul n a b. +Infix "*%" := nat_mod_mul (at level 33) : hacspec_scope. + +Definition nat_mod_sub {n : Z} (a:nat_mod n) (b:nat_mod n) : nat_mod n := GZnZ.sub n a b. +Infix "-%" := nat_mod_sub (at level 33) : hacspec_scope. + +Definition nat_mod_div {n : Z} (a:nat_mod n) (b:nat_mod n) : nat_mod n := GZnZ.div n a b. +Infix "/%" := nat_mod_div (at level 33) : hacspec_scope. + +(* A % B = (a * B + r) *) + +Definition nat_mod_neg {n : Z} (a:nat_mod n) : nat_mod n := GZnZ.opp n a. + +Definition nat_mod_inv {n : Z} (a:nat_mod n) : nat_mod n := GZnZ.inv n a. + +Definition nat_mod_exp_def {p : Z} (a:nat_mod p) (n : nat) : nat_mod p := + let fix exp_ (e : nat_mod p) (n : nat) := + match n with + | 0%nat => nat_mod_one + | S n => nat_mod_mul a (exp_ a n) + end in + exp_ a n. + +Module temp (WS : WORDSIZE). + Include HacspecIntegers WS. + Definition nat_mod_exp {p} a n := @nat_mod_exp_def p a (Z.to_nat (@unsigned n)). + Definition nat_mod_pow {p} a n := @nat_mod_exp_def p a (Z.to_nat (@unsigned n)). + Definition nat_mod_pow_self {p} a n := @nat_mod_exp_def p a (Z.to_nat (from_uint_size n)). +End temp. +Module temp8 := temp Wordsize_8. +Module temp16 := temp Wordsize_16. +Module temp32 := temp Wordsize_32. +Module temp64 := temp Wordsize_64. +Module temp128 := temp Wordsize_128. +Import temp8. +Import temp16. +Import temp32. +Import temp64. +Import temp128. + +Close Scope nat_scope. +Open Scope Z_scope. + +(* We assume x < m *) +Definition nat_mod_from_secret_literal {m : Z} (x:int128) : nat_mod m. +Proof. + unfold nat_mod. + (* since we assume x < m, it will be true that (unsigned x) = (unsigned x) mod m *) + remember ((Int128.unsigned x) mod m) as zmodm. + apply (GZnZ.mkznz m zmodm). + rewrite Heqzmodm. + rewrite Zmod_mod. + reflexivity. +Defined. + +Definition nat_mod_from_literal (m : Z) (x:int128) : nat_mod m := nat_mod_from_secret_literal x. + +Axiom nat_mod_to_byte_seq_le : forall {n : Z}, nat_mod n -> seq int8. +Axiom nat_mod_to_byte_seq_be : forall {n : Z}, nat_mod n -> seq int8. +Axiom nat_mod_to_public_byte_seq_le : forall (n : Z), nat_mod n -> seq int8. +Axiom nat_mod_to_public_byte_seq_be : forall (n : Z), nat_mod n -> seq int8. + +Definition nat_mod_bit {n : Z} (a : nat_mod n) (i : uint_size) := + Z.testbit (GZnZ.val n a) (from_uint_size i). + +(* Alias for nat_mod_bit *) +Definition nat_get_mod_bit {p} (a : nat_mod p) := nat_mod_bit a. +Definition nat_mod_get_bit {p} (a : nat_mod p) n := + if (nat_mod_bit a n) + then @nat_mod_one p + else @nat_mod_zero p. + +(* +Definition nat_mod_to_public_byte_seq_le (n: pos) (len: uint_size) (x: nat_mod_mod n) : lseq pub_uint8 len = + Definition n' := n % (pow2 (8 * len)) in + Lib.ByteSequence.nat_mod_to_bytes_le len n'*) + +(* Definition nat_to_public_byte_seq_be (n: pos) (len: uint_size) (x: nat_mod n) : lseq pub_uint8 len = + Definition n' := n % (pow2 (8 * len)) in + Lib.ByteSequence.nat_to_bytes_be len n' *) + +Axiom array_declassify_eq : forall {A l}, nseq A l -> nseq A l -> bool. +Axiom array_to_le_uint32s : forall {A l}, nseq A l -> seq uint32. +Axiom array_to_be_uint32s : forall {A l}, nseq A l -> seq uint32. (* nseq uint32 (l/4) *) +Axiom array_to_le_bytes : forall {A l}, nseq A l -> seq uint8. +Axiom array_to_be_bytes : forall {A l}, nseq A l -> seq uint8. +Axiom nat_mod_from_byte_seq_le : forall {A n}, seq A -> nat_mod n. +Axiom nat_mod_from_byte_seq_be : forall {A n}, seq A -> nat_mod n. +Axiom nat_mod_from_public_byte_seq_le : forall {A n}, seq A -> nat_mod n. +Axiom nat_mod_from_public_byte_seq_be : forall {A n}, seq A -> nat_mod n. +Axiom most_significant_bit : forall {m}, nat_mod m -> uint_size -> uint_size. + + +(* We assume 2^x < m *) +Definition nat_mod_pow2 (m : Z) (x : N) : nat_mod m. +Proof. + remember (Z.pow 2 (Z.of_N x) mod m) as y. + apply (GZnZ.mkznz m y). + rewrite Heqy. + rewrite Zmod_mod. + reflexivity. +Defined. + + +Section Casting. + + (* Type casts, as defined in Section 4.5 in https://arxiv.org/pdf/1106.3448.pdf *) + Class Cast A B := cast : A -> B. + + Arguments cast {_} _ {_}. + + Notation "' x" := (cast _ x) (at level 20) : hacspec_scope. + Open Scope hacspec_scope. + + (* Casting to self is always possible *) + Global Instance cast_self {A} : Cast A A := { + cast a := a + }. + + Global Instance cast_transitive {A B C} `{Hab: Cast A B} `{Hbc: Cast B C} : Cast A C := { + cast a := Hbc (Hab a) + }. + + Global Instance cast_prod {A B C D} `{Cast A B} `{Cast C D} : Cast (A * C) (B * D) := { + cast '(a, c) := ('a, 'c) + }. + + Global Instance cast_option {A B} `{Cast A B} : Cast (option A) (option B) := { + cast a := match a with Some a => Some ('a) | None => None end + }. + + Global Instance cast_option_b {A B} `{Cast A B} : Cast A (option B) := { + cast a := Some ('a) + }. + + (* Global Instances for common types *) + + Global Instance cast_nat_to_N : Cast nat N := { + cast := N.of_nat + }. + + Global Instance cast_N_to_Z : Cast N Z := { + cast := Z.of_N + }. + + (* Global Instance cast_Z_to_int {WORDSIZE} : Cast Z (@int WORDSIZE) := { *) + (* cast n := repr n *) + (* }. *) + + Global Instance cast_natmod_to_Z {p} : Cast (nat_mod p) Z := { + cast n := GZnZ.val p n + }. + + (* Global Instance cast_int_to_nat `{WORDSIZE} : Cast int nat := { *) + (* cast n := Z.to_nat (signed n) *) + (* }. *) + + Global Instance cast_int16_to_int8 : Cast int16 int8 := { + cast n := Int8.repr (Int16.unsigned n) + }. + + Global Instance cast_int32_to_int8 : Cast int32 int8 := { + cast n := Int8.repr (Int32.unsigned n) + }. + + Global Instance cast_int64_to_int8 : Cast int64 int8 := { + cast n := Int8.repr (Int64.unsigned n) + }. + + Global Instance cast_int8_to_int16 : Cast int8 int16 := { + cast n := Int16.repr (Int8.unsigned n) + }. + + Global Instance cast_int32_to_int16 : Cast int32 int16 := { + cast n := Int16.repr (Int32.unsigned n) + }. + + Global Instance cast_int64_to_int16 : Cast int64 int16 := { + cast n := Int16.repr (Int64.unsigned n) + }. + + Global Instance cast_int8_to_int32 : Cast int8 int32 := { + cast n := Int32.repr (Int8.unsigned n) + }. + + Global Instance cast_int16_to_int32 : Cast int16 int32 := { + cast n := Int32.repr (Int16.unsigned n) + }. + + Global Instance cast_int64_to_int32 : Cast int64 int32 := { + cast n := Int32.repr (Int64.unsigned n) + }. + + Global Instance cast_int8_to_int64 : Cast int8 int64 := { + cast n := Int64.repr (Int8.unsigned n) + }. + + Global Instance cast_int16_to_int64 : Cast int16 int64 := { + cast n := Int64.repr (Int16.unsigned n) + }. + + Global Instance cast_int32_to_int64 : Cast int32 int64 := { + cast n := Int64.repr (Int32.unsigned n) + }. + + Close Scope hacspec_scope. +End Casting. + + +Global Arguments pair {_ _} & _ _. +Global Arguments id {_} & _. +Section Coercions. + (* First, in order to have automatic coercions for tuples, we add bidirectionality hints: *) + + (* Integer coercions *) + (* We have nat >-> N >-> Z >-> int/int32 *) + (* and uint >-> Z *) + (* and N >-> nat *) + + Global Coercion N.to_nat : N >-> nat. + Global Coercion Z.of_N : N >-> Z. + + Global Coercion repr : Z >-> int. + + (* Definition Z_to_int `{WORDSIZE} (n : Z) : int := repr n. *) + (* Global Coercion Z_to_int : Z >-> int. *) + + Definition Z_to_uint_size (n : Z) : uint_size := Int32.repr n. + Global Coercion Z_to_uint_size : Z >-> uint_size. + Definition Z_to_int_size (n : Z) : int_size := Int32.repr n. + Global Coercion Z_to_int_size : Z >-> int_size. + + (* Definition N_to_int `{WORDSIZE} (n : N) : int := repr (Z.of_N n). *) + (* Global Coercion N.of_nat : nat >-> N. *) + (* Global Coercion N_to_int : N >-> int. *) + Definition N_to_uint_size (n : Z) : uint_size := Int32.repr n. + Global Coercion N_to_uint_size : Z >-> uint_size. + + (* Definition nat_to_int `{WORDSIZE} (n : nat) := repr (Z.of_nat n). *) + (* Global Coercion nat_to_int : nat >-> int. *) + + Definition uint_size_to_nat (n : uint_size) : nat := from_uint_size n. + Global Coercion uint_size_to_nat : uint_size >-> nat. + + Definition uint_size_to_Z (n : uint_size) : Z := from_uint_size n. + Global Coercion uint_size_to_Z : uint_size >-> Z. + + Definition uint32_to_nat (n : uint32) : nat := Int32.unsigned n. + Global Coercion uint32_to_nat : uint32 >-> nat. + + + Global Coercion GZnZ.val : GZnZ.znz >-> Z. + + Definition int8_to_nat (n : int8) : nat := Int8.unsigned n. + Global Coercion int8_to_nat : int8 >-> nat. + Definition int16_to_nat (n : int16) : nat := Int16.unsigned n. + Global Coercion int16_to_nat : int16 >-> nat. + Definition int32_to_nat (n : int32) : nat := Int32.unsigned n. + Global Coercion int32_to_nat : int32 >-> nat. + Definition int64_to_nat (n : int64) : nat := Int64.unsigned n. + Global Coercion int64_to_nat : int64 >-> nat. + Definition int128_to_nat (n : int128) : nat := Int128.unsigned n. + Global Coercion int128_to_nat : int128 >-> nat. + + (* coercions int8 >-> int16 >-> ... int128 *) + + Definition int8_to_int16 (n : int8) : int16 := Int16.repr (Int8.unsigned n). + Global Coercion int8_to_int16 : int8 >-> int16. + + Definition int8_to_int32 (n : int8) : int32 := Int32.repr (Int8.unsigned n). + Global Coercion int8_to_int32 : int8 >-> int32. + + Definition int16_to_int32 (n : int16) : int32 := Int32.repr (Int16.unsigned n). + Global Coercion int16_to_int32 : int16 >-> int32. + + Definition int32_to_int64 (n : int32) : int64 := Int64.repr (Int32.unsigned n). + Global Coercion int32_to_int64 : int32 >-> int64. + + Definition int64_to_int128 (n : int64) : int128 := Int128.repr (Int64.unsigned n). + Global Coercion int64_to_int128 : int64 >-> int128. + + Definition int32_to_int128 (n : int32) : int128 := Int128.repr (Int32.unsigned n). + Global Coercion int32_to_int128 : int32 >-> int128. + + Definition uint_size_to_int64 (n : uint_size) : int64 := Int64.repr (Int32.unsigned n). + Global Coercion uint_size_to_int64 : uint_size >-> int64. + + + (* coercions into nat_mod *) + Definition Z_in_nat_mod {m : Z} (x:Z) : nat_mod m. + Proof. + unfold nat_mod. + remember ((x) mod m) as zmodm. + apply (GZnZ.mkznz m zmodm). + rewrite Heqzmodm. + rewrite Zmod_mod. + reflexivity. + Defined. + (* Global Coercion Z_in_nat_mod : Z >-> nat_mod. *) + + (* Definition int_in_nat_mod {m : Z} `{WORDSIZE} (x:int) : nat_mod m. *) + (* Proof. *) + (* unfold nat_mod. *) + (* (* since we assume x < m, it will be true that (unsigned x) = (unsigned x) mod m *) *) + (* remember ((unsigned x) mod m) as zmodm. *) + (* apply (GZnZ.mkznz m zmodm). *) + (* rewrite Heqzmodm. *) + (* rewrite Zmod_mod. *) + (* reflexivity. *) + (* Show Proof. *) + (* Defined. *) + (* Global Coercion int_in_nat_mod : int >-> nat_mod. *) + + (* Definition uint_size_in_nat_mod (n : uint_size) : nat_mod 16 := int_in_nat_mod n. *) + (* Global Coercion uint_size_in_nat_mod : uint_size >-> nat_mod. *) + +End Coercions. + + +(* (*** Casting *) *) + +(* Definition uint128_from_usize (n : uint_size) : int128 := repr n. *) +(* Definition uint64_from_usize (n : uint_size) : int64 := repr n. *) +(* Definition uint32_from_usize (n : uint_size) : int32 := repr n. *) +(* Definition uint16_from_usize (n : uint_size) : int16 := repr n. *) +(* Definition uint8_from_usize (n : uint_size) : int8 := repr n. *) + +(* Definition uint128_from_uint8 (n : int8) : int128 := repr n. *) +(* Definition uint64_from_uint8 (n : int8) : int64 := repr n. *) +(* Definition uint32_from_uint8 (n : int8) : int32 := repr n. *) +(* Definition uint16_from_uint8 (n : int8) : int16 := repr n. *) +(* Definition usize_from_uint8 (n : int8) : uint_size := repr n. *) + +(* Definition uint128_from_uint16 (n : int16) : int128 := repr n. *) +(* Definition uint64_from_uint16 (n : int16) : int64 := repr n. *) +(* Definition uint32_from_uint16 (n : int16) : int32 := repr n. *) +(* Definition uint8_from_uint16 (n : int16) : int8 := repr n. *) +(* Definition usize_from_uint16 (n : int16) : uint_size := repr n. *) + +(* Definition uint128_from_uint32 (n : int32) : int128 := repr n. *) +(* Definition uint64_from_uint32 (n : int32) : int64 := repr n. *) +(* Definition uint16_from_uint32 (n : int32) : int16 := repr n. *) +(* Definition uint8_from_uint32 (n : int32) : int8 := repr n. *) +(* Definition usize_from_uint32 (n : int32) : uint_size := repr n. *) + +(* Definition uint128_from_uint64 (n : int64) : int128 := repr n. *) +(* Definition uint32_from_uint64 (n : int64) : int32 := repr n. *) +(* Definition uint16_from_uint64 (n : int64) : int16 := repr n. *) +(* Definition uint8_from_uint64 (n : int64) : int8 := repr n. *) +(* Definition usize_from_uint64 (n : int64) : uint_size := repr n. *) + +(* Definition uint64_from_uint128 (n : int128) : int64 := repr n. *) +(* Definition uint32_from_uint128 (n : int128) : int32 := repr n. *) +(* Definition uint16_from_uint128 (n : int128) : int16 := repr n. *) +(* Definition uint8_from_uint128 (n : int128) : int8 := repr n. *) +(* Definition usize_from_uint128 (n : int128) : uint_size := repr n. *) + + +(* Comparisons, boolean equality, and notation *) + +Class EqDec (A : Type) := + { eqb : A -> A -> bool ; + eqb_leibniz : forall x y, eqb x y = true <-> x = y }. + +Infix "=.?" := eqb (at level 40) : hacspec_scope. +Infix "!=.?" := (fun a b => negb (eqb a b)) (at level 40) : hacspec_scope. + +Class Comparable (A : Type) := { + ltb : A -> A -> bool; + leb : A -> A -> bool; + gtb : A -> A -> bool; + geb : A -> A -> bool; +}. +Infix "<.?" := ltb (at level 42) : hacspec_scope. +Infix "<=.?" := leb (at level 42) : hacspec_scope. +Infix ">.?" := gtb (at level 42) : hacspec_scope. +Infix ">=.?" := geb (at level 42) : hacspec_scope. + +Theorem eqb_refl : forall {A} {H : EqDec A} (x : A), @eqb A H x x = true. +Proof. + intros. + now rewrite eqb_leibniz. +Qed. + +Global Program Instance nat_eqdec : EqDec nat := { + eqb := Nat.eqb; + eqb_leibniz := Nat.eqb_eq ; +}. + +Global Instance nat_comparable : Comparable nat := { + ltb := Nat.ltb; + leb := Nat.leb; + gtb a b := Nat.ltb b a; + geb a b := Nat.leb b a; +}. + +Global Instance N_eqdec : EqDec N := { + eqb := N.eqb; + eqb_leibniz := N.eqb_eq ; +}. + +Global Instance N_comparable : Comparable N := { + ltb := N.ltb; + leb := N.leb; + gtb a b := N.ltb b a; + geb a b := N.leb b a; +}. + +Global Instance Z_eqdec : EqDec Z := { + eqb := Z.eqb; + eqb_leibniz := Z.eqb_eq ; +}. + +Global Instance Z_comparable : Comparable Z := { + ltb := Z.ltb; + leb := Z.leb; + gtb a b := Z.ltb b a; + geb a b := Z.leb b a; +}. + +(* Lemma int_eqb_eq : forall {WS : WORDSIZE} (a b : int), eq a b = true <-> a = b. *) +(* Proof. *) +(* intros. split. *) +(* - apply same_if_eq. *) +(* - intros. rewrite H. apply eq_true. *) +(* Qed. *) + +(* Global Instance int_eqdec `{WORDSIZE}: EqDec int := { *) +(* eqb := eq; *) +(* eqb_leibniz := int_eqb_eq ; *) +(* }. *) + +(* Global Instance int_comparable `{WORDSIZE} : Comparable int := { *) +(* ltb := lt; *) +(* leb a b := if eq a b then true else lt a b ; *) +(* gtb a b := lt b a; *) +(* geb a b := if eq a b then true else lt b a; *) +(* }. *) + +(* Definition uint8_equal : int8 -> int8 -> bool := eqb. *) + +Definition nat_mod_val (p : Z) (a : nat_mod p) : Z := GZnZ.val p a. + +Theorem nat_mod_eqb_spec : forall {p} (a b : nat_mod p), Z.eqb (nat_mod_val p a) (nat_mod_val p b) = true <-> a = b. +Proof. + split ; intros. + - apply Z.eqb_eq in H. + destruct a, b. + cbn in H. + apply (GZnZ.zirr p val val0 inZnZ inZnZ0 H). + - subst. + apply Z.eqb_eq. + reflexivity. +Qed. + +Global Instance nat_mod_eqdec {p} : EqDec (nat_mod p) := { + eqb a b := Z.eqb (nat_mod_val p a) (nat_mod_val p b); + eqb_leibniz := nat_mod_eqb_spec; +}. + +Global Instance nat_mod_comparable `{p : Z} : Comparable (nat_mod p) := { + ltb a b := Z.ltb (nat_mod_val p a) (nat_mod_val p b); + leb a b := if Zeq_bool a b then true else Z.ltb (nat_mod_val p a) (nat_mod_val p b) ; + gtb a b := Z.ltb (nat_mod_val p b) (nat_mod_val p a); + geb a b := if Zeq_bool b a then true else Z.ltb (nat_mod_val p b) (nat_mod_val p a) ; +}. + +Fixpoint nat_mod_rem_aux {n : Z} (a:nat_mod n) (b:nat_mod n) (f : nat) {struct f} : nat_mod n := + match f with + | O => a + | S f' => + if geb a b + then nat_mod_rem_aux (nat_mod_sub a b) b f' + else a + end. + +Definition nat_mod_rem {n : Z} (a:nat_mod n) (b:nat_mod n) : nat_mod n := + if nat_mod_equal b nat_mod_zero + then nat_mod_one + else nat_mod_rem_aux a b (S (nat_mod_div a b)). + +Infix "rem" := nat_mod_rem (at level 33) : hacspec_scope. + +Global Instance bool_eqdec : EqDec bool := { + eqb := Bool.eqb; + eqb_leibniz := Bool.eqb_true_iff; +}. + +Global Instance string_eqdec : EqDec String.string := { + eqb := String.eqb; + eqb_leibniz := String.eqb_eq ; +}. + +Global Instance unit_eqdec : EqDec unit := { + eqb := fun _ _ => true ; + eqb_leibniz := fun 'tt 'tt => (conj (fun _ => eq_refl) (fun _ => eq_refl)) ; +}. + +Require Import Sumbool. +Open Scope list_scope. + +Fixpoint list_eqdec {A} `{EqDec A} (l1 l2 : list A) : bool := + match l1, l2 with + | x::xs, y::ys => if eqb x y then list_eqdec xs ys else false + | [], [] => true + | _,_ => false + end. + +Lemma list_eqdec_refl : forall {A} `{EqDec A} (l1 : list A), list_eqdec l1 l1 = true. +Proof. + intros ; induction l1 ; cbn ; try rewrite eqb_refl ; easy. +Qed. + +Lemma list_eqdec_sound : forall {A} `{EqDec A} (l1 l2 : list A), list_eqdec l1 l2 = true <-> l1 = l2. +Proof. + intros A H l1. + induction l1 ; induction l2 ; split ; intros ; simpl in * ; try easy ; try inversion H0. + - (* inductive case *) + apply Field_theory.if_true in H0; destruct H0. + f_equal. + (* show heads are equal *) + + apply (proj1 (eqb_leibniz a a0) H0). + (* show tails are equal using induction hypothesis *) + + apply IHl1. assumption. + - rewrite eqb_refl. + apply list_eqdec_refl. +Qed. + +Global Instance List_eqdec {A} `{EqDec A} : EqDec (list A) := { + eqb := list_eqdec; + eqb_leibniz := list_eqdec_sound; +}. + +Lemma vector_eqb_sound : forall {A : Type} {n : nat} `{EqDec A} (v1 v2 : VectorDef.t A n), Vector.eqb _ eqb v1 v2 = true <-> v1 = v2. +Proof. + intros. + apply Vector.eqb_eq. + intros. + apply eqb_leibniz. +Qed. + +Global Program Instance Vector_eqdec {A n} `{EqDec A}: EqDec (VectorDef.t A n) := { + eqb := Vector.eqb _ eqb; + eqb_leibniz := vector_eqb_sound; +}. + +Global Program Instance Dec_eq_prod (A B : Type) `{EqDec A} `{EqDec B} : EqDec (A * B) := { + eqb '(a0, b0) '(a1, b1) := andb (eqb a0 a1) (eqb b0 b1) +}. +Next Obligation. + split ; intros. + - symmetry in H1. + apply Bool.andb_true_eq in H1. destruct H1. + symmetry in H1. apply (eqb_leibniz a0 a) in H1. + symmetry in H2. apply (eqb_leibniz b0 b) in H2. + rewrite H1, H2. reflexivity. + - inversion_clear H1. now do 2 rewrite eqb_refl. +Defined. + +(*** Result *) + +Inductive result (a: Type) (b: Type) := + | Ok : a -> result a b + | Err : b -> result a b. + +Arguments Ok {_ _}. +Arguments Err {_ _}. + +(*** Be Bytes *) + + +Fixpoint nat_be_range_at_position (k : nat) (z : Z) (n : Z) : list bool := + match k with + | O => [] + | S k' => Z.testbit z (n + Z.of_nat k') :: nat_be_range_at_position k' z n + end. + +Fixpoint nat_be_range_to_position_ (z : list bool) (val : Z) : Z := + match z with + | [] => val + | x :: xs => nat_be_range_to_position_ xs ((if x then 2 ^ Z.of_nat (List.length xs) else 0) + val) + end. + +Definition nat_be_range_to_position (k : nat) (z : list bool) (n : Z) : Z := + (nat_be_range_to_position_ z 0 * 2^(Z.of_nat k * n)). + +Definition nat_be_range (k : nat) (z : Z) (n : nat) : Z := + nat_be_range_to_position_ (nat_be_range_at_position k z (Z.of_nat (n * k)%nat)) 0. (* * 2^(k * n) *) + +Compute nat_be_range 4 0 300. + +(* Definition u64_to_be_bytes' : int64 -> nseq int8 8 := *) +(* fun k => array_from_list (int8) [@nat_to_int WORDSIZE8 (nat_be_range 4 k 7) ; *) +(* @nat_to_int WORDSIZE8 (nat_be_range 4 k 6) ; *) +(* @nat_to_int WORDSIZE8 (nat_be_range 4 k 5) ; *) +(* @nat_to_int WORDSIZE8 (nat_be_range 4 k 4) ; *) +(* @nat_to_int WORDSIZE8 (nat_be_range 4 k 3) ; *) +(* @nat_to_int WORDSIZE8 (nat_be_range 4 k 2) ; *) +(* @nat_to_int WORDSIZE8 (nat_be_range 4 k 1) ; *) +(* @nat_to_int WORDSIZE8 (nat_be_range 4 k 0)]. *) + +Open Scope hacspec_scope. + +Definition u64_from_be_bytes_fold_fun (i : int8) (s : nat × int64) : nat × int64 := + let (n,v) := s in + (S n, Int64.add v (Int64.repr (Z.of_nat (int8_to_nat i) * 2 ^ (4 * Z.of_nat n)))). + +Definition u64_from_be_bytes' : nseq int8 8 -> int64 := + (fun v => snd (VectorDef.fold_right u64_from_be_bytes_fold_fun v (0, @Int64.repr 0))). + +(* Definition u64_to_be_bytes : int64 -> nseq int8 8 := u64_to_be_bytes'. *) +(* Definition u64_from_be_bytes : nseq int8 8 -> int64 := u64_from_be_bytes'. *) + +(* Definition nat_mod_to_byte_seq_be : forall {n : Z}, nat_mod n -> seq int8 := *) +(* fun k => VectorDef.of_list . *) + +(*** Monad / Bind *) + +Class Monad (M : Type -> Type) := + { bind {A B} (x : M A) (f : A -> M B) : M B ; + ret {A} (x : A) : M A ; + }. + +Definition result2 (b: Type) (a: Type) := result a b. + +Definition result_bind {A B C} (r : result2 C A) (f : A -> result2 C B) : result2 C B := + match r with + Ok a => f a + | Err e => Err e + end. + +Definition result_ret {A C} (a : A) : result2 C A := Ok a. + +Global Instance result_monad {C} : Monad (result2 C) := + Build_Monad (result2 C) (fun A B => @result_bind A B C) (fun A => @result_ret A C). + +Definition option_bind {A B} (r : option A) (f : A -> option B) : option B := + match r with + Some (a) => f a + | None => None + end. + + + +Definition option_ret {A} (a : A) : option A := Some a. + +Global Instance option_monad : Monad option := + Build_Monad option (@option_bind) (@option_ret). + +Definition option_is_none {A} (x : option A) : bool := + match x with + | None => true + | _ => false + end. + +Definition foldi_bind {A : Type} {M : Type -> Type} `{Monad M} (a : uint_size) (b : uint_size) (f : uint_size -> A -> M A) (init : M A) : M A := + @foldi (M A) a b (fun x y => bind y (f x)) init. + +Definition lift_to_result {A B C} (r : result A C) (f : A -> B) : result B C := + result_bind r (fun x => result_ret (f x)). + +Definition result_uint_size_to_result_int64 {C} (r : result uint_size C) := lift_to_result r uint_size_to_int64. + +Definition result_uint_size_unit := (result uint_size unit). +Definition result_int64_unit := (result int64 unit). + +Definition result_uint_size_unit_to_result_int64_unit (r : result_uint_size_unit) : result_int64_unit := result_uint_size_to_result_int64 r. + +Global Coercion lift_to_result_coerce {A B C} (f : A -> B) := (fun (r : result A C) => lift_to_result r f). + +Global Coercion result_uint_size_unit_to_result_int64_unit : result_uint_size_unit >-> result_int64_unit. + +(*** Notation *) + +Notation "'ifbnd' b 'then' x 'else' y '>>' f" := (if b then f x else f y) (at level 200). +Notation "'ifbnd' b 'thenbnd' x 'else' y '>>' f" := (if b then (bind x) f else f y) (at level 200). +Notation "'ifbnd' b 'then' x 'elsebnd' y '>>' f" := (if b then f x else (bind y) f) (at level 200). +Notation "'ifbnd' b 'thenbnd' x 'elsebnd' y '>>' f" := (if b then bind x f else bind y f) (at level 200). + +Notation "'foldibnd' s 'to' e 'for' z '>>' f" := (foldi s e (fun x y => bind y (f x)) (Ok z)) (at level 50). + + +(*** Default *) + +(* Default instances for common types *) +Global Instance nat_default : Default nat := { + default := 0%nat +}. +Global Instance N_default : Default N := { + default := 0%N +}. +Global Instance Z_default : Default Z := { + default := 0%Z +}. +Global Instance uint_size_default : Default uint_size := { + default := Int32.zero +}. +Global Instance int_size_default : Default int_size := { + default := Int32.zero +}. +(* Global Instance int_default {WS : WORDSIZE} : Default int := { *) +(* default := repr 0 *) +(* }. *) +(* Global Instance uint8_default : Default uint8 := _. *) +Global Instance nat_mod_default {p : Z} : Default (nat_mod p) := { + default := nat_mod_zero +}. +Global Instance prod_default {A B} `{Default A} `{Default B} : Default (A × B) := { + default := (default, default) +}. diff --git a/proof-libs/coq/coq/src/Hacspec_TODO.v b/proof-libs/coq/coq/src/Hacspec_TODO.v new file mode 100644 index 000000000..2bf1d3c42 --- /dev/null +++ b/proof-libs/coq/coq/src/Hacspec_TODO.v @@ -0,0 +1,21 @@ +Global Set Warnings "-ambiguous-paths". +Global Set Warnings "-uniform-inheritance". +Global Set Warnings "-auto-template". +Global Set Warnings "-disj-pattern-notation". + +From Coq Require Import ZArith List. +Import ListNotations. +(* Require Import IntTypes. *) + +(* Require Import MachineIntegers. *) From compcert Require Import Integers. +From Coqprime Require GZnZ. + +Require Import Lia. + +(*** TODO *) + +Declare Scope hacspec_scope. +Definition never_to_any {A} (f : False) : A. contradiction. Defined. +Definition panic_fmt {A} (x : A): False. Admitted. +Notation impl_2__new_const := id. +Notation unsize := id. diff --git a/proof-libs/coq/coq/src/Hacspec_Types.v b/proof-libs/coq/coq/src/Hacspec_Types.v new file mode 100644 index 000000000..f4035e0b3 --- /dev/null +++ b/proof-libs/coq/coq/src/Hacspec_Types.v @@ -0,0 +1,8 @@ + +From Coqprime Require GZnZ. + +(*** Seq *) + +Definition nseq := VectorDef.t. + +Definition seq (A : Type) := list A. diff --git a/proof-libs/coq/coq/src/Hacspec_lib.v b/proof-libs/coq/coq/src/Hacspec_lib.v new file mode 100644 index 000000000..c1fef43c9 --- /dev/null +++ b/proof-libs/coq/coq/src/Hacspec_lib.v @@ -0,0 +1,146 @@ +(* File automatically generated by Hacspec *) +From Hacspec Require Import Hacspec_Lib. +(* Require Import MachineIntegers. *) From compcert Require Import Integers. + +From Coq Require Import ZArith. +Import List.ListNotations. +Open Scope Z_scope. +Open Scope bool_scope. + +From Hacspec Require Export Hacspec_Lib. + +(** Should be moved to Hacspec_Lib.v **) +(* Definition int_xI {WS : WORDSIZE} (a : int) : int := MachineIntegers.add (MachineIntegers.mul a (repr 2)) MachineIntegers.one. *) +(* Definition int_xO {WS : WORDSIZE} (a : int) : int := MachineIntegers.mul a (repr 2). *) +(* Number Notation int Pos.of_num_int Pos.to_num_int (via positive mapping [[int_xI] => xI, [int_xO] => xO , [MachineIntegers.one] => xH]) : hacspec_scope. *) +(* Notation "0" := (repr O). *) +(* Notation U8_t := int8. *) +(* Notation U8 := id. *) +(* Notation U16_t := int16. *) +(* Notation U16 := id. *) +(* Notation U32_t := int32. *) +(* Notation U32 := id. *) +(* Notation U64_t := int64. *) +(* Notation U64 := id. *) +(* Notation U128_t := int128. *) +(* Notation U128 := id. *) + +(* Definition array_index {A: Type} `{Default A} {len : nat} (s: nseq A len) {WS} (i : @int WS) := array_index s (unsigned i). *) +(* Notation " x .[ a ]" := (array_index x a) (at level 40). *) +(* Definition array_upd {A: Type} {len : nat} (s: nseq A len) {WS} (i: @int WS) (new_v: A) : nseq A len := array_upd s (unsigned i) new_v. *) +(* Notation " x .[ i ]<- a" := (array_upd x i a) (at level 40). *) + +(* Class Addition A := add : A -> A -> A. *) +(* Notation "a .+ b" := (add a b). *) +(* Instance array_add_inst {ws : WORDSIZE} {len: nat} : Addition (nseq (@int ws) len) := { add a b := a array_add b }. *) +(* Instance int_add_inst {ws : WORDSIZE} : Addition (@int ws) := { add a b := MachineIntegers.add a b }. *) + +(* Class Subtraction A := sub : A -> A -> A. *) +(* Notation "a .- b" := (sub a b). *) +(* Instance array_sub_inst {ws : WORDSIZE} {len: nat} : Subtraction (nseq (@int ws) len) := { sub := array_join_map MachineIntegers.sub }. *) +(* Instance int_sub_inst {ws : WORDSIZE} : Subtraction (@int ws) := { sub a b := MachineIntegers.sub a b }. *) + +(* Class Multiplication A := mul : A -> A -> A. *) +(* Notation "a .* b" := (mul a b). *) +(* Instance array_mul_inst {ws : WORDSIZE} {len: nat} : Multiplication (nseq (@int ws) len) := { mul a b := a array_mul b }. *) +(* Instance int_mul_inst {ws : WORDSIZE} : Multiplication (@int ws) := { mul a b := MachineIntegers.mul a b }. *) + +(* Class Xor A := xor : A -> A -> A. *) +(* Notation "a .^ b" := (xor a b). *) + +(* Instance array_xor_inst {ws : WORDSIZE} {len: nat} : Xor (nseq (@int ws) len) := { xor a b := a array_xor b }. *) +(* Instance int_xor_inst {ws : WORDSIZE} : Xor (@int ws) := { xor a b := MachineIntegers.xor a b }. *) + +(* Definition new {A : Type} `{Default A} {len} : nseq A len := array_new_ default _. *) +(* Class array_or_seq A len := *) +(* { as_seq : seq A ; as_nseq : nseq A len }. *) + +(* Arguments as_seq {_} {_} array_or_seq. *) +(* Arguments as_nseq {_} {_} array_or_seq. *) +(* Coercion as_seq : array_or_seq >-> seq. *) +(* Coercion as_nseq : array_or_seq >-> nseq. *) + +(* Instance nseq_array_or_seq {A len} (a : nseq A len) : array_or_seq A len := *) +(* { as_seq := array_to_seq a ; as_nseq := a ; }. *) +(* Coercion nseq_array_or_seq : nseq >-> array_or_seq. *) + +(* Instance seq_array_or_seq {A} `{Default A} (a : seq A) : array_or_seq A (length a) := *) +(* { as_seq := a ; as_nseq := array_from_seq _ a ; }. *) +(* Coercion seq_array_or_seq : seq >-> array_or_seq. *) + +(* Definition update {A : Type} `{Default A} {len slen} (s : nseq A len) {WS} (start : @int WS) (start_a : array_or_seq A slen) : nseq A len := *) +(* array_update (a := A) (len := len) s (unsigned start) (as_seq start_a). *) + +(* Definition to_le_U32s {A l} := array_to_le_uint32s (A := A) (l := l). *) +(* Axiom to_le_bytes : forall {ws : WORDSIZE} {len}, nseq (@int ws) len -> seq int8. *) +(* Definition from_seq {A : Type} `{Default A} {len slen} (s : array_or_seq A slen) : nseq A len := array_from_seq _ (as_seq s). *) + +(* Notation Seq_t := seq. *) +(* Notation len := (fun s => seq_len s : int32). *) + +(* Definition array_slice {a: Type} `{Default a} {len : nat} (input: nseq a len) {WS} (start: @int WS) (slice_len: @int WS) : seq a := slice (array_to_seq input) (unsigned start) (unsigned (start .+ slice_len)). *) +(* Notation slice := array_slice. *) +(* Definition seq_new {A: Type} `{Default A} {WS} (len: @int WS) : seq A := seq_new (unsigned len). *) +(* Notation new_seq := seq_new. *) +(* Notation num_exact_chunks := seq_num_exact_chunks. *) +(* Notation get_exact_chunk := seq_get_exact_chunk. *) +(* Definition set_chunk {a: Type} `{Default a} {len} (s: seq a) {WS} (chunk_len: @int WS) (chunk_num: @int WS) (chunk: array_or_seq a len) : seq a := seq_set_chunk s (unsigned chunk_len) (unsigned chunk_num) (as_seq chunk). *) +(* Definition set_exact_chunk {a} `{H : Default a} {len} s {WS} := @set_chunk a H len s WS. *) +(* Notation get_remainder_chunk := seq_get_remainder_chunk. *) +(* Notation "a <> b" := (negb (eqb a b)). *) + +(* Notation from_secret_literal := nat_mod_from_secret_literal. *) +(* Definition pow2 {m} (x : @int WORDSIZE32) := nat_mod_pow2 m (unsigned x). *) +(* Instance nat_mod_addition {n} : Addition (nat_mod n) := { add a b := a +% b }. *) +(* Instance nat_mod_subtraction {n} : Subtraction (nat_mod n) := { sub a b := a -% b }. *) +(* Instance nat_mod_multiplication {n} : Multiplication (nat_mod n) := { mul a b := a *% b }. *) +(* Definition from_slice {a: Type} `{Default a} {len slen} (x : array_or_seq a slen) {WS} (start: @int WS) (slice_len: @int WS) := array_from_slice default len (as_seq x) (unsigned start) (unsigned slice_len). *) +(* Notation zero := nat_mod_zero. *) +(* Notation to_byte_seq_le := nat_mod_to_byte_seq_le. *) +(* Notation U128_to_le_bytes := u128_to_le_bytes. *) +(* Notation U64_to_le_bytes := u64_to_le_bytes. *) +(* Notation from_byte_seq_le := nat_mod_from_byte_seq_le. *) +(* Definition from_literal {m} := nat_mod_from_literal m. *) +(* Notation inv := nat_mod_inv. *) +(* Notation update_start := array_update_start. *) +(* Notation pow := nat_mod_pow_self. *) +(* Notation bit := nat_mod_bit. *) + +(* Definition int_to_int {ws1 ws2} (i : @int ws1) : @int ws2 := repr (unsigned i). *) +(* Coercion int_to_int : int >-> int. *) +(* Notation push := seq_push. *) +(* Notation Build_secret := secret. *) +(* Notation "a -× b" := *) +(* (prod a b) (at level 80, right associativity) : hacspec_scope. *) +(* Notation Result_t := result. *) +(* Axiom TODO_name : Type. *) +(* Notation ONE := nat_mod_one. *) +(* Notation exp := nat_mod_exp. *) +(* Notation nat_mod := GZnZ.znz. *) +(* Instance nat_mod_znz_addition {n} : Addition (GZnZ.znz n) := { add a b := a +% b }. *) +(* Instance nat_mod_znz_subtraction {n} : Subtraction (GZnZ.znz n) := { sub a b := a -% b }. *) +(* Instance nat_mod_znz_multiplication {n} : Multiplication (GZnZ.znz n) := { mul a b := a *% b }. *) +(* Notation TWO := nat_mod_two. *) +(* Notation ne := (fun x y => negb (eqb x y)). *) +(* Notation eq := (eqb). *) +(* Notation rotate_right := (ror). *) +(* Notation to_be_U32s := array_to_be_uint32s. *) +(* Notation get_chunk := seq_get_chunk. *) +(* Notation num_chunks := seq_num_chunks. *) +(* Notation U64_to_be_bytes := uint64_to_be_bytes. *) +(* Notation to_be_bytes := array_to_be_bytes. *) +(* Notation U8_from_usize := uint8_from_usize. *) +(* Notation concat := seq_concat. *) +(* Notation declassify := id. *) +(* Notation U128_from_be_bytes := uint128_from_be_bytes. *) +(* Notation U128_to_be_bytes := uint128_to_be_bytes. *) +(* Notation slice_range := array_slice_range. *) +(* Notation truncate := seq_truncate. *) +(* Axiom array_to_be_uint64s : forall {A l}, nseq A l -> seq uint64. *) +(* Notation to_be_U64s := array_to_be_uint64s. *) +(* Notation classify := id. *) +(* Notation U64_from_U8 := uint64_from_uint8. *) +(* Fixpoint Build_Range_t (a b : nat) := (a,b). (* match (b - a)%nat with O => [] | S n => match b with | O => [] | S b' => Build_Range_t a b' ++ [b] end end. *) *) +(* Notation declassify_eq := eq. *) +(* Notation String_t := String.string. *) +(* (** end of: Should be moved to Hacspec_Lib.v **) *) diff --git a/proof-libs/coq/coq/src/QuickChickLib.v b/proof-libs/coq/coq/src/QuickChickLib.v new file mode 100644 index 000000000..b4853e718 --- /dev/null +++ b/proof-libs/coq/coq/src/QuickChickLib.v @@ -0,0 +1,101 @@ +From compcert Require Import Integers. +From Coq Require Import ZArith. +Import List.ListNotations. +Open Scope Z_scope. +Open Scope bool_scope. +From QuickChick Require Import QuickChick. +Require Import Coq.Lists.List. +From Hacspec Require Import Hacspec_Lib. +Open Scope hacspec_scope. + +#[global] Instance show_unit : Show (unit) := Build_Show (unit) (fun _ => "tt"%string). +Definition g_unit : G (unit) := returnGen tt. +#[global] Instance gen_unit : Gen (unit) := Build_Gen unit g_unit. + +#[global] Instance show_int8 : Show (int8) := + Build_Show (int8) (fun x => show (int8_to_nat x)). +Definition g_int8 : G (int8) := + bindGen (* arbitrary *) (choose (0,1000)) (fun x => returnGen (Int8.repr x)). +#[global] Instance gen_int8 : Gen (int8) := Build_Gen int8 g_int8. + +#[global] Instance show_int32 : Show (int32) := + Build_Show (int32) (fun x => show (int32_to_nat x)). +Definition g_int32 : G (int32) := (* restricted *) + bindGen (choose (0,1000)) (fun x => returnGen (Int32.repr x)). +#[global] Instance gen_int32 : Gen (int32) := Build_Gen int32 g_int32. + +#[global] Instance show_int64 : Show (int64) := + Build_Show (int64) (fun x => show (int64_to_nat x)). +Definition g_int64 : G (int64) := + bindGen (* arbitrary *) (choose (0,1000)) (fun x => returnGen (Int64.repr x)). +#[global] Instance gen_int64 : Gen (int64) := Build_Gen int64 g_int64. + +#[global] Instance show_uint_size : Show (uint_size) := + Build_Show (uint_size) (fun x => show x). +Definition g_uint_size : G (uint_size) := arbitrary. +#[global] Instance gen_uint_size : Gen (uint_size) := Build_Gen uint_size g_uint_size. + + +Inductive dependent_pair {A} (n : nat) := +| elem : forall (l : list A), length l = n -> dependent_pair n. + +Fixpoint g_listOf_aux {A} (gen : G (A)) (n : nat) : G (@dependent_pair A n). + destruct n. + - apply (returnGen). + exists []. + easy. + - apply (bindGen gen). + intros a. + apply (bindGen (g_listOf_aux A gen n)). + intros l. + apply returnGen. + destruct l as [l H]. + exists (a :: l). + cbn. + rewrite H. + easy. +Defined. + +Definition g_listOf {A} (gen : G (A)) : G (list A) := + bindGen arbitrary (fun n : nat => bindGen (g_listOf_aux gen n) (fun '(elem _ l _) => returnGen l)). + +#[global] Instance show_nseq {A} `{Show A} n : Show (nseq A n) := + Build_Show (nseq A n) (fun x => + match x with + | Vector.nil _ => "[]"%string + | Vector.cons _ x n xs => ("[" ++ fold_left (fun a b => (a ++ " " ++ show b)) (VectorDef.to_list xs) (show x) ++ "]")%string + end). + +Definition array_from_list_ (A : Type) (n : nat) (l : list A) `{n = (Datatypes.length l)} : nseq A n. +Proof. + rewrite H. + apply array_from_list. +Defined. +Definition g_nseq {A} `{Gen A} n : G (nseq A n). (* (usize *) + intros. + apply (bindGen (g_listOf_aux (arbitrary : G A) n)). + intros l. + apply returnGen. + + destruct l. + apply array_from_list_ with (l := l). + easy. +Defined. + +#[global] Instance gen_nseq {A} `{Gen A} n : Gen (nseq A n) := Build_Gen (nseq A n) (g_nseq n). + +#[global] Instance show_public_byte_seq : Show (public_byte_seq) := + Build_Show (public_byte_seq) (fun x => + match x with + | [] => "[]"%string + | x :: xs => ("[" ++ fold_left (fun a b => (a ++ " " ++ show b)) xs (show x) ++ "]")%string + end). +Definition g_public_byte_seq : G (public_byte_seq) := + listOf arbitrary. + (* @genList int8 gen_int8. *) + (* listOf (g_int8). *) + (* bindGen g_int8 (fun y => *) + (* bindGen g_int8 (fun x => returnGen ([y ; x]))). *) + (* listOf (g_int8). (*arbitrary*) *) +#[global] Instance gen_public_byte_seq : Gen (public_byte_seq) := + Build_Gen public_byte_seq g_public_byte_seq. diff --git a/proof-libs/coq/coq/src/dune b/proof-libs/coq/coq/src/dune new file mode 100644 index 000000000..d135007e3 --- /dev/null +++ b/proof-libs/coq/coq/src/dune @@ -0,0 +1,13 @@ +(coq.theory + (name Hacspec) ; -R flag + (package coq-hacspec) + (flags -w all) + (theories + Flocq + compcert + QuickChick mathcomp.ssreflect elpi HB ExtLib SimpleIO + Coqprime + ) + ; (libraries ) + ) +; (include_subdirs qualified)