Theory ObjectMonad

(***********************************************************************************
 * Copyright (c) 2016-2018 The University of Sheffield, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 * * Redistributions of source code must retain the above copyright notice, this
 *   list of conditions and the following disclaimer.
 *
 * * Redistributions in binary form must reproduce the above copyright notice,
 *   this list of conditions and the following disclaimer in the documentation
 *   and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 * 
 * SPDX-License-Identifier: BSD-2-Clause
 ***********************************************************************************)

section‹Object›
text‹In this theory, we introduce the monadic method setup for the Object class.›
theory ObjectMonad
  imports
    BaseMonad
    "../classes/ObjectClass"
begin

type_synonym ('object_ptr, 'Object, 'result) dom_prog
  = "((_) heap, exception, 'result) prog"
register_default_tvars "('object_ptr, 'Object, 'result) dom_prog" 

global_interpretation l_ptr_kinds_M object_ptr_kinds defines object_ptr_kinds_M = a_ptr_kinds_M .
lemmas object_ptr_kinds_M_defs = a_ptr_kinds_M_def


global_interpretation l_dummy defines get_MObject = "l_get_M.a_get_M getObject" .
lemma get_M_is_l_get_M: "l_get_M getObject type_wf object_ptr_kinds"
  by (simp add: a_type_wf_def getObject_type_wf l_get_M_def)
lemmas get_M_defs = get_MObject_def[unfolded l_get_M.a_get_M_def[OF get_M_is_l_get_M]]

adhoc_overloading get_M get_MObject

locale l_get_MObject_lemmas = l_type_wfObject
begin
interpretation l_get_M getObject type_wf object_ptr_kinds
  apply(unfold_locales)
   apply (simp add: getObject_type_wf local.type_wfObject)
  by (simp add: a_type_wf_def getObject_type_wf)
lemmas get_MObject_ok = get_M_ok[folded get_MObject_def]
lemmas get_MObject_ptr_in_heap = get_M_ptr_in_heap[folded get_MObject_def]
end

global_interpretation l_get_MObject_lemmas type_wf
  by (simp add: l_get_MObject_lemmas_def l_type_wfObject_axioms)

lemma object_ptr_kinds_M_reads: 
  "reads (⋃object_ptr. {preserved (get_MObject object_ptr RObject.nothing)}) object_ptr_kinds_M h h'"
  apply(auto simp add: object_ptr_kinds_M_defs getObject_type_wf type_wf_defs reads_def 
      preserved_def get_M_defs  
      split: option.splits)[1]
  using a_type_wf_def getObject_type_wf by blast+


global_interpretation l_put_M type_wf object_ptr_kinds getObject putObject 
  rewrites "a_get_M = get_MObject" 
  defines put_MObject = a_put_M
   apply (simp add: get_M_is_l_get_M l_put_M_def)
  by (simp add: get_MObject_def)
lemmas put_M_defs = a_put_M_def
adhoc_overloading put_M put_MObject


locale l_put_MObject_lemmas = l_type_wfObject
begin
interpretation l_put_M  type_wf object_ptr_kinds getObject putObject
  apply(unfold_locales)
  using getObject_type_wf l_type_wfObject.type_wfObject local.l_type_wfObject_axioms apply blast
  by (simp add: a_type_wf_def getObject_type_wf)
lemmas put_MObject_ok = put_M_ok[folded put_MObject_def]
lemmas put_MObject_ptr_in_heap = put_M_ptr_in_heap[folded put_MObject_def]
end

global_interpretation l_put_MObject_lemmas type_wf
  by (simp add: l_put_MObject_lemmas_def l_type_wfObject_axioms)


definition check_in_heap :: "(_) object_ptr ⇒ (_, unit) dom_prog"
  where
    "check_in_heap ptr = do {
      h ← get_heap;
      (if ptr |∈| object_ptr_kinds h then
        return ()
      else
        error SegmentationFault
      )}"

lemma check_in_heap_ptr_in_heap: "ptr |∈| object_ptr_kinds h ⟷ h ⊢ ok (check_in_heap ptr)"
  by(auto simp add: check_in_heap_def)
