Theory int128

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

theory int128
  imports AutoCorres2_Main.AutoCorres_Main
begin

install_C_file "int128.c"

autocorres [skip_word_abs] "int128.c"

context int128_all_corres
begin

lemma "u' i j ≡ UCAST(32 → 128) i * UCAST(32 → 128) j"
  by (fact u'_def)

lemma "i' i j ≡
   do {
  _ ← oguard
        (λs. - 170141183460469231731687303715884105728
              ≤ sint (SCAST(32 signed → 128 signed) i) * sint (SCAST(32 signed → 128 signed) j) ∧
              sint (SCAST(32 signed → 128 signed) i) * sint (SCAST(32 signed → 128 signed) j)
              ≤ 170141183460469231731687303715884105727);
  oreturn (UCAST(32 → 128 signed) (SCAST(32 signed → 32) i * SCAST(32 signed → 32) j))
}"
  by (fact i'_def)

end

end