Start adding tests, and use dune

.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

@@ -16,6 +16,9 @@
  (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"
@@ -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 =

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

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/_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