include "RTLabs/RTLabs_traces.ma".

(* Check that the RTLabs pc → cost label map is injective for a given RTLabs
   program.
   
   First we check functions individually, then lift to the whole program. *)

definition graph_cost_injectivity : graph statement → Prop ≝
λg. ∀l1,l2,PR1,PR2,cl.
  cost_label_of (lookup_present ?? g l1 PR1) = Some ? cl →
  cost_label_of (lookup_present ?? g l2 PR2) = Some ? cl →
  l1 = l2.

definition function_cost_injectivity ≝
λf. graph_cost_injectivity (f_graph f).

definition program_cost_injectivity : RTLabs_program → Prop ≝
λp. All ? (λx. match \snd x with [ Internal f ⇒ function_cost_injectivity f | _ ⇒ True]) (prog_funct … p).

definition reverse_label_map : graph statement → (option (identifier_map CostTag (identifier LabelTag))) ≝
λg.
  foldi
    statement
    (option (identifier_map CostTag (identifier LabelTag)))
    LabelTag
    (λl,s,m.
      match m with
      [ None ⇒ None ?
      | Some m ⇒
        match cost_label_of s with
        [ Some cl ⇒
          match lookup ?? m cl with
          [ None ⇒ Some ? (add … m cl l)
          | Some _ ⇒ None ?
          ]
        | None ⇒ Some ? m
        ]
      ])
    g
    (Some ? (empty_map …)).


definition check_fun_inj : internal_function → bool ≝
λf.
match reverse_label_map (f_graph f) with
[ None ⇒ false
| Some _ ⇒ true
].


lemma reverse_label_map_ok : ∀g,r.
  reverse_label_map g = r →
  match r with
  [ None ⇒ ¬graph_cost_injectivity g
  | Some m ⇒ graph_cost_injectivity g
  ].
#g #r #F change with (foldi ??????) in F:(??%?);
lapply (foldi_ind' ??????? (λm,ls.
  match m with
  [ None ⇒ ¬(graph_cost_injectivity g)
  | Some m ⇒ ∀l,cl. (present ?? ls l ∧ ∃PR. cost_label_of (lookup_present ?? g l PR) = Some ? cl) ↔ lookup ?? m cl = Some ? l
  ]) ?? F)
[ #l #ls #s *
  [ #FR #L #H whd in H ⊢ %; @H
  | #m #FR #L #H whd in H ⊢ (match % with [_⇒?|_⇒?]);
    lapply (refl ? (cost_label_of s)) cases (cost_label_of s) in ⊢ (???% → %);
    [ #NCS whd #l' #cl cases (H l' cl) #H1 #H2 %
      [ * #H3 * #PR' #H4 cases (present_add_cases ?????? H3)
        [ #E destruct @⊥ >(lookup_present_eq ????? L ?) in H4; >NCS #E destruct
        | * #_ #PR'' @H1 /3/
        ]
      | #Lcl cases (H2 Lcl) #PR'' * #PR''' #CS % /2/
      ]
    | #cl #CL whd in  ⊢ (match % with [_⇒?|_⇒?]);
      lapply (refl ? (lookup ?? m cl)) cases (lookup ?? m cl) in ⊢ (???% → %);
      [ #Lcl whd #l' #cl' cases (H l' cl') #H1 #H2 %
        [ * #H3 * #PRg' #H4 cases (present_add_cases ?????? H3)
          [ #E destruct >(lookup_present_eq ????? L ?) in H4; >CL #E destruct
            @lookup_add_hit
          | * #NE #PR'' lapply (H1 ?) [/3/] #Lcl' >lookup_add_miss [ // | % #E destruct >Lcl in Lcl'; #E destruct ]
          ]
        | #Lcl' cases (lookup_add_cases ??????? Lcl')
          [ * #E1 #E2 destruct % [ @present_add_hit | %{(lookup_is_present … L)} >(lookup_present_eq ????? L ?) assumption ]
          | #Lcl'' cases (H2 Lcl'') /3/
          ]
        ]
      | #l' #L' whd % #GCI whd in GCI;
        cases (H l' cl) #H1 #H2 cases (H2 L') #PR' * #PRg' #CS'
        lapply (GCI l l' (lookup_is_present … L) PRg' cl ??)
        [ assumption
        | >(lookup_present_eq ????? L ?) assumption
        | #E destruct /2/
        ]
      ]
    ]
  ]
| whd #l #cl %
  [ * * #H cases (H (refl ??))
  | #E normalize in E; destruct
  ]
| cases r
  [ //
  | #m whd in ⊢ (% → %); #H
    #l1 #l2 #PR1 #PR2 #cl #CL1 #CL2
    cases (H l1 cl) #H1 #_ lapply (H1 ?) [ % [ @(proj1 … (domain_of_map_present … )) // | %{PR1} @CL1 ] ]
    cases (H l2 cl) #H2 #_ lapply (H2 ?) [ % [ @(proj1 … (domain_of_map_present … )) // | %{PR2} @CL2 ] ]
    #E >E #E' destruct %
  ]
] qed.

lemma check_fun_inj_ok : ∀f. bool_to_Prop (check_fun_inj f) ↔ function_cost_injectivity f.
#f %
[ whd in ⊢ (?% → ?);
  lapply (reverse_label_map_ok (f_graph f))
  cases (reverse_label_map ?)
  [ #_ *
  | #m #H #_ @(H (Some ? m)) %
  ]
| lapply (reverse_label_map_ok (f_graph f))
  whd in ⊢ (? → ? → ?%);
  cases (reverse_label_map ?)
  [ #H #INJ @(absurd … INJ (H (None ?) (refl ??)))
  | //
  ]
] qed.

definition check_program_cost_injectivity : RTLabs_program → bool ≝
λp. all ? (λx. match \snd x with [ Internal f ⇒ check_fun_inj f | _ ⇒ true ]) (prog_funct … p).

theorem check_project_cost_injectivity_ok : ∀p.
  bool_to_Prop (check_program_cost_injectivity p) ↔ program_cost_injectivity p.
#p %
[ #H whd in H:(?%) ⊢ %;
  @(All_mp ????? (proj1 … (all_All …) H))
  * #_ * // #f @(proj1 … (check_fun_inj_ok f))
| whd in ⊢ (% → ?%);
  #H
  @(proj2 … (all_All …))
  @(All_mp … H)
  * #_ * // #f
  @(proj2 … (check_fun_inj_ok f))
] qed.