Commit 9dd08144 authored by Rodolphe Lepigre's avatar Rodolphe Lepigre
Browse files

Define [builtin_boolean] using [generic_boolean].

parent 10565cc1
Pipeline #53927 failed with stage
in 12 minutes and 30 seconds
......@@ -8,7 +8,7 @@
typedef bool (*comp_fn)(void *, void *);
[[rc::parameters("R : {Z → Z → Prop}", "ls : {list Z}", "x : Z", "p : loc", "ty : {Z → type}", "px : loc")]]
[[rc::args("function_ptr<{fn(∀ (x, y, px, py) : (Z * Z * loc * loc); px @ &own (ty x), py @ &own (ty y); True) → ∃ (b) : (bool), b @ boolean bool_it; px ◁ₗ ty x ∗ py ◁ₗ ty y ∗ ⌜b ↔ R x y⌝}>",
[[rc::args("function_ptr<{fn(∀ (x, y, px, py) : (Z * Z * loc * loc); px @ &own (ty x), py @ &own (ty y); True) → ∃ (b) : (bool), b @ builtin_boolean; px ◁ₗ ty x ∗ py ◁ₗ ty y ∗ ⌜b ↔ R x y⌝}>",
"p @ &own<array<void*, {(fun x => &own (ty x) : type) <$> ls}>>", "{length ls} @ int<size_t>", "px @ &own<{ty x}>")]]
[[rc::requires("{StronglySorted R ls}", "{Transitive R}")]]
[[rc::exists("n : nat")]]
......@@ -41,7 +41,7 @@ size_t binary_search(comp_fn comp, void **xs, size_t n, void *x) {
[[rc::parameters("x : Z", "y : Z", "px : loc", "py : loc")]]
[[rc::args("px @ &own<x @ int<size_t>>", "py @ &own<y @ int<size_t>>")]]
[[rc::exists("b : bool")]]
[[rc::returns("b @ boolean<bool_it>")]]
[[rc::returns("b @ builtin_boolean")]]
[[rc::ensures("own px : x @ int<size_t>", "own py : y @ int<size_t>", "{b ↔ Z.le x y}")]]
bool compare_int(void *x, void *y) {
size_t *xi = x, *yi = y;
......
......@@ -64,7 +64,7 @@ void free_btree(btree_t* t);
// Test if the key k is mapped in the B-tree t.
[[rc::parameters("p : loc", "h : nat", "m : {gmap Z type}", "k : Z")]]
[[rc::args("p @ &own<{BRroot h m} @ btree_t>", "k @ int<i32>")]]
[[rc::returns("{bool_decide (m !! k ≠ None)} @ boolean<bool_it>")]]
[[rc::returns("{bool_decide (m !! k ≠ None)} @ builtin_boolean")]]
[[rc::ensures("own p : {BRroot h m} @ btree_t")]]
bool btree_member(btree_t* t, int k);
......
......@@ -6,7 +6,7 @@
#include <stdatomic.h>
struct [[rc::refined_by("P : {iProp Σ}")]] latch {
[[rc::field("atomic_bool<bool_it, {(□ P)}, True>")]]
[[rc::field("atomic_bool<u8, {(□ P)}, True>")]]
atomic_bool released;
};
......
......@@ -215,7 +215,7 @@ void mpool_fini(struct mpool *p) {
"&own<uninit<{ly_with_align (Z.to_nat size) entry_size}>>",
"size @ int<size_t>")]]
[[rc::requires("{(entry_size | size)}")]]
[[rc::returns("{Z_of_bool (bool_decide (0 < size))} @ int<bool_it>")]]
[[rc::returns("{bool_decide (0 < size)} @ builtin_boolean")]]
[[rc::ensures("frac q p : {(n + (Z.to_nat (size `quot` entry_size)))%nat} @ mpool<entry_size>")]]
bool mpool_add_chunk(struct mpool *p, void *begin, size_t size)
{
......
......@@ -27,7 +27,7 @@ void no_alias(int *a, int *b) {
assert(*b == old_b);
}
[[rc::args("boolean<bool_it>")]]
[[rc::args("builtin_boolean")]]
void local_vars(bool b) {
int var = 1, dummy;
int *p;
......@@ -42,7 +42,7 @@ void local_vars(bool b) {
}
[[rc::parameters("p : loc")]]
[[rc::args("boolean<bool_it>", "p @ &own<int<i32>>")]]
[[rc::args("builtin_boolean", "p @ &own<int<i32>>")]]
void ptrs(bool b, int *p) {
int *p1, *p2;
p1 = p;
......@@ -57,7 +57,7 @@ void ptrs(bool b, int *p) {
}
[[rc::parameters("p : loc")]]
[[rc::args("boolean<bool_it>", "p @ &own<int<i32>>")]]
[[rc::args("builtin_boolean", "p @ &own<int<i32>>")]]
void ptrs2(bool b, int *p) {
int **p1;
p1 = &p;
......
......@@ -6,7 +6,7 @@ Section type.
Context `{!typeG Σ} `{!lockG Σ}.
Definition spinlock (γ : lock_id) : type :=
struct struct_spinlock [atomic_bool bool_it True (lock_token γ [])].
struct struct_spinlock [atomic_bool u8 True (lock_token γ [])].
Global Program Instance movable_spinlock γ : Movable (spinlock γ) := ltac:(apply: movable_struct).
......
......@@ -14,7 +14,8 @@ Section type.
Lemma type_sl_init:
typed_function impl_sl_init type_of_sl_init.
Proof.
start_function "sl_init" (p) => vl. split_blocks ( : gmap label (iProp Σ)) ( : gmap label (iProp Σ)).
start_function "sl_init" (p) => vl.
split_blocks ( : gmap label (iProp Σ)) ( : gmap label (iProp Σ)).
iMod alloc_lock_token as (γ) "?".
......
......@@ -32,7 +32,7 @@ queue_t init_queue() {
[[rc::parameters("p : loc", "tys : {list type}")]]
[[rc::args("p @ &own<{tys} @ queue>")]]
[[rc::returns("{bool_decide (tys ≠ [])} @ boolean<bool_it>")]]
[[rc::returns("{bool_decide (tys ≠ [])} @ builtin_boolean")]]
[[rc::ensures("own p : {tys} @ queue")]]
bool is_empty(queue_t *q) {
return (*q)->head != NULL;
......
......@@ -41,7 +41,7 @@ void *pop (list_t *p) {
[[rc::parameters("l : {list Z}", "p : loc", "n : Z" )]]
[[rc::args("p @ &own<{l `at_type` int size_t} @ list_t>", "n @ int<size_t>")]]
[[rc::exists("b : bool")]]
[[rc::returns("b @ boolean<bool_it>")]]
[[rc::returns("b @ builtin_boolean")]]
[[rc::ensures("own p : {l `at_type` int size_t} @ list_t", "{b ↔ n ∈ l}")]]
[[rc::tactics("all: try set_solver.")]]
bool member_rec (list_t *p, size_t k) {
......@@ -58,7 +58,7 @@ bool member_rec (list_t *p, size_t k) {
[[rc::parameters("l : {list Z}", "p : loc", "n : Z" )]]
[[rc::args("p @ &own<{l `at_type` int size_t} @ list_t>", "n @ int<size_t>")]]
[[rc::exists("b : bool")]]
[[rc::returns("b @ boolean<bool_it>")]]
[[rc::returns("b @ builtin_boolean")]]
[[rc::ensures("own p : {l `at_type` int size_t} @ list_t", "{b ↔ n ∈ l}")]]
[[rc::tactics("all: try set_solver.")]]
bool member (list_t *p, size_t k) {
......
......@@ -10,7 +10,7 @@ void sl_init(struct spinlock* lock) {
void sl_lock(struct spinlock* lock) {
bool expected = 0;
[[rc::inv_vars("expected : false @ boolean<bool_it>")]]
[[rc::inv_vars("expected : false @ builtin_boolean")]]
while(atomic_compare_exchange_strong(&lock->lock, &expected, 1) == (bool)false) {
expected = 0;
}
......
......@@ -302,6 +302,7 @@ let rec op_type_opt loc Ctype.(Ctype(_, c_ty)) =
begin
match op_type_opt loc c_ty with
| Some(OpInt(_)) as op_ty -> op_ty
| Some(OpBool) as op_ty -> op_ty
| _ -> None
end
| Struct(_) -> None
......@@ -1045,6 +1046,7 @@ let translate_block stmts blocks ret_ty is_main =
let ty_opt = op_type_tc_opt (loc_of e) (tc_of e) in
match ty_opt with
| Some(OpInt(_)) -> ty_opt
| Some(OpBool) -> ty_opt
| _ -> None
in
let e2 = translate_expr false goal_ty e2 in
......
......@@ -195,7 +195,7 @@ struct [[rc::refined_by("mm_ops : mm_callbacks")]] kvm_pgtable_mm_ops {
[[rc::parameters("pte : Pte")]]
[[rc::args("pte @ bitfield<Pte>")]]
[[rc::requires("{bitfield_wf pte}")]]
[[rc::returns("{pte_valid pte} @ boolean<bool_it>")]]
[[rc::returns("{pte_valid pte} @ builtin_boolean")]]
static bool kvm_pte_valid(kvm_pte_t pte)
{
// TODO: remove 0 != once issue #45 is fixed
......@@ -207,7 +207,7 @@ static bool kvm_pte_valid(kvm_pte_t pte)
[[rc::requires("{bitfield_wf pte}")]]
[[rc::returns("{if bool_decide (level = max_level - 1) then false \
else if negb (pte_valid pte) then false \
else bool_decide (pte_type pte = pte_type_table)} @ boolean<bool_it>")]]
else bool_decide (pte_type pte = pte_type_table)} @ builtin_boolean")]]
[[rc::tactics("all: simpl_bool_hyp.")]]
static bool kvm_pte_table(kvm_pte_t pte, u32 level)
{
......@@ -264,7 +264,7 @@ static void kvm_set_table_pte(kvm_pte_t *ptep, kvm_pte_t *childp,
[[rc::requires("{bitfield_wf pte}", "{bitfield_wf attr}")]]
[[rc::requires("{type = (if bool_decide (level = max_level - 1) then pte_type_page else pte_type_block)}")]]
[[rc::requires("{pte1 = {| pte_valid := true; pte_type := type; pte_leaf_attr_lo := pte_leaf_attr_lo attr; pte_addr := (addr_of pa); pte_undef := 0; pte_leaf_attr_hi := pte_leaf_attr_hi attr |} }")]]
[[rc::returns("{if pte_valid pte then bool_decide (bitfield_repr pte = bitfield_repr pte1) else true} @ boolean<bool_it>")]]
[[rc::returns("{if pte_valid pte then bool_decide (bitfield_repr pte = bitfield_repr pte1) else true} @ builtin_boolean")]]
[[rc::ensures("own p : {if pte_valid pte then pte else pte1} @ bitfield<Pte>")]]
[[rc::tactics("all: simpl_bool_hyp.")]]
static bool kvm_set_valid_leaf_pte(kvm_pte_t *ptep, u64 pa, kvm_pte_t attr,
......
......@@ -35,7 +35,7 @@ Section proofs.
(* First loop: checking that we got the ticket, we do if [got_it] is [true]. *)
b : bool, i : Z,
var_lock ◁ₗ p @ &frac{s} (hyp_spinlock_t id)
local_got_it ◁ₗ b @ boolean bool_it
local_got_it ◁ₗ b @ builtin_boolean
local_ticket ◁ₗ i @ int u16
local_next ◁ₗ uninit u16
(if b then ticket id i else True) ]> $
......@@ -44,14 +44,14 @@ Section proofs.
We will know that it is not NO_TICKET when we exit the loop. *)
i : Z,
var_lock ◁ₗ p @ &frac{s} (hyp_spinlock_t id)
local_got_it ◁ₗ uninit bool_it
local_got_it ◁ₗ uninit bool_layout
local_ticket ◁ₗ i @ int u16
local_next ◁ₗ uninit u16 ]> $
<[ "#4" :=
(* Last loop: we have the ticket, waiting for our turn. *)
i : Z,
var_lock ◁ₗ p @ &frac{s} (hyp_spinlock_t id)
local_got_it ◁ₗ uninit bool_it
local_got_it ◁ₗ uninit bool_layout
local_ticket ◁ₗ i @ int u16
local_next ◁ₗ uninit u16
ticket id i ]> )%I : gmap label (iProp Σ))
......
......@@ -162,7 +162,7 @@ Definition val_of_Z (z : Z) (it : int_type) (p : option alloc_id) : option val :
None.
Definition i2v (n : Z) (it : int_type) : val :=
default [MPoison] (val_of_Z n it None).
default (replicate (bytes_per_int it) MPoison) (val_of_Z n it None).
Lemma val_of_Z_go_length z sz p:
length (val_of_Z_go z sz p) = sz.
......@@ -187,6 +187,13 @@ Proof.
by rewrite val_of_Z_go_length.
Qed.
Lemma i2v_length n it: length (i2v n it) = bytes_per_int it.
Proof.
rewrite /i2v. destruct (val_of_Z n it None) eqn:Heq.
- by apply val_of_Z_length in Heq.
- by rewrite replicate_length.
Qed.
Lemma val_to_Z_length v it z:
val_to_Z v it = Some z length v = bytes_per_int it.
Proof. rewrite /val_to_Z. by case_decide. Qed.
......@@ -309,9 +316,9 @@ Next Obligation. by destruct b. Qed.
Definition val_to_bool (v : val) : option bool :=
match v with
| [MByte (Byte 0 _) None] => Some false
| [MByte (Byte 1 _) None] => Some true
| _ => None
| [MByte (Byte 0 _) _] => Some false
| [MByte (Byte 1 _) _] => Some true
| _ => None
end.
Lemma val_to_of_bool b :
......@@ -324,15 +331,21 @@ Proof.
rewrite /val_to_bool. repeat case_match => //.
Qed.
(*
Lemma val_to_Z_bool b :
val_to_Z (val_of_bool b) u8 = Some (Z_of_bool b).
Proof. by destruct b. Qed.
*)
Lemma val_to_bool_iff_val_to_Z v b:
val_to_bool v = Some b val_to_Z v u8 = Some (Z_of_bool b).
Proof.
split.
- destruct v as [|mb []] => //=; repeat case_match => //=; by move => [<-].
- destruct v as [|mb []] => //=; repeat case_match => //=; destruct b => //.
Qed.
Lemma i2v_bool_length b it:
length (i2v (Z_of_bool b) it) = bytes_per_int it.
Proof. by have /val_of_Z_length -> := val_of_Z_bool b it. Qed.
Lemma val_of_bool_iff_val_of_Z v b:
val_of_bool b = v val_of_Z (Z_of_bool b) u8 None = Some v.
Proof.
split.
- move => <-. destruct b; cbv; do 3 f_equal; by apply byte_eq.
- destruct b; cbv; move => [<-]; do 2 f_equal; by apply byte_eq.
Qed.
Lemma i2v_bool_Some b it:
val_to_Z (i2v (Z_of_bool b) it) it = Some (Z_of_bool b).
......
......@@ -16,30 +16,36 @@ Section atomic_bool.
|}%I.
Next Obligation.
iIntros "%it %PT %PF %l %E %HE (%b&Hb&Hown)".
iDestruct (ty_aligned (IntOp _) MCNone with "Hb") as %?; [done|]. iSplitR => //.
iDestruct (ty_aligned (IntOp _) MCNone with "Hb") as %?; [by left|]. iSplitR => //.
iApply inv_alloc. iNext. iExists b. iFrame.
Qed.
Global Program Instance movable_atomic_bool it PT PF : Movable (atomic_bool it PT PF) := {|
ty_has_op_type ot mt := is_int_ot ot it;
ty_has_op_type ot mt := (is_int_ot ot it (it = u8 is_bool_ot ot))%type;
ty_own_val v := b, v ◁ᵥ b @ boolean it if b then PT else PF;
|}%I.
Next Obligation. iIntros (???????) "[% [Hb _]]". by iApply (ty_aligned with "Hb"). Qed.
Next Obligation. iIntros (???????) "[% [Hb _]]". by iApply (ty_size_eq with "Hb"). Qed.
Next Obligation.
iIntros (???????) "[% [Hb _]]".
iApply (ty_aligned _ mt with "Hb"). naive_solver.
Qed.
Next Obligation.
iIntros (???????) "[% [Hb _]]".
iApply (ty_size_eq _ mt with "Hb"); naive_solver.
Qed.
Next Obligation.
iIntros (???????) "[% [Hb ?]]".
iDestruct (ty_deref with "Hb") as (?) "[? ?]"; [done|].
iDestruct (ty_deref _ mt with "Hb") as (?) "[? ?]"; [naive_solver|].
eauto with iFrame.
Qed.
Next Obligation.
iIntros (?????????) "Hl [%b [Hb ?]]".
iDestruct (ty_ref with "[] Hl Hb") as "?" => //.
iDestruct (ty_ref _ mt with "[] Hl Hb") as "?" => //; first naive_solver.
iExists b. iFrame.
Qed.
Next Obligation.
iIntros (it PT PF v ot mt st ?) "(%&Hv&?)".
iDestruct (ty_memcast_compat with "Hv") as "Hv"; [done|]. destruct mt => //.
iExists _. iFrame.
iIntros (it PT PF v ot mt st ?) "(%&Hv&Hb)".
iDestruct (ty_memcast_compat _ _ mt with "Hv") as "Hv"; [naive_solver|].
destruct mt => //=. iExists b. iFrame.
Qed.
Global Instance alloc_alive_atomic_bool it β PT PF:
......@@ -89,7 +95,7 @@ Section programs.
iApply typed_read_end_mono_strong; [done|]. destruct β.
- iIntros "[%b [Hl Hif]] !>". iExists _, _, True%I. iFrame. iSplitR; [done|].
unshelve iApply (type_read_copy with "[HT Hif]"). { apply _. } simpl.
iSplit; [done|]. iSplit; [done|]. iIntros (v) "_ Hl Hv".
iSplit; [by iLeft|]. iSplit; [done|]. iIntros (v) "_ Hl Hv".
iDestruct ("HT" with "Hif") as "[Hif HT]". iExists _, _. iFrame "HT Hv".
iExists _. by iFrame.
- iIntros "[%Hly #Hinv] !>".
......@@ -98,7 +104,7 @@ Section programs.
iApply typed_read_end_mono_strong; [done|]. iIntros "_ !>".
iExists _, _, _. iFrame.
unshelve iApply (type_read_copy with "[-]"). { apply _. } simpl.
iSplit; [done|]. iSplit; [iPureIntro; solve_ndisj|]. iIntros (v) "Hif Hl #Hv !>".
iSplit; [by iLeft|]. iSplit; [iPureIntro; solve_ndisj|]. iIntros (v) "Hif Hl #Hv !>".
iDestruct ("HT" with "Hif") as "[Hif HT]". iExists tytrue, (t2mt tytrue).
iSplit; [done|]. iSplit; [ done |]. iModIntro.
iSplitL "Hl Hif". { iExists _. by iFrame. }
......@@ -124,7 +130,7 @@ Section programs.
- iDestruct "Hl" as "[%bold [Hl Hif_old]]".
iExists (t2mt (_ @ boolean it)), _, _, True%I. iFrame "∗". iSplitR; [done|]. iSplitR; [done|].
unshelve iApply type_write_own_copy. { apply _. }
iSplit; [done|]. iSplit; [done|].
simpl. iSplit; [by iLeft|]. iSplit; [by iLeft|].
iIntros "Hv _ Hl !>". iExists _. iFrame "HT". iExists _. by iFrame.
- iExists (t2mt tytrue), Own, tytrue, True%I. iSplit; [done|]. iSplit; [done|]. iSplit; [done|].
iDestruct "Hl" as (?) "#Hinv".
......@@ -132,7 +138,7 @@ Section programs.
iApply typed_write_end_mono_strong; [done|]. iIntros "_ _". iModIntro.
iExists (t2mt _), _, _, True%I. iFrame. iSplitR; [done|]. iSplitR; [done|].
unshelve iApply type_write_own_copy. { apply _. }
iSplit; [done|]. iSplit; [done|].
simpl. iSplit; [by iLeft|]. iSplit; [by iLeft|].
iIntros "Hv _ Hl !>". iExists tytrue. iSplit; [done|]. iModIntro.
iSplitL "Hif_new Hl". { iExists _. by iFrame. }
iIntros "_ _ !>". iExists _. iFrame "HT". by iSplit.
......@@ -171,12 +177,12 @@ Section programs.
iDestruct "Hsub" as "[Hsub _]". iDestruct ("Hsub" with "Hif") as "[Hif HT]".
iApply "HΦ"; last first.
* iApply ("HT" with "[Hb Hif] Hexp"). iExists bnew. by iFrame.
* done.
* iPureIntro. naive_solver.
+ iApply (wp_cas_fail_boolean with "Hb Hlexp") => //.
iIntros "!# Hb Hexp". iDestruct "Hsub" as "[_ HT]".
iApply "HΦ"; last first.
* iApply ("HT" with "[Hb Hif]"). { iExists _. by iFrame. } by destruct b, bexp.
* done.
* iPureIntro. naive_solver.
- iDestruct "Hl" as (?) "#Hinv".
iInv "Hinv" as "Hb".
iDestruct "Hb" as (b) "[>Hmt Hif]".
......@@ -187,14 +193,14 @@ Section programs.
iModIntro. iSplitL "Hb Hif". { iExists bnew. iFrame. }
iApply "HΦ"; last first.
* iApply ("HT" with "[] Hexp"). by iSplit.
* done.
* iPureIntro. naive_solver.
+ iApply (wp_cas_fail_boolean with "Hmt Hlexp") => //.
iIntros "!# Hb Hexp".
iDestruct "Hsub" as "[_ HT]".
iModIntro. iSplitL "Hb Hif". { by iExists b; iFrame; rewrite /i2v Hvnew. }
iApply "HΦ"; last first.
* iApply ("HT" with "[]"); first by iSplit. by destruct b, bexp.
* done.
* iPureIntro. naive_solver.
Qed.
Global Instance type_cas_atomic_bool_inst (l : loc) β it PT PF (lexp : loc) Pexp vnew Pnew:
TypedCas (IntOp it) l (l ◁ₗ{β} (atomic_bool it PT PF))%I lexp Pexp vnew Pnew :=
......
......@@ -40,21 +40,37 @@ Section generic_boolean.
Global Program Instance rmovable_generic_boolean stn it : RMovable (generic_boolean stn it) := {|
rmovable b := {|
ty_has_op_type ot mt := is_int_ot ot it;
ty_has_op_type ot mt := (is_int_ot ot it (it = u8 stn = Strict is_bool_ot ot))%type;
ty_own_val v := n, val_to_Z v it = Some n represents_boolean stn n b;
|}
|}%I.
Next Obligation. iIntros (?????? ->%is_int_ot_layout) "(%&%&_&_&$&_)". Qed.
Next Obligation. iIntros (?????? ->%is_int_ot_layout [?[H _]]) "!%". by apply val_to_Z_length in H. Qed.
Next Obligation. iIntros (???????) "(%v&%n&%&%&%&?)". eauto with iFrame. Qed.
Next Obligation. iIntros (?????? v ->%is_int_ot_layout ?) "Hl (%n&%&%)". iExists v, n. eauto with iFrame. Qed.
Next Obligation. iIntros (????????). apply: mem_cast_compat_int; [naive_solver|]. iPureIntro; naive_solver. Qed.
Next Obligation.
iIntros (?????? [->%is_int_ot_layout|[->[->->%is_bool_ot_layout]]]) "(%&%&_&_&H&_)" => //.
Qed.
Next Obligation.
iIntros (?????? [->%is_int_ot_layout|[->[->->%is_bool_ot_layout]]] [?[H _]]) "!%".
all: by apply val_to_Z_length in H.
Qed.
Next Obligation.
iIntros (???????) "(%v&%n&%&%&%&?)". eauto with iFrame.
Qed.
Next Obligation.
iIntros (?????? v [->%is_int_ot_layout|[->[->->%is_bool_ot_layout]]] ?) "Hl (%n&%&%)".
all: iExists v, n; eauto with iFrame.
Qed.
Next Obligation.
iIntros (??????? [Hot|[->[->Hot]]]).
- apply: (mem_cast_compat_int (λ v, n, _)%I); [naive_solver|]. iPureIntro.
destruct ot; try naive_solver.
- apply: (mem_cast_compat_bool (λ v, n, _)%I); [naive_solver|]. iPureIntro.
move => /= [?[H?]]. subst. apply val_to_bool_iff_val_to_Z in H. naive_solver.
Qed.
Global Program Instance generic_boolean_copyable b stn it : Copyable (b @ generic_boolean stn it).
Next Obligation.
iIntros (??????? ->%is_int_ot_layout) "(%v&%n&%&%&%&Hl)".
iMod (heap_mapsto_own_state_to_mt with "Hl") as (q) "[_ Hl]" => //.
iSplitR; first done. iExists q, v. iFrame. iModIntro. eauto 6 with iFrame.
iIntros (??????? [->%is_int_ot_layout|[->[->->%is_bool_ot_layout]]]) "(%v&%n&%&%&%&Hl)".
all: iMod (heap_mapsto_own_state_to_mt with "Hl") as (q) "[_ Hl]" => //.
all: iSplitR; first done; iExists q, v; eauto 8 with iFrame.
Qed.
Global Instance alloc_alive_generic_boolean b stn it β: AllocAlive (b @ generic_boolean stn it) β True.
......@@ -76,6 +92,9 @@ Notation boolean := (generic_boolean Strict) (only parsing).
Notation "boolean< it >" := (boolean it)
(only printing, format "'boolean<' it '>'") : printing_sugar.
(* Type corresponding to [_Bool] (https://en.cppreference.com/w/c/types/boolean). *)
Notation builtin_boolean := (generic_boolean Strict u8) (only parsing).
Section programs.
Context `{!typeG Σ}.
......@@ -206,65 +225,13 @@ Typeclasses Opaque generic_boolean_inner_type.
Notation "'if' p " := (DestructHintIfBool p) (at level 100, only printing).
(* Type corresponding to [_Bool] (https://en.cppreference.com/w/c/types/boolean). *)
Section builtin_boolean.
Context `{!typeG Σ}.
Program Definition builtin_boolean_inner_type (b: bool) : type := {|
ty_own β l :=
v, val_to_bool v = Some b
l `has_layout_loc` bool_layout
l [β] v;
|}%I.
Next Obligation.
iIntros (????) "(%v&%&%&Hl)". iExists v.
do 2 (iSplitR; first done). by iApply heap_mapsto_own_state_share.
Qed.
Program Definition builtin_boolean : rtype := {|
rty_type := bool;
rty := builtin_boolean_inner_type;
|}.
Global Program Instance rmovable_builtin_boolean : RMovable builtin_boolean := {|
rmovable b := {|
ty_has_op_type ot mt := is_bool_ot ot;
ty_own_val v := val_to_bool v = Some b;
|}
|}%I.
Next Obligation. iIntros (???? ->%is_bool_ot_layout) "(%&_&$&_)". Qed.
Next Obligation. iIntros (???? ->%is_bool_ot_layout H) "!%". by apply val_to_bool_length in H. Qed.
Next Obligation. iIntros (?????) "(%v&%&%&?)". eauto with iFrame. Qed.
Next Obligation. iIntros (???? v ->%is_bool_ot_layout ?) "Hl %". iExists v. eauto with iFrame. Qed.
Next Obligation. iIntros (??????). apply: mem_cast_compat_bool; [done|]. iPureIntro; naive_solver. Qed.
Global Program Instance builtin_boolean_copyable b : Copyable (b @ builtin_boolean).
Next Obligation.
iIntros (????? ->%is_bool_ot_layout) "(%v&%&%&Hl)".
iMod (heap_mapsto_own_state_to_mt with "Hl") as (q) "[_ Hl]" => //.
iSplitR; first done. iExists q, v. iFrame. iModIntro. eauto with iFrame.
Qed.
Global Instance alloc_alive_builtin_boolean b β: AllocAlive (b @ builtin_boolean) β True.
Proof.
constructor. iIntros (l ?) "(%&%&%&Hl)".
iApply (heap_mapsto_own_state_alloc with "Hl").
by erewrite val_to_bool_length.
Qed.
Global Instance builtin_boolean_timeless l b:
Timeless (l ◁ₗ b @ builtin_boolean)%I.
Proof. apply _. Qed.
End builtin_boolean.
Section program.
Context `{!typeG Σ}.
Lemma type_val_builtin_boolean b T:
(T (t2mt (b @ builtin_boolean))) - typed_value (val_of_bool b) T.
Proof.
iIntros "HT". iExists _. iFrame. iPureIntro. by rewrite val_to_of_bool.
iIntros "HT". iExists _. iFrame. iPureIntro. naive_solver.
Qed.
Global Instance type_val_builtin_boolean_inst b : TypedValue (val_of_bool b) :=
λ T, i2p (type_val_builtin_boolean b T).
......@@ -275,7 +242,7 @@ Section program.
Proof.
iIntros "HT (%n&%Hv&%Hb) %Φ HΦ". move: Hb => /= ?. subst n.
iApply wp_cast_int_bool => //. iApply ("HΦ" with "[] HT") => //.
by destruct b.
iPureIntro => /=. exists (Z_of_bool b). by destruct b.
Qed.
Global Instance type_cast_boolean_builtin_boolean_inst b it v:
TypedUnOpVal v (b @ boolean it)%I (CastOp BoolOp) (IntOp it) :=
......@@ -285,11 +252,23 @@ Section program.
(b typed_stmt s fn ls R Q) -
typed_assert BoolOp v (v ◁ᵥ b @ builtin_boolean) s fn ls R Q.
Proof.
iIntros "[%H $] %Hb". iExists true. by destruct b.
iIntros "[%H $] (%&%Hn&%Hb)". iPureIntro. destruct b; last done.
move: Hb Hn => -> /val_to_bool_iff_val_to_Z ->. naive_solver.
Qed.
Global Instance type_assert_builtin_boolean_inst b v :
TypedAssert BoolOp v (v ◁ᵥ b @ builtin_boolean)%I :=
λ s fn ls R Q, i2p (type_assert_builtin_boolean _ _ _ _ _ _ _).
End program.
Typeclasses Opaque builtin_boolean_inner_type.
Lemma type_if_builtin_boolean (b : bool) v T1 T2 :
destruct_hint (DHintDestruct _ b) (DestructHintIfBool b) (if b then T1 else T2) -
typed_if BoolOp v (v ◁ᵥ b @ builtin_boolean) T1 T2.
Proof.
unfold destruct_hint. iIntros "Hs (%n&%Hv&%Hb)".
move: Hb => /= Hb. subst. apply val_to_bool_iff_val_to_Z in Hv.
iExists b. iSplit; first done. by destruct b.
Qed.
Global Instance type_if_builtin_boolean_inst b v :
TypedIf BoolOp v (v ◁ᵥ b @ builtin_boolean)%I :=
λ T1 T2, i2p (type_if_builtin_boolean b v T1 T2).
End builtin_boolean.
......@@ -476,7 +476,7 @@ Section programs.
typed_un_op v (v ◁ᵥ n @ int it)%I (CastOp BoolOp) (IntOp it) T.
Proof.
iIntros "HT %Hn %Φ HΦ". iApply wp_cast_int_bool => //.
iApply ("HΦ" with "[] HT") => //. iPureIntro. by rewrite val_to_of_bool.
iApply ("HΦ" with "[] HT") => //=. iPureIntro. naive_solver.
Qed.
Global Instance type_cast_int_builtin_boolean_inst n it v:
TypedUnOpVal v (n @ int it)%I (CastOp BoolOp) (IntOp it) :=
......
......@@ -67,6 +67,7 @@ Section judgements.
(* TODO: generalize this to PtrOp *)
<