Theory WordAbs

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

theory WordAbs
imports "AutoCorres2_Main.AutoCorres_Main"
begin

install_C_file "word_abs.c"
autocorres
  [ (* signed_word_abs is implicit; these are the functions that would be abstracted: *)
    (*signed_word_abs =
        S_add_S S_sub_S S_mul_S S_div_S S_mod_S neg_S
        S_and_S S_or_S S_xor_S not_S
        U_shiftl_U_abs_S U_shiftr_U_abs_S U_shiftl_S_abs_S U_shiftr_S_abs_S
        S_shiftl_U_abs_S S_shiftr_U_abs_S S_shiftl_S_abs_S S_shiftr_S_abs_S
        U_shiftl_U_abs_US U_shiftr_U_abs_US U_shiftl_S_abs_US U_shiftr_S_abs_US
        S_shiftl_U_abs_US S_shiftr_U_abs_US S_shiftl_S_abs_US S_shiftr_S_abs_US
  ,*) no_signed_word_abs =
        U_shiftl_U_no_abs U_shiftr_U_no_abs U_shiftl_S_no_abs U_shiftr_S_no_abs
        S_shiftl_U_no_abs S_shiftr_U_no_abs S_shiftl_S_no_abs S_shiftr_S_no_abs
        U_shiftl_U_abs_U U_shiftr_U_abs_U U_shiftl_S_abs_U U_shiftr_S_abs_U
        S_shiftl_U_abs_U S_shiftr_U_abs_U S_shiftl_S_abs_U S_shiftr_S_abs_U
  , unsigned_word_abs =
        ver366
        U_add_U U_sub_U U_mul_U U_div_U U_mod_U neg_U
        U_and_U U_or_U U_xor_U not_U
        U_shiftl_U_abs_U U_shiftr_U_abs_U U_shiftl_S_abs_U U_shiftr_S_abs_U
        S_shiftl_U_abs_U S_shiftr_U_abs_U S_shiftl_S_abs_U S_shiftr_S_abs_U
        U_shiftl_U_abs_US U_shiftr_U_abs_US U_shiftl_S_abs_US U_shiftr_S_abs_US
        S_shiftl_U_abs_US S_shiftr_U_abs_US S_shiftl_S_abs_US S_shiftr_S_abs_US
  , ts_rules = nondet
] "word_abs.c"

context word_abs_all_impl begin


lemma "(ver366' 0) ∙ s ⦃ λr _. r = Result 0⦄"
  unfolding ver366'_def
  by (runs_to_vcg)


lemma "(ver366' UINT_MAX) ∙ s ⦃λr _. r = Result (UINT_MAX - 1)⦄"
  unfolding ver366'_def
  by (runs_to_vcg)

section ‹Arithmetic ops›
thm S_add_S'_def S_sub_S'_def S_mul_S'_def S_div_S'_def S_mod_S'_def neg_S'_def
    U_add_U'_def U_sub_U'_def U_mul_U'_def U_div_U'_def U_mod_U'_def neg_U'_def

lemma "x + y < INT_MIN ∨ x + y > INT_MAX ⟹ ¬ (succeeds (S_add_S' (x::int) (y::int)) s)"
  unfolding S_add_S'_def runs_to_def_old
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def INT_MIN_def INT_MAX_def)

lemma "INT_MIN ≤ x + y ⟹ x + y ≤ INT_MAX ⟹ P s ⟹
         S_add_S' (x::int) (y::int) ∙ s
       ⦃λr s. r = Result (x + y) ∧ P s⦄"
  unfolding S_add_S'_def 
  by (runs_to_vcg ‹simp add: INT_MIN_def INT_MAX_def›)

lemma "x - y < INT_MIN ∨ x - y > INT_MAX ⟹ ¬ succeeds (S_sub_S' (x::int) (y::int)) s"
  unfolding S_sub_S'_def runs_to_def_old
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def INT_MIN_def INT_MAX_def)

lemma "INT_MIN ≤ x - y ⟹ x - y ≤ INT_MAX ⟹ P s ⟹
         S_sub_S' (x::int) (y::int) ∙ s
       ⦃λr s. r = Result (x - y) ∧ P s⦄"
  unfolding S_sub_S'_def
  by (runs_to_vcg ‹simp add: INT_MIN_def INT_MAX_def›)

lemma "x * y < INT_MIN ∨ x * y > INT_MAX ⟹ ¬ succeeds (S_mul_S' (x::int) (y::int)) s"
  unfolding S_mul_S'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def INT_MIN_def INT_MAX_def)

lemma "INT_MIN ≤ x * y ⟹ x * y ≤ INT_MAX ⟹ P s ⟹
         S_mul_S' (x::int) (y::int) ∙ s
       ⦃λr s. r = Result (x * y) ∧ P s⦄"
  unfolding S_mul_S'_def
  by (runs_to_vcg ‹simp add: INT_MIN_def INT_MAX_def›)


lemma "y = 0 ∨ x sdiv y < INT_MIN ∨ x sdiv y > INT_MAX ⟹ ¬ succeeds (S_div_S' (x::int) (y::int)) s"
  unfolding S_div_S'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def INT_MIN_def INT_MAX_def)

