Theory arithmetic_right_shift

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

theory arithmetic_right_shift
imports "AutoCorres2.CTranslation"
begin

declare [[arithmetic_right_shift]]
install_C_file "arithmetic_right_shift.c"

context f_impl
begin

lemma "Γ ⊢ ⦃ -1 = ´c ⦄ ´ret' :== CALL f() ⦃ ´ret' = -1 ⦄"
  by vcg (auto simp: sshiftr_n1)

end

context g_impl
begin

lemma "Γ ⊢ ⦃ u = ´u ⦄ ´ret' :== CALL g() ⦃ ´ret' = u >> 5 ⦄"
  by vcg simp_all

end

end