Theory mmio_assume

(*
 * Copyright (c) 2022 Apple Inc. All rights reserved.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

(*
 * Tests for handling Spec constructs emitted by the C parser.
 *)
theory mmio_assume
imports "AutoCorres2_Main.AutoCorres_Main"
begin

text ‹A variant of theory ‹mmio›, but assuming (instead of specifying) hardware behaviour.›

declare [[c_parser_assume_fnspec]]

text ‹Some placeholders for a 'hardware-step' relation.›

consts abs_step:: "word32 ⇒ word32 ⇒ bool"
consts abs_step2:: "(word32 × word32) ⇒ (word32 × word32) ⇒ bool"

declare [[c_parser_feedback_level=2]]
include_C_file "mmio.c" for "mmio_assume.c"
install_C_file "mmio_assume.c"

ML_val ‹
val x1 =  Proof_Context.read_typ @{context} "globals"
val x2 =  Proof_Context.read_typ @{context} "mmio_assume.globals"
›
(* check handling of spec-body trughout locale generation. What do we expect?*)
(* currently non-proto funs are imported to all_impl/corres. We should also add those for which
a spec-body is defined? get_defined_functions? *)

init-autocorres [in_out_parameters=(* testing IO abstraction for ‹L2_assume›*)] "mmio_assume.c"


autocorres [ts_rules = nondet] "mmio_assume.c"


lemma "step_body ≡
spec_pre_post ImpossibleSpec AssumeError
 {s. ∃st. s ∈ {s. state_' (globals s) = st}}
 ({(s, t).
   (∀st. s ∈ {s. state_' (globals s) = st} ⟶ t ∈ ⦃abs_step st ´state⦄) ∧
   (∃st. s ∈ {s. state_' (globals s) = st})} ∩
  {(s, t). t may_only_modify_globals s in [state]})"
  by (rule step_body_def)

lemma
  "step' ≡ assume_result_and_state (λa.
    {(u, t). abs_step (state_'' a) (state_'' t) ∧ (∃state_'. t = a⦇state_'' := state_'⦈)})"
  by (rule step'_def)

lemma "step2' ≡
assume_result_and_state
 (λa. {(u, t).
        abs_step2 (g1_'' a, g2_'' a) (g1_'' t, g2_'' t) ∧
        (∃g1_' g2_'. t = a⦇g1_'' := g1_', g2_'' := g2_'⦈)})"
  by (rule step2'_def)

lemma "unreachable_body ≡
spec_pre_post ImpossibleSpec AssumeError {s. s ∈ ⦃False⦄}
 ({(s, t). (s ∈ ⦃False⦄ ⟶ t ∈ ⦃True⦄) ∧ s ∈ ⦃False⦄} ∩
  {(s, t). t may_not_modify_globals s})"
  by (rule unreachable_body_def)

lemma "unreachable' ≡ fail"
  by (rule unreachable'_def)

lemma "empty_body ≡
spec_pre_post ImpossibleSpec AssumeError {s. s ∈ ⦃´state < 0x2A⦄}
 ({(s, t). (s ∈ ⦃´state < 0x2A⦄ ⟶ t ∈ ⦃False⦄) ∧ s ∈ ⦃´state < 0x2A⦄} ∩
  {(s, t). t may_not_modify_globals s})"
  by (rule empty_body_def)

lemma "empty' ≡ do {
  v ← guard (λs. state_'' s < 0x2A);
  assume_result_and_state (λa. {})
}"
  by (rule empty'_def)

end