diff options
Diffstat (limited to 'lit/scheduling.org')
-rw-r--r-- | lit/scheduling.org | 241 |
1 files changed, 117 insertions, 124 deletions
diff --git a/lit/scheduling.org b/lit/scheduling.org index c3fb12a..728dfc5 100644 --- a/lit/scheduling.org +++ b/lit/scheduling.org @@ -1572,7 +1572,123 @@ Require Import vericert.hls.RTLBlock. #+name: rtlblockgen-equalities-insert #+begin_src coq -<<rtlblockgen-equalities>> +Lemma comparison_eq: forall (x y : comparison), {x = y} + {x <> y}. +Proof. + decide equality. +Defined. + +Lemma condition_eq: forall (x y : Op.condition), {x = y} + {x <> y}. +Proof. + generalize comparison_eq; intro. + generalize Int.eq_dec; intro. + generalize Int64.eq_dec; intro. + decide equality. +Defined. + +Lemma addressing_eq : forall (x y : Op.addressing), {x = y} + {x <> y}. +Proof. + generalize Int.eq_dec; intro. + generalize AST.ident_eq; intro. + generalize Z.eq_dec; intro. + generalize Ptrofs.eq_dec; intro. + decide equality. +Defined. + +Lemma typ_eq : forall (x y : AST.typ), {x = y} + {x <> y}. +Proof. + decide equality. +Defined. + +Lemma operation_eq: forall (x y : Op.operation), {x = y} + {x <> y}. +Proof. + generalize Int.eq_dec; intro. + generalize Int64.eq_dec; intro. + generalize Float.eq_dec; intro. + generalize Float32.eq_dec; intro. + generalize AST.ident_eq; intro. + generalize condition_eq; intro. + generalize addressing_eq; intro. + generalize typ_eq; intro. + decide equality. +Defined. + +Lemma memory_chunk_eq : forall (x y : AST.memory_chunk), {x = y} + {x <> y}. +Proof. + decide equality. +Defined. + +Lemma list_typ_eq: forall (x y : list AST.typ), {x = y} + {x <> y}. +Proof. + generalize typ_eq; intro. + decide equality. +Defined. + +Lemma option_typ_eq : forall (x y : option AST.typ), {x = y} + {x <> y}. +Proof. + generalize typ_eq; intro. + decide equality. +Defined. + +Lemma signature_eq: forall (x y : AST.signature), {x = y} + {x <> y}. +Proof. + repeat decide equality. +Defined. + +Lemma list_operation_eq : forall (x y : list Op.operation), {x = y} + {x <> y}. +Proof. + generalize operation_eq; intro. + decide equality. +Defined. + +Lemma list_pos_eq : forall (x y : list positive), {x = y} + {x <> y}. +Proof. + generalize Pos.eq_dec; intros. + decide equality. +Defined. + +Lemma sig_eq : forall (x y : AST.signature), {x = y} + {x <> y}. +Proof. + repeat decide equality. +Defined. + +Lemma instr_eq: forall (x y : instr), {x = y} + {x <> y}. +Proof. + generalize Pos.eq_dec; intro. + generalize typ_eq; intro. + generalize Int.eq_dec; intro. + generalize memory_chunk_eq; intro. + generalize addressing_eq; intro. + generalize operation_eq; intro. + generalize condition_eq; intro. + generalize signature_eq; intro. + generalize list_operation_eq; intro. + generalize list_pos_eq; intro. + generalize AST.ident_eq; intro. + repeat decide equality. +Defined. + +Lemma cf_instr_eq: forall (x y : cf_instr), {x = y} + {x <> y}. +Proof. + generalize Pos.eq_dec; intro. + generalize typ_eq; intro. + generalize Int.eq_dec; intro. + generalize Int64.eq_dec; intro. + generalize Float.eq_dec; intro. + generalize Float32.eq_dec; intro. + generalize Ptrofs.eq_dec; intro. + generalize memory_chunk_eq; intro. + generalize addressing_eq; intro. + generalize operation_eq; intro. + generalize condition_eq; intro. + generalize signature_eq; intro. + generalize list_operation_eq; intro. + generalize list_pos_eq; intro. + generalize AST.ident_eq; intro. + repeat decide equality. +Defined. + +Definition ceq {A: Type} (eqd: forall a b: A, {a = b} + {a <> b}) (a b: A): bool := + if eqd a b then true else false. #+end_src #+name: rtlblockgen-main @@ -1717,129 +1833,6 @@ Definition transl_program : RTL.program -> Errors.res program := transform_partial_program transl_fundef. #+end_src -** Equalities (rtlblockgen-equalities) - -#+name: rtlblockgen-equalities -#+begin_src coq :tangle no -Lemma comparison_eq: forall (x y : comparison), {x = y} + {x <> y}. -Proof. - decide equality. -Defined. - -Lemma condition_eq: forall (x y : Op.condition), {x = y} + {x <> y}. -Proof. - generalize comparison_eq; intro. - generalize Int.eq_dec; intro. - generalize Int64.eq_dec; intro. - decide equality. -Defined. - -Lemma addressing_eq : forall (x y : Op.addressing), {x = y} + {x <> y}. -Proof. - generalize Int.eq_dec; intro. - generalize AST.ident_eq; intro. - generalize Z.eq_dec; intro. - generalize Ptrofs.eq_dec; intro. - decide equality. -Defined. - -Lemma typ_eq : forall (x y : AST.typ), {x = y} + {x <> y}. -Proof. - decide equality. -Defined. - -Lemma operation_eq: forall (x y : Op.operation), {x = y} + {x <> y}. -Proof. - generalize Int.eq_dec; intro. - generalize Int64.eq_dec; intro. - generalize Float.eq_dec; intro. - generalize Float32.eq_dec; intro. - generalize AST.ident_eq; intro. - generalize condition_eq; intro. - generalize addressing_eq; intro. - generalize typ_eq; intro. - decide equality. -Defined. - -Lemma memory_chunk_eq : forall (x y : AST.memory_chunk), {x = y} + {x <> y}. -Proof. - decide equality. -Defined. - -Lemma list_typ_eq: forall (x y : list AST.typ), {x = y} + {x <> y}. -Proof. - generalize typ_eq; intro. - decide equality. -Defined. - -Lemma option_typ_eq : forall (x y : option AST.typ), {x = y} + {x <> y}. -Proof. - generalize typ_eq; intro. - decide equality. -Defined. - -Lemma signature_eq: forall (x y : AST.signature), {x = y} + {x <> y}. -Proof. - repeat decide equality. -Defined. - -Lemma list_operation_eq : forall (x y : list Op.operation), {x = y} + {x <> y}. -Proof. - generalize operation_eq; intro. - decide equality. -Defined. - -Lemma list_pos_eq : forall (x y : list positive), {x = y} + {x <> y}. -Proof. - generalize Pos.eq_dec; intros. - decide equality. -Defined. - -Lemma sig_eq : forall (x y : AST.signature), {x = y} + {x <> y}. -Proof. - repeat decide equality. -Defined. - -Lemma instr_eq: forall (x y : instr), {x = y} + {x <> y}. -Proof. - generalize Pos.eq_dec; intro. - generalize typ_eq; intro. - generalize Int.eq_dec; intro. - generalize memory_chunk_eq; intro. - generalize addressing_eq; intro. - generalize operation_eq; intro. - generalize condition_eq; intro. - generalize signature_eq; intro. - generalize list_operation_eq; intro. - generalize list_pos_eq; intro. - generalize AST.ident_eq; intro. - repeat decide equality. -Defined. - -Lemma cf_instr_eq: forall (x y : cf_instr), {x = y} + {x <> y}. -Proof. - generalize Pos.eq_dec; intro. - generalize typ_eq; intro. - generalize Int.eq_dec; intro. - generalize Int64.eq_dec; intro. - generalize Float.eq_dec; intro. - generalize Float32.eq_dec; intro. - generalize Ptrofs.eq_dec; intro. - generalize memory_chunk_eq; intro. - generalize addressing_eq; intro. - generalize operation_eq; intro. - generalize condition_eq; intro. - generalize signature_eq; intro. - generalize list_operation_eq; intro. - generalize list_pos_eq; intro. - generalize AST.ident_eq; intro. - repeat decide equality. -Defined. - -Definition ceq {A: Type} (eqd: forall a b: A, {a = b} + {a <> b}) (a b: A): bool := - if eqd a b then true else false. -#+end_src - * RTLBlockgenproof :PROPERTIES: :header-args:coq: :comments noweb :noweb no-export :padline yes :tangle ../src/hls/RTLBlockgenproof.v |