From Stdlib Require Import List NArith.

Require Import skylabs.auto.cpp.tactics4.
Require Import skylabs.auto.cpp.prelude.proof.
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.
Import linearity.

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

Definition bytes32_evmc_bytes32_ctor_name : name :=
  "evmc::bytes32::bytes32(evmc_bytes32)".

Definition bytes32_zero_init_expr : Expr :=
  Econstructor
    bytes32_evmc_bytes32_ctor_name
    (Eimplicit
       (Einitlist
          (Eimplicit_init (Tarray Tuchar 32%N) :: nil)
          None evmc_bytes32_ty) :: nil)
    bytes32_ty.

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



End with_Sigma.

Section with_Sigma.
  Context `{Sigma : cpp_logic} {CU : genv}.

  Lemma wp_destroy_bytes32_value
      (tu : translation_unit) (base : ptr) (value : N) (Q : epred) :
    □ exec_specs.bytes32_dtor_spec
    ** base |-> exec_specs.bytes32R 1 value ** Q
    |-- wp_destroy_val tu QM bytes32_ty base Q.

  Lemma destroy_run_bytes32_array :
    ∀ (tu : translation_unit) (base : ptr) (len : nat)
      (values : list N) (Q : epred),
      length values = len →
      □ exec_specs.bytes32_dtor_spec
      ** base |-> arrayR bytes32_ty (exec_specs.bytes32R 1) values
      ** Q
      |-- destroy.run_array tu QM bytes32_ty base len Q.

  Lemma wp_destroy_bytes32_array :
    ∀ (tu : translation_unit) (base : ptr) (len : N)
      (values : list N) (Q : epred),
      length values = N.to_nat len →
      □ exec_specs.bytes32_dtor_spec
      ** base |-> arrayR bytes32_ty (exec_specs.bytes32R 1) values
      ** Q
      |-- wp_destroy_array tu QM bytes32_ty len base Q.
End with_Sigma.