Theory fncall

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

theory fncall
imports "AutoCorres2.CTranslation"
begin

declare sep_conj_ac [simp add]

primrec
  fac :: "nat ⇒ nat"
where
  "fac 0 = 1"
| "fac (Suc n) = (Suc n) * fac n"


install_C_file "fncall.c"

context fncall_simpl
begin


thm has_bogus_spec_impl
thm f_impl
thm g_impl
thm h_impl
thm i_impl
thm calls_bogus_impl
thm f_body_def
thm g_body_def
thm fact_body_def


thm has_bogus_spec_modifies
thm g_modifies
thm f_modifies
thm fact_modifies

term "f_body"
term "fact_body"

end

print_locale fncall_global_addresses

print_locale g_modifies
thm g_modifies_def

print_locale f_spec
thm f_spec_def

lemma (in g_impl)
  shows "Γ ⊢ ⦃ ´t_hrs = t ⦄ ´ret' :== PROC g() ⦃ ´t_hrs = t ⦄"
  apply (hoare_rule HoarePartial.ProcRec1)
  apply (vcg, simp)
done


lemma (in f_impl) f_impl_result:
  "Γ fncall.f = Some f_body"
  apply (rule f_impl)
  done

lemma (in g_impl) g_spec:
  shows
  "Γ ⊢ ⦃ True ⦄ ´ret' :== PROC g() ⦃ ´ret' = 257 ⦄"
  apply vcg
  apply simp
  done

lemma (in f_impl) foo:
  shows
   "Γ ⊢ ⦃ True ⦄ ´ret' :== PROC f(n) ⦃ ´ret' = 1 ⦄"
apply vcg
apply (simp )
done

lemma (in f_spec) foo :
shows
  "Γ ⊢ ⦃ True ⦄ ´ret' :== CALL f(´n) ⦃ ´ret' = 1 ⦄"

apply vcg
done

lemma (in fact_impl) bar:
shows "Γ ⊢ ⦃ 1≤ ´n & ´n ≤ 12 ⦄ ´ret' :== CALL fact(´n) ⦃ ´ret' = of_nat (fac (unat ´n)) ⦄"
apply vcg
    apply unat_arith
    apply simp
   apply simp
oops


context h_impl 
begin
interpretation h_modif: h_modifies
  apply (unfold_locales)
  apply (vcg)
  apply (simp add: meq_def)
  done

lemmas h_modifies' = h_modif.h_modifies

end

(* FIXME: I guess the issue is that A is implicitly the empty set and
this does not match with the catch rule! 
Maybe we can decouple the spec=modifies and the "real" modifies solver...
We could check if the post-conditions are canonical and only then go into
solver mode...
 *)


lemma (in i_impl) baz:
notes h_modifies = h_modifies'
shows "Γ ⊢⇘/UNIV⇙ ⦃ ´t_hrs = t ⦄ ´ret' :== PROC i() ⦃ ´t_hrs = t ⦄"

  apply (hoare_rule HoarePartial.ProcRec1)
  apply (vcg spec=modifies)
  apply simp
done

locale ih = i_impl + i_modifies + h_modifies
lemma (in ih) qux:
shows "Γ ⊢ ⦃´t_hrs = t⦄ ´ret' :== CALL i() ⦃ t = ´t_hrs ⦄"
  apply vcg
  apply simp
oops

locale ff = f_spec + f_modifies
(* this lemma is bogus, because f does actually modify the globals *)
lemma (in ff) bogus1:
shows "Γ ⊢ ⦃ ´t_hrs = t ⦄ ´ret' :== CALL f(´n) ⦃ t = ´t_hrs ⦄"
apply vcg
apply simp
done

lemma (in has_bogus_spec_spec) bogus2:
shows "Γ ⊢ ⦃ True ⦄ ´ret' :== CALL has_bogus_spec() ⦃ ´ret' = 4 ⦄"
apply vcg
done

lemma (in has_bogus_spec_impl) toldyou:
shows "Γ ⊢ ⦃ True ⦄ ´ret' :== CALL has_bogus_spec() ⦃ ´ret' = 3 ⦄"
  apply vcg
  apply simp
done

locale calls_bogus_impl_bogus_spec = has_bogus_spec_spec + calls_bogus_impl

lemma (in calls_bogus_impl_bogus_spec) bogus3:
shows "Γ ⊢ ⦃ True ⦄ ´ret' :== CALL calls_bogus() ⦃ ´ret' = 4 ⦄"
  apply vcg
  apply simp
done

end