Last active
November 22, 2022 20:30
-
-
Save RyanGlScott/1f5f63ebad0f2fb96a56036b9a797bd4 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
From Coq Require Import Program.Basics. | |
From Coq Require Program.Equality. | |
From Coq Require Import Vectors.Vector. | |
From Coq Require Import Logic.Eqdep. | |
Import VectorNotations. | |
Require Import Lia. | |
Require Import ZArith. | |
Require Import ZifyBool. | |
Import ZifyClasses. | |
Definition Vec (n : nat) (a : Type) : Type := VectorDef.t a n. | |
Notation bitvector n := (Vec n bool). | |
(* Workaround for https://github.com/coq/coq/issues/16803 *) | |
Constraint Vec.u1 <= mkapp2.u0. | |
Constraint Vec.u1 <= mkapp2.u1. | |
Constraint Vec.u1 <= mkapp2.u2. | |
Constraint Vec.u1 <= mkrel.u0. | |
Constraint Vec.u1 <= mkapp.u0. | |
Constraint Vec.u1 <= mkapp.u1. | |
(* The exact definitions here aren't terribly important, so I've omitted them | |
here for the sake of making this test case more minimal. *) | |
Definition bvToInt : forall w, bitvector w -> Z. Admitted. | |
Definition isBvult : forall w, bitvector w -> bitvector w -> Prop. Admitted. | |
Definition bvAdd : forall w, bitvector w -> bitvector w -> bitvector w. Admitted. | |
Definition bitvector_64 := bitvector 64. | |
(* Working *) | |
(* | |
Notation modulus := (Z.pow 2 64). | |
*) | |
(* Not working *) | |
Notation modulus := (Z.pow 2 (Z.of_nat 64)). | |
Global Program Instance Inj_bv_Z : InjTyp bitvector_64 Z := | |
{ inj := bvToInt 64 | |
; pred := fun x => Z.le 0 x /\ Z.lt x modulus | |
}. | |
Next Obligation. | |
Admitted. | |
Global Program Instance Rel_eq_bv : BinRel (@eq bitvector_64) := | |
{ TR := @eq Z | |
}. | |
Next Obligation. | |
Admitted. | |
Global Program Instance Rel_isBvult : BinRel (isBvult 64 : bitvector_64 -> bitvector_64 -> Prop) := | |
{ TR := Z.lt | |
}. | |
Next Obligation. | |
Admitted. | |
Global Program Instance Op_bvAdd : BinOp (bvAdd 64 : bitvector_64 -> bitvector_64 -> bitvector_64) := | |
{ TBOp := fun x y => Z.modulo (Z.add x y) modulus | |
}. | |
Next Obligation. | |
Admitted. | |
Add Zify InjTyp Inj_bv_Z. | |
Add Zify BinRel Rel_eq_bv. | |
Add Zify BinRel Rel_isBvult. | |
Add Zify BinOp Op_bvAdd. | |
Ltac Zify.zify_convert_to_euclidean_division_equations_flag ::= constr:(true). | |
Lemma test_refl : | |
forall (x : bitvector 64), x = x. | |
Proof. lia. Qed. | |
Lemma test_isBvult_trans : | |
forall (x y z : bitvector 64), | |
isBvult 64 x y -> isBvult 64 y z -> isBvult 64 x z. | |
Proof. lia. Qed. | |
Lemma test_bvAdd_comm : | |
forall (x y : bitvector 64), | |
bvAdd 64 x y = bvAdd 64 y x. | |
Proof. lia. Qed. | |
End S. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
From Coq Require Import Program.Basics. | |
From Coq Require Program.Equality. | |
From Coq Require Import Vectors.Vector. | |
From Coq Require Import Logic.Eqdep. | |
Import VectorNotations. | |
Require Import Lia. | |
Require Import ZArith. | |
Require Import ZifyBool. | |
Import ZifyClasses. | |
Definition Vec (n : nat) (a : Type) : Type := VectorDef.t a n. | |
Notation bitvector n := (Vec n bool). | |
(* Workaround for https://github.com/coq/coq/issues/16803 *) | |
Constraint Vec.u1 <= mkapp2.u0. | |
Constraint Vec.u1 <= mkapp2.u1. | |
Constraint Vec.u1 <= mkapp2.u2. | |
Constraint Vec.u1 <= mkrel.u0. | |
Constraint Vec.u1 <= mkapp.u0. | |
Constraint Vec.u1 <= mkapp.u1. | |
(* The exact definitions here aren't terribly important, so I've omitted them | |
here for the sake of making this test case more minimal. *) | |
Definition bvToInt : forall w, bitvector w -> Z. Admitted. | |
Definition isBvult : forall w, bitvector w -> bitvector w -> Prop. Admitted. | |
Definition bvAdd : forall w, bitvector w -> bitvector w -> bitvector w. Admitted. | |
Notation modulus w := | |
(Z.pow 2 (Z.of_nat w)). | |
Global Program Instance Inj_bv_Z w : InjTyp (bitvector w) Z := | |
{ inj := bvToInt w | |
; pred := fun x => Z.le 0 x /\ Z.lt x (modulus w) | |
}. | |
Next Obligation. | |
Admitted. | |
Global Program Instance Rel_eq_bv w : BinRel (@eq (bitvector w)) := | |
{ TR := @eq Z | |
}. | |
Next Obligation. | |
Admitted. | |
Global Program Instance Rel_isBvult w : BinRel (isBvult w) := | |
{ TR := Z.lt | |
}. | |
Next Obligation. | |
Admitted. | |
Global Program Instance Op_bvAdd w : BinOp (bvAdd w) := | |
{ TBOp := fun x y => Z.modulo (Z.add x y) (modulus w) | |
}. | |
Next Obligation. | |
Admitted. | |
Ltac Zify.zify_convert_to_euclidean_division_equations_flag ::= constr:(true). | |
Section S. | |
Variable w : nat. | |
Add Zify InjTyp (Inj_bv_Z w). | |
Add Zify BinRel (Rel_eq_bv w). | |
Add Zify BinRel (Rel_isBvult w). | |
Add Zify BinOp (Op_bvAdd w). | |
Lemma test_refl : | |
forall (x : bitvector w), x = x. | |
Proof. lia. Qed. | |
Lemma test_isBvult_trans : | |
forall (x y z : bitvector w), | |
isBvult w x y -> isBvult w y z -> isBvult w x z. | |
Proof. lia. Qed. | |
Lemma test_bvAdd_comm : | |
forall (x y : bitvector w), | |
bvAdd w x y = bvAdd w y x. | |
Proof. | |
(* Tactic failure: Cannot find witness. *) | |
Fail lia. | |
Admitted. | |
End S. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment