bedrock.lang.cpp.model.simple_pred

(*
 * Copyright (c) 2020-2024 BedRock Systems, Inc.
 * This software is distributed under the terms of the BedRock Open-Source License.
 * See the LICENSE-BedRock file in the repository root for details.
 *)
Require Import iris.algebra.excl.
Require Import iris.algebra.gmap.
Require Import iris.algebra.lib.frac_auth.
Require Import iris.bi.monpred.
Require Import iris.bi.lib.fractional.
Require Import bedrock.lang.proofmode.proofmode.

Require Import bedrock.lang.bi.fractional.
Require Import bedrock.lang.bi.cancelable_invariants.
Require Import bedrock.lang.cpp.bi.cfractional.
Require Import bedrock.lang.base_logic.own_instances.

Require Import bedrock.prelude.base.
Require Import bedrock.prelude.option.
Require Import bedrock.lang.cpp.arith.z_to_bytes.
Require Import bedrock.lang.cpp.algebra.cfrac.
Require Import bedrock.lang.cpp.syntax.
Require Import bedrock.lang.cpp.semantics.
Require Import bedrock.lang.cpp.logic.mpred.
Require Import bedrock.lang.cpp.logic.pred.

#[local] Set Printing Coercions.

Implicit Types (vt : validity_type) (σ resolve : genv) (q : cQp.t).

(* todo: does this not exist as a library somewhere? *)
Definition cfractionalR (V : Type) : cmra :=
  prodR cQp.tR (agreeR (leibnizO V)).
Definition cfrac {V : Type} q (v : V) : cfractionalR V :=
  (q, to_agree v).

Lemma cfrac_op {V} (l : V) q1 q2 :
  cfrac q1 l ⋅ cfrac q2 l ≡ cfrac (q1 ⋅ q2) l.
Proof. by rewrite -pair_op agree_idemp. Qed.

Lemma cfrac_valid {A : Type} {q1 q2} {v1 v2 : A} :
  ✓ (cfrac q1 v1 ⋅ cfrac q2 v2) → ✓ (q1 ⋅ q2)%Qp ∧ v1 = v2.
Proof. by move /pair_valid => /= []? /to_agree_op_inv_L. Qed.

Section fractional.
  Context {K V : Type} `{Countable K} `{!HasOwn PROP (gmapR K (cfractionalR V))}.

  Let gmap_own γ q k v :=
    own (A := gmapR K (cfractionalR V)) γ {[ k := cfrac q v ]}.
  #[global] Instance cfractional_own_frac γ k v :
    CFractional (λ q, gmap_own γ q k v).
  Proof. intros q1 q2. by rewrite -own_op singleton_op cfrac_op. Qed.

  #[global] Instance fractional_own_frac_as_fractional γ k v q :
    AsCFractional (gmap_own γ q k v) (λ q, gmap_own γ q k v) q.
  Proof. solve_as_cfrac. Qed.

  #[global] Instance gmap_own_agree
    `{!BiEmbed siPropI PROP} `{!HasOwnValid PROP (gmapR K (cfractionalR V))}
    v1 v2 γ q1 q2 k :
    Observe2 [| v1 = v2 |] (gmap_own γ q1 k v1) (gmap_own γ q2 k v2).
  Proof.
    apply: observe_2_intro_only_provable.
    apply bi.wand_intro_r; rewrite /gmap_own -own_op singleton_op.
    rewrite own_valid discrete_valid singleton_valid.
    by iIntros "!%" => /cfrac_valid [].
  Qed.

  Instance gmap_own_cfrac_valid γ
    `{!BiEmbed siPropI PROP} `{!HasOwnValid PROP (gmapR K (cfractionalR V))} :
    ∀ q k v, Observe [| cQp.frac q ≤ 1 |]%Qp (gmap_own γ q k v).
  Proof.
    intros. apply: observe_intro_only_provable.
    rewrite /gmap_own own_valid !discrete_valid singleton_valid.
    by iIntros "!%" => /pair_valid [? _].
  Qed.
End fractional.
#[local] Existing Instance gmap_own_cfrac_valid.

Require Import bedrock.lang.cpp.model.inductive_pointers.
(* Stand-in for actual models.
Ensures that everything needed is properly functorized. *)
Import PTRS_IMPL.
Declare Module Import VALUES_DEFS_IMPL : VALUES_INTF_FUNCTOR PTRS_IMPL.

Implicit Types (p : ptr).

Module SimpleCPP_BASE <: CPP_LOGIC_CLASS.

  Definition addr : Set := N.
  Definition byte : Set := N.
  Variant runtime_val' : Set :=
  | Rundef
    (* ^ undefined value, semantically, it means "any value" *)
  | Rval (_ : byte)
    (* ^ machine level byte *)
  | Rpointer_chunk (_ : ptr) (index : nat).
    (* ^ you need the same pointer and consecutive integers to "have" a pointer.
     *)

  Definition Z_to_bytes {σ:genv} (n : bitsize) (sgn: signed) (v : Z) : list runtime_val' :=
    Rval <$> _Z_to_bytes (bitsize.bytesNat n) (genv_byte_order σ) sgn v.

  Lemma length_Z_to_bytes {σ} n sgn v : length (Z_to_bytes (σ:=σ) n sgn v) = bitsize.bytesNat n.
  Proof. by rewrite /Z_to_bytes length_fmap _Z_to_bytes_length. Qed.

  Record cpp_ghost' : Type :=
    { heap_name : gname
    ; ghost_mem_name : gname
    ; mem_inj_name : gname
    ; blocks_name : gname
    ; code_name : gname
    ; derivations_name : gname
    }.
  Definition _cpp_ghost := cpp_ghost'.

  Record cppG' (Σ : gFunctors) : Type :=
    { heapGS : inG Σ (gmapR addr (cfractionalR runtime_val'))
      (* ^ this represents the contents of physical memory *)
    ; ghost_memG : inG Σ (gmapR ptr (cfractionalR val))
      (* ^ this represents the contents of the C++ runtime that might
         not be represented in physical memory, e.g. values stored in
         registers or temporaries on the stack *)
    ; mem_injG : inG Σ (gmapUR ptr (agreeR (leibnizO (option addr))))
      (* ^ this carries the (compiler-supplied) mapping from C++ locations
         (represented as pointers) to physical memory addresses. Locations that
         are not stored in physical memory (e.g. because they are register
         allocated) are mapped to None *)
    ; blocksG : inG Σ (gmapUR ptr (agreeR (leibnizO (Z * Z))))
      (* ^ this represents the minimum and maximum offset of the block *)
    ; codeG : inG Σ (gmapUR ptr (agreeR (leibnizO (Func + Method + Ctor + Dtor))))
      (* ^ this carries the (compiler-supplied) mapping from C++ locations
         to the code stored at that location *)
    ; derivationsG : inG Σ (gmapUR ptr (cfractionalR (leibnizO (globname * list globname))))
    ; has_inv' : invGS Σ
    ; has_cinv' : cinvG Σ
    }.

  Definition cppPreG : gFunctors -> Type := cppG'.

  Definition has_inv Σ : cppPreG Σ -> invGS Σ := @has_inv' Σ.
  Definition has_cinv Σ : cppPreG Σ -> cinvG Σ := @has_cinv' Σ.

  Include CPP_LOGIC_CLASS_MIXIN.

  Section with_cpp.
    Context `{!cpp_logic thread_info Σ}.

    Existing Class cppG'.
    #[local] Instance cppPreG_cppG' : cppG' Σ := cpp_has_cppG.
    #[local] Existing Instances heapGS ghost_memG mem_injG blocksG codeG derivationsG.

    Definition heap_own (a : addr) q (r : runtime_val') : mpred :=
      own (A := gmapR addr (cfractionalR runtime_val'))
        cpp_ghost.(heap_name) {[ a := cfrac q r ]}.
    Definition ghost_mem_own (p : ptr) q (v : val) : mpred :=
      own (A := gmapR ptr (cfractionalR val))
        cpp_ghost.(ghost_mem_name) {[ p := cfrac q v ]}.
    Definition mem_inj_own (p : ptr) (va : option N) : mpred :=
      own (A := gmapUR ptr (agreeR (leibnizO (option addr))))
        cpp_ghost.(mem_inj_name) {[ p := to_agree va ]}.
    Definition blocks_own (p : ptr) (l h : Z) : mpred :=
      own (A := gmapUR ptr (agreeR (leibnizO (Z * Z))))
        cpp_ghost.(blocks_name) {[ p := to_agree (l, h) ]}.
    Definition _code_own (p : ptr) (f : Func + Method + Ctor + Dtor) : mpred :=
      own cpp_ghost.(code_name)
        (A := gmapUR ptr (agreeR (leibnizO (Func + Method + Ctor + Dtor))))
        {[ p := to_agree f ]}.
    Definition derivation_own (p : ptr) q (l : globname) (mdc : list globname) : mpred :=
      own (A := gmapUR ptr (cfractionalR (leibnizO (globname * list globname))))
        cpp_ghost.(derivations_name) {[ p := cfrac q (l, mdc) ]}.

    #[global] Instance mem_inj_own_persistent p va : Persistent (mem_inj_own p va) := _.
    #[global] Instance mem_inj_own_affine p va : Affine (mem_inj_own p va) := _.
    #[global] Instance mem_inj_own_timeless p va : Timeless (mem_inj_own p va) := _.

    #[global] Instance _code_own_persistent p f : Persistent (_code_own p f) := _.
    #[global] Instance _code_own_affine p f : Affine (_code_own p f) := _.
    #[global] Instance _code_own_timeless p f : Timeless (_code_own p f) := _.
  End with_cpp.
  #[global] Typeclasses Opaque mem_inj_own _code_own.
End SimpleCPP_BASE.

(* TODO: provide an instance for this. *)
Module Type SimpleCPP_VIRTUAL.
  Import SimpleCPP_BASE.

  Parameter vbyte : forall `{!cpp_logic thread_info Σ}
    (va : addr) (rv : runtime_val') (q : Qp), mpred.
  Section with_cpp.
    Context `{cpp_logic}.

    Axiom vbyte_fractional : forall va rv, Fractional (vbyte va rv).
    Axiom vbyte_timeless : forall va rv q, Timeless (vbyte va rv q).
    #[global] Existing Instances vbyte_fractional vbyte_timeless.

    Definition vbytes (a : addr) (rv : list runtime_val') (q : Qp) : mpred :=
      [∗list] o ↦ v ∈ rv, (vbyte (a+N.of_nat o)%N v q).

    #[global] Instance vbytes_fractional va rv : Fractional (vbytes va rv).
    Proof. apply fractional_big_sepL; intros. apply vbyte_fractional. Qed.

    #[global] Instance vbytes_as_fractional va rv q :
      AsFractional (vbytes va rv q) (vbytes va rv) q.
    Proof. exact: Build_AsFractional. Qed.

    #[global] Instance vbytes_timeless va rv q : Timeless (vbytes va rv q) := _.
  End with_cpp.
End SimpleCPP_VIRTUAL.

Module SimpleCPP.
  Include SimpleCPP_BASE.
  Include SimpleCPP_VIRTUAL.

  Definition runtime_val := runtime_val'.

  Parameter live_alloc_id : forall `{!cpp_logic thread_info Σ}, alloc_id -> mpred.

  Section with_cpp.
    Context `{cpp_logic}.

    Axiom live_alloc_id_timeless : forall aid, Timeless (live_alloc_id aid).
    #[global] Existing Instance live_alloc_id_timeless.

    Definition live_ptr (p : ptr) :=
      default False%I (live_alloc_id <$> ptr_alloc_id p).
    Axiom nullptr_live : |-- live_ptr nullptr.
    Typeclasses Opaque live_ptr.

    Definition in_range (vt : validity_type) (l o h : Z) : mpred :=
      [| (l <= o < h)%Z \/ (vt = Relaxed /\ o = h) |].

    Lemma in_range_weaken l o h :
      in_range Strict l o h |-- in_range Relaxed l o h.
    Proof. rewrite /in_range/=. f_equiv. rewrite/impl. tauto. Qed.

    Definition _valid_ptr vt (p : ptr) : mpred :=
      [| p = nullptr /\ vt = Relaxed |] \\//
            Exists base l h o zo,
                blocks_own base l h **
                in_range vt l zo h **
                 (* XXX this is wrong: eval_offset shouldn't take a genv. *)
                [| exists resolve, eval_offset resolve o = Some zo /\ p = base ,, o |] **
                [| ptr_vaddr p <> Some 0%N |].
    (* strict validity (not past-the-end) *)
    Notation strict_valid_ptr := (_valid_ptr Strict).
    (* relaxed validity (past-the-end allowed) *)
    Notation valid_ptr := (_valid_ptr Relaxed).

    Instance _valid_ptr_persistent : forall b p, Persistent (_valid_ptr b p) := _.
    Instance _valid_ptr_affine : forall b p, Affine (_valid_ptr b p) := _.
    Instance _valid_ptr_timeless : forall b p, Timeless (_valid_ptr b p) := _.

    (* Needs validity to exclude non-null pointers with 0 addresses but
    non-null provenance (which can be created by pointer arithmetic!) as
    invalid. *)
    Lemma same_address_eq_null p tv :
      _valid_ptr tv p |--
      [| same_address p nullptr <-> p = nullptr |].
    Proof.
      rewrite /_valid_ptr same_address_eq; iIntros "[[-> _]|H]";
        [ |iDestruct "H" as (?????) "(_ & _ & _ & %Hne)"]; iIntros "!%".
      by rewrite same_property_iff ptr_vaddr_nullptr; naive_solver.
      rewrite same_property_iff; split; last intros ->;
        rewrite ptr_vaddr_nullptr; naive_solver.
    Qed.

    Theorem valid_ptr_nullptr : |-- valid_ptr nullptr.
    Proof. by iLeft. Qed.

    Theorem not_strictly_valid_ptr_nullptr : strict_valid_ptr nullptr |-- False.
    Proof.
      iDestruct 1 as "[[_ %]|H] /="; first done.
      by iDestruct "H" as (?????) "(_ & _ & _ & %Hne)".
    Qed.
    Typeclasses Opaque _valid_ptr.

    Lemma strict_valid_valid p :
      strict_valid_ptr p |-- valid_ptr p.
    Proof.
      rewrite /_valid_ptr/=; f_equiv. { by iIntros "!%" ([_ ?]). }
      by setoid_rewrite in_range_weaken.
    Qed.

    Axiom valid_ptr_alloc_id : forall p,
      valid_ptr p |-- [| is_Some (ptr_alloc_id p) |].

    Definition provides_storage (storage_ptr obj_ptr : ptr) (_ : type) : mpred :=
      [| same_address storage_ptr obj_ptr |] ** valid_ptr storage_ptr ** valid_ptr obj_ptr.
    #[global] Instance provides_storage_persistent storage_ptr obj_ptr ty :
      Persistent (provides_storage storage_ptr obj_ptr ty) := _.
    #[global] Instance provides_storage_affine storage_ptr obj_ptr ty :
      Affine (provides_storage storage_ptr obj_ptr ty) := _.
    #[global] Instance provides_storage_timeless storage_ptr obj_ptr ty :
      Timeless (provides_storage storage_ptr obj_ptr ty) := _.
    #[global] Instance provides_storage_same_address storage_ptr obj_ptr ty :
      Observe [| same_address storage_ptr obj_ptr |] (provides_storage storage_ptr obj_ptr ty) := _.

    #[global] Instance provides_storage_valid_storage_ptr storage_ptr obj_ptr aty :
      Observe (valid_ptr storage_ptr) (provides_storage storage_ptr obj_ptr aty) := _.
    #[global] Instance provides_storage_valid_obj_ptr storage_ptr obj_ptr aty :
      Observe (valid_ptr obj_ptr) (provides_storage storage_ptr obj_ptr aty) := _.

    Section with_genv.
      Variable σ : genv.

      Let POINTER_BITSZ : bitsize := pointer_size_bitsize σ.
      Notation POINTER_BYTES := (bitsize.bytesNat POINTER_BITSZ).

      Definition aptr (p : ptr) : list runtime_val :=
        Rpointer_chunk p <$> (seq 0 POINTER_BYTES).

      Notation Z_to_bytes := (Z_to_bytes (σ:=σ)).

      Definition cptr (a : N) : list runtime_val :=
        Z_to_bytes POINTER_BITSZ Unsigned (Z.of_N a).

      Lemma length_aptr p : length (aptr p) = POINTER_BYTES.
      Proof. by rewrite /aptr length_fmap length_seq. Qed.
      Lemma length_cptr a : length (cptr a) = POINTER_BYTES.
      Proof. by rewrite /cptr length_Z_to_bytes. Qed.

      Lemma bytesNat_pos b : bitsize.bytesNat b > 0.
      Proof. by case: b =>/=; lia. Qed.

      Lemma bytesNat_nnonnull b : bitsize.bytesNat b <> 0.
      Proof. have := bytesNat_pos b. lia. Qed.
      #[local] Hint Resolve bytesNat_nnonnull : core.

      Lemma bytesNat_nnonnull' b : bitsize.bytesNat b = S (pred (bitsize.bytesNat b)).
      Proof. by rewrite (Nat.succ_pred _ (bytesNat_nnonnull _)). Qed.

      Lemma list_not_nil_cons {T} (xs : list T) : xs <> nil -> ∃ h t, xs = h :: t.
      Proof. case: xs => //= x xs. eauto. Qed.

      Lemma _Z_to_bytes_cons n x y z : n <> 0 -> ∃ a b, _Z_to_bytes n x y z = a :: b.
      Proof.
        intros Hne.
        apply list_not_nil_cons.
        rewrite -(Nat.succ_pred n Hne) {Hne} _Z_to_bytes_eq /_Z_to_bytes_def /=.
        case: x => //= Heq.
        eapply app_cons_not_nil, symmetry, Heq.
      Qed.
      Lemma Z_to_bytes_cons bs x y : ∃ a b, Z_to_bytes bs x y = Rval a :: b.
      Proof.
        unfold Z_to_bytes.
        edestruct _Z_to_bytes_cons as (? & ? & ->) => //; eauto.
      Qed.

      Lemma cptr_ne_aptr p n : cptr n <> aptr p.
      Proof.
        rewrite /cptr /aptr bytesNat_nnonnull'.
        by edestruct Z_to_bytes_cons as (? & ? & ->).
      Qed.

      Definition pure_encodes_undef (n : bitsize) (vs : list runtime_val) : Prop :=
        vs = repeat Rundef (bitsize.bytesNat n).
      Lemma length_pure_encodes_undef n vs :
        pure_encodes_undef n vs ->
        length vs = bitsize.bytesNat n.
      Proof. rewrite /pure_encodes_undef => ->. exact: repeat_length. Qed.

      Definition in_Z_to_bytes_bounds (cnt' : bitsize) sgn z :=
        let cnt := bitsize.bytesNat cnt' in
        match sgn with
        | Signed => (- 2 ^ (8 * cnt - 1) ≤ z)%Z ∧ (z ≤ 2 ^ (8 * cnt - 1) - 1)%Z
        | Unsigned => (0 ≤ z)%Z ∧ (z < 2 ^ (8 * cnt))%Z
        end.

      Lemma _Z_to_bytes_inj_1 cnt endianness sgn z :
        in_Z_to_bytes_bounds cnt sgn z ->
        _Z_from_bytes endianness sgn (_Z_to_bytes (bitsize.bytesNat cnt) endianness sgn z) = z.
      Proof. apply _Z_from_to_bytes_roundtrip. Qed.

      Lemma _Z_to_bytes_inj_2 cnt endianness sgn z1 z2 :
        in_Z_to_bytes_bounds cnt sgn z1 ->
        in_Z_to_bytes_bounds cnt sgn z2 ->
        _Z_to_bytes (bitsize.bytesNat cnt) endianness sgn z1 = _Z_to_bytes (bitsize.bytesNat cnt) endianness sgn z2 ->
        z1 = z2.
      Proof.
        intros Hb1 Hb2 Heq%(f_equal (_Z_from_bytes endianness sgn)).
        move: Heq. by rewrite !_Z_to_bytes_inj_1.
      Qed.
      Instance: Inj eq eq Rval.
      Proof. by injection 1. Qed.

      Lemma Z_to_bytes_inj cnt sgn z1 z2 :
        in_Z_to_bytes_bounds cnt sgn z1 ->
        in_Z_to_bytes_bounds cnt sgn z2 ->
        Z_to_bytes cnt sgn z1 = Z_to_bytes cnt sgn z2 ->
        z1 = z2.
      Proof.
        rewrite /Z_to_bytes; intros Hb1 Hb2 Heq%(inj (fmap Rval)).
        exact: _Z_to_bytes_inj_2.
      Qed.

      Definition pure_encodes (t : type) (v : val) (vs : list runtime_val) : Prop :=
        match erase_qualifiers t with
        | Tnum sz sgn =>
          match v with
          | Vint v =>
            in_Z_to_bytes_bounds (int_rank.bitsize sz) sgn v /\
            vs = Z_to_bytes (int_rank.bitsize sz) sgn v
          | Vundef => pure_encodes_undef (int_rank.bitsize sz) vs
          | _ => False
          end
        | Tchar_ ct => False (* TODO *)
        | Tmember_pointer _ _ =>
          match v with
          | Vint v =>
            (* note: this is really an offset *)
            in_Z_to_bytes_bounds POINTER_BITSZ Unsigned v /\
            vs = Z_to_bytes POINTER_BITSZ Unsigned v
          | Vundef => pure_encodes_undef POINTER_BITSZ vs
          | _ => False
          end
        | Tbool =>
          if decide (v = Vint 0) then vs = [Rval 0%N]
          else if decide (v = Vint 1) then vs = [Rval 1%N]
          else False
        | Tnullptr =>
          vs = cptr 0 /\ v = Vptr nullptr
        | Tfloat_ _ => False
        | Tarch _ _ => False
        | Tptr _ =>
          match v with
          | Vptr p =>
            if decide (p = nullptr) then
              vs = cptr 0
            else
              vs = aptr p
          | _ => False
          end
        | Tfunction _
        | Tref _
        | Trv_ref _ =>
          match v with
          | Vptr p =>
            p <> nullptr /\
            vs = aptr p
          | Vundef => pure_encodes_undef POINTER_BITSZ vs
          | _ => False
          end
        | Tenum _ => False (* << TODO: incorrect *)
        | Tqualified _ _ => False (* unreachable *)
        | Tvoid
        | Tarray _ _
        | Tincomplete_array _
        | Tvariable_array _ _
        | Tnamed _ => False (* not directly encoded in memory *)
        | Tunsupported _ => False
        | Tdecltype _ => False
        | _ => False
        end.
      Definition encodes (t : type) (v : val) (vs : list runtime_val) : mpred :=
        [| pure_encodes t v vs |].

      #[global] Instance encodes_persistent : forall t v vs, Persistent (encodes t v vs) := _.

      #[global] Instance encodes_timeless : forall t v a, Timeless (encodes t v a) := _.

      #[local] Hint Resolve length_Z_to_bytes : core.
      #[local] Hint Resolve length_aptr : core.
      #[local] Hint Resolve length_cptr : core.
      #[local] Hint Resolve length_pure_encodes_undef : core.

      #[global] Instance encodes_nonvoid t v vs :
        Observe [| t <> Tvoid |] (encodes t v vs).
      Proof. apply: observe_intro_persistent; iIntros "!%". by destruct t. Qed.

      Lemma length_encodes t v vs :
        pure_encodes t v vs ->
          length vs = match erase_qualifiers t with
                      | Tbool => 1
                      | Tnum sz _ => int_rank.bytesNat sz

                      | Tmember_pointer _ _ | Tnullptr | Tptr _
                      | Tfunction _ | Tref _ | Trv_ref _ =>
                                                 POINTER_BYTES

                      | _ => 1 (* dummy for absurd case, but useful for length_encodes_pos. *)
                      end.
      Proof.
        rewrite /pure_encodes => ?.
        destruct (erase_qualifiers _) => //;
          destruct v => //; destruct_and? => //;
          repeat case_decide => //;
           simplify_eq; eauto.
        by destruct sz.
        erewrite length_pure_encodes_undef; eauto. by destruct sz.
      Qed.

      Lemma length_encodes_pos t v vs :
        pure_encodes t v vs ->
        length vs > 0.
      Proof.
        move=> /length_encodes ->. have ?: 1 > 0 by exact: le_n.
        induction t; simpl; try solve [ lia | exact: bytesNat_pos ].
        destruct sz; compute; lia.
      Qed.

      #[global] Instance Inj_aptr: Inj eq eq aptr.
      Proof.
        rewrite /aptr => p1 p2.
        by rewrite bytesNat_nnonnull'; csimpl => -[? _].
      Qed.

      Lemma pure_encodes_undef_aptr bitsz p :
        pure_encodes_undef bitsz (aptr p) -> False.
      Proof.
        rewrite /pure_encodes_undef /aptr.
        by rewrite (bytesNat_nnonnull' POINTER_BITSZ) (bytesNat_nnonnull' bitsz).
      Qed.

      Lemma pure_encodes_undef_Z_to_bytes bitsz sgn z :
        pure_encodes_undef bitsz (Z_to_bytes bitsz sgn z) ->
        False.
      Proof.
        rewrite /pure_encodes_undef /= bytesNat_nnonnull'.
        by edestruct Z_to_bytes_cons as (? & ? & ->).
      Qed.

      #[local] Hint Resolve pure_encodes_undef_aptr pure_encodes_undef_Z_to_bytes : core.

      #[global] Instance encodes_agree t v1 v2 vs :
        Observe2 [| v1 = v2 |] (encodes t v1 vs) (encodes t v2 vs).
      Proof.
        apply: observe_2_intro_persistent; rewrite /encodes /pure_encodes;
          iIntros (H1 H2) "!%".
        destruct (erase_qualifiers t) eqn:? =>//=; intros;
          repeat (try (case_decide || case_match); destruct_and?; simplify_eq => //);
        by [
          edestruct cptr_ne_aptr | edestruct pure_encodes_undef_aptr |
          edestruct pure_encodes_undef_Z_to_bytes |
          f_equiv; exact: Z_to_bytes_inj ].
      Qed.

      #[global] Instance encodes_consistent t v1 v2 vs1 vs2 :
        Observe2 [| length vs1 = length vs2 |] (encodes t v1 vs1) (encodes t v2 vs2).
      Proof. iIntros "!%". by move=> /length_encodes -> /length_encodes ->. Qed.
    End with_genv.

    Instance Z_to_bytes_proper :
      Proper (genv_leq ==> eq ==> eq ==> eq ==> eq) (@Z_to_bytes).
    Proof. intros ?? Hσ%genv_byte_order_proper. solve_proper. Qed.

    Instance cptr_proper :
      Proper (genv_leq ==> eq ==> eq) cptr.
    Proof. rewrite /cptr => σ1 σ2 Heq ?? ->. by rewrite Heq. Qed.

    Instance aptr_proper :
      Proper (genv_leq ==> eq ==> eq) aptr.
    Proof. rewrite /aptr => σ1 σ2 Heq ?? ->. by rewrite Heq. Qed.

    Instance encodes_proper :
      Proper (genv_leq ==> eq ==> eq ==> eq ==> lentails) encodes.
    Proof.
      unfold encodes; intros σ1 σ2 Heq t1 t2 -> v1 v2 -> vs1 vs2 ->.
      f_equiv; unfold pure_encodes, impl;
        destruct (erase_qualifiers t2) => //; destruct v2 => //;
        try case_decide; rewrite ?Heq //.
    Qed.

    Definition val_ (a : ptr) (v : val) q : mpred :=
      ghost_mem_own a q v.

    #[global] Instance val_agree a v1 v2 q1 q2 :
      Observe2 [| v1 = v2 |] (val_ a v1 q1) (val_ a v2 q2) := _.

    #[global] Instance val_cfrac_valid a v :
      CFracValid0 (val_ a v).
    Proof. solve_cfrac_valid. Qed.

    Instance val_cfractional a rv : CFractional (val_ a rv) := _.
    Instance val_as_cfractional a rv q :
      AsCFractional (val_ a rv q) (val_ a rv) q := _.
    Instance val_timeless a rv q : Timeless (val_ a rv q) := _.
    Typeclasses Opaque val_.

    Definition byte_ (a : addr) (rv : runtime_val) q : mpred :=
      heap_own a q rv.

    #[global] Instance byte_agree a v1 v2 q1 q2 :
      Observe2 [|v1 = v2|] (byte_ a v1 q1) (byte_ a v2 q2) := _.
    #[global] Instance byte_cfrac_valid a rv q :
      Observe [| q ≤ 1 |]%Qp (byte_ a rv q) := _.

    Instance byte_cfractional {a rv} : CFractional (byte_ a rv) := _.
    Instance byte_as_fractional a rv q :
      AsCFractional (byte_ a rv q) (fun q => byte_ a rv q) q := _.
    Instance byte_timeless {a rv q} : Timeless (byte_ a rv q) := _.

    Theorem byte_consistent a b b' q q' :
      byte_ a b q ** byte_ a b' q' |-- byte_ a b (q ⋅ q') ** [| b = b' |].
    Proof.
      iIntros "[Hb Hb']".
      iDestruct (byte_agree with "Hb Hb'") as %->.
      iCombine "Hb Hb'" as "Hb". by iFrame.
    Qed.

    Lemma byte_update (a : addr) (rv rv' : runtime_val) :
      byte_ a rv (cQp.mut 1)|-- |==> byte_ a rv' (cQp.mut 1).
    Proof. by apply own_update, singleton_update, cmra_update_exclusive. Qed.

    Definition bytes (a : addr) (vs : list runtime_val) q : mpred :=
      [∗list] o ↦ v ∈ vs, byte_ (a+N.of_nat o)%N v q.

    Instance bytes_timeless a rv q : Timeless (bytes a rv q) := _.
    Instance bytes_fractional a vs : CFractional (bytes a vs) := _.
    Instance bytes_as_fractional a vs q :
      AsCFractional (bytes a vs q) (bytes a vs) q.
    Proof. solve_as_cfrac. Qed.
    Lemma bytes_nil a q : bytes a [] q -|- emp.
    Proof. done. Qed.

    Lemma bytes_cons a v vs q :
      bytes a (v :: vs) q -|- byte_ a v q ** bytes (N.succ a) vs q.
    Proof.
      rewrite /bytes big_sepL_cons /= N.add_0_r. do 2 f_equiv.
      move => ?. do 2 f_equiv. apply leibniz_equiv_iff. lia.
    Qed.

    Lemma bytes_agree {a vs1 vs2 q1 q2} :
      length vs1 = length vs2 →
      bytes a vs1 q1 ⊢ bytes a vs2 q2 -∗ ⌜vs1 = vs2⌝.
    Proof.
      revert a vs2. induction vs1 as [ |v vs1 IH]=> a vs2.
      { intros ->%symmetry%nil_length_inv. auto. }
      destruct vs2 as [ |v' vs2]; first done. intros [= Hlen].
      rewrite !bytes_cons.
      iIntros "[Hv Hvs1] [Hv' Hvs2] /=".
      iDestruct (byte_agree with "Hv Hv'") as %->.
      by iDestruct (IH _ _ Hlen with "Hvs1 Hvs2") as %->.
    Qed.

    Lemma bytes_cfrac_valid a vs q :
      length vs > 0 ->
      bytes a vs q |-- [| q ≤ 1 |]%Qp.
    Proof.
      rewrite /bytes; case: vs => [ |v vs _] /=; first by lia.
      rewrite byte_cfrac_valid. by iIntros "[% _]".
    Qed.

    Lemma bytes_update {a : addr} {vs} vs' :
      length vs = length vs' →
      bytes a vs (cQp.mut 1) |-- |==> bytes a vs' (cQp.mut 1).
    Proof.
      rewrite /bytes -big_sepL_bupd.
      revert a vs'.
      induction vs as [ | v vs IH]; intros a vs' EqL.
      { simplify_list_eq. symmetry in EqL. apply length_zero_iff_nil in EqL.
        by subst vs'. }
      destruct vs' as [ |v' vs'].
      { exfalso. done. }
      rewrite 2!big_sepL_cons. apply bi.sep_mono'.
      { by apply byte_update. }
      iPoseProof (IH (a + 1)%N vs') as "HL".
      { simpl in EqL. lia. }
      iIntros "By".
      iDestruct ("HL" with "[By]") as "By";
        iApply (big_sepL_mono with "By"); intros; simpl;
        rewrite (_: a + N.of_nat (S k) = a + 1 + N.of_nat k)%N //; lia.
    Qed.

    Instance mem_inj_own_agree p (oa1 oa2 : option N) :
      Observe2 [| oa1 = oa2 |] (mem_inj_own p oa1) (mem_inj_own p oa2).
    Proof.
      apply /observe_2_intro_persistent /bi.wand_intro_r.
      rewrite -own_op singleton_op.
      rewrite own_valid discrete_valid singleton_valid.
      by iIntros "!%" => /= /to_agree_op_inv_L.
    Qed.

    (* Auxiliary definitions.
      They're not exported, so we don't give them a complete theory;
      however, some of their proofs can be done via TC inference *)
    #[local] Definition addr_encodes
        (σ : genv) (t : type) q (a : addr) (v : val) (vs : list runtime_val) :=
      encodes σ t v vs ** bytes a vs q ** vbytes a vs q.

    #[local] Instance addr_encodes_fractional {σ} ty a v vs :
      CFractional (λ q, addr_encodes σ ty q a v vs) := _.

    #[local] Instance addr_encodes_agree_dst σ t a v1 v2 vs1 vs2 q1 q2 :
      Observe2 [| vs1 = vs2 |]
        (addr_encodes σ t q1 a v1 vs1)
        (addr_encodes σ t q2 a v2 vs2).
    Proof.
      apply: observe_2_intro_persistent.
      iIntros "[En1 [By1 _]] [En2 [By2 _]]".
      iDestruct (encodes_consistent with "En1 En2") as %Heq.
      by iDestruct (bytes_agree Heq with "By1 By2") as %->.
    Qed.

    #[local] Instance addr_encodes_agree_src σ t v1 v2 a vs1 vs2 q1 q2 :
      Observe2 [| v1 = v2 |]
        (addr_encodes σ t q1 a v1 vs1)
        (addr_encodes σ t q2 a v2 vs2).
    Proof.
      iIntros "H1 H2".
      iDestruct (addr_encodes_agree_dst with "H1 H2") as %->.
      (* Using encodes_agree *)
      iApply (observe_2 with "H1 H2").
    Qed.

    #[global] Instance addr_encodes_cfrac_valid {σ} ty :
      CFracValid3 (addr_encodes σ ty).
    Proof.
      constructor. intros. apply: observe_intro_persistent.
      iDestruct 1 as (Hen%length_encodes_pos) "[B _]".
      by iApply (bytes_cfrac_valid with "B").
    Qed.

    #[local] Definition oaddr_encodes
        (σ : genv) (t : type) q (oa : option addr) p (v : val) :=
        match oa with
        | Some a =>
          Exists vs,
          addr_encodes σ t q a v vs
        | None => [| t <> Tvoid |] ** val_ p v q
        end.

    (* Needed by tptsto_cfractional *)
    #[local] Instance oaddr_encodes_fractional {σ} t oa p v :
      CFractional (λ q, oaddr_encodes σ t q oa p v).
    Proof. rewrite /oaddr_encodes; destruct oa; apply _. Qed.

    #[local] Instance oaddr_encodes_nonvoid {σ} ty q oa p v :
      Observe [| ty <> Tvoid |] (oaddr_encodes σ ty q oa p v).
    Proof. destruct oa; apply _. Qed.
    #[local] Instance oaddr_encodes_cfrac_valid {σ} t :
      CFracValid3 (oaddr_encodes σ t).
    Proof. constructor. intros ? oa ??. destruct oa; apply _. Qed.

    Definition code_own (p : ptr) (f : Func + Method + Ctor + Dtor) : mpred :=
      strict_valid_ptr p ** _code_own p f.
    Instance code_own_persistent f p : Persistent (code_own p f) := _.
    Instance code_own_affine f p : Affine (code_own p f) := _.
    Instance code_own_timeless f p : Timeless (code_own p f) := _.

    Lemma code_own_strict_valid f p : code_own p f ⊢ strict_valid_ptr p.
    Proof. iIntros "[$ _]". Qed.

    Lemma code_own_valid f p : code_own p f ⊢ valid_ptr p.
    Proof. by rewrite code_own_strict_valid strict_valid_valid. Qed.
    Typeclasses Opaque code_own.

    Definition code_at (_ : genv) (_ : translation_unit) (f : Func) (p : ptr) : mpred :=
      code_own p (inl (inl (inl f))).
    Definition method_at (_ : genv) (_ : translation_unit) (m : Method) (p : ptr) : mpred :=
      code_own p (inl (inl (inr m))).
    Definition ctor_at (_ : genv) (_ : translation_unit) (c : Ctor) (p : ptr) : mpred :=
      code_own p (inl (inr c)).
    Definition dtor_at (_ : genv) (_ : translation_unit) (d : Dtor) (p : ptr) : mpred :=
      code_own p (inr d).

    Instance code_at_persistent : forall s tu f p, Persistent (@code_at s tu f p) := _.
    Instance code_at_affine : forall s tu f p, Affine (@code_at s tu f p) := _.
    Instance code_at_timeless : forall s tu f p, Timeless (@code_at s tu f p) := _.

    Instance method_at_persistent : forall s tu f p, Persistent (@method_at s tu f p) := _.
    Instance method_at_affine : forall s tu f p, Affine (@method_at s tu f p) := _.
    Instance method_at_timeless : forall s tu f p, Timeless (@method_at s tu f p) := _.

    Instance ctor_at_persistent : forall s tu f p, Persistent (@ctor_at s tu f p) := _.
    Instance ctor_at_affine : forall s tu f p, Affine (@ctor_at s tu f p) := _.
    Instance ctor_at_timeless : forall s tu f p, Timeless (@ctor_at s tu f p) := _.

    Instance dtor_at_persistent : forall s tu f p, Persistent (@dtor_at s tu f p) := _.
    Instance dtor_at_affine : forall s tu f p, Affine (@dtor_at s tu f p) := _.
    Instance dtor_at_timeless : forall s tu f p, Timeless (@dtor_at s tu f p) := _.

    Axiom code_at_live : forall s tu f p, @code_at s tu f p |-- live_ptr p.
    Axiom method_at_live : forall s tu f p, @method_at s tu f p |-- live_ptr p.
    Axiom ctor_at_live : forall s tu f p, @ctor_at s tu f p |-- live_ptr p.
    Axiom dtor_at_live : forall s tu f p, @dtor_at s tu f p |-- live_ptr p.

    Section with_genv.
      Context {σ : genv}.
      #[local] Notation code_at := (code_at σ) (only parsing).
      #[local] Notation method_at := (method_at σ) (only parsing).
      #[local] Notation ctor_at := (ctor_at σ) (only parsing).
      #[local] Notation dtor_at := (dtor_at σ) (only parsing).

      Lemma code_at_strict_valid tu f p : code_at tu f p |-- strict_valid_ptr p.
      Proof. exact: code_own_strict_valid. Qed.
      Lemma method_at_strict_valid tu f p : method_at tu f p |-- strict_valid_ptr p.
      Proof. exact: code_own_strict_valid. Qed.
      Lemma ctor_at_strict_valid tu f p : ctor_at tu f p |-- strict_valid_ptr p.
      Proof. exact: code_own_strict_valid. Qed.
      Lemma dtor_at_strict_valid tu f p : dtor_at tu f p |-- strict_valid_ptr p.
      Proof. exact: code_own_strict_valid. Qed.
    End with_genv.

    #[local] Definition pinned_ptr (va : N) (p : ptr) : mpred :=
      valid_ptr p **
      ([| p = nullptr /\ va = 0%N |] \\//
      ([| p <> nullptr /\ ptr_vaddr p = Some va |] ** mem_inj_own p (Some va))).

    Lemma pinned_ptr_null : |-- pinned_ptr 0 nullptr.
    Proof. iSplit; by [iApply valid_ptr_nullptr | iLeft]. Qed.

    Definition type_ptr {resolve : genv} (ty : type) (p : ptr) : mpred :=
      [| p <> nullptr |] **
      [| aligned_ptr_ty ty p |] **
      [| is_Some (size_of resolve ty) |] **

      strict_valid_ptr p ** valid_ptr (p ,, o_sub resolve ty 1).
      (* TODO: inline valid_ptr, and assert validity of the range, like we should do in tptsto!
      For 0-byte objects, should we assert ownership of one byte, to get character pointers? *)
      (* alloc_own (alloc_id p) (l, h) ** [| l <= ptr_addr p <= ptr_addr (p ,, o_sub resolve ty 1) <= h |] *)

    Instance type_ptr_persistent σ p ty : Persistent (type_ptr (resolve:=σ) ty p) := _.
    Instance type_ptr_affine σ p ty : Affine (type_ptr (resolve:=σ) ty p) := _.
    Instance type_ptr_timeless σ p ty : Timeless (type_ptr (resolve:=σ) ty p) := _.

    Lemma type_ptr_off_nonnull {σ ty p o} :
      type_ptr ty (p ,, o) |-- [| p <> nullptr |].
    Admitted.

    Lemma type_ptr_strict_valid resolve ty p :
      type_ptr (resolve := resolve) ty p |-- strict_valid_ptr p.
    Proof. iDestruct 1 as "(_ & _ & _ & $ & _)". Qed.

    Lemma type_ptr_valid_plus_one resolve ty p :
      (* size_of resolve ty = Some sz -> *)
      type_ptr (resolve := resolve) ty p |--
      valid_ptr (p ,, o_sub resolve ty 1).
    Proof. iDestruct 1 as "(_ & _ & _ & _ & $)". Qed.

    Lemma type_ptr_erase : forall {σ} ty p,
        type_ptr ty p -|- type_ptr (erase_qualifiers ty) p.
    Proof.
      rewrite /type_ptr; intros.
      rewrite -aligned_ptr_ty_erase_qualifiers size_of_erase_qualifiers; iFrame "#%".
      iSplit.
      { iIntros "(%&%&%&#?&#?)"; iFrame "#%".
        admit. (* o_sub is independent of qualifiers *) }
      { iIntros "(%&%&%&#?&?)"; iFrame "#%".
        admit. }
    Admitted.

    Lemma type_ptr_aligned_pure σ ty p :
      type_ptr ty p |-- [| aligned_ptr_ty ty p |].
    Proof. iDestruct 1 as "(_ & $ & _)". Qed.

    Lemma type_ptr_size {σ} ty p : type_ptr ty p |-- [| is_Some (size_of σ ty) |].
    Proof. iDestruct 1 as "(_ & _ & % & _)"; eauto. Qed.

    (* See o_sub_mono in simple_pointers.v *)
    Axiom valid_ptr_o_sub_proper : forall {σ1 σ2 p ty}, genv_leq σ1 σ2 ->
      valid_ptr (p ,, o_sub σ1 ty 1) |-- valid_ptr (p ,, o_sub σ2 ty 1).

    Instance type_ptr_mono :
      Proper (genv_leq ==> eq ==> eq ==> (⊢)) (@type_ptr).
    Proof.
      rewrite /type_ptr /aligned_ptr_ty => σ1 σ2 Heq x y ????; subst.
      rewrite (valid_ptr_o_sub_proper Heq).
      do 3 f_equiv.
      - move=> -[align [HalTy Halp]]. eexists; split => //.
        move: Heq HalTy => /Proper_align_of /(_ y _ eq_refl).
        destruct 1; naive_solver.
      - f_equiv=> -[sz1].
        move: Heq => /Proper_size_of /(_ y _ eq_refl).
        destruct 1; naive_solver.
    Qed.

    (* This lemma is unused; it confirms we can lift the other half of
    pinned_ptr_aligned_divide, but we don't expose this. *)
    #[local] Lemma pinned_ptr_type_divide_2 {va n σ p ty}
      (Hal : align_of (σ := σ) ty = Some n) (Hnn : p <> nullptr) :
      pinned_ptr va p ⊢ valid_ptr (p ,, o_sub σ ty 1) -∗
      [| (n | va)%N |] -∗ type_ptr (resolve := σ) ty p.
    Proof.
      rewrite /type_ptr /aligned_ptr_ty Hal /=.
      iIntros "[V [%P|[%P P]]] #$ %HvaAl"; first by case P.
      iFrame (Hnn).
      (* iDestruct (pinned_ptr_valid with "P") as "$". *)
      iSplit; last admit.
      iExists _; iSplit; first done.
      iIntros "!%". rewrite /aligned_ptr.
      naive_solver.
    Admitted.

    (* XXX move *)
    Axiom align_of_uchar : forall resolve, @align_of resolve Tuchar = Some 1%N.

    (* Requirememnt is too strong, we'd want just (strict_)valid_ptr p; see comment
    above on aligned_ptr_mpred and mem_inj_own.
    XXX: this assumes that casting to uchar preserves the pointer.
    *)
    #[local] Lemma valid_type_uchar resolve p (Hnn : p <> nullptr) va :
      pinned_ptr va p ⊢
      valid_ptr (p ,, o_sub resolve Tuchar 1) -∗
      type_ptr (resolve := resolve) Tuchar p.
    Proof.
      iIntros "#P #V".
      iApply (pinned_ptr_type_divide_2 (n := 1)) => //. {
        exact: align_of_uchar. }
      iIntros "!%". exact: N.divide_1_l.
    Qed.

    (* todo(gmm): this isn't accurate, but it is sufficient to show that the axioms are
    instantiatable. *)
    Definition mdc_path {σ : genv} (this : globname) (most_derived : list globname)
               (q : cQp.t) (p : ptr) : mpred :=
      strict_valid_ptr p ** derivation_own p q this most_derived.

    Instance mdc_path_cfractional {σ} this mdc : CFractional1 (mdc_path this mdc) := _.
    Axiom mdc_path_cfrac_valid : forall {σ} cls path,
      CFracValid1 (mdc_path cls path).
    Instance mdc_path_timeless {σ} this mdc q p : Timeless (mdc_path this mdc q p) := _.
    Instance mdc_path_strict_valid {σ} this mdc q p : Observe (strict_valid_ptr p) (mdc_path this mdc q p).
    Proof. refine _. Qed.
    Instance mdc_path_agree {σ} cls1 cls2 q1 q2 p mdc1 mdc2 :
      Observe2 [| mdc1 = mdc2 /\ cls1 = cls2 |] (mdc_path cls1 mdc1 q1 p) (mdc_path cls2 mdc2 q2 p).
    Proof.
      rewrite /mdc_path.
      iIntros "[_ A] [_ B]".
      iDestruct (observe_2 [| _ = _ |] with "A B") as %Heq; inversion Heq; eauto.
    Qed.