More provenances

examples/intptr.c

@@ -83,7 +83,7 @@ int* roundtrip1(int* p){
 // Roundtrip cast with dummy arithmetic.
 [[rc::parameters("p : loc")]]
 [[rc::args("p @ &own<int<i32>>")]]
-[[rc::exists("id : {option alloc_id}")]] // ← Only ∃ on provenance.
+[[rc::exists("id : prov")]] // ← Only ∃ on provenance.
 [[rc::returns("{(id, p.2)} @ &own<place<{(id, p.2)}>>")]]
 int* roundtrip2(int* p){
   uintptr_t i = (uintptr_t) p;

examples/proofs/intptr/generated_spec.v

@@ -47,7 +47,7 @@ Section spec.
   (* Specifications for function [roundtrip2]. *)
   Definition type_of_roundtrip2 :=
     fn(∀ p : loc; (p @ (&own (int (i32)))); True)
-      → ∃ id : (option alloc_id), (((id, p.2)) @ (&own (place ((id, p.2))))); True.
+      → ∃ id : prov, (((id, p.2)) @ (&own (place ((id, p.2))))); True.
 
   (* Specifications for function [roundtrip3]. *)
   Definition type_of_roundtrip3 :=

theories/lang/ghost_state.v

@@ -26,7 +26,7 @@ Class heapG Σ := HeapG {
   heap_alloc_range_map_name  : gname;
   heap_alloc_alive_map_inG  :> ghost_mapG Σ alloc_id bool;
   heap_alloc_alive_map_name : gname;
-  heap_fntbl_inG             :> ghost_mapG Σ loc function;
+  heap_fntbl_inG             :> ghost_mapG Σ addr function;
   heap_fntbl_name            : gname;
 }.
 
@@ -74,7 +74,7 @@ Section definitions.
   the fact that this allocation is in bounds of allocatable memory. *)
   Definition loc_in_bounds_def (l : loc) (n : nat) : iProp Σ :=
     ∃ (id : alloc_id) (al : allocation),
-      ⌜l.1 = Some id⌝ ∗ ⌜al.(al_start) ≤ l.2⌝ ∗ ⌜l.2 + n ≤ al_end al⌝ ∗
+      ⌜l.1 = ProvAlloc (Some id)⌝ ∗ ⌜al.(al_start) ≤ l.2⌝ ∗ ⌜l.2 + n ≤ al_end al⌝ ∗
       ⌜allocation_in_range al⌝ ∗ alloc_range id al.
   Definition loc_in_bounds_aux : seal (@loc_in_bounds_def). by eexists. Qed.
   Definition loc_in_bounds := unseal loc_in_bounds_aux.
@@ -100,7 +100,7 @@ Section definitions.
   Proof. rewrite alloc_alive_eq. by apply _. Qed.
 
   Definition alloc_global (l : loc) : iProp Σ :=
-    ∃ id, ⌜l.1 = Some id⌝ ∗ alloc_alive id DfracDiscarded true.
+    ∃ id, ⌜l.1 = ProvAlloc (Some id)⌝ ∗ alloc_alive id DfracDiscarded true.
   Global Instance alloc_global_tl l : Timeless (alloc_global l).
   Proof. by apply _. Qed.
   Global Instance alloc_global_pers l : Persistent (alloc_global l).
@@ -111,7 +111,7 @@ Section definitions.
   [f] is stored at location [l]. NOTE: we use locations, but do not really
   store the code on the actual heap. *)
   Definition fntbl_entry_def (l : loc) (f: function) : iProp Σ :=
-    l ↪[ heap_fntbl_name ]□ f.
+    ∃ a, ⌜l = fn_loc a⌝ ∗ a ↪[ heap_fntbl_name ]□ f.
   Definition fntbl_entry_aux : seal (@fntbl_entry_def). by eexists. Qed.
   Definition fntbl_entry := unseal fntbl_entry_aux.
   Definition fntbl_entry_eq : @fntbl_entry = @fntbl_entry_def :=
@@ -130,7 +130,7 @@ Section definitions.
     own heap_heap_name (◯ {[ l.2 := (q, to_lock_stateR st, to_agree (id, b)) ]}).
 
   Definition heap_mapsto_mbyte_def (l : loc) (q : Qp) (b : mbyte) : iProp Σ :=
