pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-27 23:06:20 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Update AbstractInterpretation for newer Coq versions

Browse source
This commit is contained in:
Adam Chlipala 2022-02-06 13:13:29 -05:00
parent c2260bb22b
commit 22118d90be
1 changed files with 32 additions and 32 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

64
AbstractInterpretation.v
View file

@ -85,7 +85,7 @@ Definition absint_complete (a : absint) :=
-> a.(Represents) n z. -> a.(Represents) n z.
(* Let's ask [eauto] to try all of the above soundness rules automatically. *) (* Let's ask [eauto] to try all of the above soundness rules automatically. *)
Hint Resolve TopSound ConstSound AddSound SubtractSound MultiplySound Local Hint Resolve TopSound ConstSound AddSound SubtractSound MultiplySound
AddMonotone SubtractMonotone MultiplyMonotone AddMonotone SubtractMonotone MultiplyMonotone
JoinSoundLeft JoinSoundRight : core. JoinSoundLeft JoinSoundRight : core.
@ -155,7 +155,7 @@ Proof.
exists (x + 1); linear_arithmetic. exists (x + 1); linear_arithmetic.
Qed. Qed.
Hint Resolve isEven_0 isEven_1 isEven_S_Even isEven_S_Odd : core. Local Hint Resolve isEven_0 isEven_1 isEven_S_Even isEven_S_Odd : core.
(* END SPAN OF BORING THEOREMS ABOUT PARITY. *) (* END SPAN OF BORING THEOREMS ABOUT PARITY. *)
@ -218,7 +218,7 @@ Inductive parity_rep : nat -> parity -> Prop :=
| PrEither : forall n, | PrEither : forall n,
parity_rep n Either. parity_rep n Either.
Hint Constructors parity_rep : core. Local Hint Constructors parity_rep : core.
(* Putting it all together: *) (* Putting it all together: *)
Definition parity_absint := {| Definition parity_absint := {|
@ -242,7 +242,7 @@ Proof.
invert IHn; eauto. invert IHn; eauto.
Qed. Qed.
Hint Resolve parity_const_sound : core. Local Hint Resolve parity_const_sound : core.
Lemma even_not_odd : Lemma even_not_odd :
(forall n, parity_rep n Even -> parity_rep n Odd) (forall n, parity_rep n Even -> parity_rep n Odd)
@ -270,7 +270,7 @@ Proof.
linear_arithmetic. linear_arithmetic.
Qed. Qed.
Hint Resolve even_not_odd odd_not_even : core. Local Hint Resolve even_not_odd odd_not_even : core.
Lemma parity_join_complete : forall n x y, Lemma parity_join_complete : forall n x y,
parity_rep n (parity_join x y) parity_rep n (parity_join x y)
@ -283,7 +283,7 @@ Proof.
propositional; eauto using odd_notEven. propositional; eauto using odd_notEven.
Qed. Qed.
Hint Resolve parity_join_complete : core. Local Hint Resolve parity_join_complete : core.
(* The final proof uses some automation that we won't explain, to descend down (* The final proof uses some automation that we won't explain, to descend down
* to the hearts of the interesting cases. *) * to the hearts of the interesting cases. *)
@ -446,7 +446,7 @@ Inductive flow_insensitive_step a (c : cmd) : astate a -> astate a -> Prop :=
(x, e) \in assignmentsOf c (x, e) \in assignmentsOf c
-> flow_insensitive_step c s (merge_astate s (s $+ (x, absint_interp e s))). -> flow_insensitive_step c s (merge_astate s (s $+ (x, absint_interp e s))).
Hint Constructors flow_insensitive_step : core. Local Hint Constructors flow_insensitive_step : core.
Definition flow_insensitive_trsys a (s : astate a) (c : cmd) := {| Definition flow_insensitive_trsys a (s : astate a) (c : cmd) := {|
Initial := {s}; Initial := {s};
@ -477,7 +477,7 @@ Inductive Rinsensitive a (c : cmd) : valuation * cmd -> astate a -> Prop :=
-> assignmentsOf c' \subseteq assignmentsOf c -> assignmentsOf c' \subseteq assignmentsOf c
-> Rinsensitive c (v, c') s. -> Rinsensitive c (v, c') s.
Hint Constructors Rinsensitive : core. Local Hint Constructors Rinsensitive : core.
(* A helpful decomposition property for compatibility *) (* A helpful decomposition property for compatibility *)
Lemma insensitive_compatible_add : forall a (s : astate a) v x na n, Lemma insensitive_compatible_add : forall a (s : astate a) v x na n,
@ -508,7 +508,7 @@ Proof.
eauto. eauto.
Qed. Qed.
Hint Resolve insensitive_compatible_add absint_interp_ok : core. Local Hint Resolve insensitive_compatible_add absint_interp_ok : core.
(* With that, let's show that the flow-insensitive version of a program (* With that, let's show that the flow-insensitive version of a program
* *simulates* the original program, w.r.t. any sound abstract * *simulates* the original program, w.r.t. any sound abstract
@ -598,7 +598,7 @@ Proof.
cases (s $? x); equality. cases (s $? x); equality.
Qed. Qed.
Hint Resolve subsumed_refl : core. Local Hint Resolve subsumed_refl : core.
Lemma subsumed_use : forall a (s s' : astate a) x n t0 t, Lemma subsumed_use : forall a (s s' : astate a) x n t0 t,
s $? x = Some t0 s $? x = Some t0
@ -626,7 +626,7 @@ Proof.
equality. equality.
Qed. Qed.
Hint Resolve subsumed_use subsumed_use_empty : core. Local Hint Resolve subsumed_use subsumed_use_empty : core.
Lemma subsumed_trans : forall a (s1 s2 s3 : astate a), Lemma subsumed_trans : forall a (s1 s2 s3 : astate a),
subsumed s1 s2 subsumed s1 s2
@ -651,7 +651,7 @@ Proof.
invert H0; eauto. invert H0; eauto.
Qed. Qed.
Hint Resolve subsumed_merge_left : core. Local Hint Resolve subsumed_merge_left : core.
Lemma subsumed_merge_both : forall a, absint_sound a Lemma subsumed_merge_both : forall a, absint_sound a
-> absint_complete a -> absint_complete a
@ -681,7 +681,7 @@ Proof.
specialize (H0 x0); eauto. specialize (H0 x0); eauto.
Qed. Qed.
Hint Resolve subsumed_add : core. Local Hint Resolve subsumed_add : core.
(* A key property of interpreting expressions abstractly: it's *monotone*, in (* A key property of interpreting expressions abstractly: it's *monotone*, in
* the sense that moving up to a less precise [astate] leads to a less precise * the sense that moving up to a less precise [astate] leads to a less precise
@ -698,7 +698,7 @@ Proof.
cases (s $? x); eauto. cases (s $? x); eauto.
Qed. Qed.
Hint Resolve absint_interp_monotone : core. Local Hint Resolve absint_interp_monotone : core.
(* [runAllAssignments] also respects the subsumption order, in going from inputs (* [runAllAssignments] also respects the subsumption order, in going from inputs
* to outputs. *) * to outputs. *)
@ -710,7 +710,7 @@ Proof.
induct 2; simplify; eauto using subsumed_trans. induct 2; simplify; eauto using subsumed_trans.
Qed. Qed.
Hint Resolve runAllAssignments_monotone : core. Local Hint Resolve runAllAssignments_monotone : core.
(* The output of [runAllAssignments] subsumes every state reachable by running a (* The output of [runAllAssignments] subsumes every state reachable by running a
* single command. *) * single command. *)
@ -971,7 +971,7 @@ Proof.
invert H1; eauto. invert H1; eauto.
Qed. Qed.
Hint Resolve compatible_add : core. Local Hint Resolve compatible_add : core.
(* A similar result follows about soundness of expression interpretation. *) (* A similar result follows about soundness of expression interpretation. *)
Theorem absint_interp_ok2 : forall a, absint_sound a Theorem absint_interp_ok2 : forall a, absint_sound a
@ -989,7 +989,7 @@ Proof.
assumption. assumption.
Qed. Qed.
Hint Resolve absint_interp_ok2 : core. Local Hint Resolve absint_interp_ok2 : core.
(* The new type of invariant we calculate as we go: a map from commands to (* The new type of invariant we calculate as we go: a map from commands to
* [astate]s. The idea is that we populate this map with the commands that show * [astate]s. The idea is that we populate this map with the commands that show
@ -1082,7 +1082,7 @@ Inductive abs_step a : astate a * cmd -> astate a * cmd -> Prop :=
-> ss $? c' = Some s' -> ss $? c' = Some s'
-> abs_step (s, c) (s', c'). -> abs_step (s, c) (s', c').
Hint Constructors abs_step : core. Local Hint Constructors abs_step : core.
Definition absint_trsys a (c : cmd) := {| Definition absint_trsys a (c : cmd) := {|
Initial := {($0, c)}; Initial := {($0, c)};
@ -1096,7 +1096,7 @@ Inductive Rabsint a : valuation * cmd -> astate a * cmd -> Prop :=
compatible s v compatible s v
-> Rabsint (v, c) (s, c). -> Rabsint (v, c) (s, c).
Hint Constructors abs_step Rabsint : core. Local Hint Constructors abs_step Rabsint : core.
Theorem absint_simulates : forall a v c, Theorem absint_simulates : forall a v c,
absint_sound a absint_sound a
@ -1166,7 +1166,7 @@ Proof.
unfold subsumeds; simplify; eauto. unfold subsumeds; simplify; eauto.
Qed. Qed.
Hint Resolve subsumeds_refl : core. Local Hint Resolve subsumeds_refl : core.
Lemma subsumeds_add : forall a (ss1 ss2 : astates a) c s1 s2, Lemma subsumeds_add : forall a (ss1 ss2 : astates a) c s1 s2,
subsumeds ss1 ss2 subsumeds ss1 ss2
@ -1178,7 +1178,7 @@ Proof.
invert H1; eauto. invert H1; eauto.
Qed. Qed.
Hint Resolve subsumeds_add : core. Local Hint Resolve subsumeds_add : core.
Lemma subsumeds_empty : forall a (ss : astates a), Lemma subsumeds_empty : forall a (ss : astates a),
subsumeds $0 ss. subsumeds $0 ss.
@ -1389,7 +1389,7 @@ Proof.
simplify; cases y; equality. simplify; cases y; equality.
Qed. Qed.
Hint Resolve merge_astates_fok_parity merge_astates_fok2_parity : core. Local Hint Resolve merge_astates_fok_parity merge_astates_fok2_parity : core.
(* Our second corral of tactics for the day, automating iteration *) (* Our second corral of tactics for the day, automating iteration *)
Ltac interpret_simpl := unfold merge_astates, merge_astate; Ltac interpret_simpl := unfold merge_astates, merge_astate;
@ -1590,7 +1590,7 @@ Record interval_rep (n : nat) (i : interval) : Prop := {
end end
}. }.
Hint Constructors interval_rep : core. Local Hint Constructors interval_rep : core.
(* Test if an interval contains any values. *) (* Test if an interval contains any values. *)
Definition impossible (x : interval) := Definition impossible (x : interval) :=
@ -1653,7 +1653,7 @@ Proof.
rewrite H, H0; equality. rewrite H, H0; equality.
Qed. Qed.
Hint Rewrite interval_join_impossible1 interval_join_impossible2 interval_join_possible Local Hint Rewrite interval_join_impossible1 interval_join_impossible2 interval_join_possible
using assumption. using assumption.
(* We'll reuse this function to define both addition and multiplication. (* We'll reuse this function to define both addition and multiplication.
@ -1705,7 +1705,7 @@ Proof.
cases (impossible y); simplify; equality. cases (impossible y); simplify; equality.
Qed. Qed.
Hint Rewrite interval_combine_possible_fwd using assumption. Local Hint Rewrite interval_combine_possible_fwd using assumption.
Definition interval_subtract (x y : interval) := Definition interval_subtract (x y : interval) :=
if impossible x || impossible y then if impossible x || impossible y then
@ -1747,7 +1747,7 @@ Proof.
cases (impossible y); simplify; equality. cases (impossible y); simplify; equality.
Qed. Qed.
Hint Rewrite interval_subtract_possible_fwd using assumption. Local Hint Rewrite interval_subtract_possible_fwd using assumption.
Definition interval_absint := {| Definition interval_absint := {|
Top := {| Lower := 0; Upper := None |}; Top := {| Lower := 0; Upper := None |};
@ -1760,7 +1760,7 @@ Definition interval_absint := {|
Represents := interval_rep Represents := interval_rep
|}. |}.
Hint Resolve mult_le_compat : core. (* Theorem from Coq standard library *) Local Hint Resolve mult_le_compat : core. (* Theorem from Coq standard library *)
(* When one interval implies another, and the first is possible, we can deduce (* When one interval implies another, and the first is possible, we can deduce
* arithmetic relationships betwen their respective bounds. *) * arithmetic relationships betwen their respective bounds. *)
@ -1859,7 +1859,7 @@ Proof.
transitivity (a' * b'); eauto. transitivity (a' * b'); eauto.
Qed. Qed.
Hint Immediate mult_bound1 mult_bound2 : core. Local Hint Immediate mult_bound1 mult_bound2 : core.
(* Now a bruiser of an automated proof, covering all the cases to show that this (* Now a bruiser of an automated proof, covering all the cases to show that this
* abstraction is sound. *) * abstraction is sound. *)
@ -1914,7 +1914,7 @@ Proof.
simplify; cases y; equality. simplify; cases y; equality.
Qed. Qed.
Hint Resolve merge_astates_fok_interval merge_astates_fok2_interval : core. Local Hint Resolve merge_astates_fok_interval merge_astates_fok2_interval : core.
(* The same kind of lemma we've proved for finishing off each proof by abstract (* The same kind of lemma we've proved for finishing off each proof by abstract
* interpretation so far *) * interpretation so far *)
@ -1937,7 +1937,7 @@ Proof.
equality. equality.
Qed. Qed.
Hint Rewrite min_l min_r max_l max_r using linear_arithmetic. Local Hint Rewrite min_l min_r max_l max_r using linear_arithmetic.
(* Let's see which intervals are computed for this program. *) (* Let's see which intervals are computed for this program. *)
Definition interval_test := Definition interval_test :=
@ -2047,7 +2047,7 @@ Proof.
rewrite H, H0; equality. rewrite H, H0; equality.
Qed. Qed.
Hint Rewrite interval_widen_impossible1 interval_widen_impossible2 interval_widen_possible Local Hint Rewrite interval_widen_impossible1 interval_widen_impossible2 interval_widen_possible
using assumption. using assumption.
Definition interval_absint_widening := {| Definition interval_absint_widening := {|
@ -2109,7 +2109,7 @@ Proof.
simplify; cases y; equality. simplify; cases y; equality.
Qed. Qed.
Hint Resolve merge_astates_fok_interval_widening merge_astates_fok2_interval_widening : core. Local Hint Resolve merge_astates_fok_interval_widening merge_astates_fok2_interval_widening : core.
Lemma final_lower_widening : forall (s s' : astate interval_absint_widening) v x l, Lemma final_lower_widening : forall (s s' : astate interval_absint_widening) v x l,
compatible s v compatible s v