lemma "y ≠ 0 ∧ INT_MIN ≤ x sdiv y ⟹ x sdiv y ≤ INT_MAX ⟹ P s ⟹
         S_div_S' (x::int) (y::int) ∙ s
       ⦃λr s. r = Result (x sdiv y) ∧ P s⦄"
  unfolding S_div_S'_def
  by (runs_to_vcg ‹simp add: INT_MIN_def INT_MAX_def›)

lemma "y = 0 ∨ x smod y < INT_MIN ∨ x smod y > INT_MAX ⟹ ¬ succeeds (S_mod_S' (x::int) (y::int)) s"
  unfolding S_mod_S'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def INT_MIN_def INT_MAX_def)

lemma "y ≠ 0 ∧ INT_MIN ≤ x smod y ⟹ x smod y ≤ INT_MAX ⟹ P s ⟹
         S_mod_S' (x::int) (y::int) ∙ s
       ⦃λr s. r = Result (x smod y) ∧ P s⦄"
  unfolding S_mod_S'_def
  by (runs_to_vcg ‹simp add: INT_MIN_def INT_MAX_def›)

lemma "x ≤ INT_MIN ∨ x > -INT_MIN ⟹ ¬ succeeds (neg_S' (x::int)) s"
  unfolding neg_S'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def INT_MIN_def INT_MAX_def)

lemma "INT_MIN < x ⟹ x ≤ -INT_MIN ⟹ P s ⟹ 
  neg_S' (x::int) ∙ s ⦃λr s. r = Result (-x) ∧ P s⦄"
  unfolding neg_S'_def
  by (runs_to_vcg ‹simp add: INT_MIN_def INT_MAX_def›)

lemma "x + y > UINT_MAX ⟹ ¬ succeeds (U_add_U' (x::nat) (y::nat)) s"
  unfolding U_add_U'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def UINT_MAX_def)

lemma "x + y ≤ UINT_MAX ⟹ P s ⟹
         U_add_U' (x::nat) (y::nat) ∙ s
       ⦃λr s. r = Result (x + y) ∧ P s⦄"
  unfolding U_add_U'_def
  by (runs_to_vcg ‹simp add: UINT_MAX_def›)

lemma "x < y ⟹ ¬ succeeds (U_sub_U' (x::nat) (y::nat)) s"
  unfolding U_sub_U'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "x ≥ y ⟹ P s ⟹
         U_sub_U' (x::nat) (y::nat) ∙ s
       ⦃λr s. r = Result (x - y) ∧ P s⦄"
  unfolding U_sub_U'_def
  by (runs_to_vcg)

lemma "x * y > UINT_MAX ⟹ ¬ succeeds (U_mul_U' (x::nat) (y::nat)) s"
  unfolding U_mul_U'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "x * y ≤ UINT_MAX ⟹ P s ⟹
         U_mul_U' (x::nat) (y::nat) ∙ s
       ⦃λr s. r = Result (x * y) ∧ P s⦄"
  unfolding U_mul_U'_def
  by (runs_to_vcg ‹simp add: UINT_MAX_def›)

lemma "y = 0 ⟹ ¬ succeeds (U_div_U' (x::nat) (y::nat)) s"
  unfolding U_div_U'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "y ≠ 0 ⟹ P s ⟹
         U_div_U' (x::nat) (y::nat) ∙ s
       ⦃λr s. r = Result (x div y) ∧ P s⦄"
  unfolding U_div_U'_def
  by (runs_to_vcg ‹simp add: UINT_MAX_def›)

lemma "y = 0 ⟹ ¬ succeeds (U_mod_U' (x::nat) (y::nat)) s"
  unfolding U_mod_U'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "y ≠ 0 ⟹ P s ⟹
         U_mod_U' (x::nat) (y::nat) ∙ s
       ⦃λr s. r = Result (x mod y) ∧ P s⦄"
  unfolding U_mod_U'_def
  by (runs_to_vcg ‹simp add: UINT_MAX_def›)

lemma "P s ⟹ neg_U' (x::nat) ∙ s ⦃λr s. r = Result (if x = 0 then 0 else Suc UINT_MAX - x) ∧ P s⦄"
  unfolding neg_U'_def 
  by (runs_to_vcg ‹simp add: UINT_MAX_def›)

section ‹Bitwise ops›

thm S_and_S'_def S_or_S'_def S_xor_S'_def not_S'_def
    U_and_U'_def U_or_U'_def U_xor_U'_def not_U'_def

lemma "P s ⟹ S_and_S' (x::int) (y::int) ∙ s ⦃λr s. r = Result (x AND y) ∧ P s⦄"
  unfolding S_and_S'_def by runs_to_vcg

lemma "P s ⟹ S_or_S' (x::int) (y::int) ∙ s ⦃λr s. r = Result (x OR y) ∧ P s⦄"
  unfolding S_or_S'_def by runs_to_vcg

lemma "P s ⟹ S_xor_S' (x::int) (y::int) ∙ s ⦃λr s. r = Result (x XOR y) ∧ P s⦄"
  unfolding S_xor_S'_def by runs_to_vcg