-    ∃ id, ⌜l.1 = Some id⌝ ∗ heap_mapsto_mbyte_st (RSt 0) l id q b.
+    ∃ id, ⌜l.1 = ProvAlloc (Some id)⌝ ∗ heap_mapsto_mbyte_st (RSt 0) l id q b.
   Definition heap_mapsto_mbyte_aux : seal (@heap_mapsto_mbyte_def). by eexists. Qed.
   Definition heap_mapsto_mbyte := unseal heap_mapsto_mbyte_aux.
   Definition heap_mapsto_mbyte_eq : @heap_mapsto_mbyte = @heap_mapsto_mbyte_def :=
@@ -147,7 +147,7 @@ Section definitions.
 
   (** Token witnessing that [l] has an allocation identifier that is alive. *)
   Definition alloc_alive_loc_def (l : loc) : iProp Σ :=
-    (∃ id q, ⌜l.1 = Some id⌝ ∗ alloc_alive id q true) ∨
+    (∃ id q, ⌜l.1 = ProvAlloc (Some id)⌝ ∗ alloc_alive id q true) ∨
     (∃ a q v, ⌜v ≠ []⌝ ∗ heap_mapsto (l.1, a) q v).
   Definition alloc_alive_loc_aux : seal (@alloc_alive_loc_def). by eexists. Qed.
   Definition alloc_alive_loc := unseal alloc_alive_loc_aux.
@@ -157,7 +157,7 @@ Section definitions.
   (** * Freeable *)
 
   Definition freeable_def (l : loc) (n : nat) : iProp Σ :=
-    ∃ id, ⌜l.1 = Some id⌝ ∗ alloc_range id {| al_start := l.2; al_len := n; al_alive := true |} ∗
+    ∃ id, ⌜l.1 = ProvAlloc (Some id)⌝ ∗ alloc_range id {| al_start := l.2; al_len := n; al_alive := true |} ∗
      alloc_alive id (DfracOwn 1) true.
   Definition freeable_aux : seal (@freeable_def). by eexists. Qed.
   Definition freeable := unseal freeable_aux.
@@ -175,7 +175,7 @@ Section definitions.
   Definition alloc_alive_ctx (ub : allocs) : iProp Σ :=
     ghost_map_auth heap_alloc_alive_map_name 1 (to_alloc_alive_map ub).
 
-  Definition fntbl_ctx (fns : gmap loc function) : iProp Σ :=
+  Definition fntbl_ctx (fns : gmap addr function) : iProp Σ :=
     ghost_map_auth heap_fntbl_name 1 fns.
 
   Definition heap_state_ctx (st : heap_state) : iProp Σ :=
@@ -232,8 +232,13 @@ Section fntbl.
   Implicit Types E : coPset.
 
   Lemma fntbl_entry_lookup t f fn :
-    fntbl_ctx t -∗ fntbl_entry f fn -∗ ⌜t !! f = Some fn⌝.
-  Proof. rewrite fntbl_entry_eq. by apply ghost_map_lookup. Qed.
+    fntbl_ctx t -∗ fntbl_entry f fn -∗ ⌜∃ a, f = fn_loc a ∧ t !! a = Some fn⌝.
+  Proof.
+    rewrite fntbl_entry_eq.
+    iIntros "Hctx (%a&->&Hentry)".
+    iDestruct (ghost_map_lookup with "Hctx Hentry") as %?.
+    by eauto.
+  Qed.
 End fntbl.
 
 Section alloc_range.
@@ -263,7 +268,7 @@ Section alloc_range.
   Qed.
 
   Lemma alloc_range_to_loc_in_bounds l id (n : nat) al:
-    l.1 = Some id →
+    l.1 = ProvAlloc (Some id) →
     al.(al_start) ≤ l.2 ∧ l.2 + n ≤ al_end al →
     allocation_in_range al →
     alloc_range id al -∗ loc_in_bounds l n.
@@ -343,7 +348,7 @@ Section loc_in_bounds.
       iDestruct "H1" as (id al Hl1 ???) "#H1".
       iDestruct "H2" as (?? Hl2 ? Hend ?) "#H2".
       move: Hl1 Hl2 => /= Hl1 Hl2. iExists id, al.