lemma check_in_heap_pure [simp]: "pure (check_in_heap ptr) h"
  by(auto simp add: check_in_heap_def intro!: bind_pure_I)
lemma check_in_heap_is_OK [simp]: 
  "ptr |∈| object_ptr_kinds h ⟹ h ⊢ ok (check_in_heap ptr ⤜ f) = h ⊢ ok (f ())"
  by(simp add: check_in_heap_def)
lemma check_in_heap_returns_result [simp]: 
  "ptr |∈| object_ptr_kinds h ⟹ h ⊢ (check_in_heap ptr ⤜ f) →r x = h ⊢ f () →r x"
  by(simp add: check_in_heap_def)
lemma check_in_heap_returns_heap [simp]: 
  "ptr |∈| object_ptr_kinds h ⟹ h ⊢ (check_in_heap ptr ⤜ f) →h h' = h ⊢ f () →h h'"
  by(simp add: check_in_heap_def)

lemma check_in_heap_reads: 
  "reads {preserved (get_M object_ptr nothing)} (check_in_heap object_ptr) h h'"
  apply(simp add: check_in_heap_def reads_def preserved_def)
  by (metis a_type_wf_def get_MObject_ok get_MObject_ptr_in_heap is_OK_returns_result_E 
      is_OK_returns_result_I unit_all_impI)

subsection‹Invoke›

