Timings for buf_proof.v
- /home/gitlab-runner/builds/v6HyzL39/0/coq/coq/_bench/opam.OLD/ocaml-OLD/.opam-switch/build/coq-perennial.dev/./src/program_proof/buf/buf_proof.v.timing
- /home/gitlab-runner/builds/v6HyzL39/0/coq/coq/_bench/opam.NEW/ocaml-NEW/.opam-switch/build/coq-perennial.dev/./src/program_proof/buf/buf_proof.v.timing
From Coq Require Import Program.Equality.
From RecordUpdate Require Import RecordSet.
Import RecordSetNotations.
From Perennial.Helpers Require Import bytes Map.
From Perennial.program_proof Require Import disk_prelude.
From Goose.github_com.mit_pdos.go_journal Require Import buf.
From Perennial.program_proof Require Import util_proof disk_lib.
From Perennial.program_proof Require Export buf.defs.
From Perennial.program_proof Require Import addr.addr_proof wal.abstraction.
From Perennial.Helpers Require Import NamedProps PropRestore.
From Perennial.goose_lang.lib Require Import slice.typed_slice.
(* an object is the data for a sub-block object, a dynamic bundle of a kind and
data of the appropriate size *)
(* NOTE(tej): not necessarily the best name, because it's so general as to be
meaningless *)
(* TODO(tej): it would be nice if both of these were records *)
Notation object := ({K & bufDataT K}).
Notation versioned_object := ({K & (bufDataT K * bufDataT K)%type}).
Implicit Types s : Slice.t.
Implicit Types (stk:stuckness) (E: coPset).
Definition is_buf_data {K} (s : Slice.t) (d : bufDataT K) (a : addr) : iProp Σ :=
match d with
| bufBit b => ∃ (b0 : u8), slice.own_slice_small s u8T 1 (#b0 :: nil) ∗
⌜ get_bit b0 (word.modu a.(addrOff) 8) = b ⌝
| bufInode i => slice.own_slice_small s u8T 1 (inode_to_vals i)
| bufBlock b => slice.own_slice_small s u8T 1 (Block_to_vals b)
end.
Definition is_buf_without_data (bufptr : loc) (a : addr) (o : buf) (data : Slice.t) : iProp Σ :=
∃ (sz : u64),
"Haddr" ∷ bufptr ↦[Buf :: "Addr"] (addr2val a) ∗
"Hsz" ∷ bufptr ↦[Buf :: "Sz"] #sz ∗
"Hdata" ∷ bufptr ↦[Buf :: "Data"] (slice_val data) ∗
"Hdirty" ∷ bufptr ↦[Buf :: "dirty"] #o.(bufDirty) ∗
"%" ∷ ⌜ valid_addr a ∧ valid_off o.(bufKind) a.(addrOff) ⌝ ∗
"->" ∷ ⌜ sz = bufSz o.(bufKind) ⌝ ∗
"%" ∷ ⌜ #bufptr ≠ #null ⌝.
Definition is_buf (bufptr : loc) (a : addr) (o : buf) : iProp Σ :=
∃ (data : Slice.t),
"Hisbuf_without_data" ∷ is_buf_without_data bufptr a o data ∗
"Hbufdata" ∷ is_buf_data data o.(bufData) a.
Theorem is_buf_not_null bufptr a o :
is_buf bufptr a o -∗ ⌜ #bufptr ≠ #null ⌝.
iNamed "Hisbuf_without_data".
Theorem is_buf_without_data_valid_addr bufptr a o s :
is_buf_without_data bufptr a o s -∗ ⌜valid_addr a⌝.
iNamed 1; intuition auto.
Theorem is_buf_valid_addr bufptr a o :
is_buf bufptr a o -∗ ⌜valid_addr a⌝.
iApply (is_buf_without_data_valid_addr with "[$]").
Definition objKind (obj: object): bufDataKind := projT1 obj.
Definition objData (obj: object): bufDataT (objKind obj) := projT2 obj.
Definition data_has_obj (data: list byte) (a:addr) (obj: object) : Prop :=
match objData obj with
| bufBit b =>
∃ b0, data = [b0] ∧
get_bit b0 (word.modu (addrOff a) 8) = b
| bufInode i => vec_to_list i = data
| bufBlock b => vec_to_list b = data
end.
Theorem data_has_obj_to_buf_data s a obj data :
data_has_obj data a obj →
own_slice_small s u8T 1 data -∗ is_buf_data s (objData obj) a.
rewrite /data_has_obj /is_buf_data.
destruct (objData obj); subst.
destruct H as (b' & -> & <-).
Theorem is_buf_data_has_obj s a obj :
is_buf_data s (objData obj) a ⊣⊢ ∃ data, own_slice_small s u8T 1 data ∗
⌜data_has_obj data a obj⌝.
rewrite /data_has_obj /is_buf_data.
destruct (objData obj); subst; eauto.
iDestruct 1 as (b') "[Hs %]".
iDestruct 1 as (data) "[Hs %]".
iApply (data_has_obj_to_buf_data with "Hs"); auto.
Theorem wp_buf_loadField_sz bufptr a b stk E :
{{{
is_buf bufptr a b
}}}
struct.loadF buf.Buf "Sz" #bufptr @ stk; E
{{{
RET #(bufSz b.(bufKind));
is_buf bufptr a b
}}}.
iNamed "Hisbuf_without_data".
Theorem wp_buf_loadField_addr bufptr a b stk E :
{{{
is_buf bufptr a b
}}}
struct.loadF buf.Buf "Addr" #bufptr @ stk; E
{{{
RET (addr2val a);
is_buf bufptr a b
}}}.
iNamed "Hisbuf_without_data".
Theorem wp_buf_loadField_dirty bufptr a b stk E :
{{{
is_buf bufptr a b
}}}
struct.loadF buf.Buf "dirty" #bufptr @ stk ; E
{{{
RET #(b.(bufDirty));
is_buf bufptr a b
}}}.
iNamed "Hisbuf_without_data".
Theorem wp_buf_wd_loadField_sz bufptr a b dataslice stk E :
{{{
is_buf_without_data bufptr a b dataslice
}}}
struct.loadF buf.Buf "Sz" #bufptr @ stk; E
{{{
RET #(bufSz b.(bufKind));
is_buf_without_data bufptr a b dataslice
}}}.
iIntros (Φ) "Hisbuf_without_data HΦ".
iNamed "Hisbuf_without_data".
Theorem wp_buf_wd_loadField_addr bufptr a b dataslice stk E :
{{{
is_buf_without_data bufptr a b dataslice
}}}
struct.loadF buf.Buf "Addr" #bufptr @ stk; E
{{{
RET (addr2val a);
is_buf_without_data bufptr a b dataslice
}}}.
iIntros (Φ) "Hisbuf_without_data HΦ".
iNamed "Hisbuf_without_data".
Theorem wp_buf_wd_loadField_dirty bufptr a b dataslice stk E :
{{{
is_buf_without_data bufptr a b dataslice
}}}
struct.loadF buf.Buf "dirty" #bufptr @ stk; E
{{{
RET #(b.(bufDirty));
is_buf_without_data bufptr a b dataslice
}}}.
iIntros (Φ) "Hisbuf_without_data HΦ".
iNamed "Hisbuf_without_data".
Theorem is_buf_return_data bufptr a b dataslice (v' : bufDataT b.(bufKind)) :
is_buf_data dataslice v' a ∗
is_buf_without_data bufptr a b dataslice -∗
is_buf bufptr a (Build_buf b.(bufKind) v' b.(bufDirty)).
iIntros "[Hbufdata Hisbuf_without_data]".
Theorem wp_buf_loadField_data bufptr a b stk E :
{{{
is_buf bufptr a b
}}}
struct.loadF buf.Buf "Data" #bufptr @ stk; E
{{{
(vslice : Slice.t), RET (slice_val vslice);
is_buf_data vslice b.(bufData) a ∗
is_buf_without_data bufptr a b vslice
}}}.
iNamed "Hisbuf_without_data".
Theorem wp_buf_storeField_data bufptr a b (vslice: Slice.t) k' (v' : bufDataT k') stk E :
{{{
is_buf bufptr a b ∗
is_buf_data vslice v' a ∗
⌜ k' = b.(bufKind) ⌝
}}}
struct.storeF buf.Buf "Data" #bufptr (slice_val vslice) @ stk; E
{{{
RET #();
is_buf bufptr a (Build_buf k' v' b.(bufDirty))
}}}.
iIntros (Φ) "(Hisbuf & Hisbufdata & %) HΦ".
iNamed "Hisbuf_without_data".
Definition extract_nth (b : Block) (elemsize : nat) (n : nat) : list val :=
drop (n * elemsize) (take ((S n) * elemsize) (Block_to_vals b)).
Lemma roundup_multiple a b:
b > 0 ->
(a*b-1) `div` b + 1 = a.
erewrite <- Zdiv_unique with (r := b-1) (q := a-1).
Definition is_bufData_at_off {K} (b : Block) (off : u64) (d : bufDataT K) : Prop :=
valid_off K off ∧
match d with
| bufBlock d => b = d ∧ int.Z off = 0
| bufInode i => extract_nth b inode_bytes ((int.nat off)/(inode_bytes*8)) = inode_to_vals i
| bufBit d => ∃ (b0 : u8), extract_nth b 1 ((int.nat off)/8) = #b0 :: nil ∧
get_bit b0 (word.modu off 8) = d
end.
Lemma buf_mapsto_non_null b a:
b ↦[Buf :: "Addr"] addr2val a -∗ ⌜ b ≠ null ⌝.
iDestruct (heap_mapsto_non_null with "[Hb.a]") as %Hnotnull.
rewrite struct_field_mapsto_eq /struct_field_mapsto_def //= struct_mapsto_eq /struct_mapsto_def.
iDestruct "Hb.a" as "[[[Hb _] _] _]".
repeat rewrite loc_add_0.
Theorem wp_MkBuf K a data (bufdata : bufDataT K) stk E :
{{{
is_buf_data data bufdata a ∗
⌜ valid_addr a ∧ valid_off K a.(addrOff) ⌝
}}}
MkBuf (addr2val a) #(bufSz K) (slice_val data) @ stk; E
{{{
(bufptr : loc), RET #bufptr;
is_buf bufptr a (Build_buf _ bufdata false)
}}}.
iIntros (Φ) "[Hbufdata %] HΦ".
wp_apply wp_allocStruct; first val_ty.
iDestruct (struct_fields_split with "Hb") as "(Hb.a & Hb.sz & Hb.data & Hb.dirty & %)".
iDestruct (buf_mapsto_non_null with "[$]") as %Hnotnull.
Ltac Zify.zify_post_hook ::= Z.div_mod_to_equations.
Theorem wp_MkBufLoad K a blk s (bufdata : bufDataT K) stk E :
{{{
slice.own_slice_small s u8T 1%Qp (Block_to_vals blk) ∗
⌜ is_bufData_at_off blk a.(addrOff) bufdata ⌝ ∗
⌜ valid_addr a ⌝
}}}
MkBufLoad (addr2val a) #(bufSz K) (slice_val s) @ stk; E
{{{
(bufptr : loc), RET #bufptr;
is_buf bufptr a (Build_buf _ bufdata false)
}}}.
iIntros (Φ) "(Hs & % & %) HΦ".
iDestruct (slice.own_slice_small_sz with "Hs") as "%".
destruct H as [Hoff Hatoff].
wp_apply (slice.wp_SliceSubslice_small with "[$Hs]").
rewrite /valid_addr in H0.
rewrite /valid_off in Hoff.
change (bufSz KindBlock) with (Z.to_nat 4096 * 8)%nat.
replace (int.Z s.(Slice.sz)) with (length (Block_to_vals blk) : Z).
rewrite length_Block_to_vals.
assert (a.(addrOff) = 0) as Hoff0.
change (bufSz KindBlock) with (Z.to_nat 4096 * 8)%nat in Hoff.
wp_apply wp_allocStruct; first val_ty.
iDestruct (struct_fields_split with "Hb") as "(Hb.a & Hb.sz & Hb.data & Hb.dirty & %)".
iDestruct (buf_mapsto_non_null with "[$]") as %Hnotnull.
rewrite /valid_off in Hoff.
destruct bufdata; cbn; cbn in Hatoff.
destruct Hatoff; intuition.
rewrite word.unsigned_sub.
rewrite word.unsigned_add.
replace (int.Z a.(addrOff) + Z.of_nat 1 - 1) with (int.Z a.(addrOff)) by lia.
rewrite -H3 /extract_nth.
replace (int.nat a.(addrOff) `div` 8 * 1)%nat with (int.nat a.(addrOff) `div` 8)%nat by lia.
replace (S (int.nat a.(addrOff) `div` 8) * 1)%nat with (S (int.nat a.(addrOff) `div` 8))%nat by lia.
rewrite Z2Nat.inj_div; try word.
rewrite Z2Nat.inj_add; try word.
rewrite Z2Nat.inj_div; try word.
change (Z.to_nat 8) with 8%nat.
unfold inode_bytes, block_bytes in *.
rewrite word.unsigned_sub.
rewrite word.unsigned_add.
replace (int.Z a.(addrOff) + Z.of_nat (Z.to_nat 128 * 8) - 1) with (int.Z a.(addrOff) + (128*8-1)) by lia.
rewrite -Hatoff /extract_nth.
rewrite Z2Nat.inj_div; try word.
change (Z.to_nat 8) with 8%nat.
change (Z.to_nat 128) with 128%nat.
change (128 * 8)%nat with (8 * 128)%nat.
rewrite -Nat.Div0.div_div; try word.
assert ((int.nat (addrOff a) `div` 8) `mod` 128 = 0)%nat as Hx.
replace (int.Z (addrOff a)) with (Z.of_nat (int.nat (addrOff a))) in Hoff by word.
rewrite -Nat2Z.inj_mod in Hoff; try word.
assert (int.nat (addrOff a) `mod` 1024 = 0)%nat as Hy by lia.
replace (1024)%nat with (8*128)%nat in Hy by reflexivity.
rewrite Nat.Div0.mod_mul_r in Hy; try word.
apply Nat.Div0.div_exact in Hx; try word.
rewrite Z2Nat.inj_add; try word.
rewrite Z2Nat.inj_div; try word.
change (Z.to_nat 1) with 1%nat.
change (Z.to_nat 8) with 8%nat.
change (Z.to_nat 128) with 128%nat.
rewrite Z2Nat.inj_add; try word.
change (Z.to_nat (128*8-1)) with (128*8-1)%nat.
replace (128 * 8)%nat with (8 * 128)%nat by reflexivity.
rewrite -Nat.Div0.div_div; try word.
assert ((int.nat (addrOff a) `div` 8) `mod` 128 = 0)%nat as Hx.
replace (int.Z (addrOff a)) with (Z.of_nat (int.nat (addrOff a))) in Hoff by word.
rewrite -Nat2Z.inj_mod in Hoff; try word.
assert (int.nat (addrOff a) `mod` 1024 = 0)%nat as Hy by lia.
replace (1024)%nat with (8*128)%nat in Hy by reflexivity.
rewrite Nat.Div0.mod_mul_r in Hy; try word.
apply Nat.Div0.div_exact in Hx; try word.
rewrite Nat.mul_comm in Hx.
replace (S ((int.nat (addrOff a) `div` 8) `div` 128) * 128)%nat
with (((int.nat (addrOff a) `div` 8) `div` 128) * 128 + 128)%nat by lia.
edestruct (Nat.Div0.div_exact (int.nat (addrOff a)) 8) as [_ Hz].
replace (int.Z (addrOff a)) with (Z.of_nat (int.nat (addrOff a))) in Hoff by word.
rewrite -Nat2Z.inj_mod in Hoff; try word.
assert (int.nat (addrOff a) `mod` 1024 = 0)%nat as Hy by lia.
replace (1024)%nat with (8*128)%nat in Hy by reflexivity.
rewrite Nat.Div0.mod_mul_r in Hy; try word.
rewrite -> Nat.div_add_l by lia.
change ((8 * 128 - 1) `div` 8)%nat with (127)%nat.
assert (a.(addrOff) = 0) as Hoff0.
replace (bufSz KindBlock) with (Z.to_nat 4096 * 8)%nat in Hoff by reflexivity.
rewrite /valid_addr /block_bytes /= in H0.
change (word.divu 0 8) with (U64 0).
change (word.add 0 (Z.to_nat 4096 * 8)%nat) with (U64 (4096 * 8)).
change (word.sub (4096 * 8) 1) with (U64 32767).
change (word.divu 32767 8) with (U64 4095).
change (word.add 4095 1) with (U64 4096).
rewrite length_Block_to_vals /block_bytes.
Lemma insert_Block_to_vals blk i (v : u8) (Hlt : (i < block_bytes)%nat) :
<[i := #v]> (Block_to_vals blk) = Block_to_vals (vinsert (Fin.of_nat_lt Hlt) v blk).
rewrite /Block_to_vals /b2val vec_to_list_insert.
rewrite list_fmap_insert fin_to_nat_to_fin //.
(** * Operating on blocks as if they were [nat -> byte]. *)
Definition get_byte (b:Block) (off:Z) : byte :=
default inhabitant (vec_to_list b !! Z.to_nat off).
Definition update_byte (b:Block) (off:Z) (x:byte) : Block :=
if decide (0 ≤ off) then
list_to_block (<[Z.to_nat off:=x]> (vec_to_list b))
else b.
Hint Unfold block_bytes : word.
Theorem get_update_eq (b:Block) (off:Z) x :
0 ≤ off < 4096 →
get_byte (update_byte b off x) off = x.
rewrite /get_byte /update_byte.
rewrite decide_True; [|word].
rewrite list_to_block_to_list; [|len].
rewrite list_lookup_insert; [|len].
Theorem get_update_ne (b:Block) (off off':Z) x :
off ≠ off' →
0 ≤ off' →
get_byte (update_byte b off x) off' = get_byte b off'.
rewrite /get_byte /update_byte.
destruct (decide _); auto.
rewrite list_to_block_to_list; [|len].
rewrite list_lookup_insert_ne; [|word].
(** * [byte → list bool] reasoning *)
Definition get_buf_data_bit (b: Block) (off: u64) : bool :=
let b_byte := get_byte b (int.Z off `div` 8) in
let b_bit := default false (byte_to_bits b_byte !! Z.to_nat (int.Z off `mod` 8)) in
b_bit.
Theorem get_bit_ok b0 (off: u64) :
(int.Z off < 8) →
get_bit b0 off = default false (byte_to_bits b0 !! int.nat off).
bit_cases off; byte_cases b0; vm_refl.
Lemma drop_take_lookup {A} i (l: list A) x :
l !! i = Some x →
drop i (take (S i) l) = [x].
apply elem_of_list_split_length in H as (l1 & l2 & -> & ->).
rewrite take_app_ge; [ | lia ].
rewrite drop_app_ge; [ | lia ].
replace (length l1 - length l1)%nat with 0%nat by lia.
replace (S (length l1) - length l1)%nat with 1%nat by lia.
Lemma extract_nth_bit blk (off: nat) :
extract_nth blk 1 off =
if decide (off < block_bytes)%nat then
[b2val (default inhabitant (vec_to_list blk !! off))]
else [].
rewrite -fmap_take -fmap_drop.
destruct (lookup_lt_is_Some_2 blk off) as [b0 Hlookup].
erewrite drop_take_lookup; eauto.
rewrite take_ge; [ | len ].
rewrite drop_ge; [ | len ].
Lemma valid_off_bit_trivial off : valid_off KindBit off ↔ True.
Theorem is_bufData_bit blk off (d: bufDataT KindBit) :
is_bufData_at_off blk off d ↔ (int.nat off `div` 8 < block_bytes)%nat ∧ bufBit (get_buf_data_bit blk off) = d.
rewrite /is_bufData_at_off.
rewrite valid_off_bit_trivial.
destruct H as [byte0 [Hnth_byte Hget_bit]].
rewrite -> get_bit_ok in Hget_bit by word.
rewrite extract_nth_bit in Hnth_byte.
destruct (decide _); [ | congruence ].
inversion Hnth_byte; subst; clear Hnth_byte.
rewrite /get_buf_data_bit /get_byte.
rewrite Z2Nat.inj_div //.
inversion Hbeq; subst; clear Hbeq.
eexists; split; [eauto|].
rewrite -> get_bit_ok by word.
rewrite /get_buf_data_bit /get_byte.
rewrite Z2Nat.inj_div //.
(* TODO(tej): I should have used !!! (lookup_total), which is [default inhabitant
(_ !! _)] ([list_lookup_total_alt] proves that). *)
(* off is a bit offset *)
Definition get_inode (blk: Block) (off: nat) : inode_buf :=
let start_byte := (off `div` 8)%nat in
list_to_inode_buf (subslice start_byte (start_byte+inode_bytes) (vec_to_list blk)).
Lemma Nat_div_inode_bits (off:nat) :
off `mod` 1024 = 0 →
(off `div` (inode_bytes * 8) * inode_bytes =
off `div` 8)%nat.
repeat rewrite !Nat2Z.inj_div !Nat2Z.inj_mul !Z2Nat.id //; try word.
Global Instance Nat_mul_comm : Comm eq Nat.mul.
Global Instance Z_mul_comm : Comm eq Z.mul.
Global Instance Nat_mul_assoc : Assoc eq Nat.mul.
Global Instance Z_mul_assoc : Assoc eq Z.mul.
Lemma Nat_div_exact_2 : ∀ a b : nat, (b ≠ 0 → a `mod` b = 0 → a = b * a `div` b)%nat.
apply Nat.Div0.div_exact; auto.
Lemma Z_mod_1024_to_div_8 (z:Z) :
z `mod` 1024 = 0 →
z `div` 8 = 128 * (z `div` 1024).
Hint Rewrite Nat2Z.inj_mul Nat2Z.inj_div : word.
Theorem is_bufData_inode blk off (d: bufDataT KindInode) :
is_bufData_at_off blk off d ↔
(int.nat off `div` 8 < block_bytes)%nat ∧
valid_off KindInode off ∧
bufInode (get_inode blk (int.nat off)) = d.
dependent destruction d; simpl.
rewrite /is_bufData_at_off.
rewrite -fmap_take -fmap_drop.
rewrite PeanoNat.Nat.mul_succ_l in Heq.
rewrite /valid_off /= in Hvalid.
rewrite -> Nat_div_inode_bits in Heq by word.
rewrite /inode_to_vals in Heq.
apply (inj (fmap b2val)) in Heq.
assert (int.nat off `div` 8 < block_bytes)%nat.
apply (f_equal length) in Heq.
rewrite inode_buf_to_list_to_inode_buf //.
intros (Hbound&Hvalid&Hdata).
inversion Hdata; subst; clear Hdata.
rewrite /valid_off /= in Hvalid.
rewrite PeanoNat.Nat.mul_succ_l.
rewrite -> !Nat_div_inode_bits by word.
rewrite list_to_inode_buf_to_list; last first.
rewrite /subslice /inode_bytes; len.
change (Z.to_nat 128) with 128%nat.
change (Z.of_nat 1024) with 1024 in Hvalid.
pose proof (Z_mod_1024_to_div_8 (int.Z off) Hvalid) as Hdiv8.
assert (int.nat off `div` 8 = 128 * int.nat off `div` 1024)%nat.
Lemma valid_block_off off :
int.Z off < block_bytes * 8 →
valid_off KindBlock off →
off = U64 0.
rewrite /valid_off => Hvalid_off.
change (Z.of_nat (bufSz KindBlock)) with 32768 in Hvalid_off.
change (block_bytes * 8) with 32768 in Hbound.
Lemma is_bufData_block b off (d: bufDataT KindBlock) :
is_bufData_at_off b off d ↔ off = U64 0 ∧ bufBlock b = d.
rewrite /is_bufData_at_off /=.
change (Z.of_nat $ bufSz KindBlock) with 32768.
(intuition subst); try congruence; try word.
Definition install_one_bit (src dst:byte) (bit:nat) : byte :=
(* bit in src we should copy *)
let b := default false (byte_to_bits src !! bit) in
let dst'_bits := <[bit:=b]> (byte_to_bits dst) in
let dst' := bits_to_byte dst'_bits in
dst'.
Lemma install_one_bit_spec src dst (bit: nat) :
(bit < 8)%nat →
∀ bit', byte_to_bits (install_one_bit src dst bit) !! bit' =
if (decide (bit = bit')) then byte_to_bits src !! bit
else byte_to_bits dst !! bit'.
rewrite /install_one_bit.
rewrite bits_to_byte_to_bits; [|len].
destruct (decide _); subst.
rewrite list_lookup_insert; [|len].
destruct (byte_to_bits src !! bit') eqn:Hlookup; auto.
move: Hlookup; rewrite lookup_ge_None; len.
rewrite list_lookup_insert_ne //.
Lemma default_list_lookup_lt {A:Type} (l: list A) (i: nat) x def :
i < length l →
default def (l !! i) = x →
l !! i = Some x.
destruct (l !! i) eqn:Hlookup; simpl; [congruence|].
move: Hlookup; rewrite lookup_ge_None; lia.
Lemma install_one_bit_id src dst bit :
(bit < 8)%nat →
default false (byte_to_bits src !! bit) = default false (byte_to_bits dst !! bit) →
install_one_bit src dst bit = dst.
rewrite /install_one_bit.
rewrite byte_to_bits_to_byte //.
eapply default_list_lookup_lt; len; eauto.
Lemma mask_bit_ok (b: u8) (bit: u64) :
int.Z bit < 8 →
word.and b (word.slu (U8 1) (u8_from_u64 bit)) =
if default false (byte_to_bits b !! int.nat bit) then
U8 (2^(int.nat bit))
else U8 0.
bit_cases bit; byte_cases b; vm_refl.
Lemma masks_different (bit:u64) :
int.Z bit < 8 →
U8 (2^int.nat bit ) ≠ U8 0.
intros Hbound Heq%(f_equal int.Z).
change (int.Z (U8 0)) with 0 in Heq.
bit_cases bit; vm_compute; by inversion 1.
Theorem wp_installOneBit (src dst: u8) (bit: u64) stk E :
int.Z bit < 8 →
{{{ True }}}
installOneBit #src #dst #bit @ stk; E
{{{ RET #(install_one_bit src dst (int.nat bit)); True }}}.
iIntros (Hbit_bounded Φ) "_ HΦ".
iSpecialize ("HΦ" with "[//]").
wp_apply wp_ref_to; first by val_ty.
wp_if_destruct; wp_pures.
wp_if_destruct; wp_pures.
destruct (default false (byte_to_bits src !! int.nat bit)) eqn:?.
apply masks_different in Heqb0; auto; contradiction.
destruct (default false (byte_to_bits dst !! int.nat bit)) eqn:?; last contradiction.
iExactEq "HΦ"; do 3 f_equal.
rewrite /install_one_bit.
apply (inj byte_to_bits).
rewrite bits_to_byte_to_bits; [|len].
bit_cases bit; byte_cases dst; vm_refl.
destruct (default false (byte_to_bits src !! int.nat bit)) eqn:?; last contradiction.
destruct (default false (byte_to_bits dst !! int.nat bit)) eqn:?; first contradiction.
iExactEq "HΦ"; do 3 f_equal.
rewrite /install_one_bit.
apply (inj byte_to_bits).
rewrite bits_to_byte_to_bits; [|len].
bit_cases bit; byte_cases dst; vm_refl.
iExactEq "HΦ"; do 3 f_equal.
rewrite install_one_bit_id //.
destruct (default false _), (default false _); auto.
apply masks_different in Heqb; eauto; contradiction.
apply symmetry, masks_different in Heqb; eauto; contradiction.
Lemma list_alter_lookup_insert {A} (l: list A) (i: nat) (f: A → A) x0 :
l !! i = Some x0 →
alter f i l = <[i:=f x0]> l.
revert i; induction l as [|x l]; intros i.
rewrite -/(alter f i l) Halter //.
Theorem wp_installBit
(src_s: Slice.t) (src_b: u8) q (* source *)
(dst_s: Slice.t) (dst_bs: list u8) (* destination *)
(dstoff: u64) (* the offset we're modifying, in bits *) stk E :
(int.Z dstoff < 8 * Z.of_nat (length dst_bs)) →
{{{ own_slice_small src_s byteT q [src_b] ∗ own_slice_small dst_s byteT 1 dst_bs }}}
installBit (slice_val src_s) (slice_val dst_s) #dstoff @ stk; E
{{{ RET #();
let dst_bs' :=
alter
(λ dst, install_one_bit src_b dst (Z.to_nat $ int.Z dstoff `mod` 8))
(Z.to_nat $ int.Z dstoff `div` 8) dst_bs in
own_slice_small src_s byteT q [src_b] ∗ own_slice_small dst_s byteT 1 dst_bs' }}}.
iIntros (Hbound Φ) "Hpre HΦ".
iDestruct "Hpre" as "[Hsrc Hdst]".
destruct (lookup_lt_is_Some_2 dst_bs (Z.to_nat (int.Z dstoff `div` 8)))
as [dst_b Hlookup]; first word.
wp_apply (wp_SliceGet (V:=u8) with "[$Hdst]").
wp_apply (wp_SliceGet (V:=u8) with "[$Hsrc]").
change (int.nat 0) with 0%nat.
wp_apply wp_installOneBit; first word.
wp_apply (wp_SliceSet (V:=u8) with "[$Hdst]").
erewrite list_alter_lookup_insert; eauto.
Lemma list_inserts_app_r' {A} (l1 l2 l3: list A) (i: nat) :
(length l2 ≤ i)%nat →
list_inserts i l1 (l2 ++ l3) = l2 ++ list_inserts (i-length l2) l1 l3.
replace i with (length l2 + (i - length l2))%nat at 1 by lia.
rewrite list_inserts_app_r //.
Theorem wp_installBytes
(src_s: Slice.t) (src_bs: list u8) q (* source *)
(dst_s: Slice.t) (dst_bs: list u8) (* destination *)
(dstoff: u64) (* the offset we're modifying, in bits *)
(nbit: u64) (* the number of bits we're modifying *) stk E :
int.Z nbit `div` 8 ≤ Z.of_nat (length src_bs) →
int.Z dstoff `div` 8 + int.Z nbit `div` 8 ≤ Z.of_nat (length dst_bs) →
{{{ own_slice_small src_s byteT q src_bs ∗
own_slice_small dst_s byteT 1 dst_bs
}}}
installBytes (slice_val src_s) (slice_val dst_s) #dstoff #nbit @ stk; E
{{{ RET #(); own_slice_small src_s byteT q src_bs ∗
let src_bs' := take (Z.to_nat $ int.Z nbit `div` 8) src_bs in
let dst_bs' := list_inserts (Z.to_nat $ int.Z dstoff `div` 8) src_bs' dst_bs in
own_slice_small dst_s byteT 1 dst_bs'
}}}.
intros Hnbound Hdst_has_space.
iDestruct "Hpre" as "[Hsrc Hdst]".
iDestruct (own_slice_small_sz with "Hsrc") as %Hsrc_sz.
iDestruct (own_slice_small_wf with "Hsrc") as %Hsrc_wf.
iDestruct (own_slice_small_sz with "Hdst") as %Hdst_sz.
iDestruct (own_slice_small_wf with "Hdst") as %Hdst_wf.
wp_apply wp_SliceTake; first by word.
wp_apply wp_SliceSkip; first by word.
iDestruct (slice_small_split _ (word.divu dstoff 8) with "Hdst")
as "[Hdst1 Hdst2]"; first by word.
iDestruct (slice_small_split _ (word.divu nbit 8) with "Hsrc")
as "[Hsrc1 Hsrc2]"; first by word.
wp_apply (wp_SliceCopy (V:=u8) with "[$Hsrc1 $Hdst2]").
iIntros "[Hsrc1 Hdst2']".
iDestruct (own_slice_combine with "Hdst1 Hdst2'")
as "Hdst"; first by word.
iDestruct (own_slice_combine with "Hsrc1 Hsrc2")
as "Hsrc"; first by word.
rewrite -> Nat.min_l by word.
rewrite -[l in list_inserts _ _ l](take_drop (int.nat (word.divu dstoff 8)) dst_bs).
rewrite -> list_inserts_app_r' by len.
match goal with
| |- context[list_inserts ?n _ _] => replace n with 0%nat by len
end.
match goal with
| |- context[list_inserts _ _ ?l] =>
rewrite -(take_drop (int.nat (word.divu nbit 8)) l)
end.
rewrite -> list_inserts_0_r by len.
Hint Unfold valid_addr block_bytes : word.
Lemma own_slice_to_block s q bs :
length bs = block_bytes →
own_slice_small s byteT q bs ⊣⊢
is_block s q (list_to_block bs).
rewrite list_to_block_to_vals //.
(** states that [blk'] is like [blk] but with [buf_b] installed at [off'] *)
Definition is_installed_block (blk: Block) (buf_b: buf) (off': u64) (blk': Block) : Prop :=
∀ off (d0: bufDataT buf_b.(bufKind)),
is_bufData_at_off blk off d0 →
if decide (off = off')
then is_bufData_at_off blk' off buf_b.(bufData)
else is_bufData_at_off blk' off d0.
Lemma is_installed_block_bit (off:u64) (b bufDirty : bool) (blk : Block) :
int.Z off < block_bytes * 8 →
∀ src_b : u8,
get_bit src_b (word.modu off 8) = b
→ is_installed_block
blk
{| bufKind := KindBit; bufData := bufBit b; bufDirty := bufDirty |}
off
(list_to_block
(alter
(λ (dst:u8),
install_one_bit src_b dst
(Z.to_nat (int.Z off `mod` 8)))
(Z.to_nat (int.Z off `div` 8)) (vec_to_list blk))).
intros Haddroff_bound src_b <-.
rewrite -> get_bit_ok by word.
apply is_bufData_bit in H as [Hoff_bound <-].
remember (int.Z off `div` 8) as byteOff.
remember (int.Z off `mod` 8) as bitOff.
destruct (lookup_lt_is_Some_2 (vec_to_list blk) (Z.to_nat byteOff))
as [byte0 Hlookup_byte]; [ len | ].
destruct (decide _); [subst off'|].
(* modified the desired bit *)
apply is_bufData_bit; split; [done|].
rewrite /get_buf_data_bit.
rewrite list_to_block_to_list; [|len].
rewrite -!HeqbyteOff -!HeqbitOff.
rewrite list_lookup_alter.
rewrite install_one_bit_spec; [ | word ].
(* other bits are unchanged *)
apply is_bufData_bit; split; [done|].
rewrite /get_buf_data_bit.
(* are we looking up the same byte, but a different bit? *)
destruct (decide (int.Z off' `div` 8 = byteOff)).
rewrite -> list_to_block_to_list by len.
rewrite list_lookup_alter.
rewrite install_one_bit_spec; [ | word ].
rewrite -> list_to_block_to_list by len.
rewrite list_lookup_alter_ne //.
Hint Rewrite @inserts_length : len.
Lemma subslice_lookup_ge_iff {A} n m i (l: list A) :
(m ≤ length l)%nat →
(m ≤ n+i)%nat ↔
subslice n m l !! i = None.
rewrite subslice_length //.
Lemma subslice_lookup_ge {A} n m i (l: list A) :
(m ≤ length l)%nat →
(m ≤ n+i)%nat →
subslice n m l !! i = None.
apply subslice_lookup_ge_iff; auto.
Lemma subslice_list_inserts_eq {A} (k l: list A) n m :
(m = n + length k)%nat →
(n + length k ≤ length l)%nat →
subslice n m (list_inserts n k l) = k.
intros -> Hinsert_in_bounds.
destruct (decide (i < length k)) as [Hbound|?].
rewrite -> subslice_lookup by lia.
rewrite list_lookup_inserts; auto with f_equal lia.
rewrite subslice_lookup_ge; auto with lia.
rewrite lookup_ge_None_2 //; lia.
rewrite inserts_length; lia.
Lemma subslice_list_inserts_ne {A} (k l: list A) n m i :
( m ≤ length l )%nat →
( m ≤ i ∨
i + length k ≤ n )%nat →
subslice n m (list_inserts i k l) = subslice n m l.
destruct (decide (n+j < m)) as [Hbound|?].
repeat rewrite -> subslice_lookup by lia.
rewrite list_lookup_inserts_lt; last by lia.
rewrite list_lookup_inserts_ge; last by lia.
repeat rewrite -> subslice_lookup_ge; auto with lia.
rewrite inserts_length; lia.
Lemma Nat_mod_1024_to_div_8 (n:nat) :
Z.of_nat n `mod` 1024 = 0 →
(n `div` 8 = 128 * (n `div` 1024))%nat.
pose proof (Z_mod_1024_to_div_8 (Z.of_nat n) Hn_mod).
apply (f_equal Z.to_nat) in H.
rewrite Z2Nat.inj_div in H; try lia.
Lemma is_installed_block_inode (a : addr) (i : inode_buf) (bufDirty : bool) (blk : Block) :
valid_addr a ∧ valid_off KindInode (addrOff a) →
is_installed_block
blk
{| bufKind := KindInode; bufData := bufInode i; bufDirty := bufDirty |}
(addrOff a)
(list_to_block
(list_inserts (Z.to_nat (int.Z (addrOff a) `div` 8))
(take (Z.to_nat (int.Z 1024%nat `div` 8)) i) blk)).
generalize dependent (addrOff a); intros off.
intros Hoff_bound Hvalid_off.
intros off' d Hdata_at_off; simpl in *.
apply is_bufData_inode in Hdata_at_off as (Hoff'_bound&Hoff'_valid&<-).
change (Z.to_nat (int.Z 1024%nat `div` 8)) with inode_bytes.
rewrite -> take_ge by len.
destruct (decide _); [subst off'|]; apply is_bufData_inode.
rewrite /valid_off /= in Hvalid_off.
rewrite -> list_to_block_to_list by len.
rewrite Z2Nat.inj_div; try word.
change (Z.to_nat 8) with 8%nat.
rewrite subslice_list_inserts_eq; len.
rewrite inode_buf_to_list_to_inode_buf //.
cut (int.Z off `div` 8 + 128 ≤ 4096).
rewrite /inode_bytes /block_bytes.
rewrite -> Z2Nat.inj_le by word.
rewrite -> Z2Nat.inj_add by word.
rewrite -> Z2Nat.inj_div by word.
rewrite -> list_to_block_to_list by len.
rewrite /valid_off /= in Hvalid_off, Hoff'_valid.
assert (int.nat off' `div` 8 ≠ int.nat off `div` 8).
replace (Z.to_nat (int.Z off `div` 8)) with (int.nat off `div` 8)%nat; last first.
rewrite Z2Nat.inj_div //; word.
rewrite -> !Nat_mod_1024_to_div_8 by lia.
rewrite -> !Z_mod_1024_to_div_8 in H by lia.
rewrite subslice_list_inserts_ne; eauto;
rewrite vec_to_list_length.
change 1024%nat with (8 * 128)%nat.
rewrite -Nat.Div0.div_div.
generalize (int.nat off' `div` 8)%nat; intros x Hx.
assert (x `div` 128 < 32)%nat; try lia.
eapply Nat.div_lt_upper_bound; lia.
destruct (decide (int.nat off' < int.nat off)); [ left | right ].
assert ((int.nat off' `div` 1024)%nat < (int.nat off `div` 1024)%nat); last by lia.
rewrite !Nat2Z.inj_div; lia.
assert ((int.nat off' `div` 1024)%nat > (int.nat off `div` 1024)%nat); last by lia.
rewrite !Nat2Z.inj_div; lia.
Lemma is_installed_block_block (b : Block) (bufDirty : bool) (blk : Block) :
is_installed_block
blk
{| bufKind := KindBlock; bufData := bufBlock b; bufDirty := bufDirty |} 0
(list_to_block (list_inserts 0 (take block_bytes b) blk)).
rewrite -> take_ge by len.
rewrite -[l in list_inserts _ _ l]app_nil_r.
rewrite -> list_inserts_0_r by len.
rewrite block_to_list_to_block.
intros off d Hdata%is_bufData_block.
destruct Hdata as [-> <-].
destruct (decide _); [ subst | congruence ].
apply is_bufData_block; auto.
Lemma bufSz_block_eq :
Z.of_nat (bufSz KindBlock) = 32768.
Lemma valid_block_off_addr a :
valid_addr a →
valid_off KindBlock (addrOff a) →
addrOff a = U64 0.
apply valid_block_off; auto.
Theorem wp_Buf__Install bufptr a b blk_s blk stk E :
{{{
is_buf bufptr a b ∗
is_block blk_s 1 blk
}}}
Buf__Install #bufptr (slice_val blk_s) @ stk; E
{{{
(blk': Block), RET #();
is_buf bufptr a b ∗
is_block blk_s 1 blk' ∗
⌜ is_installed_block blk b a.(addrOff) blk' ⌝
}}}.
iIntros (Φ) "[Hisbuf Hblk] HΦ".
iNamed "Hisbuf_without_data".
wp_apply util_proof.wp_DPrintf.
iDestruct "Hbufdata" as (src_b) "[Hsrc %Hsrc_data]".
wp_apply (wp_installBit with "[$Hsrc $Hblk]").
rewrite vec_to_list_length.
iDestruct (own_slice_to_block with "Hdst") as "$".
iExists _; iFrame "∗%"; simpl.
apply is_installed_block_bit; auto.
rewrite bool_decide_eq_true_2; last first.
rewrite /valid_off /= in H1.
change (Z.of_nat 1024) with (8*128) in H1.
rewrite Z.rem_mul_r // in H1.
wp_apply (wp_installBytes with "[$Hbufdata $Hblk]").
change (int.Z 1024%nat `div` 8) with 128.
destruct H as [Hvalid H].
rewrite Z_mod_1024_to_div_8 //.
iIntros "[Hbufdata Hblk]".
iDestruct (own_slice_to_block with "Hblk") as "Hblk".
apply is_installed_block_inode.
destruct H as [H Hvalidoff].
rewrite (valid_block_off_addr a) //.
rewrite bool_decide_eq_true_2; last first.
rewrite /valid_off in Hvalidoff.
rewrite bufSz_block_eq in Hvalidoff.
rewrite (valid_block_off_addr a) //.
wp_apply (wp_installBytes with "[$Hbufdata $Hblk]").
iDestruct (own_slice_to_block with "Hblk") as "Hblk".
change (Z.to_nat (int.Z 0 `div` 8)) with 0%nat.
change (Z.to_nat (int.Z 32768 `div` 8)) with block_bytes.
apply is_installed_block_block.
Theorem wp_Buf__SetDirty bufptr a b stk E :
{{{
is_buf bufptr a b
}}}
Buf__SetDirty #bufptr @ stk; E
{{{
RET #();
is_buf bufptr a (Build_buf b.(bufKind) b.(bufData) true)
}}}.
iNamed "Hisbuf_without_data".