Theory Dynamic

(* Dynamic semantics *)
theory Dynamic
  imports Main "HOL-Library.Multiset"
  Exp
begin

(* Check if authority has enough permissions to see the fact *)
definition can_see_fact :: "auth ⇒ fact ⇒ bool" where
"can_see_fact a f ≡ {} ≠ (a ∩ (fact_by f ∪ fact_obs f))"

(* Predicate for gathering facts, as in set comprehension in EvGather rule in paper *)
definition check_gather :: "auth ⇒ fact_env ⇒ fact_var ⇒ fact_ctor ⇒ bool exp ⇒ fact ⇒ bool" where
"check_gather Asub h v ctor pred f =
  (fact_name f = ctor ∧
  can_see_fact Asub f ∧
  pred (h(v := f)))"

inductive EvGather :: "auth ⇒ store ⇒ fact_env ⇒ fact_var ⇒ gather ⇒ store ⇒ bool"
    ("_ | _ | _ | _ ⊢ _ ⇓ _ GATHER" [900,900,900,900,900,900] 1000) where
(* For the notation, require parentheses for almost anything other than function application.
   This should hopefully keep the grammar unambiguous. *)
  EvGather: "fs = filter_mset (check_gather Asub h v ctor pred) s ⟹
    Asub | s | h | v ⊢ gather_when ctor pred ⇓ fs GATHER"


(* Get all the facts with a minimum value according to some scoring function *)
definition find_firsts :: "store ⇒ fact_env ⇒ fact_var ⇒ nat exp ⇒ store" where
"find_firsts fs env v x = (
       let score = (λf. x (env (v := f)))
    in let v' = Min (score ` set_mset fs)
    in filter_mset (λf. score f = v') fs)"

(* Dynamic semantics for select *)
inductive EvSelect :: "store ⇒ fact_env ⇒ fact_var ⇒ select ⇒ fact ⇒ bool"
    ("_ | _ | _ ⊢ _ ⇓ _ SELECT" [900,900,900,900,900] 1000) where
  EvAny: "f ∈# fs ⟹
     fs | _ | _ ⊢ select_any ⇓ f SELECT"
| EvFirst: "f ∈# find_firsts fs h v e ⟹
     fs | h | v ⊢ select_first e ⇓ f SELECT"

inductive_cases EvSelect_inverts:
  "fs | h | v ⊢ select_any ⇓ f SELECT"
  "fs | h | v ⊢ select_first e ⇓ f SELECT"

inductive EvConsume :: "rule_name ⇒ fact ⇒ fact_env ⇒ consume ⇒ nat ⇒ bool"
    ("_ | _ | _ ⊢ _ ⇓ _ CONSUME" [900,900,900,900,900] 1000) where
  EvConsumeNone:
   "w h = 0 ⟹
    n | f | h ⊢ consume_weight w ⇓ 0 CONSUME"
| EvConsumeSome:
   "w h = w_need ⟹
    w_need > 0 ⟹
    n ∈ fact_rules f ⟹
    n | f | h ⊢ consume_weight w ⇓ w_need CONSUME"

inductive_cases EvConsume_inverts:
  "n | f | h ⊢ consume_weight w ⇓ 0 CONSUME"
  "n | f | h ⊢ consume_weight w ⇓ w_need CONSUME"


inductive EvGain :: "rule_name ⇒ fact ⇒ fact_env ⇒ gain ⇒ auth ⇒ bool"
    ("_ | _ | _ ⊢ _ ⇓ _ GAIN" [900,900,900,900,900] 1000) where
  EvGainNone:
  "t h = {} ⟹
   n | f | h ⊢ gain_auth t ⇓ {} GAIN"
| EvGainSome:
  "t h = a ⟹
   a ⊆ fact_by f ⟹
   n ∈ fact_rules f ⟹
   n | f | h ⊢ gain_auth t ⇓ a GAIN"

inductive_cases EvGain_inverts:
  "n | f | h ⊢ gain_auth t ⇓ {} GAIN"
  "n | f | h ⊢ gain_auth t ⇓ a GAIN"


inductive EvExec :: "fact_env ⇒ store exp ⇒ store ⇒ bool"
    ("_ ⊢ _ ⇓ _ EXEC" [900,900,900] 1000) where
  EvExec: "t h = s' ⟹
   h ⊢ t ⇓ s' EXEC"


inductive EvMatch :: "rule_name ⇒ auth ⇒ store ⇒ fact_env ⇒ match ⇒ factoid ⇒ auth ⇒ fact_env ⇒ bool"
    ("_ | _ | _ | _ ⊢ _ ⇓ _ | _ | _ MATCH" [900,900,900,900,900,900,900,900] 1000) where
  EvMatch: "
       asub | s | h | x  ⊢ gather ⇓ fs     GATHER  ⟹
             fs | h | x  ⊢ sel    ⇓ f      SELECT  ⟹
         rn | f |     h' ⊢ con    ⇓ w      CONSUME ⟹
         rn | f |     h' ⊢ gain   ⇓ again  GAIN    ⟹
    h' = h(x := f)                                 ⟹
    rn | asub | s | h ⊢ match x gather sel con gain ⇓ (f,w) | again | h' MATCH"

(* rn | asub | s | h ⊢ ms ⇓ fread | dspent | ahas | h' MATCHES
  In the paper fread is a set, but we use a multiset here because reasoning about converting sets
  to multisets requires lots of little conversion lemmas that aren't in the standard library.
*)
inductive EvMatches :: "rule_name ⇒ auth ⇒ store ⇒ fact_env ⇒ match list ⇒ store ⇒ store ⇒ auth ⇒ fact_env ⇒ bool"
    ("_ | _ | _ | _ ⊢ _ ⇓ _ | _ | _ | _ MATCHES" [900,900,900,900,900,900,900,900,900] 1000) where
  EvMatchNil:
    "n | a | s | h ⊢ [] ⇓ {#} | {#} | {} | h MATCHES"
  | EvMatchCons: "
    n | a | s | h  ⊢      m   ⇓   (f,w)  | ag  | h'  MATCH   ⟹
    n | a | s | h' ⊢      ms  ⇓  fs | ds | ag' | h'' MATCHES ⟹
    fs'  = {#f#} ∪# fs                                       ⟹
    ds'  = replicate_mset w f + ds                           ⟹
    ag'' = ag ∪ ag'                                          ⟹
    n | a | s | h  ⊢ (m # ms) ⇓ fs' | ds' | ag'' |  h'' MATCHES"

inductive_cases EvMatches_inverts:
  "n | a | s | h ⊢ [] ⇓ fs' | ds' | ag'' | h' MATCHES"
  "n | a | s | h  ⊢ (m # ms) ⇓ fs' | ds' | ag'' |  h'' MATCHES"

inductive EvFire :: "auth ⇒ store ⇒ rule ⇒ store ⇒ store ⇒ store ⇒ store ⇒ bool"
    ("_ | _ ⊢ _ ⇓ _ | _ | _ | _ FIRE" [900,900,900,900,900,900,900] 1000) where
  EvFire: "
    rn | asub | s | (λ_. undefined) ⊢ matches ⇓ fread | dspent | ahas | h' MATCHES ⟹
                                 h' ⊢ say     ⇓ dnew                       EXEC    ⟹
    dspent ⊆# s                                                                    ⟹
    s' = ((s - dspent) + dnew)                                                     ⟹
    (∀f ∈# dnew. fact_by f ⊆ ahas)                                                 ⟹
               asub | s ⊢ rule rn matches say ⇓ fread | dspent | dnew | s' FIRE"

end