Library Machine
Require Import List TheoryList Wf.
Require Import ListUtil.
Set Implicit Arguments.
Section reachable.
Variables instruction state : Set.
Variable program : list instruction.
Variable pc : state -> nat.
Variable exec : instruction -> state -> state.
Inductive reachable : state -> state -> Prop :=
| R_Done : forall s, reachable s s
| R_Step : forall s s' i,
nth_spec program (pc s) i
-> reachable (exec i s) s'
-> reachable s s'.
Inductive reachable_flowInsensitive : state -> state -> Prop :=
| Rfi_Done : forall s, reachable_flowInsensitive s s
| Rfi_Step : forall s s' i,
In i program
-> reachable_flowInsensitive (exec i s) s'
-> reachable_flowInsensitive s s'.
Hint Constructors reachable_flowInsensitive.
Theorem flowInsensitive_is_conservative :
forall s s', reachable s s'
-> reachable_flowInsensitive s s'.
Section approx.
Variable approx : state -> state -> Prop.
Variable approxStrict : state -> state -> Prop.
Hypothesis approx_refl : forall s,
approx s s.
Hypothesis approx_trans : forall s1 s2 s3,
approx s1 s2
-> approx s2 s3
-> approx s1 s3.
Hypothesis increasing : forall s ins,
approx s (exec ins s).
Hypothesis monotonic : forall s1 s2 ins,
approx s1 s2
-> approx (exec ins s1) (exec ins s2).
Section fixed_point.
Variable fp : state.
Hypothesis fp_ok : forall ins,
In ins program
-> approx (exec ins fp) fp.
Theorem fixed_point_ok : forall s,
approx s fp
-> forall s', reachable_flowInsensitive s s'
-> approx s' fp.
End fixed_point.
Hypothesis approxStrict_approx : forall s1 s2,
approx s2 s1
-> ~approxStrict s1 s2
-> approx s1 s2.
Hypothesis approxStrict_trans : forall s1 s2 s3,
approx s2 s1
-> approxStrict s2 s3
-> approxStrict s1 s3.
Variable approxStrict_dec : forall x y, {approxStrict x y} + {~approxStrict x y}.
Hypothesis approxStrict_wf : well_founded approxStrict.
Variable init : state.
Hypothesis init_low : forall s, approx init s.
Lemma iterate_approx : forall prog s,
approx s (fold_left (fun s ins => exec ins s) prog s).
Hint Resolve iterate_approx.
Lemma iterate_pick' : forall ins prog s s',
In ins prog
-> approx s s'
-> approxStrict (exec ins s) s
-> approxStrict
(fold_left (fun st ins => exec ins st)
prog s') s.
Lemma iterate_pick_cp : forall ins s,
In ins program
-> approxStrict (exec ins s) s
-> approxStrict
(fold_left (fun st ins => exec ins st)
program s) s.
Lemma iterate_pick : forall ins s,
In ins program
-> ~approxStrict
(fold_left (fun st ins => exec ins st)
program s) s
-> ~approxStrict (exec ins s) s.
Definition iterate : {fp : state
| approx init fp
/\ forall ins,
In ins program
-> approx (exec ins fp) fp}.
Definition fixed_point : {fp : state
| forall s, reachable_flowInsensitive init s
-> approx s fp}.
End approx.
End reachable.
Index
This page has been generated by coqdoc