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] 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.