Skip to content
GitLab
Commit 551866b2 authored by Rodolphe Lepigre's avatar Rodolphe Lepigre Committed by Michael Sammler
Browse files

Cleaning up around [lang.v]

parent 993943a7
Pipeline #42798 passed with stage
in 15 minutes and 15 seconds
Expand all Hide whitespace changes
Inline Side-by-side
theories/lang/base.v
View file @ 551866b2
......@@ -47,6 +47,12 @@ Definition Z_of_bool (b : bool) : Z :=
if b then 1 else 0.
Typeclasses Opaque Z_of_bool.
Lemma Z_of_bool_true b: Z_of_bool b ≠ 0 ↔ b = true.
Proof. destruct b; naive_solver. Qed.
Lemma Z_of_bool_false b: Z_of_bool b = 0 ↔ b = false.
Proof. destruct b; naive_solver. Qed.
Lemma big_sepL2_fupd `{BiFUpd PROP} {A B} E (Φ : nat → A → B → PROP) l1 l2 :
([∗ list] k↦x;y ∈ l1;l2, |={E}=> Φ k x y) ={E}=∗ [∗ list] k↦x;y ∈ l1;l2, Φ k x y.
Proof. rewrite !big_sepL2_alt. iIntros "[$ H]". by iApply big_sepL_fupd. Qed.
......
theories/lang/byte.v 0 → 100644
View file @ 551866b2
From refinedc.lang Require Import base.
Open Scope Z_scope.
(** Representation of a standard (8-bit) byte. *)
Definition bits_per_byte : Z := 8.
Definition byte_modulus : Z :=
Eval cbv in 2 ^ bits_per_byte.
Record byte :=
Byte {
byte_val : Z;
byte_constr : -1 < byte_val < byte_modulus;
}.
Program Definition byte0 : byte := {| byte_val := 0; |}.
Next Obligation. done. Qed.
Instance byte_eq_dec : EqDecision byte.
Proof.
move => [b1 H1] [b2 H2]. destruct (decide (b1 = b2)) as [->|].
- left. assert (H1 = H2) as ->; [|done]. apply proof_irrel.
- right. naive_solver.
Qed.
theories/lang/heap.v
View file @ 551866b2
......@@ -36,7 +36,7 @@ Definition to_lock_stateR (x : lock_state) : lock_stateR :=
match x with RSt n => Cinr n | WSt => Cinl (Excl ()) end.
Definition to_heap : heap → heapUR :=
fmap (λ v, (1%Qp, to_lock_stateR (v.1.2), to_agree (v.1.1, v.2))).
fmap (λ v, (1%Qp, to_lock_stateR v.(hc_lock_state), to_agree (v.(hc_alloc_id), v.(hc_value)))).
Definition to_alloc (a : allocation) : allocR :=
to_agree a.
......@@ -111,10 +111,13 @@ Section definitions.
Definition fntbl_ctx (t : gmap loc function) : iProp Σ :=
(own heap_fntbl_name (● to_fntbl t))%I.
Definition state_ctx (σ:state) : iProp Σ :=
Definition heap_state_ctx (st : heap_state) : iProp Σ :=
⌜True⌝ ∗ (* TODO: fill in sensible invariants here *)
heap_ctx σ.(st_heap) ∗
allocs_ctx σ.(st_allocs) ∗
heap_ctx st.(hs_heap) ∗
allocs_ctx st.(hs_allocs).
Definition state_ctx (σ:state) : iProp Σ :=
heap_state_ctx σ.(st_heap) ∗
fntbl_ctx σ.(st_fntbl).
End definitions.
......@@ -139,13 +142,13 @@ Section to_heap.
Implicit Types h : heap.
Lemma to_heap_valid h : ✓ to_heap h.
Proof. intros a. rewrite lookup_fmap. by case (h !! a) => // -[[?[]]?] /=. Qed.
Proof. intros a. rewrite lookup_fmap. by case (h !! a) => // -[?[]?]. Qed.
Lemma lookup_to_heap_None h a : h !! a = None → to_heap h !! a = None.
Proof. by rewrite /to_heap lookup_fmap=> ->. Qed.
Lemma to_heap_insert h a id v x:
to_heap (<[a:=(id, x, v)]> h)
to_heap (<[a:=HeapCell id x v]> h)
= <[a:=(1%Qp, to_lock_stateR x, to_agree (id, v))]> (to_heap h).
Proof. by rewrite /to_heap fmap_insert. Qed.
......@@ -278,10 +281,10 @@ Section loc_in_bounds.
Proof. move => ?. rewrite (le_plus_minus m n) // -loc_in_bounds_split. iIntros "[$ _]". Qed.
Lemma loc_in_bounds_to_heap_loc_in_bounds l σ n:
loc_in_bounds l n -∗ state_ctx σ -∗ ⌜heap_loc_in_bounds l n σ⌝.
loc_in_bounds l n -∗ state_ctx σ -∗ ⌜heap_state_loc_in_bounds l n σ.(st_heap)⌝.
Proof.
rewrite loc_in_bounds_eq.
iIntros "Hb (?&?&Hctx&?)". iDestruct "Hb" as (aid a [?[??]]) "Hb".
iIntros "Hb ((?&?&Hctx)&?)". iDestruct "Hb" as (aid a [?[??]]) "Hb".
iExists aid, a. iSplit; first done. iSplit; last (iPureIntro; lia).
by iApply (allocs_entry_lookup with "Hctx").
Qed.
......@@ -434,7 +437,7 @@ Section heap.
rewrite lookup_singleton_None. lia. }
rewrite to_heap_insert. setoid_rewrite Z.add_assoc.
apply alloc_local_update; last done. apply lookup_to_heap_None.
rewrite (heap_upd_lookup_lt (Some aid, a)); last lia.
rewrite heap_update_lookup_lt /=; last lia.
apply Hfree => /=. lia.
Qed.
......@@ -456,13 +459,13 @@ Section heap.
heap_ctx h -∗
heap_mapsto_mbyte_st ls l aid q b -∗
⌜∃ n' : nat,
h !! l.2 = Some (aid, match ls with RSt n => RSt (n+n') | WSt => WSt end, b)⌝.
h !! l.2 = Some (HeapCell aid (match ls with RSt n => RSt (n+n') | WSt => WSt end) b)⌝.
Proof.
iIntros "H● H◯".
iDestruct (own_valid_2 with "H● H◯") as %[Hl?]%auth_both_valid_discrete.
iPureIntro. move: Hl=> /singleton_included_l [[[q' ls'] dv]].
rewrite /to_heap lookup_fmap fmap_Some_equiv.
move=> [[[[aid'' ls''] v'] [Heq[[/=??]->]]]]; simplify_eq.
move=> [[[aid'' ls'' v'] [Heq[[/=??]->]]]]; simplify_eq.
move=> /Some_pair_included_total_2 [/Some_pair_included] [_ Hincl]
/to_agree_included ?; simplify_eq.
destruct ls as [|n], ls'' as [|n''],
......@@ -473,13 +476,13 @@ Section heap.
Lemma heap_mapsto_mbyte_lookup_1 ls l aid h b:
heap_ctx h -∗
heap_mapsto_mbyte_st ls l aid 1%Qp b -∗
⌜h !! l.2 = Some (aid, ls, b)⌝.
⌜h !! l.2 = Some (HeapCell aid ls b)⌝.
Proof.
iIntros "H● H◯".
iDestruct (own_valid_2 with "H● H◯") as %[Hl?]%auth_both_valid_discrete.
iPureIntro. move: Hl=> /singleton_included_l [[[q' ls'] dv]].
rewrite /to_heap lookup_fmap fmap_Some_equiv.
move=> [[[[aid'' ls''] v'] [?[[/=??]->]]] Hincl]; simplify_eq.
move=> [[[aid'' ls'' v'] [?[[/=??]->]]] Hincl]; simplify_eq.
apply (Some_included_exclusive _ _) in Hincl as [? Hval]; last by destruct ls''.
apply (inj to_agree) in Hval. fold_leibniz. subst.
destruct ls, ls''; rewrite ?Nat.add_0_r; naive_solver.
......@@ -487,32 +490,34 @@ Section heap.
Lemma heap_mapsto_lookup_q flk l h q v:
(∀ n, flk (RSt n) : Prop) →
heap_ctx h -∗ l ↦{q} v -∗ ⌜heap_at_go l v flk h⌝.
heap_ctx h -∗ l ↦{q} v -∗ ⌜heap_lookup_loc l v flk h⌝.
Proof.
iIntros (?) "Hh Hl".
iInduction v as [|b v] "IH" forall (l) => //.
rewrite heap_mapsto_cons_mbyte heap_mapsto_mbyte_eq /=.
iDestruct "Hl" as "[Hb [_ Hl]]". iDestruct "Hb" as (? ->) "Hb".
iSplit; last by iApply ("IH" with "Hh Hl").
iDestruct (heap_mapsto_mbyte_lookup_q with "Hh Hb") as %[n Hn]. by eauto.
iDestruct "Hl" as "[Hb [_ Hl]]". iDestruct "Hb" as (? Heq) "Hb".
rewrite /heap_lookup_loc /=. iSplit; last by iApply ("IH" with "Hh Hl").
iDestruct (heap_mapsto_mbyte_lookup_q with "Hh Hb") as %[n Hn].
by iExists _, _.
Qed.
Lemma heap_mapsto_lookup_1 (flk : lock_state → Prop) l h v:
flk (RSt 0%nat) →
heap_ctx h -∗ l ↦ v -∗ ⌜heap_at_go l v flk h⌝.
heap_ctx h -∗ l ↦ v -∗ ⌜heap_lookup_loc l v flk h⌝.
Proof.
iIntros (?) "Hh Hl".
iInduction v as [|b v] "IH" forall (l) => //.
rewrite heap_mapsto_cons_mbyte heap_mapsto_mbyte_eq /=.
iDestruct "Hl" as "[Hb [_ Hl]]". iDestruct "Hb" as (? ->) "Hb".
iSplit; last by iApply ("IH" with "Hh Hl").
iDestruct (heap_mapsto_mbyte_lookup_1 with "Hh Hb") as %Hl. by eauto.
iDestruct "Hl" as "[Hb [_ Hl]]". iDestruct "Hb" as (? Heq) "Hb".
rewrite /heap_lookup_loc /=. iSplit; last by iApply ("IH" with "Hh Hl").
iDestruct (heap_mapsto_mbyte_lookup_1 with "Hh Hb") as %Hl.
by iExists _, _.
Qed.
Lemma heap_read_mbyte_vs h n1 n2 nf l aid q b:
h !! l.2 = Some (aid, RSt (n1 + nf), b) →
h !! l.2 = Some (HeapCell aid (RSt (n1 + nf)) b) →
heap_ctx h -∗ heap_mapsto_mbyte_st (RSt n1) l aid q b
==∗ heap_ctx (<[l.2:=(aid, RSt (n2 + nf), b)]> h)
==∗ heap_ctx (<[l.2:=HeapCell aid (RSt (n2 + nf)) b]> h)
∗ heap_mapsto_mbyte_st (RSt n2) l aid q b.
Proof.
intros Hσv. apply wand_intro_r. rewrite -!own_op to_heap_insert.
......@@ -524,9 +529,9 @@ Section heap.
Lemma heap_read_na h l q v :
heap_ctx h -∗ l ↦{q} v ==∗
⌜heap_at_go l v (λ st, ∃ n, st = RSt n) h⌝ ∗
⌜heap_lookup_loc l v (λ st, ∃ n, st = RSt n) h⌝ ∗
heap_ctx (heap_upd l v (λ st, if st is Some (RSt n) then RSt (S n) else WSt) h) ∗
∀ h2, heap_ctx h2 ==∗ ⌜heap_at_go l v (λ st, ∃ n, st = RSt (S n)) h2⌝ ∗
∀ h2, heap_ctx h2 ==∗ ⌜heap_lookup_loc l v (λ st, ∃ n, st = RSt (S n)) h2⌝ ∗
heap_ctx (heap_upd l v (λ st, if st is Some (RSt (S n)) then RSt n else WSt) h2) ∗ l ↦{q} v.
Proof.
iIntros "Hh Hv".
......@@ -534,27 +539,30 @@ Section heap.
iInduction (v) as [|b v] "IH" forall (l Hat) => //=.
{ iFrame. by iIntros "!#" (?) "$ !#". }
rewrite ->heap_mapsto_cons_mbyte, heap_mapsto_mbyte_eq.
iDestruct "Hv" as "[Hb [? Hl]]". iDestruct "Hb" as (? Heq) "Hb". rewrite Heq.
move: Hat => /= -[[? [Hin [n ?]]] ?]; subst.
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]" => //.
iMod (heap_read_mbyte_vs _ 0 1 with "Hh Hb") as "[Hh Hb]".
{ rewrite heap_upd_lookup_lt // Hin Heq //. }
{ rewrite heap_update_lookup_lt // /shift_loc /=. lia. }
iModIntro. iSplitL "Hh".
{ iStopProof. f_equiv. symmetry. apply partial_alter_to_insert.
by rewrite heap_upd_lookup_lt // Hin. }
rewrite heap_update_lookup_lt /shift_loc /= ?Hin ?Heq //; lia. }
iIntros (h2) "Hh". iDestruct (heap_mapsto_mbyte_lookup_q with "Hh Hb") as %[n' Hn].
iMod ("IH" with "Hh") as (Hat) "[Hh Hl]".
iSplitR; first by iPureIntro; naive_solver.
iMod (heap_read_mbyte_vs _ 1 0 with "Hh Hb") as "[Hh Hb]". by rewrite heap_upd_lookup_lt.
iMod ("IH" with "Hh") as (Hat) "[Hh Hl]". iSplitR.
{ rewrite /shift_loc /= Z.add_1_r Heq in Hat. iPureIntro. naive_solver. }
iMod (heap_read_mbyte_vs _ 1 0 with "Hh Hb") as "[Hh Hb]".
{ rewrite heap_update_lookup_lt // /shift_loc /=. lia. }
rewrite heap_mapsto_cons_mbyte heap_mapsto_mbyte_eq. iFrame. iModIntro.
iSplitR "Hb"; [ iStopProof | iExists _; by iFrame ].
f_equiv. symmetry. apply partial_alter_to_insert. by rewrite heap_upd_lookup_lt // Hn.
f_equiv. symmetry. apply partial_alter_to_insert.
rewrite heap_update_lookup_lt /shift_loc /= ?Hn ?Heq //. lia.
Qed.
Lemma heap_write_mbyte_vs h st1 st2 l aid b b':
h !! l.2 = Some (aid, st1, b) →
h !! l.2 = Some (HeapCell aid st1 b) →
heap_ctx h -∗ heap_mapsto_mbyte_st st1 l aid 1%Qp b
==∗ heap_ctx (<[l.2:=(aid, st2, b')]> h) ∗ heap_mapsto_mbyte_st st2 l aid 1%Qp b'.
==∗ heap_ctx (<[l.2:=HeapCell aid st2 b']> h) ∗ heap_mapsto_mbyte_st st2 l aid 1%Qp b'.
Proof.
intros Hσv. apply wand_intro_r. rewrite -!own_op to_heap_insert.
eapply own_update, auth_update, singleton_local_update.
......@@ -572,18 +580,20 @@ Section heap.
iDestruct "Hmt" as "[Hb [$ Hl]]". iDestruct "Hb" as (? Heq) "Hb".
iDestruct (heap_mapsto_mbyte_lookup_1 with "Hh Hb") as % Hin; auto.
iMod ("IH" with "[//] Hh Hl") as "[Hh $]".
iMod (heap_write_mbyte_vs with "Hh Hb") as "[Hh Hb]". by rewrite heap_upd_lookup_lt.
iMod (heap_write_mbyte_vs with "Hh Hb") as "[Hh Hb]".
{ rewrite heap_update_lookup_lt /shift_loc //=. lia. }
iModIntro => /=. iSplitR "Hb"; last (iExists _; by iFrame).
iClear "IH". iStopProof. f_equiv => /=. symmetry.
apply: partial_alter_to_insert. by rewrite heap_upd_lookup_lt // Hin Heq Hf.
apply: partial_alter_to_insert.
rewrite heap_update_lookup_lt /shift_loc /= ?Heq ?Hin ?Hf //. lia.
Qed.
Lemma heap_write_na h l v v' :
length v = length v' →
heap_ctx h -∗ l ↦ v ==∗
⌜heap_at_go l v (λ st, st = RSt 0) h⌝ ∗
⌜heap_lookup_loc l v (λ st, st = RSt 0) h⌝ ∗
heap_ctx (heap_upd l v (λ _, WSt) h) ∗
∀ h2, heap_ctx h2 ==∗ ⌜heap_at_go l v (λ st, st = WSt) h2⌝ ∗
∀ h2, heap_ctx h2 ==∗ ⌜heap_lookup_loc l v (λ st, st = WSt) h2⌝ ∗
heap_ctx (heap_upd l v' (λ _, RSt 0) h2) ∗ l ↦ v'.
Proof.
iIntros (Hlen) "Hh Hv".
......@@ -592,23 +602,27 @@ Section heap.
{ iFrame. by iIntros "!#" (?) "$ !#". }
move: Hlen => -[] Hlen.
rewrite heap_mapsto_cons_mbyte heap_mapsto_mbyte_eq.
iDestruct "Hv" as "[Hb [? Hl]]". iDestruct "Hb" as (? Heq) "Hb". rewrite Heq.
move: Hat => /= -[[? [Hin ?]] ?]; subst.
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]" => //.
iMod (heap_write_mbyte_vs with "Hh Hb") as "[Hh Hb]";
first by rewrite heap_upd_lookup_lt // Hin Heq.
iFrame. iIntros "!#" (h2) "Hh". iDestruct (heap_mapsto_mbyte_lookup_1 with "Hh Hb") as %Hn.
iMod ("IH" with "Hh") as (Hat) "[Hh Hl]".
iSplitR; first by iPureIntro; naive_solver.
iMod (heap_write_mbyte_vs with "Hh Hb") as "[Hh Hb]"; first by rewrite heap_upd_lookup_lt.
rewrite Heq /=. iFrame. rewrite heap_mapsto_cons_mbyte heap_mapsto_mbyte_eq. iFrame.
iMod (heap_write_mbyte_vs with "Hh Hb") as "[Hh Hb]".
{ rewrite heap_update_lookup_lt /shift_loc /= ?Hin ?Heq //=. lia. }
iSplitL "Hh". { rewrite /heap_upd /=. erewrite partial_alter_to_insert; first done. by rewrite Heq. }
iIntros "!#" (h2) "Hh". iDestruct (heap_mapsto_mbyte_lookup_1 with "Hh Hb") as %Hn.
iMod ("IH" with "Hh") as (Hat) "[Hh Hl]". iSplitR.
{ rewrite /shift_loc /= Z.add_1_r Heq in Hat. iPureIntro. naive_solver. }
iMod (heap_write_mbyte_vs with "Hh Hb") as "[Hh Hb]".
{ rewrite heap_update_lookup_lt /shift_loc /= ?Heq ?Hin //=. lia. }
rewrite /heap_upd !Heq /=. erewrite partial_alter_to_insert; last done.
rewrite Z.add_1_r Heq. iFrame. rewrite heap_mapsto_cons_mbyte heap_mapsto_mbyte_eq. iFrame.
iExists _. by iFrame.
Qed.
Lemma heap_free_free_st l h v aid :
l.1 = 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 (length v) h).
heap_ctx (heap_free l.2 (length v) h).
Proof.
move => Haid. destruct l as [? a]. simplify_eq/=.
have [->|Hv] := decide(v = []); first by iIntros "[$ _]".
......@@ -626,12 +640,12 @@ Section heap.
rewrite -insert_singleton_op //. etrans.
{ apply (delete_local_update _ _ a (1%Qp, to_lock_stateR (RSt 0%nat), to_agree (aid, b))).
by rewrite lookup_insert. }
rewrite delete_insert // -to_heap_delete (heap_free_delete _ (Some aid, a)).
rewrite delete_insert // -to_heap_delete (heap_free_delete _ a).
setoid_rewrite Z.add_assoc. by apply IH.
Qed.
Lemma heap_free_free l ly h :
heap_ctx h -∗ l ↦|ly| ==∗ heap_ctx (heap_free l ly.(ly_size) h).
heap_ctx h -∗ l ↦|ly| ==∗ heap_ctx (heap_free l.2 ly.(ly_size) h).
Proof.
iIntros "Hctx Hl". iDestruct "Hl" as (?) "(<-&%&Hl)".
iDestruct (heap_mapsto_has_alloc_id with "Hl") as %[??].
......@@ -674,18 +688,18 @@ Section alloc_alive.
Proof. rewrite alloc_alive_eq => ?. iIntros "Hl". destruct l. iExists _, _, _. by iFrame. Qed.
Lemma alloc_alive_to_heap_alloc_alive l σ:
alloc_alive l -∗ state_ctx σ -∗ ⌜∃ aid, l.1 = Some aid ∧ heap_block_alive σ.(st_heap) aid⌝.
alloc_alive l -∗ state_ctx σ -∗ ⌜∃ aid, l.1 = Some aid ∧ heap_block_alive σ.(st_heap).(hs_heap) aid⌝.
Proof.
rewrite alloc_alive_eq.
iDestruct 1 as (addr q [|b v] Hv) "Hl" => //. iIntros "(_&Hhctx&_)".
iDestruct 1 as (addr q [|b v] Hv) "Hl" => //. iIntros "((?&Hhctx&?)&_)".
rewrite heap_mapsto_cons_mbyte heap_mapsto_mbyte_eq. iDestruct "Hl" as "[Hmt _]".
iDestruct "Hmt" as (aid ?) "Hmt".
iDestruct (heap_mapsto_mbyte_lookup_q with "Hhctx Hmt") as %[??].
iPureIntro. eexists _. split => //. by eexists _, _, _.
iDestruct (heap_mapsto_mbyte_lookup_q with "Hhctx Hmt") as %[? Heq].
iPureIntro. eexists _. split => //. eexists _. by erewrite Heq.
Qed.
Lemma alloc_alive_to_valid_ptr l σ:
loc_in_bounds l 0 -∗ alloc_alive l -∗ state_ctx σ -∗ ⌜valid_ptr l σ⌝.
loc_in_bounds l 0 -∗ alloc_alive l -∗ state_ctx σ -∗ ⌜valid_ptr l σ.(st_heap)⌝.
Proof.
iIntros "Hin Ha Hσ".
iDestruct (alloc_alive_to_heap_alloc_alive with "Ha Hσ") as %[?[??]].
......@@ -699,18 +713,19 @@ Section alloc_new_blocks.
Lemma heap_alloc_new_block_upd σ1 l v σ2:
alloc_new_block σ1 l v σ2 →
state_ctx σ1 ==∗ state_ctx σ2 ∗ l ↦ v.
heap_state_ctx σ1 ==∗ heap_state_ctx σ2 ∗ l ↦ v.
Proof.
iIntros (Halloc) "Hctx". iDestruct "Hctx" as (Hagree) "(Hhctx&Hbctx&Hfctx)".
iIntros (Halloc) "Hctx". iDestruct "Hctx" as (Hagree) "(Hhctx&Hbctx)".
destruct Halloc.
iMod (allocs_alloc with "Hbctx") as "[$ Hb]"; first done.
iDestruct (allocs_entry_to_loc_in_bounds l aid (length v) with "Hb") as "#Hinb" => //.
iMod (heap_alloc with "[Hhctx $Hinb]") as "[Hhctx Hv]" => //. iModIntro. iFrame.
iMod (heap_alloc with "[Hhctx $Hinb]") as "[Hhctx Hv]" => //=. iModIntro. iFrame.
rewrite /lang.heap_alloc /heap_upd /= H //.
Qed.
Lemma heap_alloc_new_blocks_upd σ1 ls vs σ2:
alloc_new_blocks σ1 ls vs σ2 →
state_ctx σ1 ==∗ state_ctx σ2 ∗ ([∗ list] l; v ∈ ls; vs, l ↦ v).
heap_state_ctx σ1 ==∗ heap_state_ctx σ2 ∗ ([∗ list] l; v ∈ ls; vs, l ↦ v).
Proof.
elim. { by iIntros (?) "$ !>". } clear.
iIntros (σ σ' σ'' l v ls vs Hnew _ IH) "Hσ".
......
theories/lang/int_type.v 0 → 100644
View file @ 551866b2
From refinedc.lang Require Import base byte layout.
Open Scope Z_scope.
(** Representation of an integer type (size and signedness). *)
Definition signed := bool.
Record int_type :=
IntType {
it_byte_size_log : nat;
it_signed : signed;
}.
Definition bytes_per_int (it : int_type) : nat :=
2 ^ it.(it_byte_size_log).
Definition bits_per_int (it : int_type) : Z :=
bytes_per_int it * bits_per_byte.
Definition int_modulus (it : int_type) : Z :=
2 ^ bits_per_int it.
Definition int_half_modulus (it : int_type) : Z :=
2 ^ (bits_per_int it - 1).
(* Minimal representable integer. *)
Definition min_int (it : int_type) : Z :=
if it.(it_signed) then - int_half_modulus it else 0.
(* Maximal representable integer. *)
Definition max_int (it : int_type) : Z :=
(if it.(it_signed) then int_half_modulus it else int_modulus it) - 1.
Global Instance int_elem_of_it : ElemOf Z int_type :=
λ z it, min_int it ≤ z ≤ max_int it.
Definition it_layout (it : int_type) :=
Layout (bytes_per_int it) it.(it_byte_size_log).
Definition i8 := IntType 0 true.
Definition u8 := IntType 0 false.
Definition i16 := IntType 1 true.
Definition u16 := IntType 1 false.
Definition i32 := IntType 2 true.
Definition u32 := IntType 2 false.
Definition i64 := IntType 3 true.
Definition u64 := IntType 3 false.
(* hardcoding 64bit pointers for now *)
Definition bytes_per_addr_log : nat := 3%nat.
Definition bytes_per_addr : nat := (2 ^ bytes_per_addr_log)%nat.
Definition intptr_t := IntType bytes_per_addr_log true.
Definition uintptr_t := IntType bytes_per_addr_log false.
Definition size_t := uintptr_t.
Definition ssize_t := intptr_t.
Definition bool_it := u8.
(*** Lemmas about [int_type] *)
Lemma bytes_per_int_gt_0 it : bytes_per_int it > 0.
Proof.
rewrite /bytes_per_int. move: it => [log ?] /=.
rewrite Z2Nat_inj_pow. assert (0 < 2%nat ^ log); last lia.
apply Z.pow_pos_nonneg; lia.
Qed.
Lemma bits_per_int_gt_0 it : bits_per_int it > 0.
Proof.
rewrite /bits_per_int /bits_per_byte.
suff : (bytes_per_int it > 0) by lia.
by apply: bytes_per_int_gt_0.
Qed.
Lemma int_modulus_twice_half_modulus (it : int_type) :
int_modulus it = 2 * int_half_modulus it.
Proof.
rewrite /int_modulus /int_half_modulus.
rewrite -[X in X * _]Z.pow_1_r -Z.pow_add_r; try f_equal; try lia.
rewrite /bits_per_int /bytes_per_int.
apply Z.le_add_le_sub_l. rewrite Z.add_0_r.
rewrite Z2Nat_inj_pow.
assert (0 < 2%nat ^ it_byte_size_log it * bits_per_byte); last lia.
apply Z.mul_pos_pos; last (rewrite /bits_per_byte; lia).
apply Z.pow_pos_nonneg; lia.
Qed.
Lemma it_in_range_mod n it:
n ∈ it → it_signed it = false →
n `mod` int_modulus it = n.
Proof.
move => [??] ?. rewrite Z.mod_small //.
destruct it as [? []] => //. unfold min_int, max_int in *. simpl in *.
lia.
Qed.
Lemma min_int_le_0 (it : int_type) : min_int it ≤ 0.
Proof.
have ? := bytes_per_int_gt_0 it. rewrite /min_int /int_half_modulus.
destruct (it_signed it) => //. trans (- 2 ^ 7) => //.
rewrite -Z.opp_le_mono. apply Z.pow_le_mono_r => //.
rewrite /bits_per_int /bits_per_byte. lia.
Qed.
Lemma max_int_ge_127 (it : int_type) : 127 ≤ max_int it.
Proof.
have ? := bytes_per_int_gt_0 it.
rewrite /max_int /int_modulus /int_half_modulus.
rewrite /bits_per_int /bits_per_byte.
have ->: (127 = 2 ^ 7 - 1) by []. apply Z.sub_le_mono => //.
destruct (it_signed it); apply Z.pow_le_mono_r; lia.
Qed.
Lemma int_modulus_mod_in_range n it:
it_signed it = false →
(n `mod` int_modulus it) ∈ it.
Proof.
move => ?.
have [|??]:= Z.mod_pos_bound n (int_modulus it). {
apply: Z.pow_pos_nonneg => //. rewrite /bits_per_int/bits_per_byte/=. lia.
}
destruct it as [? []] => //.
split; unfold min_int, max_int => /=; lia.
Qed.
theories/lang/lang.v
View file @ 551866b2
This diff is collapsed.
theories/lang/layout.v 0 → 100644
View file @ 551866b2
From refinedc.lang Require Import base.
Open Scope Z_scope.
(** Representation of a type layout (byte size and alignment constraint). *)
Record layout :=
Layout {
ly_size : nat;
ly_align_log : nat;
}.
Definition sizeof (ly : layout) : nat := ly.(ly_size).
Definition ly_align (ly : layout) : nat := 2 ^ ly.(ly_align_log).
Instance layout_dec_eq : EqDecision layout.
Proof. solve_decision. Defined.
Instance layout_inhabited : Inhabited layout :=
populate (Layout 0 0).
Instance layout_countable : Countable layout.
Proof.
refine (inj_countable'
(λ ly, (ly.(ly_size), ly.(ly_align_log)))
(λ '(sz, a), Layout sz a) _); by intros [].
Qed.
Instance layout_le : SqSubsetEq layout := λ ly1 ly2,
(ly1.(ly_size) ≤ ly2.(ly_size))%nat ∧
(ly1.(ly_align_log) ≤ ly2.(ly_align_log))%nat.
Instance layout_le_po : PreOrder layout_le.
Proof.
split => ?; rewrite /layout_le => *; repeat case_bool_decide => //; lia.
Qed.
Definition ly_offset (ly : layout) (n : nat) : layout := {|
ly_size := ly.(ly_size) - n;
(* Sadly we need to have the second argument to factor2 as we want
that if l is aligned to x, then l + n * x is aligned to x for all n
including 0. *)
ly_align_log := ly.(ly_align_log) `min` factor2 n ly.(ly_align_log)
|}.
Definition ly_set_size (ly : layout) (n : nat) : layout := {|
ly_size := n;
ly_align_log := ly.(ly_align_log)
|}.
Definition ly_mult (ly : layout) (n : nat) : layout := {|
ly_size := ly.(ly_size) * n;
ly_align_log := ly.(ly_align_log)