| Idealized assembly language |
Require Import Arith Eqdep List.
Require Import LambdaTamer.ListUtil.
Require Import CTPC.AllocMonad.
Require Import CTPC.Trace.
Require Import CTPC.Dict.
Require Import CTPC.Alloc.
Require Import CTPC.Flat.
Require Import CTPC.Safety.
Require Import CTPC.Asm.
Set Implicit Arguments.
Translation to assembly |
Fixpoint asmArgs tp ts (args : fargs tp ts) {struct args} : list nat :=
match args with
| FANil _ => nil
| FACons _ _ sl args' => sl :: asmArgs args'
end.
Definition asmPrimop tp t (op : fprimop tp t) (roots : list nat) : genop :=
match op with
| FSlot _ sl => Slot sl
| FConst _ n => Const n
| FCodeptr _ _ n => Const (S n)
| FNew _ _ args => New roots (asmArgs args)
| FProj _ _ sl _ n => Proj sl n
end.
Fixpoint remover (ls : list nat) (x : nat) {struct ls} : list nat :=
match ls with
| nil => nil
| y :: ls' =>
if eq_nat_dec x y
then remover ls' x
else y :: remover ls' x
end.
Definition updateRoots roots t sl :=
match t with
| ARef => sl :: roots
| _ => remover roots sl
end.
Fixpoint asmLinear tp (lin : flinear tp) (roots : list nat) {struct lin} : instrs :=
match lin with
| FJump _ _ sl _ _ => Jump sl
| FSet _ sl t op lin' =>
Assign sl (asmPrimop op roots) (asmLinear lin' (updateRoots roots t sl))
end.
Section mapI_list.
Variable A : Set.
Variable B : A -> Set.
Variable A' : Set.
Variable g : forall x, B x -> A'.
Fixpoint mapI_list (ts : list A) : listI B ts -> list A' :=
match ts return (listI B ts -> _) with
| nil => fun _ => nil
| _ :: _ => fun ls => g (headI ls) :: mapI_list _ (tailI ls)
end.
Theorem nth_mapI_list : forall (ts : list A) (ls : listI B ts) n v,
nthI ls n = value v
-> nth_error (mapI_list _ ls) n = value (g (projS2 v)).
End mapI_list.
Implicit Arguments mapI_list [A B A' ts].
Implicit Arguments nth_mapI_list [A B A' ts].
Fixpoint initRoots (tp : ftyping) (sls : list nat) {struct sls} : list nat :=
match sls with
| nil => nil
| sl :: sls' =>
match NatDict.sel tp sl with
| ARef => sl :: initRoots tp sls'
| _ => initRoots tp sls'
end
end.
Definition asmProg tp (pr : fprog tp) : program :=
Build_program
(mapI_list (fun tp lin => asmLinear lin (initRoots tp (NatDict.keys tp))) (fFuncs pr))
(asmLinear (fBody pr) (initRoots tp (NatDict.keys tp))).
Helpful safety lemmas |
Theorem followPath_refl : forall m fnums v,
validPath m v fnums
-> followPath m m v v fnums.
Hint Resolve followPath_refl.
Theorem isomorphic_pointers_refl : forall m v,
(forall fnums, validPath m v fnums)
-> isomorphic_pointers m m v v.
Hint Resolve isomorphic_pointers_refl.
Theorem isomorphic_slots_refl : forall m bound tp sls,
(forall n, In n bound
-> NatDict.sel tp n = ARef ->
forall fnums, validPath m (NatDict.sel sls n) fnums)
-> isomorphic_slots m m bound tp sls sls.
Hint Resolve isomorphic_slots_refl.
Section AllS2.
Variables A B : Set.
Variable f : A -> B -> Prop.
Theorem AllS2_len : forall (ls1 : list A) (ls2 : list B),
AllS2 f ls1 ls2
-> length ls1 = length ls2.
End AllS2.
Section list.
Variables A B : Set.
Variable f : A -> B.
Theorem map_length : forall ls, length (map f ls) = length ls.
End list.
Correctness |
Section correctness.
Variable rt : runtime.
Definition val_lr (m1 : mem adom) (t : aty) (v1 v2 : nat) : Prop :=
match t with
| ARef =>
(forall fnums, validPath m1 v1 fnums)
/\ ptrComp rt m1 v1 = v2
| _ => v1 = v2
end.
Definition slots_lr (bound : list nat) (m1 : mem adom) (tp : ftyping) (sls1 sls2 : slots) : Prop :=
forall n, In n bound
-> val_lr m1 (NatDict.sel tp n) (NatDict.sel sls1 n) (NatDict.sel sls2 n).
Theorem slots_lr_valid : forall (bound : list nat) (m1 : mem adom) (tp : ftyping) (sls1 sls2 : slots),
slots_lr bound m1 tp sls1 sls2
-> forall n, In n bound
-> NatDict.sel tp n = ARef ->
forall fnums, validPath m1 (NatDict.sel sls1 n) fnums.
Hint Resolve slots_lr_valid.
Fixpoint args_lr (m1 : mem adom) (ts : list aty) (args1 : list adom) (args2 : list nat) {struct ts} : Prop :=
match ts, args1, args2 with
| nil, nil, nil => True
| t :: ts', (tg, v1) :: args1', v2 :: args2' =>
tg = tagof t
/\ val_lr m1 t v1 v2
/\ args_lr m1 ts' args1' args2'
| _, _, _ => False
end.
Theorem asmArgs_sound : forall tp ts (args : fargs tp ts)
bound m1 sls1 sls2,
fargs_bounded bound args
-> slots_lr bound m1 tp sls1 sls2
-> args_lr m1 ts (fargsDenote args sls1) (argsDenote (asmArgs args) sls2).
Lemma roots_backup : forall G bound m1 sls1 sls2 roots,
incl roots bound
-> (forall n, In n roots -> NatDict.sel G n = ARef)
-> slots_lr bound m1 G sls1 sls2
-> argsDenote roots sls2 = map (ptrComp rt m1) (argsDenote roots sls1).
Lemma fields_backup : forall bound m1 sls1 sls2 tp ts (args : fargs tp ts),
fargs_bounded bound args
-> slots_lr bound m1 tp sls1 sls2
-> argsDenote (asmArgs args) sls2 = map (valComp (ptrComp rt m1)) (fargsDenote args sls1).
Fixpoint roots_grabber (want : nat) (roots vals : list nat) {struct roots} : nat :=
match roots, vals with
| root :: roots', val :: vals' =>
if eq_nat_dec want root
then val
else roots_grabber want roots' vals'
| _, _ => 0
end.
Theorem rootsIn_In : forall roots roots2 sls n,
In n roots
-> length roots2 = length roots
-> roots_grabber n roots roots2 = NatDict.sel (rootsIn sls roots roots2) n.
Lemma argsDenote_len : forall (e : list nat) (sls : slots),
length (argsDenote e sls) = length e.
Theorem rootsIn_notIn : forall n roots roots2 sls,
~In n roots
-> NatDict.sel (rootsIn sls roots roots2) n
= NatDict.sel sls n.
Ltac clear_all :=
repeat match goal with
| [ H : _ |- _ ] => clear H
end.
Lemma isomorphic_values_lr : forall bound m1 G sls1 sls2 sl,
slots_lr bound m1 G sls1 sls2
-> In sl bound
-> isomorphic_values m1 m1 (NatDict.sel G sl) (NatDict.sel sls1 sl) (NatDict.sel sls1 sl).
Hint Resolve isomorphic_values_lr.
Theorem asmPrimop_sound : forall tp t (op : fprimop tp t) (roots : list nat),
(forall n, ~In n roots -> NatDict.sel tp n <> ARef)
-> (forall n, In n roots -> NatDict.sel tp n = ARef)
-> forall bound m1 sls1 sls2, incl roots bound
-> slots_lr bound m1 tp sls1 sls2
-> fprimop_bounded bound op
-> match fprimopDenote op sls1 m1, genopDenote rt (asmPrimop op roots) sls2 (heapComp rt m1) with
| Some (m1', v1), (m2', sls2', v2) =>
exists m1'', exists sls1', exists v1',
isomorphic_slots m1' m1'' bound tp sls1 sls1'
/\ slots_lr bound m1'' tp sls1' sls2'
/\ isomorphic_values m1' m1'' t v1 v1'
/\ val_lr m1'' t v1' v2
/\ m2' = heapComp rt m1''
| _, _ => True
end.
Lemma remover_neq1 : forall n1 roots sl,
In n1 (remover roots sl)
-> sl <> n1
-> In n1 roots.
Hint Resolve remover_neq1.
Lemma remover_neq2 : forall n1 roots sl,
sl <> n1
-> In n1 roots
-> In n1 (remover roots sl).
Hint Resolve remover_neq2.
Lemma remover_neq2_cp : forall n1 roots sl,
sl <> n1
-> ~In n1 (remover roots sl)
-> ~In n1 roots.
Hint Resolve remover_neq2_cp.
Lemma remover_eq : forall n roots,
~In n (remover roots n).
Lemma remover_mono : forall a roots sl,
In a (remover roots sl)
-> In a roots.
Hint Resolve remover_mono.
Lemma followPath_trans : forall m1 m2 fnums v1 v2,
validPath m1 v1 fnums
-> validPath m2 v2 fnums
-> followPath m1 m2 v1 v2 fnums
-> forall m3 v3, validPath m3 v3 fnums
-> followPath m2 m3 v2 v3 fnums
-> followPath m1 m3 v1 v3 fnums.
Hint Resolve followPath_trans.
Lemma isomorphic_pointers_trans : forall m1 m2 v1 v2,
isomorphic_pointers m1 m2 v1 v2
-> forall m3 v3, isomorphic_pointers m2 m3 v2 v3
-> isomorphic_pointers m1 m3 v1 v3.
Hint Resolve isomorphic_pointers_trans.
Lemma isomorphic_values_trans : forall m1 m2 t v1 v2,
isomorphic_values m1 m2 t v1 v2
-> forall m3 v3, isomorphic_values m2 m3 t v2 v3
-> isomorphic_values m1 m3 t v1 v3.
Hint Resolve isomorphic_values_trans.
Lemma isomorphic_slots_trans : forall (bound : list nat) (tp : ftyping) m1 m2 sls1 sls2,
isomorphic_slots m1 m2 bound tp sls1 sls2
-> forall m3 sls3, isomorphic_slots m2 m3 bound tp sls2 sls3
-> isomorphic_slots m1 m3 bound tp sls1 sls3.
Hint Resolve isomorphic_slots_trans.
Lemma In_init_bound : forall m n,
In n (init_bound m)
-> n < m.
Hint Resolve In_init_bound.
Lemma isomorphic_slots_call : forall bound m1 G sls1 sls2 args tp',
slots_lr bound m1 G sls1 sls2
-> (forall n : nat, n < length args -> In n bound)
-> fprecondition G args
-> fprecondition tp' args
-> isomorphic_slots m1 m1 (init_bound (length args)) tp' sls1 sls1.
Hint Resolve isomorphic_slots_call.
Lemma slots_lr_call : forall m1 G sls1 sls2 args bound tp',
slots_lr bound m1 G sls1 sls2
-> (forall n : nat, n < length args -> In n bound)
-> fprecondition G args
-> fprecondition tp' args
-> slots_lr (init_bound (length args)) m1 tp' sls1 sls2.
Hint Resolve slots_lr_call.
Lemma isomorphic_slots_set : forall m0 m2 a0 tp' s s1 tp'0,
isomorphic_slots m0 m2 (init_bound (length a0)) tp' s s1
-> fprecondition tp' a0
-> fprecondition tp'0 a0
-> isomorphic_slots m0 m2 (init_bound (length a0)) tp'0 s s1.
Hint Resolve isomorphic_slots_set.
Theorem asmLinear_sound : forall tp (lin : flinear tp) (roots : list nat),
(forall n, ~In n roots -> NatDict.sel tp n <> ARef)
-> (forall n, In n roots -> NatDict.sel tp n = ARef)
-> forall bound m1 sls1 sls2, incl roots bound
-> slots_lr bound m1 tp sls1 sls2
-> flinear_bounded bound lin
-> match flinearDenote lin sls1 m1, instrsDenote rt (asmLinear lin roots) sls2 (heapComp rt m1) with
| Some (m1', (pc1, argsT, sls1')), (m2', pc2, sls2') =>
pc1 = pc2
/\ forall tp', fprecondition tp' argsT
-> exists m1'', exists sls1'',
isomorphic_slots m1' m1'' (init_bound (length argsT)) tp' sls1' sls1''
/\ slots_lr (init_bound (length argsT)) m1'' tp' sls1'' sls2'
/\ m2' = heapComp rt m1''
| _, _ => True
end.
Lemma initRoots_NotIn' : forall tp n bound,
~In n (initRoots tp bound)
-> In n bound
-> NatDict.sel tp n <> ARef.
Hint Resolve initRoots_NotIn'.
Lemma NotIn_init_bound : forall m n,
~In n (init_bound m)
-> n >= m.
Hint Resolve NotIn_init_bound.
Lemma flatContext_late : forall n ts,
n >= length ts
-> NatDict.sel (flatContext ts) n = ANat.
Lemma initRoots_NotIn : forall ts n,
~In n
(initRoots (flatContext (ts +++ nil))
(init_bound (length ts)))
-> NatDict.sel (flatContext (ts +++ nil)) n <> ARef.
Lemma initRoots_In' : forall tp n bound,
In n (initRoots tp bound)
-> NatDict.sel tp n = ARef.
Lemma initRoots_In : forall ts n,
In n
(initRoots (flatContext (ts +++ nil))
(init_bound (length ts)))
-> NatDict.sel (flatContext (ts +++ nil)) n = ARef.
Lemma initRoots_incl : forall tp bound,
incl (initRoots tp bound) bound.
Lemma keys_init : forall ts,
NatDict.keys (flatContext ts)
= init_bound (length ts).
Lemma length_revApp_nil : forall (ts : list aty),
length (ts +++ nil) = length ts.
Theorem flatContext_sel_direct : forall argsT n t,
nth_error argsT n = Some t
-> NatDict.sel (flatContext (argsT +++ nil)) n = t.
Lemma trace_precondition : forall argsT,
fprecondition (flatContext (argsT +++ nil)) argsT.
Theorem flinear_safe_alt : forall tp (lin : flinear tp)
(m1 : mem adom) sls1 bound m2 sls2,
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.
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).
Variable body_argsT : list aty.
Hypothesis body_bounded : G = flatContext (body_argsT +++ nil)
/\ flinear_bounded (init_bound (length body_argsT)) (fBody pr).
Theorem ftrace_safe_alt : forall (m1 : mem adom)
pc argsT (sls1 : slots) m2 sls2 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.
Lemma asmTrace_sound' : forall tr output, runTrace tr output
-> forall argsT m1 sls1 sls2 pc,
tr = fmakeTrace pr m1 pc argsT sls1
-> slots_lr (init_bound (length argsT)) m1 (flatContext (argsT +++ nil)) sls1 sls2
-> runTrace (makeTrace rt (asmProg pr) (heapComp rt m1) pc sls2) output.
Theorem asmTrace_sound : forall argsT m1 sls1 sls2 pc output,
slots_lr (init_bound (length argsT)) m1 (flatContext (argsT +++ nil)) sls1 sls2
-> runTrace (fmakeTrace pr m1 pc argsT sls1) output
-> runTrace (makeTrace rt (asmProg pr) (heapComp rt m1) pc sls2) output.
Theorem asmProg_sound : forall m1 sls1 sls2 output,
slots_lr (init_bound (length body_argsT)) m1 (flatContext (body_argsT +++ nil)) sls1 sls2
-> runTrace (fprogDenote pr sls1 m1) output
-> runTrace (programDenote rt (asmProg pr) sls2 (heapComp rt m1)) output.
End Traces.
End correctness.