lemma "P s ⟹ not_S' (x::int) ∙ s ⦃λr s. r = Result (NOT x) ∧ P s⦄"
  unfolding not_S'_def by runs_to_vcg

lemma "P s ⟹ U_and_U' (x::nat) (y::nat) ∙ s ⦃λr s. r = Result (x AND y) ∧ P s⦄"
  unfolding U_and_U'_def by runs_to_vcg

lemma "P s ⟹ U_or_U' (x::nat) (y::nat) ∙ s ⦃λr s. r = Result (x OR y) ∧ P s⦄"
  unfolding U_or_U'_def by runs_to_vcg

lemma "P s ⟹ U_xor_U' (x::nat) (y::nat) ∙ s ⦃λr s. r = Result (x XOR y) ∧ P s⦄"
  unfolding U_xor_U'_def by runs_to_vcg

lemma "P s ⟹ not_U' (x::nat) ∙ s ⦃λr s. r = Result (UINT_MAX - x) ∧ P s⦄"
  unfolding not_U'_def by runs_to_vcg

section ‹Left shifts›

thm U_shiftl_U_abs_US'_def U_shiftr_U_abs_US'_def U_shiftl_S_abs_US'_def U_shiftr_S_abs_US'_def
    S_shiftl_U_abs_US'_def S_shiftr_U_abs_US'_def S_shiftl_S_abs_US'_def S_shiftr_S_abs_US'_def
thm U_shiftl_U_abs_U'_def U_shiftr_U_abs_U'_def U_shiftl_S_abs_U'_def U_shiftr_S_abs_U'_def
    S_shiftl_U_abs_U'_def S_shiftr_U_abs_U'_def S_shiftl_S_abs_U'_def S_shiftr_S_abs_U'_def
thm U_shiftl_U_abs_S'_def U_shiftr_U_abs_S'_def U_shiftl_S_abs_S'_def U_shiftr_S_abs_S'_def
    S_shiftl_U_abs_S'_def S_shiftr_U_abs_S'_def S_shiftl_S_abs_S'_def S_shiftr_S_abs_S'_def
thm U_shiftl_U_no_abs'_def U_shiftr_U_no_abs'_def U_shiftl_S_no_abs'_def U_shiftr_S_no_abs'_def
    S_shiftl_U_no_abs'_def S_shiftr_U_no_abs'_def S_shiftl_S_no_abs'_def S_shiftr_S_no_abs'_def

subsection ‹@{text U_shiftl_U}›

lemma "n ≥ 32 ⟹ ¬ succeeds (U_shiftl_U_abs_US' (x :: nat) (n :: nat)) s"
  unfolding U_shiftl_U_abs_US'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "n < 32 ⟹ x << n ≤ UINT_MAX ⟹
         U_shiftl_U_abs_US' (x::nat) (n::nat) ∙ s
       ⦃λr s. r = Result (x << n)⦄"
  unfolding U_shiftl_U_abs_US'_def
  by (runs_to_vcg ‹simp add: UINT_MAX_def›)

lemma "n ≥ 32 ⟹ ¬ succeeds (U_shiftl_U_abs_U' (x :: nat) (n :: nat)) s"
  unfolding U_shiftl_U_abs_U'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "n < 32 ⟹ x << n ≤ UINT_MAX ⟹
         U_shiftl_U_abs_U' (x::nat) (n::nat) ∙ s
       ⦃λr s. r = Result (x << n)⦄"
  unfolding U_shiftl_U_abs_U'_def
  by (runs_to_vcg ‹simp add: UINT_MAX_def›)

lemma "n ≥ 32 ⟹ ¬ succeeds (U_shiftl_U_abs_S' (x :: word32) (n :: word32)) s"
  unfolding U_shiftl_U_abs_S'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "n < 32 ⟹
         U_shiftl_U_abs_S' (x::word32) (n::word32) ∙ s
       ⦃λr s. r = Result (x << unat n)⦄"
  unfolding U_shiftl_U_abs_S'_def
  by (runs_to_vcg ‹simp add: UINT_MAX_def›)

lemma "n ≥ 32 ⟹ ¬ succeeds (U_shiftl_U_no_abs' (x :: word32) (n :: word32)) s"
  unfolding U_shiftl_U_no_abs'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "n < 32 ⟹
         U_shiftl_U_no_abs' (x::word32) (n::word32) ∙ s
       ⦃λr s. r = Result (x << unat n)⦄"
  unfolding U_shiftl_U_no_abs'_def by runs_to_vcg

subsection ‹@{text U_shiftl_S}›

lemma "n < 0 ⟹ ¬ succeeds (U_shiftl_S_abs_US' (x :: nat) (n :: int)) s"
  unfolding U_shiftl_S_abs_US'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "n ≥ 32 ⟹ ¬ succeeds (U_shiftl_S_abs_US' (x :: nat) (n :: int)) s"
  unfolding U_shiftl_S_abs_US'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "x << nat n > UINT_MAX ⟹ ¬ succeeds (U_shiftl_S_abs_US' (x :: nat) (n :: int)) s"
  unfolding U_shiftl_S_abs_US'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "0 ≤ n ⟹ n < 32 ⟹ x << nat n ≤ UINT_MAX ⟹
         U_shiftl_S_abs_US' (x::nat) (n::int) ∙ s
       ⦃λr s. r = Result (x << nat n)⦄"
  unfolding U_shiftl_S_abs_US'_def
  by (runs_to_vcg ‹simp add: UINT_MAX_def›)