-      unfold al_end in *. simpl in *. simplify_eq.
+      destruct l. unfold al_end in *. simpl in *. simplify_eq.
       iDestruct (alloc_range_agree with "H2 H1") as %[? <-].
       iFrame "H1". iPureIntro. rewrite /shift_loc /= in Hend. naive_solver lia.
     - iIntros "H". iDestruct "H" as (id al ????) "#H".
@@ -418,7 +423,7 @@ Section heap.
     intros p q. rewrite heap_mapsto_mbyte_eq. iSplit.
     - iDestruct 1 as (??) "[H1 H2]". iSplitL "H1"; iExists id; by iSplit.
     - iIntros "[H1 H2]". iDestruct "H1" as (??) "H1". iDestruct "H2" as (??) "H2".
-      simplify_eq. iExists id. iSplit; first done. by iSplitL "H1".
+      destruct l; simplify_eq/=. iExists _. iSplit; first done. by iSplitL "H1".
   Qed.
 
   Global Instance heap_mapsto_mbyte_as_fractional l q v:
@@ -439,13 +444,13 @@ Section heap.
     l ↦{q} v -∗ loc_in_bounds l (length v).
   Proof. rewrite heap_mapsto_eq. iIntros "[$ _]". Qed.
 
-  Lemma loc_in_bounds_has_alloc_id l n: loc_in_bounds l n -∗ ⌜is_Some l.1⌝.
+  Lemma loc_in_bounds_has_alloc_id l n: loc_in_bounds l n -∗ ⌜∃ aid, l.1 = ProvAlloc (Some aid)⌝.
   Proof.
     rewrite loc_in_bounds_eq. iIntros "H". iDestruct "H" as (id ?????) "H".
     iPureIntro. by exists id.
   Qed.
 
-  Lemma heap_mapsto_has_alloc_id l q v : l ↦{q} v -∗ ⌜is_Some l.1⌝.
+  Lemma heap_mapsto_has_alloc_id l q v : l ↦{q} v -∗ ⌜∃ aid, l.1 = ProvAlloc (Some aid)⌝.
   Proof.
     iIntros "Hl". iApply loc_in_bounds_has_alloc_id.
     by iApply heap_mapsto_loc_in_bounds.
@@ -519,7 +524,7 @@ Section heap.
   Qed.
 
   Lemma heap_alloc_st l h v aid :
-    l.1 = Some aid →
+    l.1 = ProvAlloc (Some aid) →
     heap_range_free h l.2 (length v) →
     heap_ctx h ==∗
       heap_ctx (heap_alloc l.2 v aid h) ∗
@@ -544,7 +549,7 @@ Section heap.
   Qed.
 
   Lemma heap_alloc l h v id al :
-    l.1 = Some id →
+    l.1 = ProvAlloc (Some id) →
     heap_range_free h l.2 (length v) →
     al.(al_start) = l.2 →
     al.(al_len) = length v →
@@ -654,9 +659,9 @@ Section heap.
     { iFrame. by iIntros "!#" (?) "$ !#". }
     rewrite ->heap_mapsto_cons_mbyte, heap_mapsto_mbyte_eq.
     iDestruct "Hv" as "[Hb [? Hl]]". iDestruct "Hb" as (? Heq) "Hb".