fun invoke_rec :: "(((_) object_ptr ⇒ bool) × ((_) object_ptr ⇒ 'args 
                  ⇒ (_, 'result) dom_prog)) list ⇒ (_) object_ptr ⇒ 'args 
                  ⇒ (_, 'result) dom_prog"
  where
    "invoke_rec ((P, f)#xs) ptr args = (if P ptr then f ptr args else invoke_rec xs ptr args)"
  | "invoke_rec [] ptr args = error InvokeError"

definition invoke :: "(((_) object_ptr ⇒ bool) × ((_) object_ptr ⇒ 'args 
                     ⇒ (_, 'result) dom_prog)) list 
                     ⇒ (_) object_ptr ⇒ 'args ⇒ (_, 'result) dom_prog"
  where                               
    "invoke xs ptr args = do { check_in_heap ptr; invoke_rec xs ptr args}"

lemma invoke_split: "P (invoke ((Pred, f) # xs) ptr args) =
    ((¬(Pred ptr) ⟶ P (invoke xs ptr args))
  ∧ (Pred ptr ⟶ P (do {check_in_heap ptr; f ptr args})))"
  by(simp add: invoke_def)

lemma invoke_split_asm: "P (invoke ((Pred, f) # xs) ptr args) =
    (¬((¬(Pred ptr) ∧ (¬ P (invoke xs ptr args)))
    ∨ (Pred ptr ∧ (¬ P (do {check_in_heap ptr; f ptr args})))))"
  by(simp add: invoke_def)
lemmas invoke_splits = invoke_split invoke_split_asm

lemma invoke_ptr_in_heap: "h ⊢ ok (invoke xs ptr args) ⟹ ptr |∈| object_ptr_kinds h"
  by (metis bind_is_OK_E check_in_heap_ptr_in_heap invoke_def is_OK_returns_heap_I)

lemma invoke_pure [simp]: "pure (invoke [] ptr args) h"
  by(auto simp add: invoke_def intro!: bind_pure_I)

lemma invoke_is_OK [simp]: 
  "ptr |∈| object_ptr_kinds h ⟹ Pred ptr 
    ⟹ h ⊢ ok (invoke ((Pred, f) # xs) ptr args) = h ⊢ ok (f ptr args)"
  by(simp add: invoke_def)
lemma invoke_returns_result [simp]: 
  "ptr |∈| object_ptr_kinds h ⟹ Pred ptr 
   ⟹ h ⊢ (invoke ((Pred, f) # xs) ptr args) →r x = h ⊢ f ptr args →r x"
  by(simp add: invoke_def)
lemma invoke_returns_heap [simp]: 
  "ptr |∈| object_ptr_kinds h ⟹ Pred ptr 
   ⟹ h ⊢ (invoke ((Pred, f) # xs) ptr args) →h h' = h ⊢ f ptr args →h h'"
  by(simp add: invoke_def)

lemma invoke_not [simp]: "¬Pred ptr ⟹ invoke ((Pred, f) # xs) ptr args = invoke xs ptr args"
  by(auto simp add: invoke_def)

lemma invoke_empty [simp]: "¬h ⊢ ok (invoke [] ptr args)"
  by(auto simp add: invoke_def check_in_heap_def)

lemma invoke_empty_reads [simp]: "∀P ∈ S. reflp P ∧ transp P ⟹ reads S (invoke [] ptr args) h h'"
  apply(simp add: invoke_def reads_def preserved_def)
  by (meson bind_returns_result_E error_returns_result)


subsection‹Modified Heaps›

lemma get_object_ptr_simp [simp]: 
  "getObject object_ptr (putObject ptr obj h) = (if ptr = object_ptr then Some obj else get object_ptr h)"
  by(auto simp add: getObject_def putObject_def split: option.splits Option.bind_splits)

lemma object_ptr_kinds_simp [simp]: "object_ptr_kinds (putObject ptr obj h) = object_ptr_kinds h |∪| {|ptr|}"
  by(auto simp add: object_ptr_kinds_def putObject_def split: option.splits)

lemma type_wf_put_I:
  assumes "type_wf h"
  shows "type_wf (putObject ptr obj h)"
  using assms
  by(auto simp add: type_wf_defs split: option.splits)

lemma type_wf_put_ptr_not_in_heap_E:
  assumes "type_wf (putObject ptr obj h)"
  assumes "ptr |∉| object_ptr_kinds h"
  shows "type_wf h"
  using assms
  by(auto simp add: type_wf_defs split: option.splits if_splits)

lemma type_wf_put_ptr_in_heap_E:
  assumes "type_wf (putObject ptr obj h)"
  assumes "ptr |∈| object_ptr_kinds h"
  shows "type_wf h"
  using assms
  by(auto simp add: type_wf_defs split: option.splits if_splits)


subsection‹Preserving Types›

lemma type_wf_preserved: "type_wf h = type_wf h'"
  by(auto simp add: type_wf_defs)


lemma object_ptr_kinds_preserved_small:
  assumes "⋀object_ptr. preserved (get_MObject object_ptr RObject.nothing) h h'"
  shows "object_ptr_kinds h = object_ptr_kinds h'"
  using assms
  apply(auto simp add: object_ptr_kinds_def preserved_def get_M_defs getObject_def 
      split: option.splits)[1]
   apply (metis (mono_tags, lifting) domIff error_returns_result fmdom.rep_eq 
      old.unit.exhaust option.case_eq_if return_returns_result)
  by (metis (mono_tags, lifting) domIff error_returns_result fmdom.rep_eq 
      old.unit.exhaust option.case_eq_if return_returns_result)

lemma object_ptr_kinds_preserved:
  assumes "writes SW setter h h'"
  assumes "h ⊢ setter →h h'"
  assumes "⋀h h' w object_ptr. w ∈ SW ⟹ h ⊢ w →h h' 
          ⟹ preserved (get_MObject object_ptr RObject.nothing) h h'"
  shows "object_ptr_kinds h = object_ptr_kinds h'"
proof -
  {
    fix object_ptr w
    have "preserved (get_MObject object_ptr RObject.nothing) h h'"
      apply(rule writes_small_big[OF assms])
      by auto
  }
  then show ?thesis
    using object_ptr_kinds_preserved_small by blast
qed


lemma reads_writes_preserved2:
  assumes "writes SW setter h h'"
  assumes "h ⊢ setter →h h'"
  assumes "⋀h h' x. ∀w ∈ SW. h ⊢ w →h h' ⟶ preserved (get_MObject ptr getter) h h'"
  shows "preserved (get_M ptr getter) h h'"
  apply(clarsimp simp add: preserved_def)
  using reads_singleton assms(1) assms(2)
  apply(rule reads_writes_preserved)
  using assms(3)
  by(auto simp add: preserved_def)
end