Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
tree: 8514018bf8
Fetching contributors…

Cannot retrieve contributors at this time

610 lines (434 sloc) 19.486 kb
%{
********* PROPERTIES *********
}%
%block det-1 : some {FTL} {Defs : pbundle FTL -> l-def-list FTL} {P}
block {pb : pbundle FTL} {lbind : l-bind pb (Defs pb)}
{wb : wf-pb P (Defs pb)}.
%worlds (det-1) (pbundle-lookup _ _) (l-apply _ _ _) (l-bind _ _).
%{
**** MAPS ****
}%
pb-bind-map : {PB : pbundle FTL} l-bind PB Defs -> type.
%mode pb-bind-map +F -B.
%{ To appease Twelfs splitter }%
fb-bind-map0 : pb-bind-map pbundle0 l-bind0.
l-def-eq : l-def FT -> l-def FT -> type.
l-def-eq/refl : l-def-eq FD FD.
pbundle-lookup-unique : pbundle-lookup FB (l-def-list/cons FD1 _)
-> pbundle-lookup FB (l-def-list/cons FD2 _) -> l-def-eq FD1 FD2 -> type.
%mode pbundle-lookup-unique +FB1 +FB2 -FDEF.
- : pbundle-lookup-unique FB1 FB2 l-def-eq/refl.
branch-lookup-unique : branch-lookup PB Def1 -> branch-lookup PB Def2
-> l-def-eq Def1 Def2 -> type.
%mode branch-lookup-unique +BL1 +BL2 -FDEF.
- : branch-lookup-unique BL1 BL2 l-def-eq/refl.
insn-eq : insn T -> insn T -> type.
insn-eq/ : insn-eq I I.
function-apply-unique : l-def-eq FD1 FD2
-> l-apply FD1 TL E1 -> l-apply FD2 TL E2
-> insn-eq E1 E2 -> type.
%mode function-apply-unique +EQ +FA1 +FA2 -TMEQ.
- : function-apply-unique l-def-eq/refl l-apply/body l-apply/body insn-eq/.
- : function-apply-unique l-def-eq/refl (l-apply/phi FA1) (l-apply/phi FA2) Q
<- function-apply-unique l-def-eq/refl FA1 FA2 Q.
%{ General relation capturing the basics of type progress }%
progress-good : defs -> insn T -> type.
progress-good/value : progress-good D V
<- value V.
progress-good/step : progress-good D E
<- step D E E'.
can-pbundle-lookup : {FB : pbundle+ (l-tp-list/cons FT FTL)}
pbundle-lookup FB FDL -> type.
%mode can-pbundle-lookup +FB -FL.
- : can-pbundle-lookup (f-tl/z FB) (pbundle-lookup/ctx-hit FBind)
<- pb-bind-map FB FBind.
- : can-pbundle-lookup (f-tl/s FB) (pbundle-lookup/dig Q)
<- can-pbundle-lookup FB Q.
can-branch-lookup : {PB : pbundle+ (l-tp-list/cons LT R)}
branch-lookup PB Def -> type.
%mode can-branch-lookup +PB -Def.
- : can-branch-lookup PB (branch-lookup/ CPL)
<- can-pbundle-lookup PB CPL.
can-l-apply : {RL : cst-list TL} l-apply Parms RL T -> type.
%mode +{T : tp} +{TL : tp-list} +{Parms}
-{E : insn T}
+{RL : cst-list TL}
-{FA : l-apply Parms RL E}
can-l-apply RL FA.
- : can-l-apply cst-list/nil l-apply/body.
- : can-l-apply (cst-list/cons E EL) (l-apply/phi Q)
<- can-l-apply EL Q.
%{ Effectiveness, step-op }%
can-step-op : {O : op T} step-op O V -> type.
%mode can-step-op +O -SOP.
- : can-step-op (op/cst R) step-op/cst.
- : can-step-op (op/plus _ _) (step-op/plus CNP)
<- can-nat-plus _ _ CNP.
- : can-step-op (op/mone _ _) (step-op/mone CNM)
<- can-nat-mone _ _ CNM.
- : can-step-op (op/cmp-lt _ _) (step-op/cmp-lt CLT)
<- can-nat-lt _ _ CLT.
progress-letrec : ({F : pbundle FTL} {FB : l-bind F (Defs F)}
progress-good D (Body F))
-> progress-good D (insn/letrec Defs ([fb] Body fb)) -> type.
%mode +{FTL} +{T} +{F : pbundle FTL}
+{Body : pbundle FTL -> insn T}
+{Defs : pbundle FTL -> l-def-list FTL}
+{D : defs}
+{PG : {F} {FB} progress-good D (Body F)}
-{PGG : progress-good D (insn/letrec Defs Body)}
progress-letrec PG PGG.
- : progress-letrec ([fb] [fbind] progress-good/value VP)
(progress-good/step (step/letrec-v VP)).
- : progress-letrec ([fb] [fbind] progress-good/step (SP fb fbind))
(progress-good/step (step/letrec-s ([fb] [fbind] SP fb fbind))).
progress-do : progress-good D I1 -> progress-good D (insn/do I1 B) -> type.
%mode +{T} +{T'} +{D : defs}
+{I1 : insn T'} +{B : (cst T' -> insn T)} +{PG : progress-good D I1}
-{PGG : progress-good D (insn/do I1 B)}
progress-do PG PGG.
- : progress-do (progress-good/value VP) (progress-good/step step/do-v).
- : progress-do (progress-good/step SP) (progress-good/step (step/do-s SP)).
%{
%% Helper: If f is not in the list, then for any g in the list, we have f /= g
%% under the assumptions of wellformedness
notin-neq : f-notin (fun-id/ N1) D -> wf-defs P D G'
-> phi-lookup G' (fun-id/ N2) -> nat-neq N1 N2 -> type.
%mode notin-neq +FIN +WFD +GL -NEQ.
- : notin-neq (f-notin/s _ NEQ) (wf-defs/s _ _ _) phi-lookup/hit NEQ.
- : notin-neq (f-notin/s R _) (wf-defs/s WFD _ _) (phi-lookup/miss GL) NEQ
<- notin-neq R WFD GL NEQ.
}%
%% Relate a Phi lookup to a function lookup if good
lookup-good : wf-defs P D G' -> phi-lookup G' F
-> function-lookup F D FD -> type.
%mode +{P:phi} +{D:defs} +{P':phi} +{Tp1:tp} +{TpL1:tp-list}
+{F:fun-id Tp1 TpL1}
-{FD:fun-decl Tp1 TpL1} +{WFD:wf-defs P D P'}
+{GL:phi-lookup P' F} -{FLU:function-lookup F D FD}
(lookup-good WFD GL FLU).
- : lookup-good (wf-defs/s _ _ _) phi-lookup/hit function-lookup/hit.
- : lookup-good (wf-defs/s WFD NI _) (phi-lookup/miss GL)
(function-lookup/miss DL)
<- lookup-good WFD GL DL.
%% Effectiveness, we can always function apply
can-function-apply : {FD : fun-decl T TL} {RL : cst-list TL}
function-apply FD RL I -> type.
%mode +{TL:tp-list} +{T:tp} -{I:insn T} +{FD:fun-decl T TL} +{RL:cst-list TL}
-{FA:function-apply FD RL I} (can-function-apply FD RL FA).
- : can-function-apply (fun-decl/body B) cst-list/nil function-apply/body.
- : can-function-apply (fun-decl/parm B) (cst-list/cons R RL)
(function-apply/parm Q)
<- can-function-apply (B R) RL Q.
%{
**** MAIN PROGRESS LEMMA ****
}%
progress : {E : insn T} wf P E -> wf-defs P D P -> progress-good D E -> type.
%mode +{D : defs} +{T : tp} +{P : phi}
+{E : insn T} +{WF : wf P E} +{WFD : wf-defs P D P}
-{PG : progress-good D E}
progress E WF WFD PG.
-/return : progress (insn/return _) _ _ (progress-good/value value/return).
-/lr : progress (insn/letrec (Defs : pbundle FTL -> l-def-list FTL) Body)
(wf/letrec WF1) WFD Q
<- ({fb : pbundle FTL} {fbind : l-bind fb (Defs fb)} {wb : wf-pb P (Defs fb)}
pb-bind-map fb fbind ->
progress (Body fb) (WF1 fb wb) WFD (PG fb fbind))
<- progress-letrec PG Q.
-/br : progress (insn/br (f-hd PB) EL) _ _
(progress-good/step (step/br CFA BL))
<- can-branch-lookup PB BL
<- can-l-apply EL CFA.
-/brc-t : progress (insn/brc (cst/b (s _)) _ _ _ _) _ _
(progress-good/step step/brc-t).
-/brc-f : progress (insn/brc (cst/b z) L1 R1 L2 R2) _ _
(progress-good/step step/brc-f).
-/let : progress (insn/let Op _) _ _ (progress-good/step (step/let SOP))
<- can-step-op Op SOP.
-/do : progress (insn/do T1 B) (wf/do WF2 WF1) WFD Q
<- progress T1 WF1 WFD PG
<- progress-do PG Q.
-/call : progress (insn/call F RL1 Bdy) (wf/call WFBdy GL) WFD
(progress-good/step (step/call FA FL))
<- lookup-good WFD GL FL
<- can-function-apply _ RL1 FA.
pgm-progress-good : pgm -> type.
pgm-progress-good/value : pgm-progress-good (pgm/ D T)
<- value T.
pgm-progress-good/step : pgm-progress-good (pgm/ D T)
<- step D T T'.
progress-pgm-factor : (progress-good D I)
-> pgm-progress-good (pgm/ D I) -> type.
%mode progress-pgm-factor +PG -PGG.
- : progress-pgm-factor (progress-good/value VP) (pgm-progress-good/value VP).
- : progress-pgm-factor (progress-good/step SP) (pgm-progress-good/step SP).
progress-pgm : {P : pgm} wf-pgm P -> pgm-progress-good P -> type.
%mode progress-pgm +P +WF -PG.
- : progress-pgm (pgm/ D T) (wf-pgm/ WFD WF) Q
<- progress T WF WFD IPP
<- progress-pgm-factor IPP Q.
%{ Congruence on letrec }%
insn-eq-letrec-cong : ({fb} {fbind: l-bind fb (Defs fb)}
insn-eq (B1 fb) (B2 fb)) ->
insn-eq (insn/letrec Defs B1) (insn/letrec Defs B2) -> type.
%mode insn-eq-letrec-cong +EQ -TEQLR.
- : insn-eq-letrec-cong ([fb] [fbind] insn-eq/) insn-eq/.
op-eq : op A -> op A -> type.
op-eq/ : op-eq O O.
cst-eq : cst T -> cst T -> type.
cst-eq/ : cst-eq R R.
insn-eq-let-cong : {Bd : cst T -> insn T'} cst-eq R1 R2
-> insn-eq (Bd R1) (Bd R2) -> type.
%mode +{T : tp} +{T' : tp} +{R1 : cst T} +{R2 : cst T}
+{Bd : cst T -> insn T'}
+{EQ : cst-eq R1 R2}
-{IEQ : insn-eq (Bd R1) (Bd R2)}
insn-eq-let-cong Bd EQ IEQ.
- : insn-eq-let-cong Bd cst-eq/ insn-eq/.
insn-eq-do-cong : insn-eq T1 T2
-> insn-eq (insn/do T1 B) (insn/do T2 B) -> type.
%mode +{A : tp} +{B : tp} +{T1 : insn A} +{T2 : insn A} +{Bd : cst A -> insn B}
+{EQ1 : insn-eq T1 T2}
-{DEQ : insn-eq (insn/do T1 Bd) (insn/do T2 Bd)}
insn-eq-do-cong EQ1 DEQ.
- : insn-eq-do-cong insn-eq/ insn-eq/.
det-op : step-op O R1 -> step-op O R2 -> cst-eq R1 R2 -> type.
%mode det-op +SOP1 +SOP -REQ.
- : det-op step-op/cst step-op/cst cst-eq/.
- : det-op (step-op/plus P1) (step-op/plus P2) cst-eq/.
- : det-op (step-op/mone M1) (step-op/mone M2) cst-eq/.
- : det-op (step-op/cmp-lt L1) (step-op/cmp-lt L2) cst-eq/.
eq-fun-decl : fun-decl T1 T2 -> fun-decl T1 T2 -> type.
eq-fun-decl/ : eq-fun-decl FD FD.
void-eq-fun-decl : void -> eq-fun-decl FD FD' -> type.
%mode +{Tp1:tp} +{TpL1:tp-list} +{FD:fun-decl Tp1 TpL1} +{FD':fun-decl Tp1 TpL1}
+{V:void} -{EQ:eq-fun-decl FD FD'} (void-eq-fun-decl V EQ).
notin-void : f-notin (fun-id/ N) D
-> function-lookup (fun-id/ N) D T -> void -> type.
%mode notin-void +FIN +DL -V.
- : notin-void (f-notin/s R NEQ) (function-lookup/miss DL) V
<- notin-void R DL V.
- : notin-void (f-notin/s R FNEQ) function-lookup/hit V
<- fun-id-eq-neq (fun-id-eq/eq nat-eq/refl) FNEQ V.
function-lookup-unique : phi-lookup G' F -> wf-defs P D G'
-> function-lookup F D FD1 -> function-lookup F D FD2
-> eq-fun-decl FD1 FD2 -> type.
%mode function-lookup-unique +GL +WFD +FD1 +FD2 -EQ.
- : function-lookup-unique GL WFD
function-lookup/hit function-lookup/hit eq-fun-decl/.
- : function-lookup-unique (phi-lookup/miss GL') (wf-defs/s WFD' _ _)
(function-lookup/miss DL1) (function-lookup/miss DL2) EQ
<- function-lookup-unique GL' WFD' DL1 DL2 EQ.
- : function-lookup-unique phi-lookup/hit (wf-defs/s WFD NI _)
(function-lookup/miss DL1) (function-lookup/miss DL2) EQ
<- notin-void NI DL1 V
<- void-eq-fun-decl V EQ.
- : function-lookup-unique GL (wf-defs/s WFD NI _) function-lookup/hit
(function-lookup/miss DL2) EQ
<- notin-void NI DL2 V
<- void-eq-fun-decl V EQ.
- : function-lookup-unique GL (wf-defs/s WFD NI _) (function-lookup/miss DL1)
function-lookup/hit EQ
<- notin-void NI DL1 V
<- void-eq-fun-decl V EQ.
fap-unique : eq-fun-decl FD1 FD2 -> function-apply FD1 RL T1
-> function-apply FD2 RL T2
-> insn-eq T1 T2 -> type.
%mode fap-unique +EQ +FA1 +FA2 -IEQ.
- : fap-unique eq-fun-decl/ function-apply/body function-apply/body insn-eq/.
- : fap-unique eq-fun-decl/
(function-apply/parm FA1) (function-apply/parm FA2) EQ
<- fap-unique eq-fun-decl/ FA1 FA2 EQ.
%{ Determinism of the system }%
det : wf P T -> wf-defs P D P -> step D T T1 -> step D T T2
-> insn-eq T1 T2 -> type.
%mode det +WF +WFD +S1 +S2 -EQ.
- : det _ _ ((step/let SOP1) : step D (insn/let O B) (B R1))
(step/let SOP2) insn-eq/
<- det-op SOP1 SOP2 REQ
<- insn-eq-let-cong B REQ Q.
- : det _ _ (step/letrec-v VP) (step/letrec-v VP') insn-eq/.
- : det (wf/letrec WFB) WFD (step/letrec-s Run1) (step/letrec-s Run2) Q
<- ({fb : pbundle FTL}
{fbind : l-bind fb (Defs fb)}
{wb : wf-pb P (Defs fb)}
det (WFB fb wb) WFD (Run1 fb fbind) (Run2 fb fbind) (INEQ fb fbind))
<- insn-eq-letrec-cong INEQ Q.
- : det _ _ step/brc-t step/brc-t insn-eq/.
- : det _ _ step/brc-f step/brc-f insn-eq/.
- : det (wf/do DB DI) WFD(step/do-s SP1) (step/do-s SP2) Q
<- det DI WFD SP1 SP2 IEQ
<- insn-eq-do-cong IEQ Q.
- : det WF WFD (step/br FA1 FL1) (step/br FA2 FL2) Q
<- branch-lookup-unique FL1 FL2 FBEQ
<- function-apply-unique FBEQ FA1 FA2 Q.
- : det (wf/call WFB GL) WFD (step/call FA1 FL1) (step/call FA2 FL2) Q
<- function-lookup-unique GL WFD FL1 FL2 FBEQ
<- fap-unique FBEQ FA1 FA2 IEQ
<- insn-eq-do-cong IEQ Q.
- : det WF WFD step/do-v step/do-v insn-eq/.
pgm-eq : pgm -> pgm -> type.
pgm-eq/ : pgm-eq P P.
det-pgm-cong : insn-eq I1 I2 -> pgm-eq (pgm/ D I1) (pgm/ D I2) -> type.
%mode +{Tp1:tp} +{I1:insn Tp1} +{I2:insn Tp1} +{D:defs} +{EQ:insn-eq I1 I2}
-{Q:pgm-eq (pgm/ D I1) (pgm/ D I2)} (det-pgm-cong EQ Q).
- : det-pgm-cong insn-eq/ pgm-eq/.
det-pgm : wf-pgm P -> step-pgm P P' -> step-pgm P P'' -> pgm-eq P' P'' -> type.
%mode det-pgm +WF +SP1 +SP2 -PEQ.
- : det-pgm (wf-pgm/ WFD WF) (step-pgm/ SP1) (step-pgm/ SP2) EQ
<- det WF WFD SP1 SP2 IEQ
<- det-pgm-cong IEQ EQ.
%{ Blocks we need. The first one gives us the block we need in step relations }%
%block progress-1 : some {FTL : l-tp-list} {Defs} {P}
block {fb : pbundle FTL}
{bind : l-bind fb (Defs fb)}
{wb : wf-pb P (Defs fb)}
{map : pb-bind-map fb bind}.
%worlds (progress-1) (progress-letrec _ _)
(progress-do _ _)
(pb-bind-map _ _)
(progress _ _ _ _)
(can-step-op _ _)
(lookup-good _ _ _)
(can-function-apply _ _ _)
(can-l-apply _ _)
(can-pbundle-lookup _ _)
(can-branch-lookup _ _).
%worlds () (progress-pgm-factor _ _)
(progress-pgm _ _ _).
%worlds (det-1) (insn-eq-letrec-cong _ _)
(insn-eq-do-cong _ _)
(insn-eq-let-cong _ _ _)
(det-op _ _ _)
(pbundle-lookup-unique _ _ _)
(branch-lookup-unique _ _ _)
(function-apply-unique _ _ _ _).
%worlds (det-1)
(void-eq-fun-decl _ _)
(notin-void _ _ _)
(function-lookup-unique _ _ _ _ _)
(fap-unique _ _ _ _)
(det _ _ _ _ _).
%worlds () (det-pgm-cong _ _)
(det-pgm _ _ _ _).
%{ Various obvious uniqueness lemmas }%
%unique det-op +SOP1 +SOP2 -1REQ.
%unique l-apply +FD +TL -1T.
%unique l-bind +F -1B.
%unique pbundle-lookup +FB -1FDef.
%unique can-nat-plus +N1 +N2 -CNP.
%unique can-nat-mone +N1 +N2 -CNM.
%unique can-nat-lt +N1 +N2 -CLT.
%unique can-step-op +O -R.
%{ Progress totality }%
%total E (can-l-apply E _).
%total O (can-step-op O _).
%total PG (progress-letrec PG _).
%total T (progress-do T _).
%total E (pb-bind-map E _).
%total WF (lookup-good WF _ _).
%total FA (can-function-apply FA _ _).
%total N (can-pbundle-lookup N _).
%total B (can-branch-lookup B _).
%total T (progress T _ _ _).
%total PG (progress-pgm-factor PG _).
%total P (progress-pgm P _ _).
%{ Determinism totality }%
%total FB (pbundle-lookup-unique FB _ _).
%total BL (branch-lookup-unique BL _ _).
%total FB (function-apply-unique _ FB _ _).
%total T (insn-eq-let-cong T _ _).
%total IEQ (insn-eq-do-cong IEQ _).
%total FB (insn-eq-letrec-cong FB _).
%total S (det-op S _ _).
%total V (void-eq-fun-decl V _).
%total DL (notin-void _ DL _).
%total GL (function-lookup-unique GL _ _ _ _).
%total FA1 (fap-unique _ FA1 _ _).
%total S (det _ _ S _ _).
%total D (det-pgm-cong D _).
%total P (det-pgm _ P _ _).
%{
**** MAIN PRESERVATION THEOREM ****
}%
wf-l-bind : l-bind PB FL -> wf-pb P FL -> type.
%mode +{LTpL1:l-tp-list} +{PB:pbundle LTpL1} +{FL:l-def-list LTpL1}
-{P:phi} +{L:l-bind PB FL} -{WFPB:wf-pb P FL} (wf-l-bind L WFPB).
wf-l-bind0 : wf-l-bind l-bind0 (wf-pb/nil : wf-pb phi/z _).
preservation-pbundle-lookup : pbundle-lookup PB Bundle -> wf-defs P D P
-> wf-pb P Bundle -> type.
%mode preservation-pbundle-lookup +PL +WFD -WF.
- : preservation-pbundle-lookup (pbundle-lookup/ctx-hit L) WFD Q
<- wf-l-bind L Q.
- : preservation-pbundle-lookup (pbundle-lookup/dig PBL) WFD Q
<- preservation-pbundle-lookup PBL WFD (wf-pb/cons Q _).
preservation-branch-lookup : branch-lookup PB Def -> wf-defs P D P
-> wf-l P Def -> type.
%mode preservation-branch-lookup +BL +WFD -WF.
- : preservation-branch-lookup (branch-lookup/ PBL) WFD L
<- preservation-pbundle-lookup PBL WFD (wf-pb/cons _ L).
preservation-pbundle-apply : wf-l P L -> l-apply L RL T -> wf P T -> type.
%mode preservation-pbundle-apply +WFL +L -WF.
- : preservation-pbundle-apply (wf-l/phi WFP)
((l-apply/phi LP) : l-apply (l-def/phi _) (cst-list/cons E _) _) Q
<- preservation-pbundle-apply (WFP E) LP Q.
- : preservation-pbundle-apply (wf-l/body WF) l-apply/body WF.
preservation-lookup : function-lookup F D Df -> wf-defs P D G'
-> wf-decl P Df -> type.
%mode preservation-lookup +FL +WFD -Decl.
- : preservation-lookup function-lookup/hit (wf-defs/s WFD _ WF) WF.
- : preservation-lookup (function-lookup/miss L) (wf-defs/s WFD _ WF) Q
<- preservation-lookup L WFD Q.
preservation-fun-apply : wf-decl P Df -> function-apply Df RL I
-> wf P I -> type.
%mode preservation-fun-apply +Decl +FA -WF.
- : preservation-fun-apply (wf-decl/body WF) function-apply/body WF.
- : preservation-fun-apply (wf-decl/parm WD)
((function-apply/parm FA') : function-apply _ (cst-list/cons E _) _) Q
<- preservation-fun-apply (WD E) FA' Q.
preservation : wf P I -> wf-defs P D P -> step D I I' -> wf P I' -> type.
%mode preservation +WF +WFD +SD -WF'.
- : preservation (wf/let WB) WFD (step/let (SOP : step-op O R)) (WB R).
- : preservation wf/brc WFD step/brc-t wf/br.
- : preservation wf/brc WFD step/brc-f wf/br.
- : preservation (wf/do WB WI) WFD (step/do-s SI) (wf/do WB WFI)
<- preservation WI WFD SI WFI.
- : preservation (wf/do WB WI) WFD (step/do-v : step D
(insn/do (insn/return R) B) _) (WB R).
- : preservation (wf/letrec WFB) WFD (step/letrec-v value/return) wf/return.
- : preservation (wf/letrec WFB) WFD (step/letrec-s ISP) (wf/letrec WFB')
<- ({pb} {pbind} {wb : wf-pb P (WFPB pb)} wf-l-bind pbind wb ->
preservation (WFB pb wb) WFD (ISP pb pbind) (WFB' pb wb)).
- : preservation wf/br WFD (step/br LA PBL) Q
<- preservation-branch-lookup PBL WFD L
<- preservation-pbundle-apply L LA Q.
- : preservation (wf/call WFBdy GL) WFD (step/call FA FL) (wf/do WFBdy Q)
<- preservation-lookup FL WFD WFDecl
<- preservation-fun-apply WFDecl FA Q.
preservation-pgm : wf-pgm P -> step-pgm P P' -> wf-pgm P' -> type.
%mode preservation-pgm +WFP +SP -WFP'.
- : preservation-pgm (wf-pgm/ WFD WF) (step-pgm/ TSP) (wf-pgm/ WFD WF')
<- preservation WF WFD TSP WF'.
%block preservation-1 : some {FTL : l-tp-list} {Defs} {P}
block {pb : pbundle FTL}
{pbind : l-bind pb (Defs pb)}
{wb : wf-pb P (Defs pb)}
{wf-bind : wf-l-bind pbind wb}.
%worlds (preservation-1) (preservation _ _ _ _)
(preservation-pgm _ _ _)
(preservation-pbundle-apply _ _ _)
(preservation-branch-lookup _ _ _)
(preservation-pbundle-lookup _ _ _)
(preservation-lookup _ _ _)
(preservation-fun-apply _ _ _)
(wf-l-bind _ _).
%total B (wf-l-bind B _).
%trustme
%total E (preservation-pbundle-lookup E _ _).
%trustme
%total B (preservation-branch-lookup B _ _).
%total WF (preservation-pbundle-apply WF _ _).
%total FL (preservation-lookup FL _ _).
%total FA (preservation-fun-apply _ FA _).
%total SP (preservation _ _ SP _).
%total SP (preservation-pgm _ SP _).
Jump to Line
Something went wrong with that request. Please try again.