-    rewrite /heap_lookup_loc Heq.
-    move: Hat => /= -[[? [? [Hin [?[n ?]]]]] ?]; simplify_eq.
-    iMod ("IH" with "[] Hh Hl") as "{IH}[Hh IH]" => //.
+    move: Hat. rewrite /heap_lookup_loc Heq /= => -[[? [? [Hin [?[n ?]]]]] ?]; simplify_eq/=.
+    iMod ("IH" with "[] Hh Hl") as "{IH}[Hh IH]".
+    { iPureIntro => /=. by destruct l; simplify_eq/=. }
     iMod (heap_read_mbyte_vs _ 0 1 with "Hh Hb") as "[Hh Hb]".
     { rewrite heap_update_lookup_not_in_range // /shift_loc /=. lia. }
     iModIntro. iSplitL "Hh".
@@ -717,9 +722,9 @@ Section heap.
     move: Hlen => -[] Hlen.
     rewrite heap_mapsto_cons_mbyte heap_mapsto_mbyte_eq.
     iDestruct "Hv" as "[Hb [? Hl]]". iDestruct "Hb" as (? Heq) "Hb".
-    rewrite /heap_lookup_loc Heq.
-    move: Hat => /= -[[? [? [Hin [??]]]] ?]; simplify_eq.
-    iMod ("IH" with "[] [] Hh Hl") as "{IH}[Hh IH]" => //.
+    move: Hat. rewrite /heap_lookup_loc Heq /= => -[[? [? [Hin [??]]]] ?]; simplify_eq/=.
+    iMod ("IH" with "[] [] Hh Hl") as "{IH}[Hh IH]"; [|done|].
+    { iPureIntro => /=. by destruct l; simplify_eq/=. }
     iMod (heap_write_mbyte_vs with "Hh Hb") as "[Hh Hb]".
     { rewrite heap_update_lookup_not_in_range /shift_loc /= ?Hin ?Heq //=. lia. }
     iSplitL "Hh". { rewrite /heap_upd /=. erewrite partial_alter_to_insert; first done.
@@ -737,7 +742,7 @@ Section heap.
   Qed.
 
   Lemma heap_free_free_st l h v aid :
-    l.1 = Some aid →
+    l.1 = ProvAlloc (Some aid) →
     heap_ctx h ∗ ([∗ list] i↦b ∈ v, heap_mapsto_mbyte_st (RSt 0) (l +ₗ i) aid 1 b) ==∗
       heap_ctx (heap_free l.2 (length v) h).
   Proof.
@@ -770,7 +775,7 @@ Section heap.
     rewrite heap_mapsto_eq /heap_mapsto_def. iDestruct "Hl" as "[_ Hl]".
     iApply (big_sepL_impl with "Hl"). iIntros (???) "!> H".
     rewrite heap_mapsto_mbyte_eq /heap_mapsto_mbyte_def /=.
-    iDestruct "H" as (?) "[% H]". by simplify_eq.
+    iDestruct "H" as (?) "[% H]". by destruct l; simplify_eq/=.
   Qed.
 End heap.
 

theories/lang/heap.v

@@ -50,18 +50,18 @@ Fixpoint heap_update (a : addr) (v : val) (faid : option alloc_id → alloc_id)
 
 Definition heap_lookup_loc (l : loc) (v : val) (Plk : lock_state → Prop)
                            (h : heap) : Prop :=
-  heap_lookup l.2 v (λ aid, l.1 = Some aid) Plk h.
+  heap_lookup l.2 v (λ aid, l.1 = ProvAlloc (Some aid)) Plk h.
 
 Definition heap_alloc (a : addr) (v : val) (aid : alloc_id) (h : heap) : heap :=
   heap_update a v (λ _, aid) (λ _, RSt 0%nat) h.
 
 Definition heap_at (l : loc) (ly : layout) (v : val) (Plk : lock_state → Prop)
                    (h : heap) : Prop :=
-  is_Some l.1 ∧ l `has_layout_loc` ly ∧ v `has_layout_val` ly ∧
+  (∃ aid, l.1 = ProvAlloc (Some aid))  ∧ l `has_layout_loc` ly ∧ v `has_layout_val` ly ∧
   heap_lookup_loc l v Plk h.
 
-Definition heap_upd l v flk h :=
-  heap_update l.2 v (default (default dummy_alloc_id l.1)) flk h.
+Definition heap_upd (l : loc) v flk h :=
+  heap_update l.2 v (default (default dummy_alloc_id (prov_alloc_id l.1))) flk h.
 
 (** Predicate stating that the [n] first bytes from address [a] in [h] have
 not been allocated. *)
@@ -229,14 +229,14 @@ Definition alloc_id_alive (aid : alloc_id) (st : heap_state) : Prop :=
   ∃ alloc, st.(hs_allocs) !! aid = Some alloc ∧ alloc.(al_alive).
 
 Definition block_alive (l : loc) (st : heap_state) : Prop :=
-  ∃ aid, l.1 = Some aid ∧ alloc_id_alive aid st.
+  ∃ aid, l.1 = ProvAlloc (Some aid) ∧ alloc_id_alive aid st.
 
 (** The address range between [l] and [l +ₗ n] (included) is in range of the
     allocation that contains [l]. Note that we consider the 1-past-the-end
     pointer to be in range of an allocation. *)
 Definition heap_state_loc_in_bounds (l : loc) (n : nat) (st : heap_state) : Prop :=
   ∃ alloc_id al,
-    l.1 = Some alloc_id ∧
+    l.1 = ProvAlloc (Some alloc_id) ∧
     st.(hs_allocs) !! alloc_id = Some al ∧
     al.(al_start) ≤ l.2 ∧
     l.2 + n ≤ al_end al.
@@ -252,7 +252,7 @@ Definition addr_in_range_alloc (a : addr) (aid : alloc_id) (st : heap_state) : P
 Inductive alloc_new_block : heap_state → loc → val → heap_state → Prop :=
 | AllocNewBlock σ l aid v:
     let alloc := Allocation l.2 (length v) true in
-    l.1 = Some aid →
+    l.1 = ProvAlloc (Some aid) →
     σ.(hs_allocs) !! aid = None →
     allocation_in_range alloc →
     heap_range_free σ.(hs_heap) l.2 (length v) →
@@ -273,7 +273,7 @@ Inductive free_block : heap_state → loc → layout → heap_state → Prop :=
 | FreeBlock σ l aid ly v:
     let al_alive := Allocation l.2 ly.(ly_size) true  in
     let al_dead  := Allocation l.2 ly.(ly_size) false in
-    l.1 = Some aid →
+    l.1 = ProvAlloc (Some aid) →
     σ.(hs_allocs) !! aid = Some al_alive →
     length v = ly.(ly_size) →
     heap_lookup_loc l v (λ st, st = RSt 0%nat) σ.(hs_heap) →
@@ -290,9 +290,17 @@ Inductive free_blocks : heap_state → list (loc * layout) → heap_state → Pr
     free_blocks σ' ls σ'' →
     free_blocks σ ((l, ly) :: ls) σ''.
 
+Lemma heap_state_loc_in_bounds_has_alloc_id l n σ:
+  heap_state_loc_in_bounds l n σ → ∃ aid, l.1 = ProvAlloc (Some aid).
+Proof. rewrite /heap_state_loc_in_bounds. naive_solver. Qed.
+
+Lemma valid_ptr_has_alloc_id l σ:
+  valid_ptr l σ → ∃ aid, l.1 = ProvAlloc (Some aid).
+Proof. rewrite /valid_ptr => ?. apply: heap_state_loc_in_bounds_has_alloc_id. naive_solver. Qed.
+
 Lemma free_block_inj hs l ly hs1 hs2:
   free_block hs l ly hs1 → free_block hs l ly hs2 → hs1 = hs2.
-Proof. inversion 1; simplify_eq. by inversion 1; simplify_eq. Qed.
+Proof. destruct l. inversion 1; simplify_eq. by inversion 1; simplify_eq/=. Qed.
 
 Lemma free_blocks_inj hs1 hs2 hs ls:
   free_blocks hs ls hs1 → free_blocks hs ls hs2 → hs1 = hs2.

theories/lang/lang.v

@@ -95,7 +95,7 @@ Record function := {
 (* TODO: put both function and bytes in the same heap or make pointers disjoint *)
 Record state := {
   st_heap: heap_state;
-  st_fntbl: gmap loc function;
+  st_fntbl: gmap addr function;
 }.
 
 Definition heap_fmap (f : heap → heap) (σ : state) := {|
@@ -241,24 +241,24 @@ Inductive eval_bin_op : bin_op → op_type → op_type → state → val → val
 | EqOpPNull v1 v2 σ l v:
     heap_state_loc_in_bounds l 0%nat σ.(st_heap) →
     val_to_loc v1 = Some l →
-    val_to_Z v2 size_t = Some 0 →
+    v2 = NULL →
     (* TODO ( see below ): Should we really hard code i32 here because of C? *)
     i2v (Z_of_bool false) i32 = v →
     eval_bin_op EqOp PtrOp PtrOp σ v1 v2 v
 | NeOpPNull v1 v2 σ l v:
     heap_state_loc_in_bounds l 0%nat σ.(st_heap) →
     val_to_loc v1 = Some l →
-    val_to_Z v2 size_t = Some 0 →
+    v2 = NULL →
     i2v (Z_of_bool true) i32 = v →
     eval_bin_op NeOp PtrOp PtrOp σ v1 v2 v
 | EqOpNullNull v1 v2 σ v:
-    val_to_Z v1 size_t = Some 0 →
-    val_to_Z v2 size_t = Some 0 →
+    v1 = NULL →
+    v2 = NULL →
     i2v (Z_of_bool true) i32 = v →
     eval_bin_op EqOp PtrOp PtrOp σ v1 v2 v
 | NeOpNullNull v1 v2 σ v:
-    val_to_Z v1 size_t = Some 0 →
-    val_to_Z v2 size_t = Some 0 →
+    v1 = NULL →
+    v2 = NULL →
     i2v (Z_of_bool false) i32 = v →
     eval_bin_op NeOp PtrOp PtrOp σ v1 v2 v
 | RelOpPP v1 v2 σ l1 l2 v b op:
@@ -402,9 +402,10 @@ comparing pointers? (see lambda rust) *)
     z1 = z2 →
     expr_step (CAS (IntOp it) (Val v1) (Val v2) (Val v3)) σ []
               (Val (val_of_bool true)) (heap_fmap (heap_upd l1 v3 (λ _, RSt 0%nat)) σ) []
-| CallS lsa lsv σ hs' hs'' vf vs f rf fn fn' :
+| CallS lsa lsv σ hs' hs'' vf vs f rf fn fn' a:
     val_to_loc vf = Some f →
-    σ.(st_fntbl) !! f = Some fn →
+    f = fn_loc a →
+    σ.(st_fntbl) !! a = Some fn →
     length lsa = length fn.(f_args) →
     length lsv = length fn.(f_local_vars) →
     (* substitute the variables in fn with the corresponding locations *)
@@ -421,9 +422,10 @@ comparing pointers? (see lambda rust) *)
     (* add used blocks allocations  *)
     rf = {| rf_fn := fn'; rf_locs := zip lsa fn.(f_args).*2 ++ zip lsv fn.(f_local_vars).*2; |} →
     expr_step (Call (Val vf) (Val <$> vs)) σ [] (to_rtstmt rf (Goto fn'.(f_init))) {| st_heap := hs''; st_fntbl := σ.(st_fntbl)|} []
-| CallFailS σ vf vs f fn:
+| CallFailS σ vf vs f fn a:
     val_to_loc vf = Some f →
-    σ.(st_fntbl) !! f = Some fn →
+    f = fn_loc a →
+    σ.(st_fntbl) !! a = Some fn →
     Forall2 has_layout_val vs fn.(f_args).*2 →
     expr_step (Call (Val vf) (Val <$> vs)) σ [] AllocFailed σ []
 | ConcatS vs σ:

theories/lang/lifting.v

@@ -427,6 +427,8 @@ Lemma wp_ptr_relop Φ op v1 v2 l1 l2 E b:
   WP BinOp op PtrOp PtrOp (Val v1) (Val v2) @ E {{ Φ }}.
 Proof.
   iIntros (Hv1 Hv2 Hop) "#Hl1 #Hl2 HΦ".
+  iDestruct (loc_in_bounds_has_alloc_id with "Hl1") as %[??].
+  iDestruct (loc_in_bounds_has_alloc_id with "Hl2") as %[??].
   iApply wp_binop. iIntros (σ) "Hσ".
   iAssert ⌜valid_ptr l1 σ.(st_heap)⌝%I as %?. {
     iApply (alloc_alive_loc_to_valid_ptr with "Hl1 [HΦ] Hσ").
@@ -438,7 +440,9 @@ Proof.
   }
   iSplit; first by iPureIntro; eexists _; econstructor.
   iDestruct "HΦ" as "(_&_&HΦ)". iIntros "!>" (v' Hstep). iFrame.
-  inversion Hstep; simplify_eq => //; by move: Hv1 Hv2 => /val_of_to_loc ?/val_of_to_loc?; subst.
+  inversion Hstep; simplify_eq => //.
+  all: try rewrite val_to_of_loc in Hv1; simplify_eq.
+  all: try rewrite val_to_of_loc in Hv2; simplify_eq.
 Qed.
 
 Lemma wp_ptr_offset Φ vl l E it o ly vo:
@@ -688,7 +692,7 @@ Proof.
   move => Hf Hly. move: (Hly) => /Forall2_length. rewrite fmap_length => Hlen_vs.
   iIntros "Hf HWP". iApply wp_lift_expr_step; first done.
   iIntros (σ1) "((%&Hhctx&Hbctx)&Hfctx)".
-  iDestruct (fntbl_entry_lookup with "Hfctx Hf") as %Hfn. iModIntro.
+  iDestruct (fntbl_entry_lookup with "Hfctx Hf") as %[a [? Hfn]]; subst. iModIntro.
   iSplit; first by eauto 10 using CallFailS.
   iIntros (??[??]? Hstep _) "!>". inv_expr_step; last first. {
     (* Alloc failure case. *)

theories/lang/loc.v

@@ -17,10 +17,43 @@ Definition addr := Z.
 Definition alloc_id := Z.
 Definition dummy_alloc_id : alloc_id := 0.
 
+(** Provenances *)
+Inductive prov :=
+| ProvNull
+| ProvAlloc (aid : option alloc_id)
+| ProvFnPtr.
+Global Instance prov_inhabited : Inhabited prov := populate ProvNull.
+Global Instance prov_eq_dec : EqDecision prov.
+Proof. solve_decision. Qed.
+Global Instance prov_countable : Countable prov.
+Proof.
+  refine (inj_countable'
+    (λ prov,
+     match prov with
+     | ProvNull => inl (inl tt)
+     | ProvAlloc aid => inl (inr aid)
+     | ProvFnPtr => inr tt
+     end
+    )
+    (λ prov,
+     match prov with
+     | inl (inl _) => ProvNull
+     | inl (inr aid) => ProvAlloc aid
+     | inr _ => ProvFnPtr
+     end) _); abstract by intros [].
+Defined.
+
+Definition prov_alloc_id (p : prov) : option alloc_id :=
+  if p is ProvAlloc aid then aid else None.
+
 (** Memory location. *)
-Definition loc : Set := option alloc_id * addr.
+Definition loc : Set := prov * addr.
 Bind Scope loc_scope with loc.
 
+Definition fn_loc (a : addr) : loc := (ProvFnPtr, a).
+Definition NULL_loc : loc := (ProvNull, 0).
+Typeclasses Opaque NULL_loc fn_loc.
+
 (** Shifts location [l] by offset [z]. *)
 Definition shift_loc (l : loc) (z : Z) : loc := (l.1, l.2 + z).
 Notation "l +ₗ z" := (shift_loc l%L z%Z)

theories/lang/notation.v

@@ -150,9 +150,7 @@ Definition void_layout : layout := {| ly_size := 0; ly_align_log := 0 |}.
 Definition void_ptr : layout := {| ly_size := bytes_per_addr; ly_align_log := bytes_per_addr_log |}.
 Notation "'void*'" := (void_ptr).
 
-Definition NULL : val := i2v 0 size_t.
 Definition VOID : val := [].
-Typeclasses Opaque NULL.
 
 Definition field_list := list (option var_name * layout).
 

theories/lang/val.v

@@ -44,6 +44,9 @@ Definition val_to_loc_n (n : nat) (v : val) : option loc :=
 Definition val_to_loc : val → option loc :=
   val_to_loc_n bytes_per_addr.
 
+Definition NULL : val := val_of_loc NULL_loc.
+Typeclasses Opaque NULL.
+
 Lemma val_of_loc_n_length n l:
   length (val_of_loc_n n l) = n.
 Proof.
@@ -93,6 +96,9 @@ Proof.
   apply val_to_loc_n_length.
 Qed.
 
+Global Instance val_of_loc_inj : Inj (=) (=) val_of_loc.
+Proof. move => x y Heq. have := val_to_of_loc x. have := val_to_of_loc y. rewrite Heq. by simplify_eq. Qed.
+
 Typeclasses Opaque val_of_loc_n val_to_loc_n val_of_loc val_to_loc.
 Arguments val_of_loc : simpl never.
 Arguments val_to_loc : simpl never.
@@ -328,7 +334,7 @@ Definition int_repr_to_Z (i : int_repr) : Z :=
 
 Definition int_repr_to_loc (i : int_repr) : loc :=
   match i with
-  | IRInt z => (None, z)
+  | IRInt z => (ProvAlloc None, z)
   | IRLoc l => l
   end.
 

theories/lithium/interpreter.v

@@ -524,6 +524,7 @@ Ltac liTrue :=
 
 Ltac liFalse :=
   lazymatch goal with
+  | |- envs_entails _ False => exfalso; shelve
   | |- False => shelve
   end.
 

theories/typing/adequacy.v

@@ -12,7 +12,7 @@ Class typePreG Σ := PreTypeG {
   type_heap_heap_inG             :> inG Σ (authR heapUR);
   type_heap_alloc_range_map_inG  :> ghost_mapG Σ alloc_id (Z * nat);
   type_heap_alloc_alive_map_inG  :> ghost_mapG Σ alloc_id bool;
-  type_heap_fntbl_inG            :> ghost_mapG Σ loc function;
+  type_heap_fntbl_inG            :> ghost_mapG Σ addr function;
 }.
 
 Definition typeΣ : gFunctors :=
@@ -20,7 +20,7 @@ Definition typeΣ : gFunctors :=
    GFunctor (constRF (authR heapUR));
    ghost_mapΣ alloc_id (Z * nat);
    ghost_mapΣ alloc_id bool;
-   ghost_mapΣ loc function].
+   ghost_mapΣ addr function].
 Instance subG_typePreG {Σ} : subG typeΣ Σ → typePreG Σ.
 Proof. solve_inG. Qed.
 
@@ -30,20 +30,20 @@ Definition initial_prog (main : loc) : runtime_expr :=
 Definition initial_heap_state :=
   {| hs_heap := ∅; hs_allocs := ∅; |}.
 
-Definition initial_state (fns : gmap loc function) :=
+Definition initial_state (fns : gmap addr function) :=
   {| st_heap := initial_heap_state; st_fntbl := fns; |}.
 
 Definition main_type `{!typeG Σ} (P : iProp Σ) :=
   fn(∀ () : (); P) → ∃ () : (), int i32; True.
 
 (** * The main adequacy lemma *)
-Lemma refinedc_adequacy Σ `{!typePreG Σ} (thread_mains : list loc) (fns : gmap loc function) (gls : list loc) (gvs : list val.val) n t2 σ2 κs hs σ:
+Lemma refinedc_adequacy Σ `{!typePreG Σ} (thread_mains : list loc) (fns : gmap addr function) (gls : list loc) (gvs : list val.val) n t2 σ2 κs hs σ:
   alloc_new_blocks initial_heap_state gls gvs hs →
   σ = {| st_heap := hs; st_fntbl := fns; |} →
   (∀ {HtypeG : typeG Σ}, ∃ gl gt,
   let Hglobals : globalG Σ := {| global_locs := gl; global_initialized_types := gt; |} in
     ([∗ list] l; v ∈ gls; gvs, l ↦ v) -∗
-    ([∗ map] k↦qs∈fns, fntbl_entry k qs) ={⊤}=∗
+    ([∗ map] k↦qs∈fns, fntbl_entry (fn_loc k) qs) ={⊤}=∗
       [∗ list] main ∈ thread_mains, ∃ P, main ◁ᵥ main @ function_ptr (main_type P) ∗ P) →
   nsteps (Λ := c_lang) n (initial_prog <$> thread_mains, σ) κs (t2, σ2) →
   ∀ e2, e2 ∈ t2 → not_stuck e2 σ2.
@@ -66,10 +66,10 @@ Proof.
     by iFrame.
   }
   rewrite big_sepL2_sep. iDestruct "Hmt" as "[Hmt Hfree]".
-  iAssert (|==> [∗ map] k↦qs ∈ fns, fntbl_entry k qs)%I with "[Hfm]" as ">Hfm". {
+  iAssert (|==> [∗ map] k↦qs ∈ fns, fntbl_entry (fn_loc k) qs)%I with "[Hfm]" as ">Hfm". {
     iApply big_sepM_bupd. iApply (big_sepM_impl with "Hfm").
     iIntros "!>" (???) "Hm". rewrite fntbl_entry_eq.
-    by iApply ghost_map_elem_persist.
+    iExists _. iSplitR; [done|]. by iApply ghost_map_elem_persist.
   }
   iMod (Hwp with "Hmt Hfm") as "Hmains".
 
@@ -86,14 +86,14 @@ Proof.
 Qed.
 
 (** * Helper functions for using the adequacy lemma *)
-Definition fn_lists_to_fns (locs : list loc) (fns : list function) : gmap loc function :=
-  list_to_map (zip locs fns).
+Definition fn_lists_to_fns (addrs : list addr) (fns : list function) : gmap addr function :=
+  list_to_map (zip addrs fns).
 
-Lemma fn_lists_to_fns_cons `{!refinedcG Σ} loc