lemma "n <s 0 ⟹ ¬ succeeds (U_shiftl_S_abs_U' (x :: nat) (n :: sword32)) s"
  unfolding  U_shiftl_S_abs_U'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "32 <=s n ⟹ ¬ succeeds (U_shiftl_S_abs_U' (x :: nat) (n :: sword32)) s"
  unfolding  U_shiftl_S_abs_U'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "x << unat n > UINT_MAX ⟹ ¬ succeeds (U_shiftl_S_abs_U' (x :: nat) (n :: sword32)) s"
  unfolding  U_shiftl_S_abs_U'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def
      word_sless_alt word_sle_def nat_sint)

lemma "0 <=s n ⟹ n <s 32 ⟹ x << unat n ≤ UINT_MAX ⟹
         U_shiftl_S_abs_U' (x::nat) (n::sword32) ∙ s
       ⦃λr s. r = Result (x << unat n)⦄"
  unfolding  U_shiftl_S_abs_U'_def
  by (runs_to_vcg ‹simp add: UINT_MAX_def  nat_sint word_sle_def word_sless_alt›)

lemma "n < 0 ⟹ ¬ succeeds (U_shiftl_S_abs_S' (x :: word32) (n :: int)) s"
  unfolding U_shiftl_S_abs_S'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "n ≥ 32 ⟹ ¬ succeeds (U_shiftl_S_abs_S' (x :: word32) (n :: int)) s"
  unfolding U_shiftl_S_abs_S'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "0 ≤ n ⟹ n < 32 ⟹
         U_shiftl_S_abs_S' (x::word32) (n::int) ∙ s
       ⦃λr s. r = Result (x << nat n)⦄"
  unfolding U_shiftl_S_abs_S'_def
  supply unsigned_of_int [simp del]
  by (runs_to_vcg ‹simp add: UINT_MAX_def unat_of_int›)

lemma "n <s 0 ⟹ ¬ succeeds (U_shiftl_S_no_abs' (x :: word32) (n :: sword32)) s"
  unfolding U_shiftl_S_no_abs'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def word_sle_def word_sless_alt)

lemma "32 <=s n ⟹ ¬ succeeds (U_shiftl_S_no_abs' (x :: word32) (n :: sword32)) s"
  unfolding U_shiftl_S_no_abs'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def word_sle_def word_sless_alt)

lemma "0 <=s n ⟹ n <s 32 ⟹
         U_shiftl_S_no_abs' (x :: word32) (n :: sword32) ∙ s
       ⦃λr s. r = Result (x << unat n)⦄"
  unfolding U_shiftl_S_no_abs'_def by (runs_to_vcg ‹simp add: UINT_MAX_def›)

subsection ‹@{text S_shiftl_U}›

lemma "x < 0 ⟹ ¬ succeeds (S_shiftl_U_abs_US' (x :: int) (n :: nat)) s"
  unfolding S_shiftl_U_abs_US'_def   
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "n ≥ 32 ⟹ ¬ succeeds (S_shiftl_U_abs_US' (x :: int) (n :: nat)) s"
  unfolding S_shiftl_U_abs_US'_def   
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "x << nat (int n) > INT_MAX ⟹ ¬ succeeds (S_shiftl_U_abs_US' (x :: int) (n :: nat)) s"
  unfolding S_shiftl_U_abs_US'_def   
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "n < 32 ⟹ 0 ≤ x ⟹ x << nat (int n) ≤ INT_MAX ⟹
         S_shiftl_U_abs_US' (x::int) (n::nat) ∙ s
       ⦃λr s. r = Result (x << nat (int n))⦄"
  unfolding S_shiftl_U_abs_US'_def
  by (runs_to_vcg 
      ‹simp add: INT_MAX_def shiftl_int_def flip: nat_mult_distrib nat_power_eq nat_numeral›)

lemma "x <s 0 ⟹ ¬ succeeds (S_shiftl_U_abs_U' (x :: sword32) (n :: nat)) s"
  unfolding S_shiftl_U_abs_U'_def   
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def word_sle_def word_sless_alt)

lemma "n ≥ 32 ⟹ ¬ succeeds (S_shiftl_U_abs_U' (x :: sword32) (n :: nat)) s"
  unfolding S_shiftl_U_abs_U'_def   
  apply (auto simp add: succeeds_def run_bind run_guard top_post_state_def word_sle_def word_sless_alt)
  oops ― ‹C parser issue: Jira VER-509›
  thm S_shiftl_U_abs_U'_def
  thm int_unat_nonneg

lemma uint_sint_nonneg:
  "0 <=s (x :: 'a::len signed word) ⟹ uint x = sint x"
  by (simp add: int_unat word_sle_msb_le sint_eq_uint)

