Coq proof lib

.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
+ }
+ ]
+ }
+ ]
+}

.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

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<[email protected]>")
+ (authors "Lasse Letager Hansen<[email protected]>")
+ (depends
+ ocaml
+ dune
+ (base (>= "0.16.2"))
+ (coq (>= "8.18.0"))
+ coq-compcert
+ coq-coqprime
+ coq-quickchick
+ )
+ (tags
+ (topics "to describe" your project)))
+

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"
@@ -168,8 +168,7 @@ struct
  | 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))
@@ -385,9 +384,7 @@ 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 } ->
@@ -437,7 +434,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 +446,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
@@ -459,7 +455,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 +466,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 +476,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 +487,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
@@ -505,15 +501,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
@@ -536,7 +531,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 +542,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 +662,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 =

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,8 +304,14 @@ 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
  let expr_str = term_to_string_without_paren bind (depth + 1) in

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<[email protected]>"]
+authors: ["Lasse Letager Hansen<[email protected]>"]
+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}
+ ]
+]

proof-libs/coq/coq/.gitignore

@@ -0,0 +1,7 @@
+*.vo*
+*.aux
+*.glob
+*.cache
+.Makefile.d
+Makefile
+Makefile.conf

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.

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