| A proof that Flat programs can't detect sound heap re-orderings |
Require Import Arith List.
Require Import Max.
Require Import LambdaTamer.ListUtil.
Require Import LambdaTamer.LambdaTamer.
Require Import CTPC.AllocMonad.
Require Import CTPC.Trace.
Require Import CTPC.Dict.
Require Import CTPC.Alloc.
Require Import CTPC.Flat.
Set Implicit Arguments.
A characterization of programs with in-bounds slot accesses |
Section bounded.
Variable bound : list nat.
Fixpoint fargs_bounded tp ts (args : fargs tp ts) {struct args} : Prop :=
match args with
| FANil _ => True
| FACons _ _ sl args' => In sl bound /\ fargs_bounded args'
end.
Definition fprimop_bounded tp t (op : fprimop tp t) : Prop :=
match op with
| FSlot _ sl => In sl bound
| FConst _ _ => True
| FCodeptr _ _ _ => True
| FNew _ _ args => fargs_bounded args
| FProj _ _ sl _ _ => In sl bound
end.
End bounded.
Fixpoint flinear_bounded (bound : list nat) tp (lin : flinear tp) {struct lin} : Prop :=
match lin with
| FJump _ args sl _ _ =>
(forall n, n < length args -> In n bound)
/\ In sl bound
| FSet _ sl _ op lin =>
fprimop_bounded bound op
/\ flinear_bounded (sl :: bound) lin
end.
What it means for two heaps to be isomorphic with respect to two roots |
Section validPath.
Variable m : mem adom.
Fixpoint validPath (ptr : nat) (fnums : list nat) {struct fnums} : Prop :=
match fnums with
| nil => True
| fnum :: fnums' =>
match nth_error m ptr with
| None => False
| Some fds =>
match nth_error fds fnum with
| None => True
| Some (Untraced, _) => True
| Some (Traced, ptr') => validPath ptr' fnums'
end
end
end.
End validPath.
Section isomorphic_heaps.
Variables m1 m2 : mem adom.
Fixpoint followPath (ptr1 ptr2 : nat) (fnums : list nat) {struct fnums} : Prop :=
match fnums with
| nil => True
| fnum :: fnums' =>
match nth_error m1 ptr1, nth_error m2 ptr2 with
| None, None => True
| Some fds1, Some fds2 =>
match nth_error fds1 fnum, nth_error fds2 fnum with
| None, None => True
| Some (Untraced, v1), Some (Untraced, v2) => v1 = v2
| Some (Traced, ptr1'), Some (Traced, ptr2') => followPath ptr1' ptr2' fnums'
| _, _ => False
end
| _, _ => False
end
end.
Definition isomorphic_pointers (ptr1 ptr2 : nat) :=
forall fnums, validPath m1 ptr1 fnums
/\ validPath m2 ptr2 fnums
/\ followPath ptr1 ptr2 fnums.
Definition isomorphic_values (t : aty) (v1 v2 : nat) : Prop :=
match t with
| ARef => isomorphic_pointers v1 v2
| _ => v1 = v2
end.
Definition isomorphic_slots (bound : list nat) (tp : ftyping) (sls1 sls2 : slots) : Prop :=
forall n, In n bound
-> isomorphic_values (NatDict.sel tp n)
(NatDict.sel sls1 n) (NatDict.sel sls2 n).
Theorem isomorphic_slots_mono : forall (bound1 : list nat) (tp : ftyping) (sls1 sls2 : slots),
isomorphic_slots bound1 tp sls1 sls2
-> forall bound2, incl bound2 bound1
-> isomorphic_slots bound2 tp sls1 sls2.
Definition isomorphic_args (ts : atys) (args1 args2 : list adom) : Prop :=
forall n,
match nth_error ts n with
| None =>
match nth_error args1 n, nth_error args2 n with
| None, None => True
| _, _ => False
end
| Some t =>
match nth_error args1 n, nth_error args2 n with
| Some (tg1, arg1), Some (tg2, arg2) =>
tg1 = tagof t /\ tg2 = tagof t
/\ isomorphic_values t arg1 arg2
| _, _ => False
end
end.
Theorem fargs_safe : forall bound (sls1 sls2 : slots) tp ts (e : fargs tp ts),
isomorphic_slots bound tp sls1 sls2
-> fargs_bounded bound e
-> isomorphic_args ts (fargsDenote e sls1) (fargsDenote e sls2).
End isomorphic_heaps.
Hint Resolve nth_error_monotone.
Ltac caseEq e := generalize (refl_equal e); pattern e at -1; case e.
Theorem validPath_monotone : forall m fnums v,
validPath m v fnums
-> forall m',
validPath (m ++ m') v fnums.
Hint Resolve validPath_monotone.
Theorem followPath_monotone : forall m1 m2 fnums v1 v2,
validPath m1 v1 fnums
-> validPath m2 v2 fnums
-> followPath m1 m2 v1 v2 fnums
-> forall m1' m2',
followPath (m1 ++ m1') (m2 ++ m2') v1 v2 fnums.
Hint Resolve followPath_monotone.
Theorem isomorphic_pointers_monotone : forall m1 m2 v1 v2,
isomorphic_pointers m1 m2 v1 v2
-> forall m1' m2',
isomorphic_pointers (m1 ++ m1') (m2 ++ m2') v1 v2.
Hint Resolve isomorphic_pointers_monotone.
Theorem isomorphic_values_monotone : forall m1 m2 t v1 v2,
isomorphic_values m1 m2 t v1 v2
-> forall m1' m2',
isomorphic_values (m1 ++ m1') (m2 ++ m2') t v1 v2.
Hint Resolve isomorphic_values_monotone.
Theorem isomorphic_slots_monotone : forall bound m1 m2 tp sls1 sls2,
isomorphic_slots m1 m2 bound tp sls1 sls2
-> forall m1' m2',
isomorphic_slots (m1 ++ m1') (m2 ++ m2') bound tp sls1 sls2.
Hint Resolve isomorphic_slots_monotone.
More safety results |
Lemma isomorphic_new : forall m1 m2 ts args1 args2,
isomorphic_args m1 m2 ts args1 args2
-> isomorphic_pointers (m1 ++ args1 :: nil) (m2 ++ args2 :: nil)
(length m1) (length m2).
Hint Resolve isomorphic_new fargs_safe.
Ltac rewriter :=
repeat match goal with
| [ H : _ |- _ ] => rewrite H
end.
Theorem fprimop_safe : forall tp t (op : fprimop tp t)
(m1 m2 : mem adom) bound (sls1 sls2 : slots),
isomorphic_slots m1 m2 bound tp sls1 sls2
-> fprimop_bounded bound op
-> match fprimopDenote op sls1 m1, fprimopDenote op sls2 m2 with
| None, None => True
| Some (m1', v1), Some (m2', v2) =>
isomorphic_slots m1' m2' bound tp sls1 sls2
/\ isomorphic_values m1' m2' t v1 v2
| _, _ => False
end.
Fixpoint init_bound (n : nat) : list nat :=
match n with
| O => nil
| S n' => n' :: init_bound n'
end.
Theorem init_bound_incl : forall m bound,
(forall n, n < m -> In n bound)
-> incl (init_bound m) bound.
Hint Resolve init_bound_incl.
Theorem flinear_safe : forall tp (lin : flinear tp)
(m1 m2 : mem adom) bound (sls1 sls2 : slots),
isomorphic_slots m1 m2 bound tp sls1 sls2
-> flinear_bounded bound lin
-> match flinearDenote lin sls1 m1, flinearDenote lin sls2 m2 with
| None, None => True
| Some (m1', (pc1, argsT1, sls'1)), Some (m2', (pc2, argsT2, sls'2)) =>
exists tp',
isomorphic_slots m1' m2' (init_bound (length argsT1)) tp' sls'1 sls'2
/\ pc1 = pc2
/\ argsT1 = argsT2
/\ fprecondition tp' argsT1
| _, _ => False
end.
Lemma flatContext_sel'' : forall argsT t argsT',
NatDict.sel (flatContext (argsT ++ t :: argsT')) (length argsT') = t.
Lemma flatContext_sel' : forall argsT t argsT',
NatDict.sel (flatContext (argsT +++ t :: argsT')) (length argsT') = t.
Theorem flatContext_sel : forall argsT argsT' n t,
nth_error argsT n = Some t
-> NatDict.sel (flatContext (argsT +++ argsT')) (length argsT' + n) = t.
Theorem nth_error_total : forall (argsT : list aty) n,
n < length argsT
-> exists t, nth_error argsT n = Some t.
Theorem In_init_bound : forall m n,
In n (init_bound m)
-> n < m.
Theorem precondition_safe : forall tp argsT m1 m2 sls1 sls2,
fprecondition tp argsT
-> isomorphic_slots m1 m2 (init_bound (length argsT)) tp sls1 sls2
-> isomorphic_slots m1 m2 (init_bound (length argsT)) (flatContext (argsT +++ nil)) sls1 sls2.
Theorem flatContext_inj : forall ts1 ts2,
flatContext ts1 = flatContext ts2
-> ts1 = ts2.
Theorem revApp_inj : forall (ls1 : list aty) ls2 ls'1 ls'2,
ls1 +++ ls'1 = ls2 +++ ls'2
-> length ls'1 = length ls'2
-> ls1 = ls2 /\ ls'1 = ls'2.
Theorem flatContext_revApp_inj : forall ts1 ts2,
flatContext (ts1 +++ nil) = flatContext (ts2 +++ nil)
-> ts1 = ts2.
Section Traces.
Variable G : ftyping.
Variable pr : fprog G.
Hypothesis funcs_bounded : forall pc sg,
nthI (fFuncs pr) pc = Some sg
-> exists argsT, projS1 sg = flatContext (argsT +++ nil)
/\ flinear_bounded (init_bound (length argsT)) (projS2 sg).
Theorem ftrace_safe' : forall tr output,
runTrace tr output
-> forall (m1 m2 : mem adom)
pc argsT (sls1 sls2 : slots) tp,
fprecondition tp argsT
-> isomorphic_slots m1 m2 (init_bound (length argsT)) tp sls1 sls2
-> tr = fmakeTrace pr m1 pc argsT sls1
-> fmakeTrace pr m1 pc argsT sls1 = fmakeTrace pr m2 pc argsT sls2.
Theorem ftrace_safe : forall (m1 m2 : mem adom)
pc argsT (sls1 sls2 : slots) tp,
fprecondition tp argsT
-> isomorphic_slots m1 m2 (init_bound (length argsT)) tp sls1 sls2
-> forall output,
runTrace (fmakeTrace pr m1 pc argsT sls1) output
-> fmakeTrace pr m1 pc argsT sls1 = fmakeTrace pr m2 pc argsT sls2.
Hypothesis body_bounded : exists argsT, G = flatContext (argsT +++ nil)
/\ flinear_bounded (init_bound (length argsT)) (fBody pr).
Theorem fprog_safe : forall argsT,
G = flatContext (argsT +++ nil)
-> (forall argsT', G = flatContext (argsT' +++ nil)
-> flinear_bounded (init_bound (length argsT')) (fBody pr))
-> forall m1 m2 sls1 sls2,
isomorphic_slots m1 m2 (init_bound (length argsT)) G sls1 sls2
-> forall output, runTrace (fprogDenote pr sls1 m1) output
-> fprogDenote pr sls1 m1 = fprogDenote pr sls2 m2.
End Traces.
Prove that Flatify generates well-bounded programs |
Require Import Eqdep.
Require Import CTPC.Flatify.
Theorem flatVar_bounded : forall G t (v : Var G t),
In (flatVar v) (init_bound (length G)).
Hint Resolve flatVar_bounded.
Theorem flatArgs_bounded : forall G ts (args : aargs G ts),
fargs_bounded (init_bound (length G)) (flatArgs args).
Hint Resolve flatArgs_bounded.
Theorem flatPrimop_bounded : forall G t (op : aprimop G t),
fprimop_bounded (init_bound (length G)) (flatPrimop op).
Hint Resolve flatPrimop_bounded.
Fixpoint stash_bound (ts : list aty) (start : nat) (bound : list nat) {struct ts} : list nat :=
match ts with
| nil => bound
| t :: ts' => start :: stash_bound ts' (S start) bound
end.
Theorem stash_bound_mono : forall (ts : list aty) (start : nat) (bound : list nat),
incl bound (stash_bound ts start bound).
Theorem stash_bounded : forall (tp : ftyping) (ts : list aty) (args : fargs tp ts) (start : nat)
(Hearly : args_early args start) (lin : flinear (stashType tp start ts)) bound,
flinear_bounded (stash_bound ts start bound) lin
-> fargs_bounded bound args
-> flinear_bounded bound (stash args _ Hearly lin).
Hint Resolve stash_bounded.
Fixpoint copy_bound (to from len : nat) (bound : list nat) {struct len} : list nat :=
match len with
| O => bound
| S len' => to :: copy_bound (S to) (S from) len' bound
end.
Theorem copy_bound_mono : forall (len to from : nat) (bound : list nat),
incl bound (copy_bound to from len bound).
Theorem copy_bounded : forall (len : nat) (tp : ftyping) (to from : nat)
(lin : flinear (copyType tp to from len)) bound,
(forall n, from <= n < from + len -> In n bound)
-> flinear_bounded (copy_bound to from len bound) lin
-> flinear_bounded bound (copy tp to from len lin).
Theorem stash_bound_has : forall (ts : list aty) (start : nat) (bound : list nat) n,
start <= n < start + length ts
-> In n (stash_bound ts start bound).
Hint Resolve stash_bound_has.
Theorem copy_bound_has : forall (len to from : nat) (bound : list nat) n,
to <= n < to + len
-> In n (copy_bound to from len bound).
Hint Resolve copy_bound_has.
Theorem frob_args_bounded : forall tp ts (args : fargs tp ts) a t
(Hearly : args_early args a) bound,
fargs_bounded bound args
-> fargs_bounded bound (frob_args args a t Hearly).
Hint Resolve frob_args_bounded.
Theorem fargs_bounded_mono : forall tp ts (args : fargs tp ts) bound,
fargs_bounded bound args
-> forall bound', fargs_bounded (bound' ++ bound) args.
Hint Resolve fargs_bounded_mono.
Theorem fargs_bounded_mono' : forall tp ts (args : fargs tp ts) bound,
fargs_bounded bound args
-> forall bound', fargs_bounded (bound' :: bound) args.
Hint Resolve fargs_bounded_mono'.
Theorem flatLinear_bounded : forall G t (lin : alinear G t),
flinear_bounded (init_bound (length G)) (flatLinear lin).
Hint Resolve flatLinear_bounded.
Theorem flatFunc_bounded : forall G ts (f : afunc G ts),
flinear_bounded (init_bound (length (ts +++ G))) (flatFunc f).
Hint Resolve flatFunc_bounded.
Section mapI.
Variable A : Set.
Variable B : A -> Set.
Variable A' : Set.
Variable f : A -> A'.
Variable B' : A' -> Set.
Variable g : forall x, B x -> B' (f x).
Theorem nthI_mapI' : forall (ts : list A) (ls : listI B ts) n sg,
nthI (A:= A') (mapI g ls) n = value sg
-> exists v, nthI ls n = value v
/\ projS1 sg = f (projS1 v)
/\ forall (Heq : projS1 sg = f (projS1 v)),
eq_rec _ _ (projS2 sg) _ Heq = g (projS2 v).
End mapI.
Theorem flatProg_funcs_bounded : forall (G : list aty) (pr : aprog G) pc sg,
nthI (fFuncs (flatProg pr)) pc = Some sg
-> exists argsT, projS1 sg = flatContext (argsT +++ nil)
/\ flinear_bounded (init_bound (length argsT)) (projS2 sg).
Theorem flatProg_body_bounded : forall (G : list aty) (pr : aprog G),
exists argsT, flatContext (G +++ nil) = flatContext (argsT +++ nil)
/\ flinear_bounded (init_bound (length argsT)) (fBody (flatProg pr)).