lemma "sint x << n > INT_MAX ⟹ ¬ succeeds (S_shiftl_U_abs_U' (x :: sword32) (n :: nat)) s"
  unfolding S_shiftl_U_abs_U'_def   
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def 
      shiftl_int_def INT_MAX_def nat_int_comparison(2) uint_sint_nonneg)

lemma "n < 32 ⟹ 0 <=s x ⟹ sint x << nat (int n) ≤ INT_MAX ⟹
         S_shiftl_U_abs_U' (x::sword32) (n::nat) ∙ s
       ⦃λr s. r = Result (x << nat (int n))⦄"
  unfolding  S_shiftl_U_abs_U'_def
  by (runs_to_vcg ‹simp add: INT_MAX_def shiftl_int_def
      nat_int_comparison(2) uint_sint_nonneg del: of_nat_less_numeral_iff›)

lemma "x < 0 ⟹ ¬ succeeds (S_shiftl_U_abs_S' (x :: int) (n :: word32)) s"
  unfolding S_shiftl_U_abs_S'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "n ≥ 32 ⟹ ¬ succeeds (S_shiftl_U_abs_S' (x :: int) (n :: word32)) s"
 unfolding S_shiftl_U_abs_S'_def
 by (auto simp add: succeeds_def run_bind run_guard top_post_state_def word_le_nat_alt)

lemma "x << unat n > INT_MAX ⟹ ¬ succeeds (S_shiftl_U_abs_S' (x :: int) (n :: word32)) s"
  unfolding S_shiftl_U_abs_S'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def INT_MAX_def)

lemma "n < 32 ⟹ 0 ≤ x ⟹ x << unat n ≤ INT_MAX ⟹
         S_shiftl_U_abs_S' (x::int) (n::word32) ∙ s
       ⦃λr s. r = Result (x << unat n)⦄"
  unfolding S_shiftl_U_abs_S'_def 
  supply unsigned_of_nat [simp del] unsigned_of_nat [simp del]
  apply (runs_to_vcg)
  apply (simp_all add: INT_MAX_def shiftl_int_def
                      word_less_nat_alt)
  apply (simp flip: nat_mult_distrib nat_power_eq nat_numeral)
  done

lemma "x <s 0 ⟹ ¬ succeeds (S_shiftl_U_no_abs' (x :: sword32) (n :: word32)) s"
  unfolding S_shiftl_U_no_abs'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def word_le_nat_alt)

lemma "n ≥ 32 ⟹ ¬ succeeds (S_shiftl_U_no_abs' (x :: sword32) (n :: word32)) s"
  unfolding S_shiftl_U_no_abs'_def
  apply (auto simp add: succeeds_def run_bind run_guard top_post_state_def)
  oops ― ‹C parser issue: Jira VER-509›

lemma "sint x << unat n > INT_MAX ⟹ ¬ succeeds (S_shiftl_U_no_abs' (x :: sword32) (n :: word32)) s"
  unfolding S_shiftl_U_no_abs'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def shiftl_int_def INT_MAX_def
                     nat_int_comparison(2) uint_sint_nonneg)

lemma "n < 32 ⟹ 0 <=s x == sint x << unat n ≤ INT_MAX ⟹
         S_shiftl_U_no_abs' (x::sword32) (n::word32) ∙ s
       ⦃λr s. r = Result (x << unat n)⦄"
  unfolding S_shiftl_U_no_abs'_def
  apply (runs_to_vcg )
  apply (simp_all add:  INT_MAX_def shiftl_int_def
                   nat_int_comparison(2) uint_sint_nonneg )
   apply (smt (verit) Word.sint_0 Word_Lib_Sumo.word_sle_def not_exp_less_eq_0_int 
      uint_sint_nonneg zero_le_mult_iff)+
  done

subsection ‹@{text S_shiftl_S}›

lemma "x < 0 ⟹ ¬ succeeds (S_shiftl_S_abs_US' (x :: int) (n :: int)) s"
  unfolding S_shiftl_S_abs_US'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "n < 0 ⟹ ¬ succeeds (S_shiftl_S_abs_US' (x :: int) (n :: int)) s"
  unfolding S_shiftl_S_abs_US'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "x << nat n > INT_MAX ⟹ ¬ succeeds (S_shiftl_S_abs_US' (x :: int) (n :: int)) s"
  unfolding S_shiftl_S_abs_US'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "n ≥ 32 ⟹ ¬ succeeds (S_shiftl_S_abs_US' (x :: int) (n :: int)) s"
  unfolding S_shiftl_S_abs_US'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "0 ≤ n ⟹ n < 32 ⟹ 0 ≤ x ⟹ x << nat n ≤ INT_MAX ⟹
         S_shiftl_S_abs_US' (x::int) (n::int) ∙ s
       ⦃λr s. r = Result (x << nat n)⦄"
  supply unsigned_of_nat [simp del] unsigned_of_int [simp del]
  unfolding S_shiftl_S_abs_US'_def
  apply runs_to_vcg
  apply (simp_all add: INT_MAX_def shiftl_int_def)
  apply (simp flip: nat_mult_distrib nat_power_eq nat_numeral)
  done

