From Stdlib Require Import List NArith ZArith.

Require Import skylabs.auto.cpp.proof.
Require Import skylabs.lang.cpp.cpp.
Require Import monad.asts.storage_page_cpp.
Require Import monad.proofs.exec_specs.

Import cQp_compat.

Local Open Scope N_scope.

Fixpoint countr_zero_fuel (fuel : nat) (word : N) : N :=
  match fuel with
  | O ⇒ 64
  | S fuel' ⇒
      if N.eqb word 0
      then 64
      else if N.odd word
           then 0
           else 1 + countr_zero_fuel fuel' (N.shiftr word 1)
  end.

Definition countr_zero64 (word : N) : N :=
  countr_zero_fuel 64 word.

Fixpoint popcount_fuel (fuel : nat) (word : N) : N :=
  match fuel with
  | O ⇒ 0
  | S fuel' ⇒
      (if N.odd word then 1 else 0)
      + popcount_fuel fuel' (N.shiftr word 1)
  end.

Definition popcount64 (word : N) : N :=
  popcount_fuel 64 word.

Section with_Sigma.
  Context `{Sigma : cpp_logic} {CU : genv} {hh : HasOwn mpredI fracR}.

  Definition bytes32_ty : type := "evmc::bytes32"%cpp_type.

  Definition storage_page_is_empty_lambda_name : name :=
    "monad::storage_page_t::is_empty() const::@0"%cpp_name.






End with_Sigma.