Changeset 2307 for src/RTLabs/CostCheck.ma

Timestamp:

Aug 30, 2012, 4:47:58 PM (7 years ago)

Author:

campbell

Message:

Half the proofs for sound cost labelling check.

File:

• src/RTLabs/CostCheck.ma (modified) (10 diffs)

src/RTLabs/CostCheck.ma

@@ -29 +29 @@
 definition check_well_cost_fn : internal_function → bool ≝
 λf.
-  idmap_all … (f_graph f) (λl,s,PR. well_cost_labelled_statement f s (f_closed f l s PR)) ∧
+  idmap_all … (f_graph f) (λl,s,PR. well_cost_labelled_statement (f_graph f) s (f_closed f l s PR)) ∧
   is_cost_label (lookup_present … (f_graph f) (f_entry f) ?).
 cases (f_entry f) //
@@ -96 +96 @@
       match try_remove … to_check h return λx. (∀a,m'. x = ? → ?) → ? with
       [ Some to_check' ⇒ λH'.
-        if h ∈ checking_tail then None ? else
         let PR' ≝ ? in
         let st' ≝ lookup_present … g h PR' in
         if is_cost_label st' then stop_now else
-          check_label_bounded g CL h PR' (checking::checking_tail) (\snd to_check') term_check' ?
-      | None ⇒ λ_. stop_now (* already checked successor *)
+          if h ∈ checking_tail then None ? else
+            check_label_bounded g CL h PR' (checking::checking_tail) (\snd to_check') term_check' ?
+      | None ⇒ λ_.
+          if h == checking ∨ h ∈ checking_tail then None ? else
+            stop_now (* already checked successor *)
       ] (try_remove_some_card … to_check h)
     | cons _ _ ⇒ λ_. stop_now (* all branches are followed by a cost label *)
