diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 9e6b228..e80ef3c 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -17,14 +17,14 @@ jobs: strategy: matrix: image: - - 'mathcomp/mathcomp:1.16.0-coq-8.17' - - 'mathcomp/mathcomp:1.15.0-coq-8.16' - - 'mathcomp/mathcomp:1.14.0-coq-8.15' - - 'mathcomp/mathcomp:1.13.0-coq-8.14' - - 'mathcomp/mathcomp:1.12.0-coq-8.14' + - 'mathcomp/mathcomp:2.1.0-coq-8.18' + - 'mathcomp/mathcomp:2.0.0-coq-8.18' + - 'mathcomp/mathcomp:2.1.0-coq-8.17' + - 'mathcomp/mathcomp:2.1.0-coq-8.16' + - 'mathcomp/mathcomp:2.0.0-coq-8.16' fail-fast: false steps: - - uses: actions/checkout@v2 + - uses: actions/checkout@v3 - uses: coq-community/docker-coq-action@v1 with: opam_file: 'coq-bits.opam' diff --git a/README.md b/README.md index b3e5b77..17e5745 100644 --- a/README.md +++ b/README.md @@ -10,8 +10,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener [![Zulip][zulip-shield]][zulip-link] [![DOI][doi-shield]][doi-link] -[docker-action-shield]: https://github.com/coq-community/bits/workflows/Docker%20CI/badge.svg?branch=master -[docker-action-link]: https://github.com/coq-community/bits/actions?query=workflow:"Docker%20CI" +[docker-action-shield]: https://github.com/coq-community/bits/actions/workflows/docker-action.yml/badge.svg?branch=master +[docker-action-link]: https://github.com/coq-community/bits/actions/workflows/docker-action.yml [contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg [contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md @@ -38,11 +38,10 @@ axiomatization and extraction to OCaml native integers. - Coq-community maintainer(s): - Anton Trunov ([**@anton-trunov**](https://github.com/anton-trunov)) - License: [Apache License 2.0](LICENSE) -- Compatible Coq versions: 8.10 or later (use releases for other Coq versions) -- Compatible OCaml versions: 4.05 or later (not tested on previous versions) +- Compatible Coq versions: 8.16 or later (use releases for other Coq versions) - Additional dependencies: - OCamlbuild - - [MathComp](https://math-comp.github.io) 1.12.0 or later (`algebra` suffices) + - [MathComp](https://math-comp.github.io) 2.0 or later (`algebra` suffices) - Coq namespace: `Bits` - Related publication(s): - [From Sets to Bits in Coq](https://hal.archives-ouvertes.fr/hal-01251943/document) doi:[10.1007/978-3-319-29604-3_2](https://doi.org/10.1007/978-3-319-29604-3_2) diff --git a/coq-bits.opam b/coq-bits.opam index fb4321b..2db0cec 100644 --- a/coq-bits.opam +++ b/coq-bits.opam @@ -18,10 +18,9 @@ axiomatization and extraction to OCaml native integers.""" build: [make "-j%{jobs}%"] install: [make "install"] depends: [ - "ocaml" {(>= "4.05" & < "4.15~")} - "coq" {(>= "8.14" & < "8.18~")} + "coq" {(>= "8.16" & < "8.19~")} "ocamlbuild" - "coq-mathcomp-algebra" {(>= "1.12" & < "1.17~")} + "coq-mathcomp-algebra" {(>= "2.0" & < "2.2~")} ] tags: [ diff --git a/meta.yml b/meta.yml index 17d1612..875f156 100644 --- a/meta.yml +++ b/meta.yml @@ -46,28 +46,20 @@ license: identifier: Apache-2.0 file: LICENSE -supported_ocaml_versions: - text: 4.05 or later (not tested on previous versions) - opam: '{(>= "4.05" & < "4.15~")}' - supported_coq_versions: - text: 8.10 or later (use releases for other Coq versions) - opam: '{(>= "8.10" & < "8.17~")}' + text: 8.16 or later (use releases for other Coq versions) + opam: '{(>= "8.16" & < "8.19~")}' tested_coq_opam_versions: -- version: '1.15.0-coq-8.16' - repo: 'mathcomp/mathcomp' -- version: '1.14.0-coq-8.15' - repo: 'mathcomp/mathcomp' -- version: '1.13.0-coq-8.14' +- version: '2.1.0-coq-8.18' repo: 'mathcomp/mathcomp' -- version: '1.12.0-coq-8.13' +- version: '2.0.0-coq-8.18' repo: 'mathcomp/mathcomp' -- version: '1.12.0-coq-8.12' +- version: '2.1.0-coq-8.17' repo: 'mathcomp/mathcomp' -- version: '1.12.0-coq-8.11' +- version: '2.1.0-coq-8.16' repo: 'mathcomp/mathcomp' -- version: '1.12.0-coq-8.10' +- version: '2.0.0-coq-8.16' repo: 'mathcomp/mathcomp' dependencies: @@ -76,9 +68,9 @@ dependencies: description: OCamlbuild - opam: name: coq-mathcomp-algebra - version: '{(>= "1.12" & < "1.16~")}' + version: '{(>= "2.0" & < "2.2~")}' description: |- - [MathComp](https://math-comp.github.io) 1.12.0 or later (`algebra` suffices) + [MathComp](https://math-comp.github.io) 2.0 or later (`algebra` suffices) namespace: Bits diff --git a/src/spec/operations/properties.v b/src/spec/operations/properties.v index 39475bb..b70e083 100644 --- a/src/spec/operations/properties.v +++ b/src/spec/operations/properties.v @@ -1,6 +1,7 @@ (*=========================================================================== Proofs of properties of arithmetic and logical operations on n-bit words ===========================================================================*) +From HB Require Import structures. Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div. @@ -1196,22 +1197,27 @@ specialize (IHn true p1 p2). case E: (splitmsb (adcBmain true p1 p2)) => [carry' p']. destruct b2. (* b2 = true *) -rewrite beheadCons theadCons E in H. inversion H. apply val_inj in H3. subst. +rewrite beheadCons theadCons E in H. inversion H. +rewrite -[LHS]/(\val p') -[RHS]/(\val p) in H3. apply val_inj in H3. subst. rewrite IHn; first by rewrite orTb. done. (* b2 = false *) -rewrite beheadCons E in H. inversion H. apply val_inj in H3. subst. +rewrite beheadCons E in H. inversion H. +rewrite -[LHS]/(\val p') -[RHS]/(\val p) in H3. apply val_inj in H3. subst. rewrite IHn; first by rewrite orTb. done. (* b1 = false *) destruct b2. (* b2 = true *) specialize (IHn true p1 p2). case E: (splitmsb (adcBmain true p1 p2)) => [carry' p']. -rewrite beheadCons E in H. inversion H. apply val_inj in H3. subst. +rewrite beheadCons E in H. inversion H. +rewrite -[LHS]/(\val p') -[RHS]/(\val p) in H3. apply val_inj in H3. subst. rewrite IHn; first by rewrite orTb. done. (* b2 = false *) specialize (IHn false p1 p2). case E: (splitmsb (adcBmain false p1 p2)) => [carry' p']. -rewrite beheadCons E in H. inversion H. apply val_inj in H3. subst. simpl. +rewrite beheadCons E in H. inversion H. +rewrite -[LHS]/(\val p') -[RHS]/(\val p) in H3. apply val_inj in H3. +subst. simpl. rewrite /leB in IHn. rewrite !andbT. by rewrite IHn. (* c = false *) @@ -1222,26 +1228,30 @@ destruct b2. (* b2 = true *) specialize (IHn true p1 p2). case E: (splitmsb (adcBmain true p1 p2)) => [carry' p']. -rewrite beheadCons E in H. inversion H. apply val_inj in H3. subst. +rewrite beheadCons E in H. inversion H. +rewrite -[LHS]/(\val p') -[RHS]/(\val p) in H3. apply val_inj in H3. subst. specialize (IHn _ E). rewrite /leB. simpl. rewrite !beheadCons. by rewrite IHn. (* b2 = false *) specialize (IHn false p1 p2). case E: (splitmsb (adcBmain false p1 p2)) => [carry' p']. -rewrite beheadCons E in H. inversion H. apply val_inj in H3. subst. +rewrite beheadCons E in H. inversion H. +rewrite -[LHS]/(\val p') -[RHS]/(\val p) in H3. apply val_inj in H3. subst. rewrite /leB. simpl. rewrite !beheadCons. specialize (IHn _ E). rewrite /leB in IHn. rewrite andbF. rewrite orbF. done. (* b1 = false *) specialize (IHn false p1 p2). destruct b2. (* b2 = true *) case E: (splitmsb (adcBmain false p1 p2)) => [carry' p']. -rewrite beheadCons E in H. inversion H. apply val_inj in H3. subst. +rewrite beheadCons E in H. inversion H. +rewrite -[LHS]/(\val p') -[RHS]/(\val p) in H3. apply val_inj in H3. subst. rewrite /leB. simpl. rewrite !beheadCons !theadCons. rewrite /leB in IHn. specialize (IHn _ E). rewrite orbA. rewrite orbF. rewrite orbA. rewrite orbF. rewrite IHn. done. (* b2 = false *) case E: (splitmsb (adcBmain false p1 p2)) => [carry' p']. -rewrite beheadCons E in H. inversion H. apply val_inj in H3. subst. +rewrite beheadCons E in H. inversion H. +rewrite -[LHS]/(\val p') -[RHS]/(\val p) in H3. apply val_inj in H3. subst. rewrite /leB. simpl. rewrite !beheadCons !theadCons. specialize (IHn _ E). rewrite /leB in IHn. rewrite andbT. rewrite andbF. rewrite orbF. @@ -1962,13 +1972,11 @@ Section Structures. Variable n:nat. -Definition BITS_zmodMixin := ZmodMixin (@addBA n) (@addBC n) (@add0B n) (@addBN n). -Canonical Structure BITS_zmodType := Eval hnf in ZmodType (BITS n) BITS_zmodMixin. -Canonical Structure BITS_finZmodType := Eval hnf in [finZmodType of BITS n]. -Canonical Structure BITS_baseFinGroupType := - Eval hnf in [baseFinGroupType of (BITS n) for +%R]. -Canonical Structure BITS_finGroupType := - Eval hnf in [finGroupType of (BITS n) for +%R]. +HB.instance Definition _ := Finite.copy (BITS n) [finType of BITS n]. +HB.instance Definition _ := GRing.isZmodule.Build (BITS n) + (@addBA n) (@addBC n) (@add0B n) (@addBN n). +HB.instance Definition _ := isMulGroup.Build (BITS n) + (@addBA n) (@add0B n) (@addBN n). End Structures.