Theory signed_div

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

theory signed_div
imports "AutoCorres2.CTranslation"
begin

install_C_file "signed_div.c"

lemma exec_lvar_nondet_init_simp: "(Γ⊢ ⟨lvar_nondet_init upd, Normal s⟩ ⇒ t) = (∃v. t = Normal (upd (λ_. v) s))"
  apply (simp add: lvar_nondet_init_def)
  apply (subst exec.simps)
  apply auto
  done

lemma ex_extend:"((∃v. s = f v) ∧ P s) = (∃v. s = f v ∧ P (f v))"
by auto




lemma (in signed_div_global_addresses) includes f_variables shows f_result:
  "Γ ⊢ ⦃ True ⦄ ´ret' :== CALL f(5, -1) ⦃ ´ret' = -5 ⦄"
  apply vcg
  apply (clarsimp simp: sdiv_word_def sdiv_int_def)
  done

lemma (in signed_div_global_addresses) includes f_variables shows f_overflow:
  "⟦ s ⋅⇩ℒ a = of_int (- (2^31)); s ⋅⇩ℒ b = -1 ⟧ ⟹ Γ ⊢ ⟨ Call signed_div.f ,Normal s⟩ ⇒ Fault SignedArithmetic"
  apply (rule exec.Call [where Γ=Γ, OF f_impl, simplified f_body_def creturn_def])
  apply (rule exec.CatchMiss)
  apply (subst exec.simps, clarsimp simp del: word_neq_0_conv simp: sdiv_word_def sdiv_int_def)
  apply (rule_tac x = "Fault SignedArithmetic" in exI)
  apply (subst exec.simps, clarsimp simp del: word_neq_0_conv simp: sdiv_word_def sdiv_int_def)
  apply (subst exec_lvar_nondet_init_simp)
  apply (subst (1) ex_extend)
  apply (subst exec.simps, clarsimp simp del: word_neq_0_conv simp: sdiv_word_def sdiv_int_def)
  apply (subst exec.simps, clarsimp simp del: word_neq_0_conv simp: sdiv_word_def sdiv_int_def)
  apply simp 
  done

lemma (in signed_div_global_addresses) includes g_variables shows g_result:
  "Γ ⊢ ⦃ True ⦄ ´ret' :== CALL g(-5, 10) ⦃ ´ret' = -5 ⦄"
  apply vcg
  apply (clarsimp simp: smod_word_def smod_int_def sdiv_int_def)
  done

lemma (in signed_div_global_addresses) includes h_variables shows h_result:
  "Γ ⊢ ⦃ True ⦄ ´ret' :== CALL h(5, -1) ⦃ ´ret' = 0 ⦄"
  apply vcg
  apply (simp add: word_div_def uint_word_ariths)
  done

lemma (in signed_div_global_addresses) includes f_variables shows i_result:
  "Γ ⊢ ⦃ True ⦄ ´ret' :== CALL f(5, -1) ⦃ ´ret' = -5 ⦄"
  apply vcg
  apply (clarsimp simp: sdiv_word_def sdiv_int_def)
  done

end