Theory SINVAR_Dependability

theory SINVAR_Dependability
imports "../TopoS_Helper"
begin

subsection ‹SecurityInvariant Dependability›


type_synonym dependability_level = nat

definition default_node_properties :: "dependability_level"
  where  "default_node_properties ≡ 0"

text ‹Less-equal other nodes depend on the output of a node than its dependability level.›
fun sinvar :: "'v graph ⇒ ('v ⇒ dependability_level) ⇒ bool" where
  "sinvar G nP = (∀ (e1,e2) ∈ edges G. (num_reachable G e1) ≤ (nP e1))"

definition receiver_violation :: "bool" where 
  "receiver_violation ≡ False"


text‹It does not matter whether we iterate over all edges or all nodes. We chose all edges because it is in line with the other models.›
  fun sinvar_nodes :: "'v graph ⇒ ('v ⇒ dependability_level) ⇒ bool" where
    "sinvar_nodes G nP = (∀ v ∈ nodes G. (num_reachable G v) ≤ (nP v))"
  
  theorem sinvar_edges_nodes_iff: "wf_graph G ⟹ 
    sinvar_nodes G nP = sinvar G nP"
  proof(unfold sinvar_nodes.simps sinvar.simps, rule iffI)
    assume a1: "wf_graph G"
      and  a2: "∀v∈nodes G. num_reachable G v ≤ nP v"

      from a1[simplified wf_graph_def] have f1: "fst ` edges G ⊆ nodes G" by simp
      from f1 a2 have "∀v ∈ (fst ` edges G). num_reachable G v ≤ nP v" by auto

      thus "∀(e1, _) ∈ edges G. num_reachable G e1 ≤ nP e1" by auto
    next
    assume a1: "wf_graph G"
      and  a2: "∀(e1, _)∈edges G. num_reachable G e1 ≤ nP e1"

      from a2 have g1: "∀ v ∈ (fst ` edges G). num_reachable G v ≤ nP v" by auto

      from FiniteGraph.succ_tran_empty[OF a1] num_reachable_zero_iff[OF a1, symmetric]
      have g2: "∀ v. v ∉ (fst ` edges G) ⟶ num_reachable G v ≤ nP v" by (metis le0)

      from g1 g2 show "∀v∈nodes G. num_reachable G v ≤ nP v" by metis
  qed




  lemma num_reachable_le_nodes: "⟦ wf_graph G ⟧ ⟹ num_reachable G v ≤ card (nodes G)"
    unfolding num_reachable_def
    using succ_tran_subseteq_nodes card_seteq nat_le_linear wf_graph.finiteV by metis


  text‹nP is valid if all dependability level are greater equal the total number of nodes in the graph›
  lemma "⟦ wf_graph G; ∀v ∈ nodes G. nP v ≥ card (nodes G) ⟧ ⟹ sinvar G nP"
    apply(subst sinvar_edges_nodes_iff[symmetric], simp)
    apply(simp add:)
    using num_reachable_le_nodes by (metis le_trans)



  text‹Generate a valid configuration to start from:›
   text‹Takes arbitrary configuration, returns a valid one›
   fun dependability_fix_nP :: "'v graph ⇒ ('v ⇒ dependability_level) ⇒ ('v ⇒ dependability_level)" where
      "dependability_fix_nP G nP = (λv. if num_reachable G v ≤ (nP v) then (nP v) else num_reachable G v)"
  
   text‹@{const dependability_fix_nP} always gives you a valid solution›
   lemma dependability_fix_nP_valid: "⟦ wf_graph G ⟧ ⟹ sinvar G (dependability_fix_nP G nP)"
      by(subst sinvar_edges_nodes_iff[symmetric], simp_all)
  
   text‹furthermore, it gives you a minimal solution, i.e. if someone supplies a configuration with a value lower than
          calculated by @{const dependability_fix_nP}, this is invalid!›
   lemma dependability_fix_nP_minimal_solution: "⟦ wf_graph G; ∃ v ∈ nodes G. (nP v) < (dependability_fix_nP G (λ_. 0)) v ⟧ ⟹ ¬ sinvar G nP"
      apply(subst sinvar_edges_nodes_iff[symmetric], simp)
      apply(simp)
      apply(clarify)
      apply(rule_tac x="v" in bexI)
       apply(simp_all)
      done

