From d2fbf651863b1f690a9d27b3434adba66e464388 Mon Sep 17 00:00:00 2001 From: Lasse Letager Hansen Date: Tue, 9 Apr 2024 18:47:51 +0200 Subject: [PATCH] Start adding tests, and use dune --- .github/workflows/coq-hacspec-lib.yml | 100 +++++++ dune-project | 3 + engine/backends/coq/coq/coq_backend.ml | 42 +-- engine/backends/coq/coq_ast.ml | 4 +- opam/coq-hacspec.opam | 31 ++ proof-libs/coq/coq/_CoqProject | 1 + proof-libs/coq/coq/src/Hacspec_Integers.v | 330 ++++++++++++---------- proof-libs/coq/coq/src/Hacspec_Lib.v | 76 +++-- proof-libs/coq/coq/src/Hacspec_TODO.v | 21 ++ proof-libs/coq/coq/src/Hacspec_lib.v | 272 +++++++++--------- proof-libs/coq/coq/src/QuickChickLib.v | 15 +- proof-libs/coq/coq/src/dune | 4 +- 12 files changed, 560 insertions(+), 339 deletions(-) create mode 100644 .github/workflows/coq-hacspec-lib.yml create mode 100644 opam/coq-hacspec.opam create mode 100644 proof-libs/coq/coq/src/Hacspec_TODO.v 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 index 811388526..2c8058a98 100644 --- a/dune-project +++ b/dune-project @@ -16,6 +16,9 @@ (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 c90877015..4ac4dc509 100644 --- a/engine/backends/coq/coq/coq_backend.ml +++ b/engine/backends/coq/coq/coq_backend.ml @@ -68,7 +68,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" @@ -169,7 +169,7 @@ struct 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.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)) @@ -385,7 +385,7 @@ struct | TyAlias { name; ty; _ } -> [ C.AST.Notation - ( "'" ^ pconcrete_ident name ^ "_t" ^ "'", + ( "'" ^ pconcrete_ident name ^ "'", C.AST.Type (pty span ty), None ); ] @@ -437,7 +437,7 @@ struct in [ C.AST.Notation - ( "'" ^ o.type_name ^ "_t" ^ "'", + ( "'" ^ o.type_name ^ "'", C.AST.Type (C.AST.NatMod ( o.type_of_canvas, @@ -449,8 +449,8 @@ 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 @@ -459,7 +459,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 }, @@ -470,8 +470,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 @@ -480,7 +480,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 }, @@ -491,8 +491,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 @@ -506,14 +506,14 @@ struct in [ C.AST.Notation - ("'" ^ o.bytes_name ^ "_t" ^ "'", C.AST.Type typ, None); + ("'" ^ 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 @@ -536,7 +536,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 }, @@ -547,8 +547,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 ()) @@ -667,11 +667,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..d062bfa72 100644 --- a/engine/backends/coq/coq_ast.ml +++ b/engine/backends/coq/coq_ast.ml @@ -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 @@ -304,7 +304,7 @@ functor 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 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/_CoqProject b/proof-libs/coq/coq/_CoqProject index ff25a5d44..c9279aeb1 100644 --- a/proof-libs/coq/coq/_CoqProject +++ b/proof-libs/coq/coq/_CoqProject @@ -4,6 +4,7 @@ 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/src/Hacspec_Integers.v b/proof-libs/coq/coq/src/Hacspec_Integers.v index ed373dad7..17ae34a86 100644 --- a/proof-libs/coq/coq/src/Hacspec_Integers.v +++ b/proof-libs/coq/coq/src/Hacspec_Integers.v @@ -55,10 +55,12 @@ Qed. (*** Hacspec Integers *) -Module HacspecIntegers (WS : WORDSIZE). +Class MyAdd (A : Type) := myadd : A -> A -> A. +Infix ".+" := (myadd) (at level 77) : hacspec_scope. +Module HacspecIntegers (WS : WORDSIZE). + Include (Make WS). (**** Public integers *) - Include Make WS. Definition pub (n : Z) : int := repr n. @@ -78,8 +80,10 @@ Module HacspecIntegers (WS : WORDSIZE). 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 ".+" := (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. @@ -93,170 +97,170 @@ Module HacspecIntegers (WS : WORDSIZE). (* Definition zero := (@zero WORDSIZE32). *) Notation "A × B" := (prod A B) (at level 79, left associativity) : hacspec_scope. -(*** Uint size util *) + (*** 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. + (* 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. + (* 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). + 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. + 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. + (* 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). -(* destruct int as you would a natural number *) -Definition destruct_int_as_nat (a : int) : forall (P : int -> Prop), + 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. + 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. - + 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 + 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. + 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. - + 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 ; [ | | ]. + 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. @@ -276,12 +280,24 @@ 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. *) @@ -343,3 +359,5 @@ 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 index 24b0bb9ed..277174a92 100644 --- a/proof-libs/coq/coq/src/Hacspec_Lib.v +++ b/proof-libs/coq/coq/src/Hacspec_Lib.v @@ -14,9 +14,13 @@ Require Import Lia. Declare Scope hacspec_scope. -Require Import Hacspec_Types. -Require Import Hacspec_Integers. +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 *) @@ -134,7 +138,9 @@ Proof. induction fuel ; intros. - reflexivity. - do 2 rewrite <- foldi__nat_move_S. - replace (S fuel + i)%nat with (fuel + (S i))%nat by (symmetry ; apply plus_Snm_nSm). + + Require Import PeanoNat. + replace (S fuel + i)%nat with (fuel + (S i))%nat by (symmetry ; apply plus_n_Sm). rewrite IHfuel. + reflexivity. + lia. @@ -320,10 +326,10 @@ Definition seq_new_ {A: Type} (init : A) (len: nat) : seq A := 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) := +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 A xs) + | x :: xs => VectorDef.cons A x (length xs) (array_from_list xs) end. (* match l, length l with *) @@ -910,22 +916,58 @@ Section Casting. cast n := GZnZ.val p n }. - (* Note: should be aware of typeclass resolution with int/uint since they are just aliases of each other currently *) - Global Instance cast_int8_to_uint32 : Cast int8 uint32 := { - cast n := Int32.repr (Int8.unsigned n) - }. - Global Instance cast_int8_to_int32 : Cast int8 int32 := { - cast n := Int32.repr (Int8.signed n) - }. - - Global Instance cast_uint8_to_uint32 : Cast uint8 uint32 := { - cast n := Int32.repr (Int8.unsigned 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. 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_lib.v b/proof-libs/coq/coq/src/Hacspec_lib.v index b274c7dd5..c1fef43c9 100644 --- a/proof-libs/coq/coq/src/Hacspec_lib.v +++ b/proof-libs/coq/coq/src/Hacspec_lib.v @@ -1,146 +1,146 @@ (* File automatically generated by Hacspec *) -From Hacspec Require Import Hacspec_Lib MachineIntegers. +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 MachineIntegers. 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 **) +(* 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 index 55e6dc8f3..b4853e718 100644 --- a/proof-libs/coq/coq/src/QuickChickLib.v +++ b/proof-libs/coq/coq/src/QuickChickLib.v @@ -1,11 +1,12 @@ -Require Import Hacspec_Lib MachineIntegers. +From compcert Require Import Integers. From Coq Require Import ZArith. Import List.ListNotations. Open Scope Z_scope. Open Scope bool_scope. -Open Scope hacspec_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. @@ -14,19 +15,19 @@ Definition g_unit : G (unit) := returnGen tt. #[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 (pub_u8 x)). + 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 (pub_u32 x)). + 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 (pub_u64 x)). + 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) := @@ -72,8 +73,8 @@ Proof. 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 sem. + apply (bindGen (g_listOf_aux (arbitrary : G A) n)). + intros l. apply returnGen. destruct l. diff --git a/proof-libs/coq/coq/src/dune b/proof-libs/coq/coq/src/dune index ecc1a1daa..d135007e3 100644 --- a/proof-libs/coq/coq/src/dune +++ b/proof-libs/coq/coq/src/dune @@ -3,8 +3,10 @@ (package coq-hacspec) (flags -w all) (theories + Flocq compcert - Equations + QuickChick mathcomp.ssreflect elpi HB ExtLib SimpleIO + Coqprime ) ; (libraries ) )