From bb4e37a9c74aa92652f9c143bb63965544256794 Mon Sep 17 00:00:00 2001 From: Vadim Zaliva Date: Mon, 26 Aug 2024 16:33:38 -0700 Subject: [PATCH 1/4] added `sizeof_cap`, `cap_exact_encode_decode`, `cap_encode_length` --- theories/Common/Capabilities.v | 12 +++++-- theories/Morello/Capabilities.v | 60 +++++++++++++++++++++++++++++++-- 2 files changed, 68 insertions(+), 4 deletions(-) diff --git a/theories/Common/Capabilities.v b/theories/Common/Capabilities.v index 5c14ddf..ff0990a 100644 --- a/theories/Common/Capabilities.v +++ b/theories/Common/Capabilities.v @@ -8,7 +8,7 @@ Require Import Coq.Numbers.BinNums. Require Import Coq.Init.Datatypes. Require Import Coq.Bool.Bool. -Require Import Addr. +From CheriCaps.Common Require Import Addr. Set Implicit Arguments. Set Strict Implicit. @@ -129,7 +129,8 @@ Module Type CAPABILITY Parameter min_ptraddr : V.t. Parameter max_ptraddr : V.t. - Parameter sizeof_ptraddr: nat. + Parameter sizeof_cap: nat. (* in bytes, without tag *) + Parameter sizeof_ptraddr: nat. (* in bytes *) (** access to various cap fields **) @@ -331,4 +332,11 @@ Module Type CAPABILITY Parameter cap_invalidate_preserves_value: forall c, cap_get_value c = cap_get_value (cap_invalidate c). + Parameter cap_encode_length: + forall c t l t', encode t c = Some (l, t') -> List.length l = sizeof_cap. + + Parameter cap_exact_encode_decode: + forall c c' t l, encode true c = Some (l, t) -> decode l t = Some c' -> eqb c c' = true. + + End CAPABILITY. diff --git a/theories/Morello/Capabilities.v b/theories/Morello/Capabilities.v index aca9b02..b8f1253 100644 --- a/theories/Morello/Capabilities.v +++ b/theories/Morello/Capabilities.v @@ -667,6 +667,7 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou Definition cap_SEAL_TYPE_LB : ObjType.t := ObjType.of_Z 3. Definition sizeof_ptraddr := 8%nat. (* in bytes *) + Definition sizeof_cap := 16%nat. (* in bytes, without tag *) (* Definition ptraddr_bits := sizeof_ptraddr * 8. *) Definition min_ptraddr := Z_to_bv (N.of_nat (sizeof_ptraddr*8)) 0. Definition max_ptraddr := Z_to_bv (N.of_nat (sizeof_ptraddr*8)) (Z.sub (bv_modulus (N.of_nat (sizeof_ptraddr*8))) 1). @@ -1380,8 +1381,63 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou { unfold_cap. bitblast. } { fold (cap_get_value c). fold (cap_get_value (cap_invalidate (cap_set_objtype c ot))). rewrite <- cap_invalidate_preserves_value. unfold_cap. bitblast. } Qed. - -End Capability. + + Fact try_map_length + {A B:Type} + (f : A -> option B) (l:list A) + (l':list B): + try_map f l = Some l' -> length l = length l'. + Proof. + intros H. + revert l' H. + induction l. + - + intros l' H. + cbn in *. + inversion H. + reflexivity. + - + intros l' H. + cbn in *. + destruct (f a) eqn:Hfa; [| inversion H]. + destruct (try_map f l) eqn:Htry; [| inversion H]. + destruct l' as [| l0' l']; inversion H. + subst. + cbn. + f_equal. + apply IHl. + reflexivity. + Qed. + + Lemma cap_encode_length: + forall c t l t', encode t c = Some (l, t') -> List.length l = sizeof_cap. + Proof. + intros c t l t' H. + unfold encode in H. + repeat match goal with + | [ H : context [ match ?X with _ => _ end ] |- _] => + match type of X with + | sumbool _ _ => destruct X + | _ => destruct X eqn:? + end + end; inversion H. + + clear H H2. + subst l1. + unfold sizeof_cap. + apply try_map_length in Heqo0. + rewrite <- Heqo0. + clear Heqo0. + Admitted. + + Lemma cap_exact_encode_decode: + forall c c' t l, encode true c = Some (l, t) -> decode l t = Some c' -> eqb c c' = true. + Proof. + intros c c' t l E D. + apply eqb_eq. + Admitted. + +End Capability. Module ExampleCaps. From e4c0ae005873b9cc5e11d9ad8ba16b7efb2da543 Mon Sep 17 00:00:00 2001 From: Ricardo Almeida <3705908+ric-almeida@users.noreply.github.com> Date: Tue, 3 Sep 2024 18:58:17 +0100 Subject: [PATCH 2/4] Finished proof of cap_encode_length and added auxiliary lemmas about lengths of the outputs of byte_chunks and bits_of --- theories/Morello/Capabilities.v | 55 +++++++++++++++++++++++++++++++-- 1 file changed, 53 insertions(+), 2 deletions(-) diff --git a/theories/Morello/Capabilities.v b/theories/Morello/Capabilities.v index b8f1253..0323331 100644 --- a/theories/Morello/Capabilities.v +++ b/theories/Morello/Capabilities.v @@ -1409,6 +1409,41 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou reflexivity. Qed. + (* Consider migrating these functions to the libraries where the functions that reason about are defined *) + Lemma byte_chunks_len {a} (l : list a) l' : + (8 | length l)%nat → + byte_chunks l = Some l' → + length l' = ((length l)/8)%nat. + Proof. + intro Hdiv. unfold Nat.divide in Hdiv. destruct Hdiv as [q Hdiv]. + + assert (P: ∀ q (l : list a) l', length l = (q*8)%nat → byte_chunks l = Some l' → length l' = q). + { intro q'. induction q' as [| n IH]. + { intros l0 l0' Hlen Hbytes. simpl in Hlen. apply nil_length_inv in Hlen. subst. + simpl in Hbytes. injection Hbytes. intros. subst. done. } + { intros l0 l0' Hlen Hbytes. unfold byte_chunks in Hbytes. + destruct l0 eqn:E; [ done |]. + repeat case_match; try done. + assert (Hlensub: length l8 = (n*8)%nat). + { repeat rewrite cons_length in Hlen. simpl in Hlen. lia. } + specialize IH with (l:=l8) (l':=l9). + apply IH in Hlensub; [| done]. + injection Hbytes. intro H'. + rewrite <- H'. rewrite cons_length. lia. } } + + intro Hbytes. specialize P with (l:=l). apply P; try done. + rewrite Hdiv. rewrite Nat.div_mul; lia. + Qed. + + Lemma bits_of_len {n} (w : mword n) : + length (bits_of w) = Z.to_nat n. + Proof. + unfold bits_of. rewrite map_length. + unfold mword_to_bools. + rewrite MachineWord.word_to_bools_length. + reflexivity. + Qed. + Lemma cap_encode_length: forall c t l t', encode t c = Some (l, t') -> List.length l = sizeof_cap. Proof. @@ -1421,14 +1456,30 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou | _ => destruct X eqn:? end end; inversion H. - clear H H2. subst l1. unfold sizeof_cap. apply try_map_length in Heqo0. rewrite <- Heqo0. clear Heqo0. - Admitted. + unfold mem_bytes_of_bits in Heqo. + unfold option_map in Heqo. case_match; try done. + injection Heqo; clear Heqo; intro Heqo. + unfold bytes_of_bits in H. + unfold len in *. + change (Z.of_N 129) with 129%Z in *. + rewrite <- Heqo. + rewrite rev_length. + assert (L : base.length (bits_of (vec_of_bits (list.tail (@bits_of 129 c)))) = 128%nat). + { rewrite bits_of_len. unfold length_list. rewrite Nat2Z.id. + destruct (@bits_of 129 c) eqn:E; [discriminate|]. + simpl. replace (length l2) with (length (@bits_of 129 c) - 1)%nat. + { by rewrite bits_of_len. } + { rewrite E. simpl. lia. } } + apply byte_chunks_len in H. + { rewrite H. rewrite L. simpl. reflexivity. } + { rewrite L. exists 16%nat. simpl. reflexivity. } + Qed. Lemma cap_exact_encode_decode: forall c c' t l, encode true c = Some (l, t) -> decode l t = Some c' -> eqb c c' = true. From 4b2bc7b12305e7d5a92f3d58b19258ed5c707872 Mon Sep 17 00:00:00 2001 From: Ricardo Almeida <3705908+ric-almeida@users.noreply.github.com> Date: Fri, 6 Sep 2024 18:04:36 +0100 Subject: [PATCH 3/4] wip: proof of cap_exact_encode_decode --- theories/Morello/Capabilities.v | 56 ++++++++++++++++++++++++++++++++- 1 file changed, 55 insertions(+), 1 deletion(-) diff --git a/theories/Morello/Capabilities.v b/theories/Morello/Capabilities.v index 0323331..47cd00f 100644 --- a/theories/Morello/Capabilities.v +++ b/theories/Morello/Capabilities.v @@ -991,7 +991,7 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou Definition encode (isexact : bool) (c : t) : option ((list ascii) * bool) := let tag : bool := cap_is_valid c in - let c : (mword (Z.of_N len)) := c in (* why does Z.of_N len need to be specified? *) + let c : (mword (Z.of_N len)) := c in let cap_bits := bits_of c in let w : (mword _) := vec_of_bits (List.tail cap_bits) in match mem_bytes_of_bits w with @@ -1481,11 +1481,65 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou { rewrite L. exists 16%nat. simpl. reflexivity. } Qed. + Lemma cap_is_valid_bv c : + cap_is_valid c = ((@bv_extract 129 1 1 c) =? 1)%bv. + Admitted. + + Lemma bits_to_vec_to_bits l : + bits_of (vec_of_bits l) = l. + Admitted. + + Lemma mword_to_bits_to_mword {n} (c : mword n) : + uint (vec_of_bits (bits_of c)) = uint c. + 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'' → + map bitU_of_bool (bool_bits_of_bytes (rev l'')) = l. + Admitted. + Lemma cap_exact_encode_decode: forall c c' t l, encode true c = Some (l, t) -> decode l t = Some c' -> eqb c c' = true. Proof. intros c c' t l E D. apply eqb_eq. + + unfold encode in E. case_match eqn:E1; try done. case_match eqn:E2; try done. + inversion E; clear E; subst. + + unfold decode in D. case_match eqn:D1; try done. case_match eqn:D2; try done. + inversion D; clear D; subst; clear D1. + + unfold mem_bytes_of_bits in E1. unfold bytes_of_bits in E1. + unfold option_map in E1. case_match eqn:E3; try done. + inversion E1; clear E1; subst. + unfold t, len in *. + + replace (list.tail (@bits_of (Z.of_N 129) c)) with (@bits_of (Z.of_N 128) (bv_extract 0 128 c)) in E3. + { + apply (bytes_to_bits_to_bytes _ l1 l) in E3; try assumption. + replace (map bitU_of_bool (cap_is_valid c :: bool_bits_of_bytes (rev l))) with + (bitU_of_bool (cap_is_valid c) :: map bitU_of_bool (bool_bits_of_bytes (rev l))) in D2. + { rewrite E3 in D2. rewrite bits_to_vec_to_bits in D2. rewrite cap_is_valid_bv in D2. + + unfold bitU_of_bool in D2. case_match eqn:M. + + replace (B1 :: @bits_of (Z.of_N 128) (bv_extract 0 128 c)) with (@bits_of (Z.of_N 129) c) in D2. + - apply Z_to_bv_checked_Some in D2. apply bv_eq. rewrite <- D2. + rewrite mword_to_bits_to_mword. unfold uint. simpl. + unfold MachineWord.word_to_N. rewrite Z2N.id; [ done | apply bv_unsigned_in_range ]. + - replace B1 with (bitU_of_bool ((bv_extract 1 1 c =? 1))). + { unfold bits_of at 2. unfold mword_to_bools; simpl; unfold MachineWord.word_to_bools. + admit. } + { rewrite M. reflexivity. } + + admit. + } + { reflexivity. } + } + { unfold bits_of. unfold mword_to_bools, MachineWord.word_to_bools; simpl. + replace c with (bv_concat 129 (bv_extract 128 1 c) (bv_extract 0 128 c)) at 2; [| bv_simplify; bitblast]. + admit. } + Admitted. End Capability. From 8336a4b48f6a291998fb2e65dfd8beeb4e12e2ff Mon Sep 17 00:00:00 2001 From: Ricardo Almeida <3705908+ric-almeida@users.noreply.github.com> Date: Thu, 12 Sep 2024 19:06:06 +0100 Subject: [PATCH 4/4] - wip: proof of cap_exact_encode_decode - Removed redundant boolean isExact param of encode --- theories/Common/Capabilities.v | 11 +-- theories/Morello/Capabilities.v | 126 ++++++++++++++++++++------------ theories/Morello/MorelloTests.v | 2 +- 3 files changed, 86 insertions(+), 53 deletions(-) diff --git a/theories/Common/Capabilities.v b/theories/Common/Capabilities.v index ff0990a..e8db3a2 100644 --- a/theories/Common/Capabilities.v +++ b/theories/Common/Capabilities.v @@ -279,12 +279,9 @@ Module Type CAPABILITY Parameter decode: list ascii -> bool -> option t. (** Encode capability as list of bytes. - boolean argument specifies if bounds need to be encoded - exactly. if exact encoding is requested but not possible, inParameterid - capability will be returned. - Retuns memory-encoded capability and validity tag. + Retuns memory-encoded capability and validity tag. *) - Parameter encode: bool -> t -> option ((list ascii) * bool). + Parameter encode: t -> option ((list ascii) * bool). (* --- Compression-related --- *) @@ -333,10 +330,10 @@ Module Type CAPABILITY Parameter cap_invalidate_preserves_value: forall c, cap_get_value c = cap_get_value (cap_invalidate c). Parameter cap_encode_length: - forall c t l t', encode t c = Some (l, t') -> List.length l = sizeof_cap. + forall c l t, encode c = Some (l, t) -> List.length l = sizeof_cap. Parameter cap_exact_encode_decode: - forall c c' t l, encode true c = Some (l, t) -> decode l t = Some c' -> eqb c c' = true. + forall c c' t l, encode c = Some (l, t) -> decode l t = Some c' -> eqb c c' = true. End CAPABILITY. diff --git a/theories/Morello/Capabilities.v b/theories/Morello/Capabilities.v index 47cd00f..fb49640 100644 --- a/theories/Morello/Capabilities.v +++ b/theories/Morello/Capabilities.v @@ -989,7 +989,7 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou end end. - Definition encode (isexact : bool) (c : t) : option ((list ascii) * bool) := + Definition encode (c : t) : option ((list ascii) * bool) := let tag : bool := cap_is_valid c in let c : (mword (Z.of_N len)) := c in let cap_bits := bits_of c in @@ -1445,9 +1445,9 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou Qed. Lemma cap_encode_length: - forall c t l t', encode t c = Some (l, t') -> List.length l = sizeof_cap. + forall c l t', encode c = Some (l, t') -> List.length l = sizeof_cap. Proof. - intros c t l t' H. + intros c l t' H. unfold encode in H. repeat match goal with | [ H : context [ match ?X with _ => _ end ] |- _] => @@ -1481,66 +1481,102 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou { rewrite L. exists 16%nat. simpl. reflexivity. } Qed. - Lemma cap_is_valid_bv c : - cap_is_valid c = ((@bv_extract 129 1 1 c) =? 1)%bv. + Lemma cap_is_valid_bv c : + cap_is_valid c = ((@bv_extract 129 128 1 c) =? 1)%bv. Admitted. + 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))). + 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. + assert (H: ∀ n l, length l = n → bits_of (concat_vec (vec_of_bits [h]) (vec_of_bits l)) = h :: bits_of (vec_of_bits l)). + { + intro n. induction n as [ | m IH ]. + + intros l' H. apply nil_length_inv in H. subst. + destruct h eqn:H. + - by vm_compute. + - by vm_compute. + - simpl. vm_compute (vec_of_bits []). + unfold vec_of_bits. unfold bool_of_bit. simpl. unfold of_bools. + unfold bools_to_mword. unfold MachineWord.bools_to_word. simpl. + unfold MachineWord.N_to_word. + unfold to_word_nat. + simpl. + unfold bits_of. + destruct (dummy false) eqn:D. + { simpl. admit. } + vm_compute (dummy false). + replace (dummy false) with false. + 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 mword_to_bits_to_mword {n} (c : mword n) : + + Lemma mword_to_bits_to_mword {n} (c : mword n) : uint (vec_of_bits (bits_of c)) = uint c. Admitted. - - Lemma bytes_to_bits_to_bytes l l' l'' : + + Lemma bytes_to_bits_to_bytes l l' l'' : byte_chunks l = Some l' → try_map memory_byte_to_ascii (rev l') = Some l'' → map bitU_of_bool (bool_bits_of_bytes (rev l'')) = l. Admitted. - - Lemma cap_exact_encode_decode: - forall c c' t l, encode true c = Some (l, t) -> decode l t = Some c' -> eqb c c' = true. + + Lemma mword_to_bools_split (c: bv 129) : + @mword_to_bools 129 c = (((@bv_extract 129 128 1 c =? 1)) :: (@mword_to_bools 128(@bv_extract 129 0 128 c)))%list. + Admitted. + + Lemma cap_exact_encode_decode : + forall c c' t l, encode c = Some (l, t) -> decode l t = Some c' -> eqb c c' = true. Proof. - intros c c' t l E D. - apply eqb_eq. + intros c c' t l E D. apply eqb_eq. - unfold encode in E. case_match eqn:E1; try done. case_match eqn:E2; try done. + unfold encode in E. case_match eqn:E1; try done. case_match; try done. inversion E; clear E; subst. - unfold decode in D. case_match eqn:D1; try done. case_match eqn:D2; try done. - inversion D; clear D; subst; clear D1. + unfold decode in D. case_match eqn:D1; try done; clear D1. case_match eqn:D2; try done. + inversion D; clear D; subst. - unfold mem_bytes_of_bits in E1. unfold bytes_of_bits in E1. - unfold option_map in E1. case_match eqn:E3; try done. + unfold mem_bytes_of_bits in E1. unfold bytes_of_bits in E1. unfold option_map in E1. case_match eqn:E3; try done. inversion E1; clear E1; subst. - unfold t, len in *. - - replace (list.tail (@bits_of (Z.of_N 129) c)) with (@bits_of (Z.of_N 128) (bv_extract 0 128 c)) in E3. - { - apply (bytes_to_bits_to_bytes _ l1 l) in E3; try assumption. - replace (map bitU_of_bool (cap_is_valid c :: bool_bits_of_bytes (rev l))) with - (bitU_of_bool (cap_is_valid c) :: map bitU_of_bool (bool_bits_of_bytes (rev l))) in D2. - { rewrite E3 in D2. rewrite bits_to_vec_to_bits in D2. rewrite cap_is_valid_bv in D2. - - unfold bitU_of_bool in D2. case_match eqn:M. - + replace (B1 :: @bits_of (Z.of_N 128) (bv_extract 0 128 c)) with (@bits_of (Z.of_N 129) c) in D2. - - apply Z_to_bv_checked_Some in D2. apply bv_eq. rewrite <- D2. - rewrite mword_to_bits_to_mword. unfold uint. simpl. - unfold MachineWord.word_to_N. rewrite Z2N.id; [ done | apply bv_unsigned_in_range ]. - - replace B1 with (bitU_of_bool ((bv_extract 1 1 c =? 1))). - { unfold bits_of at 2. unfold mword_to_bools; simpl; unfold MachineWord.word_to_bools. - admit. } - { rewrite M. reflexivity. } - + admit. - } - { reflexivity. } - } - { unfold bits_of. unfold mword_to_bools, MachineWord.word_to_bools; simpl. - replace c with (bv_concat 129 (bv_extract 128 1 c) (bv_extract 0 128 c)) at 2; [| bv_simplify; bitblast]. - admit. } - Admitted. + apply Z_to_bv_checked_Some in D2. apply bv_eq. rewrite <- D2. + apply (bytes_to_bits_to_bytes _ l1 l) in E3; try assumption. simpl. + rewrite E3. rewrite bits_to_vec_to_bits. + + rewrite cap_is_valid_bv. + + destruct (bv_extract 128 1 c =? 1) eqn:H_c_valid; + unfold t, len in *; rewrite H_c_valid; simpl; + [ replace B1 with (bitU_of_bool (bv_extract 128 1 c =? 1)); [| rewrite H_c_valid; reflexivity] + | replace B0 with (bitU_of_bool (bv_extract 128 1 c =? 1)); [| rewrite H_c_valid; reflexivity]]. + all: + unfold bits_of; + rewrite mword_to_bools_split; + rewrite map_cons; simpl; rewrite <- map_cons; rewrite <- mword_to_bools_split; + fold (@bits_of 129 c); + rewrite mword_to_bits_to_mword; + unfold uint; simpl; + unfold MachineWord.word_to_N; rewrite Z2N.id; [ done | apply bv_unsigned_in_range ]. + Qed. End Capability. diff --git a/theories/Morello/MorelloTests.v b/theories/Morello/MorelloTests.v index be8cb87..e1a8b08 100644 --- a/theories/Morello/MorelloTests.v +++ b/theories/Morello/MorelloTests.v @@ -251,7 +251,7 @@ Module test_cap_getters_and_setters. Example encode_and_decode_test_1 : let tester := fun cap:Capability.t => - let encoded_cap : option ((list ascii) * bool) := encode true cap in + let encoded_cap : option ((list ascii) * bool) := encode cap in let decoded_cap : option Capability.t := match encoded_cap with Some (l,tag) => (decode l tag) | None => None