(*
lemma card_less_equal_trancl: "finite A ⟹ card {e2. (aa, e2) ∈ (A - X)⇧+} ≤ card {e2. (aa, e2) ∈ (A)⇧+}"
apply(subgoal_tac "{e2. (aa, e2) ∈ (A - X)⇧+} ⊆ {e2. (aa, e2) ∈ (A)⇧+}")
apply(rule card_mono)
defer
apply(simp)
apply (metis (lifting) Collect_mono Diff_subset trancl_mono)
by (metis (lifting) Range_iff finite_Range mem_Collect_eq rev_finite_subset subsetI trancl_range)
*)


lemma sinvar_mono: "SecurityInvariant_withOffendingFlows.sinvar_mono sinvar"
  apply(rule_tac SecurityInvariant_withOffendingFlows.sinvar_mono_I_proofrule)
   apply(auto) (*TODO: auto in the midddle*)
  apply(rename_tac nP e1 e2 N E' e1' e2' E)
  apply(drule_tac E'="E'" and v="e1'" in num_reachable_mono)
   apply simp
  apply(subgoal_tac "(e1', e2') ∈ E")
   apply(force)
  apply(blast)
 done
  

interpretation SecurityInvariant_preliminaries
where sinvar = sinvar
  apply unfold_locales
    apply(frule_tac finite_distinct_list[OF wf_graph.finiteE])
    apply(erule_tac exE)
    apply(rename_tac list_edges)
    apply(rule_tac ff="list_edges" in SecurityInvariant_withOffendingFlows.mono_imp_set_offending_flows_not_empty[OF sinvar_mono])
        apply(auto)[4]
    apply(auto simp add: SecurityInvariant_withOffendingFlows.is_offending_flows_def graph_ops)[1]
   apply(fact SecurityInvariant_withOffendingFlows.sinvar_mono_imp_sinvar_mono[OF sinvar_mono])
  apply(fact SecurityInvariant_withOffendingFlows.sinvar_mono_imp_is_offending_flows_mono[OF sinvar_mono])
done


interpretation Dependability: SecurityInvariant_ACS
where default_node_properties = SINVAR_Dependability.default_node_properties
and sinvar = SINVAR_Dependability.sinvar
  unfolding SINVAR_Dependability.default_node_properties_def
  proof
    fix G::"'a graph" and f nP
    assume "wf_graph G" and "f ∈ set_offending_flows G nP"
    thus "∀i∈fst ` f. ¬ sinvar G (nP(i := 0))"
     apply (simp add: SecurityInvariant_withOffendingFlows.set_offending_flows_def
      SecurityInvariant_withOffendingFlows.is_offending_flows_min_set_def
      SecurityInvariant_withOffendingFlows.is_offending_flows_def)
     apply (simp split: prod.split_asm prod.split)
     apply (simp add:graph_ops)
     apply(clarify)
     apply (metis gr0I le0)
     done
  next
   fix otherbot 
   assume assm: "∀G f nP i. wf_graph G ∧ f ∈ set_offending_flows G nP ∧ i ∈ fst ` f ⟶ ¬ sinvar G (nP(i := otherbot))"
   have unique_default_example_succ_tran:
    "succ_tran ⦇nodes = {vertex_1, vertex_2}, edges = {(vertex_1, vertex_2)}⦈ vertex_1 = {vertex_2}"
    using unique_default_example1 by blast
   from assm show "otherbot = 0"
    apply -
    apply(elim default_uniqueness_by_counterexample_ACS)
    apply(simp)
    apply (simp add: SecurityInvariant_withOffendingFlows.set_offending_flows_def
        SecurityInvariant_withOffendingFlows.is_offending_flows_min_set_def
        SecurityInvariant_withOffendingFlows.is_offending_flows_def)
    apply (simp add:graph_ops)
    apply (simp split: prod.split_asm prod.split)
    apply(rule_tac x="⦇ nodes={vertex_1,vertex_2}, edges = {(vertex_1,vertex_2)} ⦈" in exI, simp)
    apply(rule conjI)
     apply(simp add: wf_graph_def)
    apply(rule_tac x="(λ x. 0)(vertex_1 := 0, vertex_2 := 0)" in exI, simp)
    apply(rule conjI)
     apply(simp add: unique_default_example_succ_tran num_reachable_def)
    apply(rule_tac x="vertex_1" in exI, simp)
    apply(rule_tac x="{(vertex_1,vertex_2)}" in exI, simp)
    apply(simp add: unique_default_example_succ_tran num_reachable_def)
    apply(simp add: succ_tran_def unique_default_example_simp1 unique_default_example_simp2)
    done
  qed

  lemma TopoS_Dependability: "SecurityInvariant sinvar default_node_properties receiver_violation"
  unfolding receiver_violation_def by unfold_locales  

hide_const (open) sinvar receiver_violation default_node_properties

end