Skip to content

Commit

Permalink
Factor ZRange Proper proof (mit-plv#1764)
Browse files Browse the repository at this point in the history 
For mit-plv#1761
  • Loading branch information
@JasonGross
JasonGross committed Dec 4, 2023
1 parent 6389e4b commit 2974901
Show file tree
Hide file tree
Showing 2 changed files with 67 additions and 33 deletions.
37 changes: 4 additions & 33 deletions src/AbstractInterpretation/Wf.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,14 +25,17 @@ Require Import Rewriter.Language.Inversion.
Require Import Crypto.Language.InversionExtra.
Require Import Rewriter.Language.Wf.
Require Import Rewriter.Language.UnderLetsProofs.
Require Import Rewriter.Util.Decidable.
Require Import Crypto.AbstractInterpretation.AbstractInterpretation.
Require Import Crypto.AbstractInterpretation.ZRangeCommonProofs.
Import Coq.Lists.List.

Import EqNotations.
Module Compilers.
Import Language.Compilers.
Import UnderLets.Compilers.
Import AbstractInterpretation.Compilers.
Import AbstractInterpretation.ZRangeCommonProofs.Compilers.
Import Language.Inversion.Compilers.
Import Language.InversionExtra.Compilers.
Import Language.Wf.Compilers.
Expand Down Expand Up @@ -852,39 +855,7 @@ Module Compilers.

Global Instance abstract_interp_ident_Proper {opts : AbstractInterpretation.Options} {assume_cast_truncates : bool} {t}
: Proper (eq ==> @abstract_domain_R t) (abstract_interp_ident assume_cast_truncates t).
Proof using Type.
cbv [abstract_interp_ident abstract_domain_R type.related respectful type.interp]; intros idc idc' ?; subst idc'; destruct idc;
repeat first [ reflexivity
| progress subst
| progress cbn [ZRange.type.base.option.interp ZRange.type.base.interp base.interp base.base_interp Crypto.Util.Option.bind] in *
| progress cbv [Crypto.Util.Option.bind]
| intro
| progress destruct_head'_prod
| progress destruct_head'_bool
| progress destruct_head' option
| progress inversion_option
| discriminate
| solve [ eauto ]
| apply NatUtil.nat_rect_Proper_nondep
| apply ListUtil.list_rect_Proper
| apply ListUtil.list_rect_arrow_Proper
| apply ListUtil.list_case_Proper
| apply ListUtil.pointwise_map
| apply ListUtil.fold_right_Proper
| apply ListUtil.update_nth_Proper
| apply (@nat_rect_Proper_nondep_gen (_ -> _) (eq ==> eq)%signature)
| cbn; apply (f_equal (@Some _))
| progress cbn [ZRange.ident.option.interp]
| progress cbv [zrange_rect]
| apply (f_equal2 pair)
| break_innermost_match_step
| match goal with
| [ H : _ |- _ ] => erewrite H by (eauto; (eassumption || reflexivity))
| [ H : forall x y, x = y -> _ |- _ ] => specialize (fun x => H x x eq_refl)
| [ H : forall x, ?f x = ?g x, H1 : ?f ?y = _, H2 : ?g ?y = _ |- _ ]
=> specialize (H y); rewrite H1, H2 in H
end ].
Qed.
Proof using Type. apply ZRange.ident.option.interp_Proper. Qed.

Global Instance extract_list_state_Proper {t}
: Proper (abstract_domain'_R _ ==> option_eq (SetoidList.eqlistA (@abstract_domain'_R t)))
Expand Down
63 changes: 63 additions & 0 deletions src/AbstractInterpretation/ZRangeCommonProofs.v
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,63 @@
(* Proofs shared by Wf and Proofs *)
Require Import Coq.Classes.Morphisms.
Require Import Coq.Relations.Relations.
Require Import Crypto.Util.ZRange.
Require Import Crypto.Util.Option.
Require Import Crypto.Util.ListUtil.
Require Import Crypto.Util.ListUtil.FoldBool.
Require Import Crypto.Util.NatUtil.
Require Import Crypto.Util.ZUtil.Morphisms.
Require Import Crypto.Util.Tactics.BreakMatch.
Require Import Crypto.Util.Tactics.DestructHead.
Require Import Crypto.AbstractInterpretation.ZRange.

Module Compilers.
Import AbstractInterpretation.ZRange.Compilers.
Export ZRange.Settings.

Module ZRange.
Module ident.
Module option.
Section interp_related.
Context {shiftr_avoid_uint1 : shiftr_avoid_uint1_opt}
(assume_cast_truncates : bool).
Global Instance interp_Proper {t} : Proper (eq ==> @type.eqv t) (ZRange.ident.option.interp assume_cast_truncates).
Proof using Type.
intros idc idc' ?; subst idc'.
cbv [type.related respectful type.interp]; destruct idc;
repeat first [ reflexivity
| progress subst
| progress cbn [ZRange.type.base.option.interp ZRange.type.base.interp base.interp base.base_interp Crypto.Util.Option.bind] in *
| progress cbv [Crypto.Util.Option.bind]
| intro
| progress destruct_head'_prod
| progress destruct_head'_bool
| progress destruct_head' option
| progress inversion_option
| discriminate
| solve [ eauto ]
| apply NatUtil.nat_rect_Proper_nondep
| apply ListUtil.list_rect_Proper
| apply ListUtil.list_rect_arrow_Proper
| apply ListUtil.list_case_Proper
| apply ListUtil.pointwise_map
| apply ListUtil.fold_right_Proper
| apply ListUtil.update_nth_Proper
| apply (@nat_rect_Proper_nondep_gen (_ -> _) (eq ==> eq)%signature)
| cbn; apply (f_equal (@Some _))
| progress cbn [ZRange.ident.option.interp]
| progress cbv [zrange_rect]
| apply (f_equal2 pair)
| break_innermost_match_step
| match goal with
| [ H : _ |- _ ] => erewrite H by (eauto; (eassumption || reflexivity))
| [ H : forall x y, x = y -> _ |- _ ] => specialize (fun x => H x x eq_refl)
| [ H : forall x, ?f x = ?g x, H1 : ?f ?y = _, H2 : ?g ?y = _ |- _ ]
=> specialize (H y); rewrite H1, H2 in H
end ].
Qed.
End interp_related.
End option.
End ident.
End ZRange.
End Compilers.

0 comments on commit 2974901

Please sign in to comment.