Theory IMAP-def

section ‹IMAP-CRDT Definitions›

text‹We begin by defining the operations on a mailbox state. In addition to the interpretation of 
the operations, we define valid behaviours for the operations as assumptions for the network.
We use the \texttt{network\_with\_constrained\_ops} locale from the framework.›

theory
  "IMAP-def"
  imports
    "CRDT.Network"
begin

datatype ('id, 'a) operation = 
  Create "'id" "'a" | 
  Delete "'id set" "'a" | 
  Append "'id" "'a" | 
  Expunge "'a" "'id" "'id" | 
  Store "'a" "'id" "'id"

type_synonym ('id, 'a) state = "'a ⇒ ('id set × 'id set)"

definition op_elem :: "('id, 'a) operation ⇒ 'a" where
  "op_elem oper ≡ case oper of 
    Create i e ⇒ e | 
    Delete is e ⇒ e | 
    Append i e ⇒ e | 
    Expunge e mo i ⇒ e | 
    Store e mo i ⇒ e"

definition interpret_op :: "('id, 'a) operation ⇒ ('id, 'a) state ⇀ ('id, 'a) state" 
  (‹⟨_⟩› [0] 1000) where
  "interpret_op oper state ≡
    let metadata = fst (state (op_elem oper));
        files = snd (state (op_elem oper));
        after  = case oper of 
          Create i e ⇒ (metadata ∪ {i}, files) |
          Delete is e ⇒ (metadata - is, files - is) |
          Append i e ⇒ (metadata, files ∪ {i}) |
          Expunge e mo i ⇒ (metadata ∪ {i}, files - {mo}) |
          Store e mo i ⇒ (metadata, insert i (files - {mo}))
    in  Some (state ((op_elem oper) := after))"

text‹In the definition of the valid behaviours of the operations, we define additional assumption 
the state where the operation is executed. In essence, a the tag of a \create, \append, \expunge,  
and \store\ operation is identical to the message number and therefore unique. A \delete\ operation 
deletes all metadata and the content of a folder. The \store\ and \expunge\ operations must refer 
to an existing message.›

definition valid_behaviours :: "('id, 'a) state ⇒ 'id × ('id, 'a) operation ⇒ bool" where
  "valid_behaviours state msg ≡
    case msg of
      (i, Create j e) ⇒ i = j |
      (i, Delete is e) ⇒ is = fst (state e) ∪ snd (state e) |
      (i, Append j e) ⇒ i = j |
      (i, Expunge e mo j) ⇒ i = j ∧ mo ∈ snd (state e) |
      (i, Store e mo j) ⇒ i = j ∧ mo ∈ snd (state e)"

locale imap = network_with_constrained_ops _ interpret_op "λx. ({},{})" valid_behaviours

end