lemma "x <s 0 ⟹ ¬ succeeds (S_shiftl_S_abs_U' (x :: sword32) (n :: sword32)) s"
  unfolding S_shiftl_S_abs_U'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "n <s 0 ⟹ ¬ succeeds (S_shiftl_S_abs_U' (x :: sword32) (n :: sword32)) s"
  unfolding S_shiftl_S_abs_U'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "32 <=s n ⟹ ¬ succeeds (S_shiftl_S_abs_U' (x :: sword32) (n :: sword32)) s"
  unfolding S_shiftl_S_abs_U'_def
  apply (auto simp add: succeeds_def run_bind run_guard top_post_state_def)
  oops ― ‹C parser issue: Jira VER-509›

lemma "sint x << unat n > INT_MAX ⟹ ¬ succeeds (S_shiftl_S_abs_U' (x :: sword32) (n :: sword32)) s"
  unfolding S_shiftl_S_abs_U'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def shiftl_int_def INT_MAX_def
                     nat_int_comparison(2) uint_sint_nonneg)

lemma "0 <=s n ⟹ n <s 32 ⟹ 0 <=s x ⟹ sint x << unat n ≤ INT_MAX ⟹
         S_shiftl_S_abs_U' (x::sword32) (n::sword32) ∙ s
       ⦃λr s. r = Result (x << unat n)⦄"
  unfolding S_shiftl_S_abs_U'_def
  by (runs_to_vcg ‹simp add: INT_MAX_def shiftl_int_def
                   nat_int_comparison(2) uint_sint_nonneg›)
 
lemma "x < 0 ⟹ ¬ succeeds (S_shiftl_S_abs_S' (x :: int) (n :: int)) s"
  unfolding S_shiftl_S_abs_S'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "n < 0 ⟹ ¬ succeeds (S_shiftl_S_abs_S' (x :: int) (n :: int)) s"
  unfolding S_shiftl_S_abs_S'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "n ≥ 32 ⟹ ¬ succeeds (S_shiftl_S_abs_S' (x :: int) (n :: int)) s"
  unfolding S_shiftl_S_abs_S'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "x << nat n > INT_MAX ⟹ ¬ succeeds (S_shiftl_S_abs_S' (x :: int) (n :: int)) s"
  unfolding S_shiftl_S_abs_S'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "0 ≤ n ⟹ n < 32 ⟹ 0 ≤ x ∧ x << n ≤ INT_MAX ⟹
         S_shiftl_S_abs_S' (x::int) (int n) ∙ s
       ⦃λr s. r = Result (x << nat (int n))⦄"
  supply unsigned_of_nat [simp del] unsigned_of_int [simp del]
  unfolding S_shiftl_S_abs_S'_def
  apply (runs_to_vcg)
  apply (simp_all add: INT_MAX_def shiftl_int_def)
  apply (simp flip: nat_mult_distrib nat_power_eq nat_numeral)
  done

lemma "x <s 0 ⟹ ¬ succeeds (S_shiftl_S_no_abs' (x :: sword32) (n :: sword32)) s"
  unfolding S_shiftl_S_no_abs'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "n <s 0 ⟹ ¬ succeeds (S_shiftl_S_no_abs' (x :: sword32) (n :: sword32)) s"
  unfolding S_shiftl_S_no_abs'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "32 <=s n ⟹ ¬ succeeds (S_shiftl_S_no_abs' (x :: sword32) (n :: sword32)) s"
  unfolding S_shiftl_S_no_abs'_def
  apply (auto simp add: succeeds_def run_bind run_guard top_post_state_def)
  oops ― ‹C parser issue: Jira VER-509›

lemma "sint x << unat n > INT_MAX ⟹ ¬ succeeds (S_shiftl_S_no_abs' (x :: sword32) (n :: sword32)) s"
  unfolding S_shiftl_S_no_abs'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def shiftl_int_def INT_MAX_def
                     nat_int_comparison(2) uint_sint_nonneg)

lemma "0 <=s n ⟹ n <s 32 ⟹ 0 <=s x ⟹ sint x << unat n ≤ INT_MAX ⟹
         S_shiftl_S_no_abs' (x::sword32) (n::sword32) ∙ s
       ⦃λr s. r = Result (x << unat n)⦄"
  unfolding S_shiftl_S_no_abs'_def
  by (runs_to_vcg ‹simp add: INT_MAX_def shiftl_int_def
                   nat_int_comparison(2) uint_sint_nonneg›)

section ‹Right shifts›

subsection ‹@{text U_shiftr_U}›

lemma "n ≥ 32 ⟹ ¬ succeeds (U_shiftr_U_abs_US' (x :: nat) (n :: nat)) s"
  unfolding U_shiftr_U_abs_US'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "n < 32 ⟹ U_shiftr_U_abs_US' (x::nat) (n::nat) ∙ s ⦃λr s. r = Result (x >> n)⦄"
  unfolding U_shiftr_U_abs_US'_def by runs_to_vcg

