# Theory AllocImpl

Up to index of Isabelle/HOL/UNITY

theory AllocImpl
imports AllocBase Follows PPROD
begin

    (*  Title:      HOL/UNITY/AllocImpl
        ID:         $Id: AllocImpl.thy,v 1.5 2005/06/17 14:13:10 haftmann Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1998  University of Cambridge
    *)

    header{*Implementation of a multiple-client allocator from a single-client allocator*}

    theory AllocImpl imports AllocBase Follows PPROD begin

    (** State definitions.  OUTPUT variables are locals **)

    (*Type variable 'b is the type of items being merged*)
    record 'b merge =
      In   :: "nat => 'b list"  (*merge's INPUT histories: streams to merge*)
      Out  :: "'b list"         (*merge's OUTPUT history: merged items*)
      iOut :: "nat list"        (*merge's OUTPUT history: origins of merged items*)

    record ('a,'b) merge_d =
      "'b merge" +
      dummy :: 'a       (*dummy field for new variables*)

    constdefs
      non_dummy :: "('a,'b) merge_d => 'b merge"
        "non_dummy s == (|In = In s, Out = Out s, iOut = iOut s|)"

    record 'b distr =
      In  :: "'b list"          (*items to distribute*)
      iIn :: "nat list"         (*destinations of items to distribute*)
      Out :: "nat => 'b list"   (*distributed items*)

    record ('a,'b) distr_d =
      "'b distr" +
      dummy :: 'a       (*dummy field for new variables*)

    record allocState =
      giv :: "nat list"   (*OUTPUT history: source of tokens*)
      ask :: "nat list"   (*INPUT: tokens requested from allocator*)
      rel :: "nat list"   (*INPUT: tokens released to allocator*)

    record 'a allocState_d =
      allocState +
      dummy    :: 'a                (*dummy field for new variables*)

    record 'a systemState =
      allocState +
      mergeRel :: "nat merge"
      mergeAsk :: "nat merge"
      distr    :: "nat distr"
      dummy    :: 'a                  (*dummy field for new variables*)

    constdefs

    (** Merge specification (the number of inputs is Nclients) ***)

      (*spec (10)*)
      merge_increasing :: "('a,'b) merge_d program set"
        "merge_increasing ==
             UNIV guarantees (Increasing merge.Out) Int (Increasing merge.iOut)"

      (*spec (11)*)
      merge_eqOut :: "('a,'b) merge_d program set"
        "merge_eqOut ==
             UNIV guarantees
             Always {s. length (merge.Out s) = length (merge.iOut s)}"

      (*spec (12)*)
      merge_bounded :: "('a,'b) merge_d program set"
        "merge_bounded ==
             UNIV guarantees
             Always {s. ∀elt ∈ set (merge.iOut s). elt < Nclients}"

      (*spec (13)*)
      merge_follows :: "('a,'b) merge_d program set"
        "merge_follows ==
             (\<Inter>i ∈ lessThan Nclients. Increasing (sub i o merge.In))
             guarantees
             (\<Inter>i ∈ lessThan Nclients.
              (%s. sublist (merge.Out s)
                           {k. k < size(merge.iOut s) & merge.iOut s! k = i})
              Fols (sub i o merge.In))"

      (*spec: preserves part*)
      merge_preserves :: "('a,'b) merge_d program set"
        "merge_preserves == preserves merge.In Int preserves merge_d.dummy"

      (*environmental constraints*)
      merge_allowed_acts :: "('a,'b) merge_d program set"
        "merge_allowed_acts ==
           {F. AllowedActs F =
                insert Id (UNION (preserves (funPair merge.Out merge.iOut)) Acts)}"

      merge_spec :: "('a,'b) merge_d program set"
        "merge_spec == merge_increasing Int merge_eqOut Int merge_bounded Int
                       merge_follows Int merge_allowed_acts Int merge_preserves"

    (** Distributor specification (the number of outputs is Nclients) ***)

      (*spec (14)*)
      distr_follows :: "('a,'b) distr_d program set"
        "distr_follows ==
             Increasing distr.In Int Increasing distr.iIn Int
             Always {s. ∀elt ∈ set (distr.iIn s). elt < Nclients}
             guarantees
             (\<Inter>i ∈ lessThan Nclients.
              (sub i o distr.Out) Fols
              (%s. sublist (distr.In s)
                           {k. k < size(distr.iIn s) & distr.iIn s ! k = i}))"

      distr_allowed_acts :: "('a,'b) distr_d program set"
        "distr_allowed_acts ==
           {D. AllowedActs D = insert Id (UNION (preserves distr.Out) Acts)}"

      distr_spec :: "('a,'b) distr_d program set"
        "distr_spec == distr_follows Int distr_allowed_acts"

    (** Single-client allocator specification (required) ***)

      (*spec (18)*)
      alloc_increasing :: "'a allocState_d program set"
        "alloc_increasing == UNIV  guarantees  Increasing giv"

      (*spec (19)*)
      alloc_safety :: "'a allocState_d program set"
        "alloc_safety ==
             Increasing rel
             guarantees  Always {s. tokens (giv s) ≤ NbT + tokens (rel s)}"

      (*spec (20)*)
      alloc_progress :: "'a allocState_d program set"
        "alloc_progress ==
             Increasing ask Int Increasing rel Int
             Always {s. ∀elt ∈ set (ask s). elt ≤ NbT}
             Int
             (\<Inter>h. {s. h ≤ giv s & h pfixGe (ask s)}
                     LeadsTo
                     {s. tokens h ≤ tokens (rel s)})
             guarantees  (\<Inter>h. {s. h ≤ ask s} LeadsTo {s. h pfixLe giv s})"

      (*spec: preserves part*)
      alloc_preserves :: "'a allocState_d program set"
        "alloc_preserves == preserves rel Int
                            preserves ask Int
                            preserves allocState_d.dummy"

      (*environmental constraints*)
      alloc_allowed_acts :: "'a allocState_d program set"
        "alloc_allowed_acts ==
           {F. AllowedActs F = insert Id (UNION (preserves giv) Acts)}"

      alloc_spec :: "'a allocState_d program set"
        "alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int
                       alloc_allowed_acts Int alloc_preserves"

    locale Merge =
      fixes M :: "('a,'b::order) merge_d program"
      assumes
        Merge_spec:  "M  ∈ merge_spec"

    locale Distrib =
      fixes D :: "('a,'b::order) distr_d program"
      assumes
        Distrib_spec:  "D ∈ distr_spec"

    (****
    #  {** Network specification ***}

    #    {*spec (9.1)*}
    #    network_ask :: "'a systemState program set
    #       "network_ask == \<Inter>i ∈ lessThan Nclients.
    #                           Increasing (ask o sub i o client)
    #                           guarantees[ask]
    #                           (ask  Fols (ask o sub i o client))"

    #    {*spec (9.2)*}
    #    network_giv :: "'a systemState program set
    #       "network_giv == \<Inter>i ∈ lessThan Nclients.
    #                           Increasing giv
    #                           guarantees[giv o sub i o client]
    #                           ((giv o sub i o client) Fols giv)"

    #    {*spec (9.3)*}
    #    network_rel :: "'a systemState program set
    #       "network_rel == \<Inter>i ∈ lessThan Nclients.
    #                           Increasing (rel o sub i o client)
    #                           guarantees[rel]
    #                           (rel  Fols (rel o sub i o client))"

    #    {*spec: preserves part*}
    #       network_preserves :: "'a systemState program set
    #       "network_preserves == preserves giv  Int
    #                             (\<Inter>i ∈ lessThan Nclients.
    #                              preserves (funPair rel ask o sub i o client))"

    #    network_spec :: "'a systemState program set
    #       "network_spec == network_ask Int network_giv Int
    #                        network_rel Int network_preserves"

    #  {** State mappings **}
    #    sysOfAlloc :: "((nat => merge) * 'a) allocState_d => 'a systemState"
    #       "sysOfAlloc == %s. let (cl,xtr) = allocState_d.dummy s
    #                          in (| giv = giv s,
    #                                ask = ask s,
    #                                rel = rel s,
    #                                client   = cl,
    #                                dummy    = xtr|)"

    #    sysOfClient :: "(nat => merge) * 'a allocState_d => 'a systemState"
    #       "sysOfClient == %(cl,al). (| giv = giv al,
    #                                    ask = ask al,
    #                                    rel = rel al,
    #                                    client   = cl,
    #                                    systemState.dummy = allocState_d.dummy al|)"
    ****)

    declare subset_preserves_o [THEN subsetD, intro]
    declare funPair_o_distrib [simp]
    declare Always_INT_distrib [simp]
    declare o_apply [simp del]

    subsection{*Theorems for Merge*}

    lemma (in Merge) Merge_Allowed:
         "Allowed M = (preserves merge.Out) Int (preserves merge.iOut)"
    apply (cut_tac Merge_spec)
    apply (auto simp add: merge_spec_def merge_allowed_acts_def Allowed_def
                          safety_prop_Acts_iff)
    done

    lemma (in Merge) M_ok_iff [iff]:
         "M ok G = (G ∈ preserves merge.Out & G ∈ preserves merge.iOut &
                         M ∈ Allowed G)"
    by (auto simp add: Merge_Allowed ok_iff_Allowed)

    lemma (in Merge) Merge_Always_Out_eq_iOut:
         "[| G ∈ preserves merge.Out; G ∈ preserves merge.iOut; M ∈ Allowed G |]
          ==> M Join G ∈ Always {s. length (merge.Out s) = length (merge.iOut s)}"
    apply (cut_tac Merge_spec)
    apply (force dest: guaranteesD simp add: merge_spec_def merge_eqOut_def)
    done

    lemma (in Merge) Merge_Bounded:
         "[| G ∈ preserves merge.iOut; G ∈ preserves merge.Out; M ∈ Allowed G |]
          ==> M Join G ∈ Always {s. ∀elt ∈ set (merge.iOut s). elt < Nclients}"
    apply (cut_tac Merge_spec)
    apply (force dest: guaranteesD simp add: merge_spec_def merge_bounded_def)
    done

    lemma (in Merge) Merge_Bag_Follows_lemma:
         "[| G ∈ preserves merge.iOut; G ∈ preserves merge.Out; M ∈ Allowed G |]
      ==> M Join G ∈ Always
              {s. (∑i ∈ lessThan Nclients. bag_of (sublist (merge.Out s)
                                      {k. k < length (iOut s) & iOut s ! k = i})) =
                  (bag_of o merge.Out) s}"
    apply (rule Always_Compl_Un_eq [THEN iffD1])
    apply (blast intro: Always_Int_I [OF Merge_Always_Out_eq_iOut Merge_Bounded])
    apply (rule UNIV_AlwaysI, clarify)
    apply (subst bag_of_sublist_UN_disjoint [symmetric])
      apply (simp)
     apply blast
    apply (simp add: set_conv_nth)
    apply (subgoal_tac
           "(\<Union>i ∈ lessThan Nclients. {k. k < length (iOut x) & iOut x ! k = i}) =
           lessThan (length (iOut x))")
     apply (simp (no_asm_simp) add: o_def)
    apply blast
    done

    lemma (in Merge) Merge_Bag_Follows:
         "M ∈ (\<Inter>i ∈ lessThan Nclients. Increasing (sub i o merge.In))
              guarantees
                 (bag_of o merge.Out) Fols
                 (%s. ∑i ∈ lessThan Nclients. (bag_of o sub i o merge.In) s)"
    apply (rule Merge_Bag_Follows_lemma [THEN Always_Follows1, THEN guaranteesI], auto)
    apply (rule Follows_setsum)
    apply (cut_tac Merge_spec)
    apply (auto simp add: merge_spec_def merge_follows_def o_def)
    apply (drule guaranteesD)
      prefer 3
      apply (best intro: mono_bag_of [THEN mono_Follows_apply, THEN subsetD], auto)
    done

    subsection{*Theorems for Distributor*}

    lemma (in Distrib) Distr_Increasing_Out:
         "D ∈ Increasing distr.In Int Increasing distr.iIn Int
              Always {s. ∀elt ∈ set (distr.iIn s). elt < Nclients}
              guarantees
              (\<Inter>i ∈ lessThan Nclients. Increasing (sub i o distr.Out))"
    apply (cut_tac Distrib_spec)
    apply (simp add: distr_spec_def distr_follows_def)
    apply clarify
    apply (blast intro: guaranteesI Follows_Increasing1 dest: guaranteesD)
    done

    lemma (in Distrib) Distr_Bag_Follows_lemma:
         "[| G ∈ preserves distr.Out;
             D Join G ∈ Always {s. ∀elt ∈ set (distr.iIn s). elt < Nclients} |]
      ==> D Join G ∈ Always
              {s. (∑i ∈ lessThan Nclients. bag_of (sublist (distr.In s)
                                      {k. k < length (iIn s) & iIn s ! k = i})) =
                  bag_of (sublist (distr.In s) (lessThan (length (iIn s))))}"
    apply (erule Always_Compl_Un_eq [THEN iffD1])
    apply (rule UNIV_AlwaysI, clarify)
    apply (subst bag_of_sublist_UN_disjoint [symmetric])
      apply (simp (no_asm))
     apply blast
    apply (simp add: set_conv_nth)
    apply (subgoal_tac
           "(\<Union>i ∈ lessThan Nclients. {k. k < length (iIn x) & iIn x ! k = i}) =
            lessThan (length (iIn x))")
     apply (simp (no_asm_simp))
    apply blast
    done

    lemma (in Distrib) D_ok_iff [iff]:
         "D ok G = (G ∈ preserves distr.Out & D ∈ Allowed G)"
    apply (cut_tac Distrib_spec)
    apply (auto simp add: distr_spec_def distr_allowed_acts_def Allowed_def
                          safety_prop_Acts_iff ok_iff_Allowed)
    done

    lemma (in Distrib) Distr_Bag_Follows:
     "D ∈ Increasing distr.In Int Increasing distr.iIn Int
          Always {s. ∀elt ∈ set (distr.iIn s). elt < Nclients}
          guarantees
           (\<Inter>i ∈ lessThan Nclients.
            (%s. ∑i ∈ lessThan Nclients. (bag_of o sub i o distr.Out) s)
            Fols
            (%s. bag_of (sublist (distr.In s) (lessThan (length(distr.iIn s))))))"
    apply (rule guaranteesI, clarify)
    apply (rule Distr_Bag_Follows_lemma [THEN Always_Follows2], auto)
    apply (rule Follows_setsum)
    apply (cut_tac Distrib_spec)
    apply (auto simp add: distr_spec_def distr_follows_def o_def)
    apply (drule guaranteesD)
      prefer 3
      apply (best intro: mono_bag_of [THEN mono_Follows_apply, THEN subsetD], auto)
    done

    subsection{*Theorems for Allocator*}

    lemma alloc_refinement_lemma:
         "!!f::nat=>nat. (\<Inter>i ∈ lessThan n. {s. f i ≤ g i s})
          ⊆ {s. (SUM x: lessThan n. f x) ≤ (SUM x: lessThan n. g x s)}"
    apply (induct_tac "n")
    apply (auto simp add: lessThan_Suc)
    done

    lemma alloc_refinement:
    "(\<Inter>i ∈ lessThan Nclients. Increasing (sub i o allocAsk) Int
                               Increasing (sub i o allocRel))
      Int
      Always {s. ∀i. i<Nclients -->
                  (∀elt ∈ set ((sub i o allocAsk) s). elt ≤ NbT)}
      Int
      (\<Inter>i ∈ lessThan Nclients.
       \<Inter>h. {s. h ≤ (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s}
            LeadsTo {s. tokens h ≤ (tokens o sub i o allocRel)s})
      ⊆
     (\<Inter>i ∈ lessThan Nclients. Increasing (sub i o allocAsk) Int
                               Increasing (sub i o allocRel))
      Int
      Always {s. ∀i. i<Nclients -->
                  (∀elt ∈ set ((sub i o allocAsk) s). elt ≤ NbT)}
      Int
      (\<Inter>hf. (\<Inter>i ∈ lessThan Nclients.
             {s. hf i ≤ (sub i o allocGiv)s & hf i pfixGe (sub i o allocAsk)s})
      LeadsTo {s. (∑i ∈ lessThan Nclients. tokens (hf i)) ≤
                  (∑i ∈ lessThan Nclients. (tokens o sub i o allocRel)s)})"
    apply (auto simp add: ball_conj_distrib)
    apply (rename_tac F hf)
    apply (rule LeadsTo_weaken_R [OF Finite_stable_completion alloc_refinement_lemma], blast, blast)
    apply (subgoal_tac "F ∈ Increasing (tokens o (sub i o allocRel))")
     apply (simp add: Increasing_def o_assoc)
    apply (blast intro: mono_tokens [THEN mono_Increasing_o, THEN subsetD])
    done

    end

### Theorems for Merge

lemma Merge_Allowed:

      Merge M ==> Allowed M = preserves merge.Out ∩ preserves iOut

lemma M_ok_iff:

      Merge M
      ==> M ok G = (G ∈ preserves merge.Out ∧ G ∈ preserves iOut ∧ M ∈ Allowed G)

lemma Merge_Always_Out_eq_iOut:

      [| Merge M; G ∈ preserves merge.Out; G ∈ preserves iOut; M ∈ Allowed G |]
      ==> M Join G ∈ Always {s. length (merge.Out s) = length (iOut s)}

lemma Merge_Bounded:

      [| Merge M; G ∈ preserves iOut; G ∈ preserves merge.Out; M ∈ Allowed G |]
      ==> M Join G ∈ Always {s. ∀elt∈set (iOut s). elt < Nclients}

lemma Merge_Bag_Follows_lemma:

      [| Merge M; G ∈ preserves iOut; G ∈ preserves merge.Out; M ∈ Allowed G |]
      ==> M Join G
          ∈ Always
             {s. (∑i<Nclients.
                     bag_of
                      (sublist (merge.Out s)
                        {k. k < length (iOut s) ∧ iOut s ! k = i})) =
                 (bag_of o merge.Out) s}

lemma Merge_Bag_Follows:

      Merge M
      ==> M ∈ (INT i<Nclients. Increasing (sub i o merge.In)) guarantees
              (bag_of o merge.Out) Fols
              (%s. ∑i<Nclients. (bag_of o sub i o merge.In) s)

### Theorems for Distributor

lemma Distr_Increasing_Out:

      Distrib D
      ==> D ∈ Increasing distr.In ∩ Increasing iIn ∩
              Always {s. ∀elt∈set (iIn s). elt < Nclients} guarantees
              (INT i<Nclients. Increasing (sub i o distr.Out))

lemma Distr_Bag_Follows_lemma:

      [| Distrib D; G ∈ preserves distr.Out;
         D Join G ∈ Always {s. ∀elt∈set (iIn s). elt < Nclients} |]
      ==> D Join G
          ∈ Always
             {s. (∑i<Nclients.
                     bag_of
                      (sublist (distr.In s)
                        {k. k < length (iIn s) ∧ iIn s ! k = i})) =
                 bag_of (sublist (distr.In s) {..<length (iIn s)})}

lemma D_ok_iff:

      Distrib D ==> D ok G = (G ∈ preserves distr.Out ∧ D ∈ Allowed G)

lemma Distr_Bag_Follows:

      Distrib D
      ==> D ∈ Increasing distr.In ∩ Increasing iIn ∩
              Always {s. ∀elt∈set (iIn s). elt < Nclients} guarantees
              (INT i<Nclients.
                  (%s. ∑i<Nclients. (bag_of o sub i o distr.Out) s) Fols
                  (%s. bag_of (sublist (distr.In s) {..<length (iIn s)})))

### Theorems for Allocator

lemma alloc_refinement_lemma:

      (INT i<n. {s. f i ≤ g i s}) ⊆ {s. setsum f {..<n} ≤ (∑x<n. g x s)}

lemma alloc_refinement:

      (INT i<Nclients.
          Increasing (sub i o allocAsk) ∩ Increasing (sub i o allocRel)) ∩
      Always {s. ∀i<Nclients. ∀elt∈set ((sub i o allocAsk) s). elt ≤ NbT} ∩
      (INT i<Nclients.
          INT h. {s. h ≤ (sub i o allocGiv) s ∧ h pfixGe (sub i o allocAsk) s} LeadsTo
                 {s. tokens h ≤ (tokens o sub i o allocRel) s})
      ⊆ (INT i<Nclients.
            Increasing (sub i o allocAsk) ∩ Increasing (sub i o allocRel)) ∩
        Always {s. ∀i<Nclients. ∀elt∈set ((sub i o allocAsk) s). elt ≤ NbT} ∩
        (INT hf.
            (INT i<Nclients.
                {s. hf i ≤ (sub i o allocGiv) s ∧
                    hf i pfixGe (sub i o allocAsk) s}) LeadsTo
            {s. (∑i<Nclients. tokens (hf i))
                ≤ (∑i<Nclients. (tokens o sub i o allocRel) s)})