From 66b90c58a75ee5a82866c3292106c68e21be14e5 Mon Sep 17 00:00:00 2001 From: Alejandro Gomez-Londono Date: Wed, 16 May 2018 17:27:55 +0200 Subject: [PATCH] Prove `Com`, `Sel` and `Let` cases of `compile_network_preservation` --- .../proofs/bakery_to_endpointProofScript.sml | 140 ++++++++++++++++++ 1 file changed, 140 insertions(+) diff --git a/projection/proofs/bakery_to_endpointProofScript.sml b/projection/proofs/bakery_to_endpointProofScript.sml index 8033b86..796ed20 100644 --- a/projection/proofs/bakery_to_endpointProofScript.sml +++ b/projection/proofs/bakery_to_endpointProofScript.sml @@ -80,6 +80,146 @@ val compile_network_preservation = Q.store_thm("compile_network_preservation", , FILTER_FILTER , FOLDL , fupdate_projectS] + (* Com *) + >- (MAP_EVERY Q.EXISTS_TAC [`s |+ ((v2,p2),d)`,`c'`] + \\ IMP_RES_TAC lookup_projectS + \\ rw [trans_s_def,fupdate_projectS] + \\ MAP_EVERY Q.ABBREV_TAC [ `l = FILTER (λy. p1 ≠ y ∧ p2 ≠ y) (nub' (procsOf c'))` + , `s' = s |+ ((v2,p2),d)` + , `s1 = projectS p1 s` + , `s2 = projectS p2 s` + , `s2' = projectS p2 s'` + , `cp1 = SND (project p1 c')` + , `cp2 = SND (project p2 c')` + , `ns = compile_network s' c' l` + , `s1q = <|bindings := s1; queue := []|>` + , `s2q = <|bindings := s2; queue := []|>` + ] + \\ `compile_network s (Com p1 v1 p2 v2 c') l = ns` + by (rw [Abbr `l`, Abbr `ns`, Abbr `s'` + , MEM_FILTER, cn_ignore_com, cn_ignore_state_update]) + \\ ASM_REWRITE_TAC [] + \\ pop_assum (K ALL_TAC) + \\ ho_match_mp_tac RTC_TRANS + \\ Q.EXISTS_TAC + `NPar (NEndpoint p1 s1q cp1) + (NPar (NEndpoint p2 (s2q with queue := SNOC (p1,d) s2q.queue) + (Receive p1 v2 cp2)) ns)` + \\ rw [reduction_def] + >- (ho_match_mp_tac trans_com_l + \\ MAP_EVERY Q.EXISTS_TAC [`p1`,`p2`,`d`] + \\ rw [] + >- (ho_match_mp_tac trans_send + \\ rw [Abbr `s1q`]) + >- (ho_match_mp_tac trans_par_l + \\ ho_match_mp_tac trans_enqueue + \\ rw [])) + >- (ho_match_mp_tac RTC_SINGLE + \\ rw [reduction_def] + \\ ho_match_mp_tac trans_par_r + \\ ho_match_mp_tac trans_par_l + \\ ho_match_mp_tac trans_dequeue_gen + \\ MAP_EVERY Q.EXISTS_TAC [`d`,`[]`,`[]`] + \\ rw [Abbr `s2q`, Abbr `s2`,Abbr `s'`,Abbr `s2'`,projectS_fupdate])) + (* Sel-T *) + >- (MAP_EVERY Q.EXISTS_TAC [`s`,`c'`] + \\ rw [trans_s_def] + \\ MAP_EVERY Q.ABBREV_TAC [ `l = FILTER (λy. p1 ≠ y ∧ p2 ≠ y) (nub' (procsOf c'))` + , `s1 = <| bindings := projectS p1 s; + queue := [] |>` + , `s2 = <| bindings := projectS p2 s; + queue := [] |>` + , `cp1 = SND (project p1 c')` + , `cp2 = SND (project p2 c')` + , `ns = compile_network s c' l` + ] + \\ `compile_network s (Sel p1 T p2 c') l = ns` + by (rw [Abbr `l`, Abbr `ns`, MEM_FILTER, cn_ignore_sel]) + \\ ASM_REWRITE_TAC [] + \\ pop_assum (K ALL_TAC) + \\ ho_match_mp_tac RTC_TRANS + \\ Q.EXISTS_TAC `NPar (NEndpoint p1 s1 cp1) + (NPar (NEndpoint p2 (s2 with <|queue := [(p1,[1w])]|>) + (ExtChoice p1 cp2 Nil)) + ns)` + \\ rw [] + >- (rw [reduction_def,Abbr `s1`,Abbr `s2`] + \\ ho_match_mp_tac trans_com_choice_l + \\ MAP_EVERY Q.EXISTS_TAC [`p1`,`p2`,`T`] + \\ rw [] + >- (ho_match_mp_tac trans_int_choice >> rw []) + >- (ho_match_mp_tac trans_par_l + \\ ho_match_mp_tac trans_enqueue_choice_gen + \\ rw [])) + >- (ho_match_mp_tac RTC_SINGLE + \\ rw [reduction_def,Abbr `s1`,Abbr `s2`] + \\ ho_match_mp_tac trans_par_r + \\ ho_match_mp_tac trans_par_l + \\ ho_match_mp_tac trans_ext_choice_l_gen + \\ rw [])) + (* Sel-F *) + >- (MAP_EVERY Q.EXISTS_TAC [`s`,`c'`] + \\ rw [trans_s_def] + \\ MAP_EVERY Q.ABBREV_TAC [ `l = FILTER (λy. p1 ≠ y ∧ p2 ≠ y) (nub' (procsOf c'))` + , `s1 = <| bindings := projectS p1 s; + queue := [] |>` + , `s2 = <| bindings := projectS p2 s; + queue := [] |>` + , `cp1 = SND (project p1 c')` + , `cp2 = SND (project p2 c')` + , `ns = compile_network s c' l` + ] + \\ `compile_network s (Sel p1 F p2 c') l = ns` + by (rw [Abbr `l`, Abbr `ns`, MEM_FILTER, cn_ignore_sel]) + \\ ASM_REWRITE_TAC [] + \\ pop_assum (K ALL_TAC) + \\ ho_match_mp_tac RTC_TRANS + \\ Q.EXISTS_TAC `NPar (NEndpoint p1 s1 cp1) + (NPar (NEndpoint p2 (s2 with <|queue := [(p1,[0w])]|>) + (ExtChoice p1 Nil cp2)) + ns)` + \\ rw [] + >- (rw [reduction_def,Abbr `s1`,Abbr `s2`] + \\ ho_match_mp_tac trans_com_choice_l + \\ MAP_EVERY Q.EXISTS_TAC [`p1`,`p2`,`F`] + \\ rw [] + >- (ho_match_mp_tac trans_int_choice >> rw []) + >- (ho_match_mp_tac trans_par_l + \\ ho_match_mp_tac trans_enqueue_choice_gen + \\ rw [])) + >- (ho_match_mp_tac RTC_SINGLE + \\ rw [reduction_def,Abbr `s1`,Abbr `s2`] + \\ ho_match_mp_tac trans_par_r + \\ ho_match_mp_tac trans_par_l + \\ ho_match_mp_tac trans_ext_choice_r_gen + \\ rw [])) + (* Let *) + >- (MAP_EVERY Q.EXISTS_TAC [`s |+ ((v,p),f (MAP (THE ∘ FLOOKUP s) (MAP (λv. (v,p)) vl)))`,`c'`] + \\ rw [trans_s_def] + \\ MAP_EVERY Q.ABBREV_TAC [ `l = FILTER (λy. p ≠ y) (nub' (procsOf c'))` + , `s' = s |+ ((v,p),f (MAP (THE ∘ FLOOKUP s) (MAP (λv. (v,p)) vl)))` + , `s1 = projectS p s` + , `s1' = projectS p s'` + , `cp1 = project p c'` + , `cp2 = project p c'` + , `ns = compile_network s' c' l` + , `sq = <|bindings := s1; queue := []|>` + , `sq' = <|bindings := s1'; queue := []|>` + ] + \\ `compile_network s (Let v p f vl c') l = ns` + by (rw [ Abbr `l`, Abbr `ns`, Abbr `s'`, MEM_FILTER + , cn_ignore_let , cn_ignore_state_update]) + \\ ASM_REWRITE_TAC [] + \\ pop_assum (K ALL_TAC) + \\ ho_match_mp_tac RTC_SINGLE + \\ rw [reduction_def] + \\ ho_match_mp_tac trans_par_l + \\ ho_match_mp_tac trans_let_gen + \\ UNABBREV_ALL_TAC + \\ rw [] + >- (Induct_on `vl` \\ rw [lookup_projectS']) + >- (rw [projectS_fupdate] >> rpt AP_TERM_TAC + \\ Induct_on `vl` >> rw [lookup_projectS'])) \\ cheat );