diff options
author | Yann Herklotz <git@yannherklotz.com> | 2021-10-24 19:59:09 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2021-10-24 19:59:09 +0100 |
commit | 934b137726cf0ef093db0a7bb8112326e29b256f (patch) | |
tree | 8ae356178cc4e86c54e4139344fdcfb8fe503ea6 /src/hls/RTLBlockInstr.v | |
parent | 9355fe644b65539bfb508706899c4dd351d136bb (diff) | |
download | vericert-934b137726cf0ef093db0a7bb8112326e29b256f.tar.gz vericert-934b137726cf0ef093db0a7bb8112326e29b256f.zip |
Add type-class proofs to Predicate.v
Diffstat (limited to 'src/hls/RTLBlockInstr.v')
-rw-r--r-- | src/hls/RTLBlockInstr.v | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v index 51beedc..e9e85f7 100644 --- a/src/hls/RTLBlockInstr.v +++ b/src/hls/RTLBlockInstr.v @@ -100,14 +100,16 @@ Fixpoint max_reg_cfi (m : positive) (i : cf_instr) := Definition regset := Regmap.t val. Definition predset := PMap.t bool. -Fixpoint eval_predf (pr: predset) (p: pred_op) {struct p} := - match p with - | Pvar (b, p') => if b then PMap.get p' pr else negb (PMap.get p' pr) - | Ptrue => true - | Pfalse => false - | Pand p' p'' => (eval_predf pr p') && (eval_predf pr p'') - | Por p' p'' => (eval_predf pr p') || (eval_predf pr p'') - end. +Definition eval_predf (pr: predset) (p: pred_op) := + sat_predicate p (fun x => pr !! (Pos.of_nat x)). + +#[global] +Instance eval_predf_Proper : Proper (eq ==> equiv ==> eq) eval_predf. +Proof. + unfold Proper. simplify. unfold "==>". + intros. + unfold sat_equiv in *. intros. unfold eval_predf. subst. apply H0. +Qed. Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset := match rl, vl with |