lemma "n ≥ 32 ⟹ ¬ succeeds (U_shiftr_U_abs_U' (x :: nat) (n :: nat)) s"
  unfolding U_shiftr_U_abs_U'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "n < 32 ⟹ U_shiftr_U_abs_U' (x::nat) (n::nat) ∙ s ⦃λr s. r = Result (x >> n)⦄"
  unfolding U_shiftr_U_abs_U'_def by runs_to_vcg

lemma "n ≥ 32 ⟹ ¬ succeeds (U_shiftr_U_abs_S' (x :: word32) (n :: word32)) s"
  unfolding U_shiftr_U_abs_S'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "n < 32 ⟹ U_shiftr_U_abs_S' (x::word32) (n::word32) ∙ s ⦃λr s. r = Result (x >> unat n)⦄"
  unfolding U_shiftr_U_abs_S'_def by runs_to_vcg

lemma "n ≥ 32 ⟹ ¬ succeeds (U_shiftr_U_no_abs' (x :: word32) (n :: word32)) s"
  unfolding U_shiftr_U_no_abs'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "n < 32 ⟹ U_shiftr_U_no_abs' (x::word32) (n::word32) ∙ s ⦃λr s. r = Result (x >> unat n)⦄"
  unfolding U_shiftr_U_no_abs'_def by runs_to_vcg

subsection ‹@{text U_shiftr_S}›

lemma "n < 0 ⟹ ¬ succeeds (U_shiftr_S_abs_US' (x :: nat) (n :: int)) s"
  unfolding U_shiftr_S_abs_US'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "n ≥ 32 ⟹ ¬ succeeds (U_shiftr_S_abs_US' (x :: nat) (n :: int)) s"
  unfolding U_shiftr_S_abs_US'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "0 ≤ n ⟹ n < 32 ⟹ U_shiftr_S_abs_US' (x::nat) (n::int) ∙ s ⦃λr s. r = Result (x >> nat n)⦄"
  unfolding U_shiftr_S_abs_US'_def by runs_to_vcg

lemma "n <s 0 ⟹ ¬ succeeds (U_shiftr_S_abs_U' (x :: nat) (n :: sword32)) s"
  unfolding U_shiftr_S_abs_U'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "32 <=s n ⟹ ¬ succeeds (U_shiftr_S_abs_U' (x :: nat) (n :: sword32)) s"
  unfolding U_shiftr_S_abs_U'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "0 <=s n ⟹ n <s 32 ⟹ U_shiftr_S_abs_U' (x::nat) (n::sword32) ∙ s ⦃λr s. r = Result (x >> unat n)⦄"
  unfolding U_shiftr_S_abs_U'_def by (runs_to_vcg ‹simp add: nat_sint word_sle_def word_sless_alt›)

lemma "n < 0 ⟹ ¬ succeeds (U_shiftr_S_abs_S' (x :: word32) (n :: int)) s"
  unfolding U_shiftr_S_abs_S'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "n ≥ 32 ⟹ ¬ succeeds (U_shiftr_S_abs_S' (x :: word32) (n :: int)) s"
  unfolding U_shiftr_S_abs_S'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "0 ≤ n ⟹ n < 32 ⟹ U_shiftr_S_abs_S' (x::word32) (n::int) ∙ s ⦃λr s. r = Result (x >> nat n)⦄"
  unfolding U_shiftr_S_abs_S'_def by (runs_to_vcg)

lemma "n <s 0 ⟹ ¬ succeeds (U_shiftr_S_no_abs' (x :: word32) (n :: sword32)) s"
  unfolding U_shiftr_S_no_abs'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "32 <=s n ⟹ ¬ succeeds (U_shiftr_S_no_abs' (x :: word32) (n :: sword32)) s"
  unfolding U_shiftr_S_no_abs'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "0 <=s n ⟹ n <s 32 ⟹ 
  U_shiftr_S_no_abs' (x :: word32) (n :: sword32) ∙ s ⦃λr s. r = Result (x >> unat n)⦄"
  unfolding U_shiftr_S_no_abs'_def by runs_to_vcg

subsection ‹@{text S_shiftr_U}›

lemma "x < 0 ⟹ ¬ succeeds (S_shiftr_U_abs_US' (x :: int) (n :: nat)) s"
  unfolding S_shiftr_U_abs_US'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "n ≥ 32 ⟹ ¬ succeeds (S_shiftr_U_abs_US' (x :: int) (n :: nat)) s"
  unfolding S_shiftr_U_abs_US'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "n < 32 ⟹ 0 ≤ x ⟹ S_shiftr_U_abs_US' (x::int) (n::nat) ∙ s ⦃λr s. r = Result (x >> nat (int n))⦄"
  unfolding S_shiftr_U_abs_US'_def by runs_to_vcg

lemma "x <s 0 ⟹ ¬ succeeds (S_shiftr_U_abs_U' (x :: sword32) (n :: nat)) s"
  unfolding S_shiftr_U_abs_U'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "n ≥ 32 ⟹ ¬ succeeds (S_shiftr_U_abs_U' (x :: sword32) (n :: nat)) s"
  unfolding S_shiftr_U_abs_U'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "n < 32 ⟹ 0 <=s x ⟹ S_shiftr_U_abs_U' (x::sword32) (n::nat) ∙ s ⦃λr s. r = Result (x >> nat (int n))⦄"
  unfolding S_shiftr_U_abs_U'_def by runs_to_vcg

