Theory IndirectCalls

(*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 * Copyright (c) 2022 Apple Inc. All rights reserved.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

theory IndirectCalls

imports
  "PrettyProgs"

begin

lemma hoare_indirect_call_known_proc:
assumes spec: "Γ ⊢ P (call_exn init q return result_exn c) Q,A"
shows "Γ⊢ ({s. p s = q} ∩ P) (dynCall_exn f UNIV init p return result_exn c) Q,A"
  using spec
  apply -
  apply (rule hoare_complete, drule hoare_sound)
  apply (clarsimp simp: cvalid_def HoarePartialDef.valid_def dynCall_exn_def)
  apply (auto elim: exec_Normal_elim_cases)
  done


lemma hoare_indirect_call_guard:
assumes conseq: "P ⊆ g ∩ R" 
assumes spec: "Γ ⊢ R (dynCall_exn f UNIV init p return result_exn c) Q,A"
shows "Γ⊢ P (dynCall_exn f g init p return result_exn c) Q,A"
  using spec conseq
  apply -
  apply (rule hoare_complete, drule hoare_sound)
  apply (clarsimp simp: cvalid_def HoarePartialDef.valid_def dynCall_exn_def maybe_guard_def)
  apply (cases "g = UNIV")
  subgoal
    by force
  subgoal
    apply (clarsimp elim: exec_Normal_elim_cases )
    by (meson exec_Normal_elim_cases(5) imageI subsetD)
  done

end