-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathsummary.v
171 lines (143 loc) · 7.96 KB
/
summary.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
From Undecidability.Shared.Libs.PSL Require Import FinTypes Vectors.
From Undecidability.L Require Import TimeInvarianceTermination TimeInvarianceComputability.
From Undecidability.L.Datatypes Require Import LNat Lists LProd LFinType LVector Lists.
From Undecidability.TM Require Import TM_facts.
Import VectorNotations2.
From Undecidability.L Require Import TM.TMinL.TMinL_extract.
From Undecidability.L Require Import Functions.FinTypeLookup Functions.EqBool.
From Undecidability.TM.L Require CompilerBoolFuns.Compiler.
From Undecidability.TM.L Require Import CompilerBoolFuns.Compiler Alphabets StepTM M_LHeapInterpreter LMBounds_Loop.
From Undecidability.TM.L Require Import (*JumpTargetTM*) Alphabets StepTM M_LHeapInterpreter LMBounds_Loop SizeBoundsL.
From Undecidability Require Import L.AbstractMachines.FlatPro.LM_heap_correct.
Import L_Notations.
From Equations Require Import Equations.
Require Import Ring ZArith Arith Lia.
From Undecidability Require Import ProgrammingTools LM_heap_def (*WriteValue CaseList Copy*) ListTM Hoare LsimTMterm TimeInvarianceLtoTM.
Import Vector.VectorNotations.
Import ListNotations ResourceMeasures.
(****************)
(** THEOREM 1.1 *)
(****************)
Theorem TimeInvarianceThesis_wrt_Simulation_L_to_TM :
{C : nat &
let p := fun i m => C * (3*i+2)^2 * (3*i+1+m) * m in
let M := projT1 M_LHeapInterpreter.Loop in
forall s, closed s ->
let tps := [|inTape _ retr_closures_step [(0,compile s)]%list;inTape _ retr_closures_step []%list;inTape _ retr_heap_step []%list|] ++ Vector.const (inVoid _) _ in
(forall v i,
s ⇓(i) v ->
exists q tps',
loopM (initc M tps) (p i (size (compile s)) ) = Some (mk_mconfig q tps') /\
exists g H, reprC H g v /\ tps'[@Fin1] ≃(retr_closures_step) [g]%list /\ tps'[@Fin2] ≃(retr_heap_step) H) /\
(forall i q tps', loopM (initc M tps) i = Some (mk_mconfig q tps') -> exists v, L.eval s v)}.
Proof.
evar (c:nat). exists c. intros p M s cs tps. split.
- intros v i R.
edestruct (@completenessTime s v i) as (g&H&rep&R'). now eapply timeBS_evalIn. easy.
edestruct @TripleT_loopM_correct with (pM:= M_LHeapInterpreter.Loop) (t:=tps) as (q&tps'&Hloop&Htps').
{eapply Interpreter_SpecT. eassumption. inversion 1. }
{eapply tspec_tspec_withSpace. hnf. intros i'. cbn; destruct_fin i';cbn. 1-8:eapply inVoid_correct. all:eapply inTape_correct. }
do 2 eexists. hnf. split.
{ eapply loop_monotone. eassumption.
unshelve (erewrite UpToC.correct__leUpToC with (l:=@Loop_steps_nice ) (x:=(_,_))).
unfold p. cbn ["^"]. replace (3 * i + 1 + 1) with (3 * i + 2) by nia. rewrite Nat.mul_1_r. rewrite !mult_assoc.
rewrite sizeP_le_size. unfold c. reflexivity.
}
do 2 eexists. split. eassumption.
hnf in Htps'.
split.
1:specialize (Htps' Fin1).
2:specialize (Htps' Fin2).
all:unfold withSpace in Htps'; cbn in Htps'. 1,2:try contains_ext.
-
intros i q tps' H. unshelve eassert (Htmp:=Triple_loopM_sound (Interpreter_Spec [(0,compile s)] [] [])%list _ H).
{intros i'. cbn; destruct_fin i';cbn. 1-8:eapply inVoid_correct. all:eapply inTape_correct. }
edestruct Htmp as ([[[T' V'] H'] k] & (HR&HHalt) & G').
cbn in HR.
edestruct soundness with (1:=cs) as (g&H''&t&Heq&HE&?). { split. eapply pow_star in HR. exact HR. eassumption. }
injection Heq as [= -> -> ->]. eexists. eapply eval_iff. eassumption.
Qed.
(****************)
(** THEOREM 1.2 *)
(****************)
Theorem TimeInvarianceThesis_wrt_Simulation_TM_to_L : let C := 10 in
forall n (Σ : finType), forall M : TM Σ n, forall tps,
(forall tps' i q',
loopM (mk_mconfig (start M) tps) i = Some (mk_mconfig q' tps') ->
evalLe (C * (S i) * sizeTM M + C) (s_sim (encTM M) (encTps tps)) (encTps tps')) /\
(forall v, L_facts.eval (s_sim (encTM M) (encTps tps)) v -> exists q' tps' i, loopM (mk_mconfig (start M) tps) i = Some (mk_mconfig q' tps')).
Proof.
intros C n Σ. subst C.
pose (reg_sig := @encodable_finType Σ).
intros M tps. split.
- intros tps' i q' H.
rewrite TM_alt.loopSumM_loopM_iff in H.
eapply TimeInvarianceNF_forward in H.
eapply evalLe_trans_rev with (k := 7) in H as (H1 & H & _).
2:{ unfold s_sim. Lsimpl. } cbn -[mult].
unfold s_sim. unfold encTM, encTps.
eapply evalIn_mono. Lsimpl. eapply (evalIn_refl 0). Lproc.
fold (sizeTM M). ring_simplify. lia.
- intros v (q' & t' & [] & H) % TimeInvarianceNF_backward. inv H. setoid_rewrite TM_alt.loopSumM_loopM_iff. eauto.
Qed.
Definition encBoolsListTM {Σ : Type} (s b : Σ) (l : list bool) :=
(map (fun (x : bool) => (if x then s else b)) l).
Definition encBoolsTM {Σ : Type} (s b : Σ) (l : list bool) :=
@midtape Σ [] b (encBoolsListTM s b l).
Definition encNatTM {Σ : Type} (s b : Σ) (n : nat) :=
@midtape Σ [] b (repeat s n).
Definition TM_bool_computable {k} (R : Vector.t (list bool) k -> (list bool) -> Prop) (τ : nat -> Vector.t nat k -> nat -> Prop) :=
exists n : nat, exists Σ : finType, exists s b : Σ, s <> b /\
exists M : TM Σ (1 + k + n),
forall v : Vector.t (list bool) k,
(forall l, R v l -> exists q t i, loopM (mk_mconfig (start M) (Vector.append (niltape ::: Vector.map (encBoolsTM s b) v) (Vector.const niltape n))) i = Some (mk_mconfig q t) /\ (τ (length l) (Vector.map (@length bool) v)) i /\ Vector.hd t = encBoolsTM s b l) /\
(forall q t, TM.eval M (start M) (Vector.append (niltape ::: Vector.map (encBoolsTM s b) v) (Vector.const niltape n)) q t ->
exists l, R v l).
Definition encBoolsL (l : list bool) := Eval cbv in (enc l).
Definition L_bool_computable {k} (R : Vector.t (list bool) k -> (list bool) -> Prop) (τ : nat -> Vector.t nat k -> nat -> Prop) :=
exists s, closed s /\ forall v : Vector.t (list bool) k,
(forall l, R v l -> exists i, (Vector.fold_left (fun s n => L.app s (encBoolsL n)) s v) ⇓(<= i) (encBoolsL l) /\ τ (length l) (Vector.map (@length bool) v) i) /\
(forall o, L.eval (Vector.fold_left (fun s n => L.app s (encBoolsL n)) s v) o -> exists l, R v l).
(****************)
(** THEOREM 2.1 *)
(****************)
Theorem TimeInvarianceThesis_wrt_Computability_L_to_TM {k} (R : Vector.t (list bool) k -> (list bool) -> Prop) (τ : nat -> Vector.t nat k -> nat -> Prop) :
L_bool_computable R τ -> exists (c:nat),
let p m v j := let m_v := sumn (Vector.to_list v) in c*(j + 1) * (j + m_v + 1) * ((m_v + 1) * (j + 1) + m) in
TM_bool_computable R (fun m v i => exists j, τ m v j /\ i <= p m v j ).
Proof.
intros H. destruct (compiler_correct_timeInv H) as [c Hc].
exists c. eapply TM_bool_computable_hoare'_spec. now eapply L_bool_computable_time_function.
eassumption.
Qed.
(****************)
(** THEOREM 2.2 *)
(****************)
Theorem TimeInvarianceThesis_wrt_Computability_TM_to_L {k} (R : Vector.t (list bool) k -> (list bool) -> Prop) (τ : nat -> Vector.t nat k -> nat -> Prop) :
TM_bool_computable R τ -> exists p1, L_bool_computable R (fun m v i => exists j, τ m v j /\ p1 v j = i).
Proof.
intros (n & Σ & s & b & Heq & M & H).
pose (p := fun (v : Vector.t nat k) N =>
1 + 3 * k +
(1 +
(10 * S N * sizeTM M + 10 + 12 * n +
(c__prepare * (1 + sumn (Vector.to_list v) + k) + (N * c__unencListTM Σ + c__unencListTM Σ + 25))))
).
exists p, (the_term s b M).
split. eapply the_term_closed.
intros v. specialize (H v) as [H1 H2]. split.
- intros l (q & t & i & H & He & Hi) % H1.
exists (p (Vector.map (length (A :=bool)) v) i).
split. 2: eauto.
eapply evalIn_mono.
econstructor. 2:{ change (lambda (enc l)). Lproc. }
eapply the_term_forward; eauto. unfold list_size. unfold p.
assert (Hleq : (| encBoolsListTM s b l |) <= i). {
transitivity (sizeOfTape (Vector.hd t)). rewrite Hi.
cbn. lia.
assert (Vector.hd t = t[@Fin0]) as -> by now depelim t.
eapply TM_size_diff in H. cbn in H. rewrite H. cbn. lia.
}
rewrite Hleq, vector_map_to_list, vector_to_list_length. solverec.
- intros o (? & ? & ?) % the_term_backward. now eapply H2. eauto.
Qed.