lemma "x < 0 ⟹ ¬ succeeds (S_shiftr_U_abs_S' (x :: int) (n :: word32)) s"
  unfolding S_shiftr_U_abs_S'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "n ≥ 32 ⟹ ¬ succeeds (S_shiftr_U_abs_S' (x :: int) (n :: word32)) s"
  unfolding S_shiftr_U_abs_S'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "n < 32 ⟹ 0 ≤ x ⟹ 
  S_shiftr_U_abs_S' (x::int) (n::word32) ∙ s ⦃λr s. r = Result (x >> unat n)⦄"
  unfolding S_shiftr_U_abs_S'_def by runs_to_vcg

lemma "x <s 0 ⟹ ¬ succeeds (S_shiftr_U_no_abs' (x :: sword32) (n :: word32)) s"
  unfolding S_shiftr_U_no_abs'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "n ≥ 32 ⟹ ¬ succeeds (S_shiftr_U_no_abs' (x :: sword32) (n :: word32)) s"
  unfolding S_shiftr_U_no_abs'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "n < 32 ⟹ 0 <=s x ⟹ 
  S_shiftr_U_no_abs' (x::sword32) (n::word32) ∙ s ⦃λr s. r = Result (x >> unat n)⦄"
  unfolding S_shiftr_U_no_abs'_def by runs_to_vcg

subsection ‹@{text S_shiftr_S}›

lemma "x < 0 ⟹ ¬ succeeds (S_shiftr_S_abs_US' (x :: int) (n :: int)) s"
  unfolding S_shiftr_S_abs_US'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "n < 0 ⟹ ¬ succeeds (S_shiftr_S_abs_US' (x :: int) (n :: int)) s"
  unfolding S_shiftr_S_abs_US'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "n ≥ 32 ⟹ ¬ succeeds (S_shiftr_S_abs_US' (x :: int) (n :: int)) s"
  unfolding S_shiftr_S_abs_US'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "0 ≤ n ⟹ n < 32 ⟹ 0 ≤ x ⟹ 
  S_shiftr_S_abs_US' (x::int) (n::int) ∙ s ⦃λr s. r = Result (x >> nat n)⦄"
  unfolding S_shiftr_S_abs_US'_def by runs_to_vcg

lemma "x <s 0 ⟹ ¬ succeeds (S_shiftr_S_abs_U' (x :: sword32) (n :: sword32)) s"
  unfolding S_shiftr_S_abs_U'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "n <s 0 ⟹ ¬ succeeds (S_shiftr_S_abs_U' (x :: sword32) (n :: sword32)) s"
  unfolding S_shiftr_S_abs_U'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "32 <=s n ⟹ ¬ succeeds (S_shiftr_S_abs_U' (x :: sword32) (n :: sword32)) s"
  unfolding S_shiftr_S_abs_U'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "0 <=s n ⟹ n <s 32 ⟹ 0 <=s x ⟹
         S_shiftr_S_abs_U' (x::sword32) (n::sword32) ∙ s
       ⦃λr s. r = Result (x >> unat n)⦄"
  unfolding S_shiftr_S_abs_U'_def by runs_to_vcg

lemma "x < 0 ⟹ ¬ succeeds (S_shiftr_S_abs_S' (x :: int) (n :: int)) s"
  unfolding S_shiftr_S_abs_S'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "n < 0 ⟹ ¬ succeeds (S_shiftr_S_abs_S' (x :: int) (n :: int)) s"
  unfolding S_shiftr_S_abs_S'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "n ≥ 32 ⟹ ¬ succeeds (S_shiftr_S_abs_S' (x :: int) (n :: int)) s"
  unfolding S_shiftr_S_abs_S'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "0 ≤ n ⟹ n < 32 ⟹ 0 ≤ x ⟹
         S_shiftr_S_abs_S' (x::int) (n::int) ∙ s
       ⦃λr s. r = Result (x >> nat n)⦄"
  unfolding S_shiftr_S_abs_S'_def by runs_to_vcg

lemma "x <s 0 ⟹ ¬ succeeds (S_shiftr_S_no_abs' (x :: sword32) (n :: sword32)) s"
  unfolding S_shiftr_S_no_abs'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "n <s 0 ⟹ ¬ succeeds (S_shiftr_S_no_abs' (x :: sword32) (n :: sword32)) s"
  unfolding S_shiftr_S_no_abs'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "32 <=s n ⟹ ¬ succeeds (S_shiftr_S_no_abs' (x :: sword32) (n :: sword32)) s"
  unfolding S_shiftr_S_no_abs'_def
  by (auto simp add: succeeds_def run_bind run_guard top_post_state_def)

lemma "0 <=s n ⟹ n <s 32 ⟹ 0 <=s x ⟹
         S_shiftr_S_no_abs' (x::sword32) (n::sword32) ∙ s
       ⦃λr s. r = Result (x >> unat n)⦄"
  unfolding S_shiftr_S_no_abs'_def by runs_to_vcg

end

end