@@ -122 +124 @@
     successors (lookup_present … g l PR) = [l'] →
     ¬ l' ∈ toch →
+    l' ≠ l →
+    ¬ l' ∈ tl →
     check_label_bounded_spec g l tl toch toch
 | clbs_cost : ∀l,PR,l',PR',tl,toch.
@@ -148 +152 @@
 qed.
 
+lemma not_orb : ∀b,c:bool.
+  ¬ (b∨c) →
+  (bool_to_Prop (¬b))∧(bool_to_Prop (¬c)).
+* * normalize /2/
+qed.
+
 lemma check_label_bounded_s : ∀term_check,g,CL,checking,PR,checking_tail,to_check,TERM,to_check'.
   check_label_bounded g CL checking PR checking_tail to_check term_check TERM = Some ? to_check' →
@@ -162 +172 @@
            lapply (refl ? (try_remove … to_check h))
            cases (try_remove ????) in ⊢ (???% → %);
-           [ #RM whd in ⊢ (? → ??%? → ?); #H #E destruct @(clbs_checked … SUCC)
-             whd in ⊢ (?(?%)); >(proj1 … (try_remove_empty …) RM) //
+           [ #RM whd in ⊢ (? → ??%? → ?); #H @if_elim
+             [ #H' #E destruct
+             | #H' cases (not_orb ?? H') #H1 #H2 #E destruct @(clbs_checked … SUCC)
+               [ whd in ⊢ (?(?%)); >(proj1 … (try_remove_empty …) RM) //
+               | % #E >E in H1; >(proj2 … (eqb_true …) (refl ??)) *
+               | assumption
+               ]
+             ]
            | * * #to_check'' #RM #H whd in ⊢ (??%? → ?);
              @if_elim
-             [ #IN whd in ⊢ (??%? → ?); #E destruct
-             | #OUT whd in ⊢ (??%? → ?);
+             [ #CS #E destruct @(clbs_cost … SUCC … CS)
+               cases (try_remove_some ?????? RM) * #L #_ #_ whd in ⊢ (?%); >L //
+             | #CS
                @if_elim
-               [ #CS #E destruct @(clbs_cost … SUCC … CS)
-                 cases (try_remove_some ?????? RM) * #L #_ #_ whd in ⊢ (?%); >L //
-               | #CS #H @(clbs_step … SUCC OUT CS RM) @(IH … H)
+               [ #IN whd in ⊢ (??%? → ?); #E destruct
+               | #OUT whd in ⊢ (??%? → ?); #H
+                 @(clbs_step … SUCC OUT CS RM) @(IH … H)
                ]
              ]
@@ -181 +198 @@
 ] qed.
 
-
+lemma check_label_bounded_c : ∀g,CL,checking,checking_tail,to_check,to_check'.
+  check_label_bounded_spec g checking checking_tail to_check to_check' →
+  ∀term_check,TERM,PR.
+  check_label_bounded g CL checking PR checking_tail to_check term_check TERM = Some ? to_check'.
+#g #CL #X1 #X2 #X3 #X4 #X elim X
+[ #l #PR #tl #toch #SUCC
+  * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR
+  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1
+  whd in ⊢ (??%?); %
+| #l #PR #l' #tl #toch #SUCC #NIN_toch #NEQ #NIN_tl
+  * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR
+  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1
+  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?);
+  cut (lookup … toch l' = None ?) [ whd in NIN_toch:(?(?%)); cases (lookup ????) in NIN_toch ⊢ %; [ // | * * ] ]
+  #L >(proj2 … (try_remove_empty …) L) #H2
+  whd in ⊢ (??%?); >(proj2 … (eqb_false …) NEQ) >(Prop_notb … NIN_tl)
+  %
+| #l #PR #l' #PR' #tl #toch #SUCC #IN #CS
+  * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR
+  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1
+  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?);
+  cut (lookup … toch l' = Some ? it) [ whd in IN:(?%); cases (lookup ????) in IN ⊢ %; [ * | * // ] ]
+  #L cases (try_remove_this ????? L) #to_check' #RM >RM #H2
+  whd in ⊢ (??%?); >CS whd in ⊢ (??%?); %
+| #l #PR #l' #PR' #tl #toch #toch' #toch'' #SUCC #NIN #NCS #RM #H #IH
+  * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR
+  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1
+  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >RM #H2
+  whd in ⊢ (??%?); >(not_b_to_eq_false ? (Prop_notb ? NCS))
+  whd in ⊢ (??%?); >(not_b_to_eq_false ? (Prop_notb ? NIN))
+  whd in ⊢ (??%?); >(IH term_check' ??) %
+| #l #PR #x #y #zs #tl #toch #SUCC
+  * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR
+  whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1
+  whd in ⊢ (??%?); %
+] qed.
 
 lemma check_label_bounded_subset : ∀g,checking,checking_tail,to_check,to_check'.
@@ -192 +244 @@
 [ #E destruct whd in ⊢ (?%); >L1 //
 | #L4 whd in ⊢ (?%); >L4 @IH @IN
+] qed.
+
+lemma bound_on_instrs_to_cost_prime : ∀g,l,n.
+  bound_on_instrs_to_cost g l n →
+  bound_on_instrs_to_cost' g l n.
+#g #l #n #H inversion H
+#l' #n' #PR #H' #E1 #E2 #_ destruct
+lapply (refl ? (is_cost_label (lookup_present … g l' PR)))
+cases (is_cost_label ?) in ⊢ (???% → ?); #CS
+[ @boitc_here [ @PR | @eq_true_to_b @CS ]
+| @boitc_later [ @PR | @eq_false_to_notb @CS | @H ]
+] qed.
+
+lemma present_member : ∀tag,A,m,id.
+  present tag A m id → member tag A m id.
+#tag #A #m #id whd in ⊢ (% → ?%); cases (lookup ????) // * #H cases (H (refl ??))
+qed.
+
+(* TODO: move and eliminate dup in Traces.ma *)
+lemma Exists_memb : ∀S:DeqSet. ∀x:S. ∀l:list S.
+  Exists S (λy. y = x) l →
+  x ∈ l.
+#S #x #l elim l 
+[ //
+| #h #t #IH
+  normalize lapply (eqb_true … x h)
+  cases (x==h) *
+  [ #E #_ >(E (refl ??)) //
+  | #_ #E * [ #E' destruct lapply (E (refl ??)) #E'' destruct
+            | #H @IH @H
+            ]
+  ]
+] qed.
+
+lemma successors_inv : ∀st,x,y,zs.
+  successors st = x::y::zs →
+  ∃r,l1,l2. st = St_cond r l1 l2.
+* normalize
+#a #b #c #d try #e try #f try #g try #h try #i try #j try #k try #l destruct
+/4/
+qed.
+
+include alias "utilities/deqsets.ma".
+
+lemma after_branch_are_cost_labels : ∀g. ∀CL:graph_closed g.
+  (∀l,PR. well_cost_labelled_statement g (lookup_present … g l PR) (CL l ? (lookup_lookup_present … PR))) →
+  ∀l,PR,x,y,zs. successors (lookup_present … g l PR) = x::y::zs →
+  ∀l'. ∀IN : l' ∈ successors (lookup_present … g l PR).
+  is_cost_label (lookup_present … g l' ?).
+[2: @(successors_present … IN) @(CL l) @lookup_lookup_present ]
+#g #CL #WCL #l #PR #x #y #zs #SUCCS
+cases (successors_inv … SUCCS)
+#r * #l1 * #l2 #E
+#l' #IN generalize in ⊢ (?(?(?????%))); #OR' >E in IN;
+lapply (WCL l PR) generalize in ⊢ (?(???%) → ?); >E in ⊢ (% → % → ?); #LP #WCst
+cases (andb_Prop_true ?? WCst)
+#H1 #H2
+whd in ⊢ (?% → ?); @eqb_elim
+[ 2: #_ #IN lapply (memb_single … IN) ]
+#E destruct //
+qed.
+
+
+lemma check_label_bounded_ok : ∀g,checking,checking_tail,to_check,to_check'.
+  ∀CL:graph_closed g.
+  (∀l,PR. well_cost_labelled_statement g (lookup_present … g l PR) (CL l ? (lookup_lookup_present … PR))) →
+  check_label_bounded_spec g checking checking_tail to_check to_check' →
+  (∀l. l∈g → ¬l ∈ to_check → l≠checking → ¬l∈checking_tail → ∃n. bound_on_instrs_to_cost g l n) →
+  ∀l. l = checking ∨ bool_to_Prop (l∈to_check) →
+  bool_to_Prop (l∈to_check') ∨ ∃n. bound_on_instrs_to_cost g l n.
+#g #X1 #X2 #X3 #X4 #CL #WCL #X elim X
+[ #l #PR #tl #toch #SUCC #INV #l' *
+  [ #E destruct %2 %{1} % [ @PR | >SUCC #l' * ]
+  | #IN %1 @IN
+  ]
+| #l #PR #l' #tl #toch #SUCC #NIN_toch #NEQ #NIN_tl #INV #l'' *
+  [ #E destruct %2
+    cases (INV l' ????)
+    [ #n #B
+      %{(S n)} % [ @PR | >SUCC #l'' * [2: *] #E destruct /2/ ]
+    | @present_member @(successors_present … (CL l ? (lookup_lookup_present … PR)))
+      >SUCC @eq_true_to_b @memb_hd
+    | assumption
+    | assumption
+    | assumption
+    ]
+  | #IN %1 assumption
+  ]
+| #l #PR #l' #PR' #tl #toch #SUCC #IN #CS #INV #l'' *
+  [ #E destruct %2 %{1} % [ // | #l'' >SUCC * [2: *] #E destruct @boitc_here // ]
+  | /2/
+  ]
+| #l #PR #l' #PR' #tl #toch #toch' #toch'' #SUCC #NIN_tl #NCS #RM #H #IH #INV #l'' *
+  [ #E destruct %2 cases (IH ? l' ?)
+    [ #IN @⊥ lapply (check_label_bounded_subset … H l' IN) #IN'
+      cases (try_remove_some ?????? RM) * #_ #L #_ whd in IN':(?%);
+      cases (lookup ????) in IN' L; [ * | * #_ #E destruct ]
+    | * #n #B %{(S n)} % [ // | #l'' >SUCC * [2: *] #E destruct /2/ ]
+    | #l'' #INg #INch' #NEQ #NIN_ltl @(INV l'' INg ???)
+      [ @notb_Prop % #INch @(absurd ?? (Prop_notb … INch'))
+        cases (try_remove_some ?????? RM) * #_ #_ #L
+        cases (L l'') [ #E destruct cases NEQ #X cases (X (refl ??)) ]
+        #L' whd in ⊢ (?%); <L' @INch
+      | % #E destruct cases (Prop_notb … NIN_ltl) #X @X @eq_true_to_b @memb_hd
+      | @notb_Prop @(not_to_not … (Prop_notb … NIN_ltl)) #IN @eq_true_to_b @memb_cons @IN
+      ]
+    | %1 %
+    ]
+  | #IN @(IH ? l'' ?)
+    [ #l''' #INg #NINch' #NEQ #NINtl @INV
+      [ assumption
+      | @notb_Prop @(not_to_not … (Prop_notb … NINch'))
+        cases (try_remove_some ?????? RM) * #L1 #L2 #L3
+        cases (L3 l''')
+        [ #E destruct @⊥ cases NEQ /2/
+        | #L whd in ⊢ (?% → ?%); >L //
+        ]
+      | % #E destruct cases (Prop_notb … NINtl) #X @X @eq_true_to_b @memb_hd
+      | @notb_Prop @(not_to_not … (Prop_notb … NINtl)) #IN @eq_true_to_b @memb_cons @IN
+      ]
+    | cases (try_remove_some ?????? RM) * #L1 #L2 #L3
+      cases (L3 l'') [ #E destruct %1 % | #L %2 whd in ⊢ (?%); <L @IN ]
+    ]
+  ]
+| #l #PR #x #y #zs #tl #toch #SUCCS #INV #l' *
+  [ #E destruct %2 %{1} % [ // ]
+    #l' #EX @boitc_here
+    [ @(successors_present … (CL l ? (lookup_lookup_present … PR)))
+      @Exists_memb @EX
+    | @(after_branch_are_cost_labels … WCL … SUCCS)
+    ]
+  | /2/
+  ]
 ] qed.
 
@@ -229 +414 @@
 ] qed.
 
+lemma check_graph_bounded_ok : ∀g.∀CL:graph_closed g. ∀term_check,to_check,SUB,start,PR,SMALLER,TERM.
+  (∀l,PR. well_cost_labelled_statement g (lookup_present … g l PR) (CL l ? (lookup_lookup_present … PR))) →
+  check_graph_bounded g CL to_check SUB start PR SMALLER term_check TERM = true →
+  (∀l. l∈g → ¬l∈to_check → l≠start → ∃n. bound_on_instrs_to_cost g l n) →
+  ∀l. l∈g → ∃n. bound_on_instrs_to_cost g l n.
+#g #CL #term_check elim term_check
+[ #to_check #SUB #start #PR #SMALLER #TERM @⊥ inversion TERM #A try #B try #C try #D destruct
+| #term_check' #IH #to_check #SUB #start #PR #SMALLER #TERM #WCL
+  whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
+  cases (check_label_bounded ????????) in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)? → ?);
+  [2:#to_check'] #CHECK_LABEL whd in ⊢ (??%? → ?); [2: #E destruct ]
+  generalize in ⊢ (??(?%??)? → ?); generalize in ⊢ (? → ??(??%?)? → ?); generalize in ⊢ (? → ? → ??(???%)? → ?);
+  lapply (choose_empty … to_check')
+  cases (choose LabelTag unit to_check')
+  [ * #H1 #H1' #H2 #H3 #H4 whd in ⊢ (??%? → ?); #_ #H #l #IN
+    cases (true_or_false_Prop (l∈to_check ∨ l == start))
+    [ #CHECKED cases (check_label_bounded_ok … (check_label_bounded_s … CHECK_LABEL) ? l ?)
+      [ #IN' @⊥ lapply (H1 (refl ??) l) #E whd in IN':(?%); >E in IN'; *
+      | //
+      | //
+      | @WCL
+      | #l' #IN_g #NIN_to_check #NEQ #_ @H //
+      | cases (orb_Prop_true … CHECKED) /2/ #E %1 @(proj1 … (eqb_true …)) @E
+      ]
+    | #NOT @H // [ @notb_Prop @(not_to_not … NOT) /2/ | % #E @(absurd ?? NOT) @orb_Prop_r >(proj2 … (eqb_true …)) // ]
+    ]
+ | * * #next * #to_check'' * #H1 #H1' #H2 #H3 #H4 whd in ⊢ (??%? → ?);
+   #CHECK #H @(IH … CHECK)
+   [ @WCL
+   | #l #INg #NIN'' #NEQ
+     cut (¬l∈to_check') [ @notb_Prop @(not_to_not … (Prop_notb … NIN''))
+                          cases (H4 … (refl ??)) * #L1 #L2 #L3
+                          cases (L3 l) [ #EQ @⊥ @(absurd ?? NEQ) >EQ % | #E whd in ⊢ (?% → ?%); >E // ] ]
+     #NIN'
+      cases (true_or_false_Prop (l∈to_check ∨ l == start))
+      [ #CHECKED cases (check_label_bounded_ok … (check_label_bounded_s … CHECK_LABEL) ? l ?)
+        [ #IN' @⊥ @(absurd … IN' (Prop_notb … NIN'))
+        | //
+        | //
+        | @WCL
+        | #l' #IN_g #NIN_to_check #NEQ #_ @H //
+        | cases (orb_Prop_true … CHECKED) /2/ #E %1 @(proj1 … (eqb_true …)) @E
+        ]
+      | #NOT @H // [ @notb_Prop @(not_to_not … NOT) /2/ | % #E @(absurd ?? NOT) @orb_Prop_r >(proj2 … (eqb_true …)) // ]
+      ]
+   ]
+ ]
+] qed.
+
 (* TODO: move *)
 definition id_set_of_map : ∀tag,A. identifier_map tag A → identifier_set tag ≝
@@ -275 +509 @@
 ] qed.
 
-axiom check_sound_cost_fn_ok : ∀fn. bool_to_Prop (check_sound_cost_fn fn) ↔ soundly_labelled_fn fn.
+axiom check_sound_cost_fn_ok : ∀fn.
+  well_cost_labelled_fn fn →
+  bool_to_Prop (check_sound_cost_fn fn) ↔ soundly_labelled_fn fn.
+(*
+#fn #WCL %
+[ whd in ⊢ (?% → %);
+  generalize in ⊢ (?(?%??) → ?); generalize in ⊢ (? → ?(??%?) → ?); generalize in ⊢ (? → ? → ?(???%) → ?);
+  cases (try_remove ????)
+  [ #H1 #H2 #H3 @⊥ cases (f_entry fn) in H3; #l #PR #E
+    lapply (proj1 … (id_set_of_map_present …) PR) whd in ⊢ (% → ?);
+    >(E (refl ??)) * /3/
+  | * * #to_check #H1 #H2 #H3
+    whd in ⊢ (?% → ?); #CHECK
+    #l #PR @(check_graph_bounded_ok … CHECK)
+    [ #l' #PR' cases WCL //
+    | #l' #IN #NIN #NEQ @⊥
+      cases (H1 … (refl ??)) * #L1 #L2 #L3
+      @(absurd ?? (Prop_notb … NIN))
+      cases (L3 l')
+      [ #E >E in NEQ; * #H cases (H (refl ??))
+      | #L whd in ⊢ (?%); <L @present_member @(proj1 … (id_set_of_map_present …))
+        @member_present @IN
+      ]
+    | /2/
+    ]
+  ]
+| TODO
+*)
 
 definition check_cost_program : RTLabs_program → bool ≝
@@ -287 +548 @@
 [ #H lapply ((proj1 ?? (all_All ???)) H) @All_mp
   * #id * #fd
-  [ #H cases (andb_Prop_true … H) #W #S %
-    [ @(proj1 … (check_well_cost_fn_ok … )) //
+  [ #H cases (andb_Prop_true … H) #W #S
+    lapply (proj1 … (check_well_cost_fn_ok …) W) #W'
+    %
+    [ //
     | @(proj1 … (check_sound_cost_fn_ok …)) //
     ]