diff --git a/theories/Morello/Capabilities.v b/theories/Morello/Capabilities.v index a370b3e..ece04bc 100644 --- a/theories/Morello/Capabilities.v +++ b/theories/Morello/Capabilities.v @@ -40,7 +40,7 @@ Local Notation "x >=? y" := (geb x y) (at level 70, no associativity) : bv_scope Local Notation "(<@{ A } )" := (@lt A) (only parsing) : stdpp_scope. Local Notation LtDecision A := (RelDecision (<@{A})). -(** Utility converters **) +(** Utility converters and lemmas **) Definition bv_to_Z_unsigned {n} (v : bv n) : Z := v.(bv_unsigned). Definition bv_to_N {n} (v : bv n) : N := Z.to_N v.(bv_unsigned). @@ -67,6 +67,22 @@ Definition invert_bits {n} (m : mword n) : (mword n) := let x : Z := int_of_mword false x in mword_of_int x. +Lemma bv_eqb_eq {n} : forall (a b: bv n), (a =? b) = true <-> a = b. +Proof. + split. + - intro H. unfold Capabilities.eqb in H. + apply Z.eqb_eq in H. apply bv_eq in H. exact H. + - intro H. rewrite H. unfold Capabilities.eqb. lia. +Defined. + +Lemma bv1_neqb_eq0 : forall (a : bv 1), (a =? 1%bv) = false <-> a = 0%bv. +Proof. + intros. split. + + intro H. unfold eqb in H. apply Z.eqb_neq in H. apply bv_eq. + assert (P: (0 ≤ bv_unsigned a < 2)%Z); [ apply (bv_unsigned_in_range 1 a) |]. + change (bv_unsigned 0) with 0%Z. change (bv_unsigned 1) with 1%Z in H. lia. + + intro H. rewrite H. done. +Qed. Module Permissions <: PERMISSIONS. Definition len:N := 18. (* CAP_PERMS_NUM_BITS = 16 bits of actual perms + 2 bits for Executive and Global *) @@ -1135,12 +1151,7 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou Qed. Lemma eqb_eq : forall (a b:t), (a =? b) = true <-> a = b. - Proof. - split. - - intro H. unfold Capabilities.eqb in H. - apply Z.eqb_eq in H. apply bv_eq in H. exact H. - - intro H. rewrite H. apply eqb_refl. - Defined. + Proof. apply bv_eqb_eq. Defined. (* Beginning of Translation definitions and lemmas from Capabilities to bitvectors. *) @@ -1477,7 +1488,11 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou Lemma cap_encode_valid: forall cap cb b, cap_is_valid cap = true -> encode cap = Some (cb, b) -> b = true. - Admitted. + Proof. + intros cap bytes tag H_valid H_encode. + unfold encode in H_encode. repeat case_match; try done. + inversion H_encode. exact H_valid. + Qed. Lemma cap_is_valid_bv_extract c : cap_is_valid c ↔ bv_extract 128 1 c = (BV 1 1). @@ -1511,39 +1526,11 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou symmetry. apply Z.eqb_neq. by apply bv_neq. Qed. - Lemma bits_of_vec_hd h l : - bits_of (vec_of_bits (h::l)) = bits_of ((concat_vec (vec_of_bits [h]) (vec_of_bits l))). + Lemma mword_to_bits_to_mword {n} (c : mword (n)) : + vec_of_bits (bits_of c) = autocast c. Proof. Admitted. - Lemma hd_bits_of_vec h l : - h ≠ BU → - bits_of (concat_vec (vec_of_bits [h]) (vec_of_bits l)) = h :: bits_of (vec_of_bits l). - Proof. - Admitted. - - Lemma bits_to_vec_to_bits l : - bits_of (vec_of_bits l) = l. - Proof. - assert (H: ∀ n l, length l = n → bits_of (vec_of_bits l) = l). - { intro n. induction n as [ | m IH ]. - + intros l' H. apply nil_length_inv in H. subst. by vm_compute. - + intros l' H. destruct l' as [| h tl]; try discriminate. - rewrite cons_length in H. inversion H as [H1]. - specialize IH with (l:=tl). apply IH in H1 as H2. - - rewrite bits_of_vec_hd. - rewrite hd_bits_of_vec; [| by rewrite H2 ]. - admit. - } - by apply (H (length l)). - Admitted. - - Lemma cap_to_bits_to_cap (c : mword 129) : - vec_of_bits (bits_of c) = c. - Proof. - Admitted. - Lemma bytes_to_bits_to_bytes l l' l'' : byte_chunks l = Some l' → try_map memory_byte_to_ascii (rev l') = Some l'' → @@ -1553,7 +1540,30 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou Lemma bv_to_bits_app_last (c : bv 129) : bv_to_bits c = (bv_to_bits (bv_extract 0 128 c) ++ [bv_extract 128 1 c =? 1])%list. - Admitted. + Proof. + have -> : bv_to_bits c = bv_to_bits (@bv_concat 129 1 128 (@bv_extract 129 128 1 c) (@bv_extract 129 0 128 c)). + { apply f_equal. bv_simplify. bitblast. } + set (l1 := bv_to_bits (bv_concat 129 (bv_extract 128 1 c) (bv_extract 0 128 c))). + set (l2 := (bv_to_bits (bv_extract 0 128 c) ++ [bv_extract 128 1 c =? 1])%list). + apply list_eq. intro i. + destruct (128 : bv_unsigned vec = bv_unsigned (@bv_to_bv _ 129 vec). { unfold bv_to_bv, bv_to_Z_unsigned. by rewrite Z_to_bv_bv_unsigned. } @@ -1587,20 +1605,19 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou rewrite cap_is_valid_bv_extract_bool. destruct (bv_extract 128 1 c =? 1) eqn:H_c_valid; simpl; [ replace B1 with (bitU_of_bool (bv_extract 128 1 c =? 1)); [| by rewrite H_c_valid ] - | replace B0 with (bitU_of_bool (bv_extract 128 1 c =? 1)); [| by rewrite H_c_valid ]]. - all: unfold bits_of; - have -> : @mword_to_bools 129 c = (bv_extract 128 1 c =? 1) :: @mword_to_bools 128 (bv_extract 0 128 c); [ by rewrite mword_to_bools_cons_last |]; - rewrite map_cons; simpl; + | replace B0 with (bitU_of_bool (bv_extract 128 1 c =? 1)); [| by rewrite H_c_valid ]]. + all: unfold bits_of; + change (autocast (bv_extract 0 128 c)) with ((bv_extract 0 128 c)); have -> : vec_of_bits (bitU_of_bool (bv_extract 128 1 c =? 1) :: map bitU_of_bool (@mword_to_bools 128 (bv_extract 0 128 c))) = (vec_of_bits (map bitU_of_bool ((bv_extract 128 1 c =? 1) :: @mword_to_bools 128 (bv_extract 0 128 c)))); [ unfold vec_of_bits; apply f_equal; by rewrite map_cons | have -> : bv_unsigned (vec_of_bits (map bitU_of_bool ((@bv_extract 129 128 1 c =? 1) :: @mword_to_bools 128 (@bv_extract 129 0 128 c)))) = bv_unsigned (vec_of_bits (map bitU_of_bool (@mword_to_bools 129 c))); [ change (N.of_nat (Pos.to_nat (Pos.of_succ_nat _ ))) with 129%N; apply f_equal; unfold vec_of_bits; apply f_equal; by rewrite <- mword_to_bools_cons_last - | fold (@bits_of 129 c); rewrite cap_to_bits_to_cap; by rewrite Z_to_bv_bv_unsigned ] + | fold (@bits_of 129 c); rewrite mword_to_bits_to_mword; by rewrite Z_to_bv_bv_unsigned ] ]. } Qed. - + Lemma cap_encode_decode_bounds: ∀ cap bytes t, encode cap = Some (bytes, t) →