Theory IsaSAT_EMA_LLVM

theory IsaSAT_EMA_LLVM
  imports IsaSAT_EMA IsaSAT_Literals_LLVM
begin

abbreviation ema_rel :: ‹(ema×ema) set› where
  ‹ema_rel ≡ word64_rel ×⇩r word64_rel ×⇩r word64_rel ×⇩r word64_rel ×⇩r word64_rel›

abbreviation ema_assn :: ‹ema ⇒ ema ⇒ assn› where
  ‹ema_assn ≡ word64_assn ×⇩a word64_assn ×⇩a word64_assn ×⇩a word64_assn ×⇩a word64_assn›

lemma [sepref_import_param]:
  ‹(ema_get_value, ema_get_value) ∈ ema_rel → word64_rel›
  ‹(ema_bitshifting,ema_bitshifting) ∈ word64_rel›
  ‹(ema_reinit,ema_reinit) ∈ ema_rel → ema_rel›
  ‹(ema_init,ema_init) ∈ word_rel → ema_rel›
  by auto

sepref_register EMA_FIXPOINT_SIZE ema_bitshifting
sepref_def EMA_FIXPOINT_SIZE_impl
  is ‹uncurry0 (RETURN EMA_FIXPOINT_SIZE)›
  :: ‹unit_assn⇧k →⇩a uint64_nat_assn›
  unfolding EMA_FIXPOINT_SIZE_def
  apply (annot_unat_const ‹TYPE(64)›)
  by sepref

lemma EMA[simp]:
  ‹EMA_FIXPOINT_SIZE < 64›
  ‹EMA_MULT_SHIFT < 64›
  ‹EMA_FIXPOINT_SIZE - EMA_MULT_SHIFT < 64›
  ‹EMA_MULT_SHIFT ≤ EMA_FIXPOINT_SIZE›
  ‹EMA_FIXPOINT_SIZE - 32 < 64›
  ‹EMA_FIXPOINT_SIZE ≥ 32›
  by (auto simp: EMA_FIXPOINT_SIZE_def EMA_MULT_SHIFT_def)

sepref_def ema_bitshifting_impl
  is ‹uncurry0 (RETURN ema_bitshifting)›
  :: ‹unit_assn⇧k →⇩a word64_assn›
  unfolding ema_bitshifting_def
  by sepref

lemma ema_reinit_inline[llvm_inline]:
  "ema_reinit = (λ(value, α, β, wait, period).
    (value, α, ema_bitshifting, 1::_ word, 0:: _ word))"
  by (auto simp: ema_bitshifting_def intro!: ext)

sepref_def EMA_MULT_SHIFT_impl
  is ‹uncurry0 (RETURN EMA_MULT_SHIFT)›
  :: ‹unit_assn⇧k →⇩a uint64_nat_assn›
  unfolding EMA_MULT_SHIFT_def
  apply (annot_unat_const ‹TYPE(64)›)
  by sepref

lemmas [llvm_inline] = ema_init_def

sepref_def ema_update_impl is ‹uncurry (RETURN oo ema_update)›
  :: ‹uint32_nat_assn⇧k *⇩a ema_assn⇧k →⇩a ema_assn›
  unfolding ema_update_def Let_def[of "_ - 1"]
  apply (rewrite at ‹let _ = of_nat ⌑ * _ in _› annot_unat_unat_upcast[where 'l = 64])
  apply (annot_unat_const ‹TYPE(64)›)
  supply [[goals_limit = 1]]
  by sepref

sepref_def ema_init_impl
  is ‹RETURN o ema_init›
  :: ‹word64_assn⇧k →⇩a ema_assn›
  unfolding ema_init_def
  apply (annot_unat_const ‹TYPE(64)›)
  by sepref

end