diff options
Diffstat (limited to 'src/common')
| -rw-r--r-- | src/common/Coquplib.v | 6 | ||||
| -rw-r--r-- | src/common/IntegerExtra.v | 38 | ||||
| -rw-r--r-- | src/common/Maps.v | 2 | ||||
| -rw-r--r-- | src/common/Monad.v | 4 | ||||
| -rw-r--r-- | src/common/Show.v | 2 | ||||
| -rw-r--r-- | src/common/Statemonad.v | 2 |
6 files changed, 22 insertions, 32 deletions
diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v index 469eddc..d9176db 100644 --- a/src/common/Coquplib.v +++ b/src/common/Coquplib.v @@ -1,5 +1,5 @@ (* - * CoqUp: Verified high-level synthesis. + * Vericert: Verified high-level synthesis. * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com> * * This program is free software: you can redistribute it and/or modify @@ -25,7 +25,7 @@ From Coq Require Export Require Import Lia. -From coqup Require Import Show. +From vericert Require Import Show. (* Depend on CompCert for the basic library, as they declare and prove some useful theorems. *) @@ -235,5 +235,3 @@ Definition debug_show {A B : Type} `{Show A} (a : A) (b : B) : B := Definition debug_show_msg {A B : Type} `{Show A} (s : string) (a : A) (b : B) : B := let unused := debug_print (s ++ show a) in b. - -Notation "f $ x" := (f x) (at level 60, right associativity, only parsing). diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v index 8e32c2c..c9b5dbd 100644 --- a/src/common/IntegerExtra.v +++ b/src/common/IntegerExtra.v @@ -5,7 +5,7 @@ Require Import ZBinary. From bbv Require Import ZLib. From compcert Require Import Integers Coqlib. -Require Import Coquplib. +Require Import Vericertlib. Local Open Scope Z_scope. @@ -298,48 +298,44 @@ Module IntExtra. (or (shl (repr (Byte.unsigned c)) (repr Byte.zwordsize)) (repr (Byte.unsigned d)))). - Definition byte0 (n: int) : byte := Byte.repr $ unsigned n. - Definition ibyte0 (n: int) : int := Int.repr $ Byte.unsigned $ byte0 n. + Definition byte1 (n: int) : byte := Byte.repr (unsigned n). - Definition byte1 (n: int) : byte := Byte.repr $ unsigned $ shru n $ repr Byte.zwordsize. - Definition ibyte1 (n: int) : int := Int.repr $ Byte.unsigned $ byte1 n. + Definition byte2 (n: int) : byte := Byte.repr (unsigned (shru n (repr Byte.zwordsize))). - Definition byte2 (n: int) : byte := Byte.repr $ unsigned $ shru n $ repr (2 * Byte.zwordsize). - Definition ibyte2 (n: int) : int := Int.repr $ Byte.unsigned $ byte2 n. + Definition byte3 (n: int) : byte := Byte.repr (unsigned (shru n (repr (2 * Byte.zwordsize)))). - Definition byte3 (n: int) : byte := Byte.repr $ unsigned $ shru n $ repr (3 * Byte.zwordsize). - Definition ibyte3 (n: int) : int := Int.repr $ Byte.unsigned $ byte3 n. + Definition byte4 (n: int) : byte := Byte.repr (unsigned (shru n (repr (3 * Byte.zwordsize)))). - Lemma bits_byte0: - forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte0 n) i = testbit n i. + Lemma bits_byte1: + forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte1 n) i = testbit n i. Proof. - intros. unfold byte0. rewrite Byte.testbit_repr; auto. + intros. unfold byte1. rewrite Byte.testbit_repr; auto. Qed. - Lemma bits_byte1: - forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte1 n) i = testbit n (i + Byte.zwordsize). + Lemma bits_byte2: + forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte2 n) i = testbit n (i + Byte.zwordsize). Proof. - intros. unfold byte1. rewrite Byte.testbit_repr; auto. + intros. unfold byte2. rewrite Byte.testbit_repr; auto. assert (zwordsize = 4 * Byte.zwordsize) by reflexivity. fold (testbit (shru n (repr Byte.zwordsize)) i). rewrite bits_shru. change (unsigned (repr Byte.zwordsize)) with Byte.zwordsize. apply zlt_true. omega. omega. Qed. - Lemma bits_byte2: - forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte2 n) i = testbit n (i + (2 * Byte.zwordsize)). + Lemma bits_byte3: + forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte3 n) i = testbit n (i + (2 * Byte.zwordsize)). Proof. - intros. unfold byte2. rewrite Byte.testbit_repr; auto. + intros. unfold byte3. rewrite Byte.testbit_repr; auto. assert (zwordsize = 4 * Byte.zwordsize) by reflexivity. fold (testbit (shru n (repr (2 * Byte.zwordsize))) i). rewrite bits_shru. change (unsigned (repr (2 * Byte.zwordsize))) with (2 * Byte.zwordsize). apply zlt_true. omega. omega. Qed. - Lemma bits_byte3: - forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte3 n) i = testbit n (i + (3 * Byte.zwordsize)). + Lemma bits_byte4: + forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte4 n) i = testbit n (i + (3 * Byte.zwordsize)). Proof. - intros. unfold byte3. rewrite Byte.testbit_repr; auto. + intros. unfold byte4. rewrite Byte.testbit_repr; auto. assert (zwordsize = 4 * Byte.zwordsize) by reflexivity. fold (testbit (shru n (repr (3 * Byte.zwordsize))) i). rewrite bits_shru. change (unsigned (repr (3 * Byte.zwordsize))) with (3 * Byte.zwordsize). diff --git a/src/common/Maps.v b/src/common/Maps.v index 3236417..b5a2fb2 100644 --- a/src/common/Maps.v +++ b/src/common/Maps.v @@ -1,4 +1,4 @@ -From coqup Require Import Coquplib. +From vericert Require Import Vericertlib. From compcert Require Export Maps. From compcert Require Import Errors. diff --git a/src/common/Monad.v b/src/common/Monad.v index 628963e..8517186 100644 --- a/src/common/Monad.v +++ b/src/common/Monad.v @@ -20,10 +20,6 @@ Module MonadExtra(M : Monad). Module MonadNotation. - Notation "A ; B" := - (bind A (fun _ => B)) - (at level 200, B at level 200). - Notation "'do' X <- A ; B" := (bind A (fun X => B)) (at level 200, X ident, A at level 100, B at level 200). diff --git a/src/common/Show.v b/src/common/Show.v index c994df3..4c66725 100644 --- a/src/common/Show.v +++ b/src/common/Show.v @@ -1,5 +1,5 @@ (* - * CoqUp: Verified high-level synthesis. + * Vericert: Verified high-level synthesis. * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com> * * This program is free software: you can redistribute it and/or modify diff --git a/src/common/Statemonad.v b/src/common/Statemonad.v index ed1b9e7..2eada2f 100644 --- a/src/common/Statemonad.v +++ b/src/common/Statemonad.v @@ -1,5 +1,5 @@ From compcert Require Errors. -From coqup Require Import Monad. +From vericert Require Import Monad. From Coq Require Import Lists.List. Module Type State. |