diff options
Diffstat (limited to 'src/array/Array_checker.v')
| -rw-r--r-- | src/array/Array_checker.v | 83 |
1 files changed, 73 insertions, 10 deletions
diff --git a/src/array/Array_checker.v b/src/array/Array_checker.v index da0f6f2..5bf0eaa 100644 --- a/src/array/Array_checker.v +++ b/src/array/Array_checker.v @@ -380,8 +380,11 @@ Section certif. rewrite H6d1, H6d2, H14. intros. - specialize (Atom.Bval_inj2 t_i (Typ.TFArray t0 t) - (store v_val2 v_val3 v_val4) (v_val0)). + specialize (Atom.Bval_inj2 t_i (Typ.TFArray t0 t) + (@store _ _ + (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i t0))) + _ _ _ (Typ.comp_interp t_i t) _ + v_val2 v_val3 v_val4) v_val0). intros. specialize (H18 H6). rewrite <- H18. @@ -397,7 +400,8 @@ Section certif. intros. specialize (H20 Htia2). rewrite <- H20. apply Typ.i_eqb_spec. - apply (read_over_write (elt_dec:=(EqbToDecType _ (@Eqb _ _)))). + apply (read_over_write (elt_dec:=(@EqbToDecType _ (@Eqb _ + (projT2 (Typ.interp_compdec_aux t_i _)))))). Qed. @@ -677,9 +681,12 @@ Section certif. rewrite H25a, H25b, H10. intros. specialize (Atom.Bval_inj2 t_i (Typ.TFArray t1 t2) - (store v_vale1 v_vale2 v_vale3) (v_vald1')). + (@store _ _ + (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i t1))) + _ _ _ (Typ.comp_interp t_i t2) _ + v_vale1 v_vale2 v_vale3) (v_vald1')). intro H25. specialize (H25 Htid1'). - + unfold Atom.interp_form_hatom, interp_hatom. rewrite !Atom.t_interp_wf; trivial. rewrite Heq6. simpl. @@ -725,7 +732,7 @@ Section certif. subst; intros; rewrite Htid2 in Htic2; - rewrite <- (Atom.Bval_inj2 _ _ (v_vald2) (v_valc2) Htic2) in *. + rewrite <- (Atom.Bval_inj2 _ _ (v_vald2) (v_valc2) Htic2) in *. + rewrite Htie2 in Htia1. rewrite Htia2 in Htic2''. @@ -831,7 +838,10 @@ Section certif. rewrite H25a, H25b, H10. intros. specialize (Atom.Bval_inj2 t_i (Typ.TFArray t1 t2) - (store v_vale1 v_vale2 v_vale3) (v_valc1')). + (@store _ _ + (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i t1))) + _ _ _ (Typ.comp_interp t_i t2) _ + v_vale1 v_vale2 v_vale3) (v_valc1')). intro H25. specialize (H25 Htic1'). unfold Atom.interp_form_hatom, interp_hatom. @@ -878,7 +888,7 @@ Section certif. subst; intros; rewrite Htid2 in Htic2; - rewrite <- (Atom.Bval_inj2 _ _ (v_vald2) (v_valc2) Htic2) in *. + rewrite <- (Atom.Bval_inj2 _ _ (v_vald2) (v_valc2) Htic2) in *. + rewrite Htie2 in Htia1. rewrite Htia2 in Htic2''. @@ -1169,7 +1179,10 @@ Section certif. unfold Bval. rewrite <- H25. rewrite !Typ.cast_refl. intros. - specialize (Atom.Bval_inj2 t_i t0 (diff v_valf1 v_valf2) (v_vald2')). + specialize (Atom.Bval_inj2 t_i t0 (@diff _ _ + (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i t0))) + _ _ (Typ.dec_interp t_i v_typec2') _ (Typ.comp_interp t_i v_typec2') (Typ.inh_interp t_i t0) _ + v_valf1 v_valf2) (v_vald2')). intros. specialize (H29 Htid2'). (* semantics *) @@ -1212,7 +1225,57 @@ Section certif. apply negb_true_iff. apply Typ.i_eqb_spec_false. subst. - specialize (Atom.Bval_inj2 t_i v_typed2' (v_vald2) (diff v_valf1 v_valf2)). + specialize (Atom.Bval_inj2 t_i v_typed2' (v_vald2) (@diff (Typ.interp t_i v_typed2') (Typ.interp t_i v_typec1') + (@EqbToDecType + _ + (@eqbtype_of_compdec + _ + (Typ.interp_compdec t_i v_typed2'))) + _ + (@comp_of_compdec (Typ.interp t_i v_typed2') + (projT2 + ((fix interp_compdec_aux (t : Typ.type) : + @sigT Type (fun ty : Type => CompDec ty) := + match t return (@sigT Type (fun ty : Type => CompDec ty)) with + | Typ.TFArray ti te => + @existT Type (fun ty : Type => CompDec ty) + (@farray + (@projT1 Type (fun ty : Type => CompDec ty) (interp_compdec_aux ti)) + (@projT1 Type (fun ty : Type => CompDec ty) (interp_compdec_aux te)) + (@ord_of_compdec + (@projT1 Type (fun ty : Type => CompDec ty) + (interp_compdec_aux ti)) + (@projT2 Type (fun ty : Type => CompDec ty) + (interp_compdec_aux ti))) + (@inh_of_compdec + (@projT1 Type (fun ty : Type => CompDec ty) + (interp_compdec_aux te)) + (@projT2 Type (fun ty : Type => CompDec ty) + (interp_compdec_aux te)))) + (@SMT_classes_instances.FArray_compdec + (@projT1 Type (fun ty : Type => CompDec ty) (interp_compdec_aux ti)) + (@projT1 Type (fun ty : Type => CompDec ty) (interp_compdec_aux te)) + (@projT2 Type (fun ty : Type => CompDec ty) (interp_compdec_aux ti)) + (@projT2 Type (fun ty : Type => CompDec ty) (interp_compdec_aux te))) + | Typ.Tindex i => + @existT Type (fun ty : Type => CompDec ty) + (te_carrier (@get typ_compdec t_i i)) + (te_compdec (@get typ_compdec t_i i)) + | Typ.TZ => + @existT Type (fun ty : Type => CompDec ty) BinNums.Z + SMT_classes_instances.Z_compdec + | Typ.Tbool => + @existT Type (fun ty : Type => CompDec ty) bool + SMT_classes_instances.bool_compdec + | Typ.Tpositive => + @existT Type (fun ty : Type => CompDec ty) BinNums.positive + SMT_classes_instances.Positive_compdec + | Typ.TBV n => + @existT Type (fun ty : Type => CompDec ty) + (BVList.BITVECTOR_LIST.bitvector n) (SMT_classes_instances.BV_compdec n) + end) v_typed2'))) (Typ.dec_interp t_i v_typec1') + _ (Typ.comp_interp t_i v_typec1') + (Typ.inh_interp t_i v_typed2') (Typ.inh_interp t_i v_typec1') v_valf1 v_valf2)). intros. specialize (H5 Htid2'''). rewrite <- H5. specialize (Atom.Bval_inj2 t_i v_typed2' (v_vale2) (v_vald2)). |