Merge branch 'taramana_pulse_no_slice_pair' of github.com:project-eve…

…rest/everparse into taramana_cbor_no_slice_pair
project-everest · Oct 30, 2024 · 94ee2db · 94ee2db
2 parents 1ebca60 + 28f4e3b
commit 94ee2db
Show file tree

Hide file tree

Showing 5 changed files with 42 additions and 42 deletions.
diff --git a/.docker/build/config.json b/.docker/build/config.json
@@ -29,7 +29,7 @@
 
     "RepoVersions" : {
         "mitls_version" : "origin/dev",
-        "pulse_version" : "origin/main",
+        "pulse_version" : "origin/_taramana_no_slice_pair",
         "karamel_version" : "origin/master"
     }
 }
diff --git a/src/lowparse/pulse/LowParse.Pulse.Base.fst b/src/lowparse/pulse/LowParse.Pulse.Base.fst
@@ -352,9 +352,9 @@ let peek_post
   (pm: perm)
   (v: bytes)
   (consumed: SZ.t)
-  (res: slice_pair byte)
+  (res: (slice byte & slice byte))
 : Tot slprop
-= let SlicePair left right = res in
+= let (left, right) = res in
   peek_post' s input pm v consumed left right
 
 inline_for_extraction
@@ -366,20 +366,20 @@ fn peek
   (#v: Ghost.erased bytes)
   (consumed: SZ.t)
   requires (pts_to input #pm v ** pure (validator_success #k #t p 0sz v (consumed)))
-  returns res: slice_pair byte
+  returns res: (slice byte & slice byte)
   ensures peek_post s input pm v consumed res
 {
   let s1s2 = split input consumed;
   match s1s2 {
-    SlicePair s1 s2 -> {
+    Mktuple2 s1 s2 -> {
       Seq.lemma_split v (SZ.v consumed);
       let v1 = Ghost.hide (fst (Some?.v (parse p v)));
       parse_injective #k p (bare_serialize s v1) v;
       with v1' . assert (pts_to s1 #pm v1');
       rewrite (pts_to s1 #pm v1') as (pts_to_serialized s s1 #pm v1);
       fold (peek_post' s input pm v consumed s1 s2);
-      fold (peek_post s input pm v consumed (SlicePair s1 s2));
-      (SlicePair s1 s2)
+      fold (peek_post s input pm v consumed (s1, s2));
+      (s1, s2)
     }
   }
 }
@@ -408,9 +408,9 @@ let peek_trade_post
   (pm: perm)
   (v: bytes)
   (consumed: SZ.t)
-  (res: slice_pair byte)
+  (res: (slice byte & slice byte))
 : Tot slprop
-= let (SlicePair left right) = res in
+= let (left, right) = res in
   peek_trade_post' s input pm v consumed left right
 
 ```pulse
@@ -445,18 +445,18 @@ fn peek_trade
   (#v: Ghost.erased bytes)
   (consumed: SZ.t)
   requires (pts_to input #pm v ** pure (validator_success #k #t p 0sz v (consumed)))
-  returns res: (slice_pair byte)
+  returns res: (slice byte & slice byte)
   ensures peek_trade_post s input pm v consumed res
 {
   let res = peek s input consumed;
-  match res { SlicePair left right -> {
+  match res { Mktuple2 left right -> {
     unfold (peek_post s input pm v consumed res);
     unfold (peek_post' s input pm v consumed left right);
     with v1 v2 . assert (pts_to_serialized s left #pm v1 ** pts_to right #pm v2);
     intro_trade (pts_to_serialized s left #pm v1 ** pts_to right #pm v2) (pts_to input #pm v) (is_split input left right) (peek_trade_aux s input pm consumed v left right v1 v2 ());
     fold (peek_trade_post' s input pm v consumed left right);
-    fold (peek_trade_post s input pm v consumed (left `SlicePair` right));
-    (left `SlicePair` right)
+    fold (peek_trade_post s input pm v consumed (left, right));
+    (left, right)
   }}
 }
 ```
@@ -478,12 +478,12 @@ fn peek_trade_gen
   )
 {
   let split123 = split_trade input offset;
-  match split123 { SlicePair input1 input23 -> {
+  match split123 { Mktuple2 input1 input23 -> {
     with v23 . assert (pts_to input23 #pm v23);
     Trade.elim_hyp_l (pts_to input1 #pm _) (pts_to input23 #pm v23) _;
     let consumed = SZ.sub off offset;
     let split23 = peek_trade s input23 consumed;
-    match split23 { SlicePair input2 input3 -> {
+    match split23 { Mktuple2 input2 input3 -> {
       unfold (peek_trade_post s input23 pm v23 consumed split23);
       unfold (peek_trade_post' s input23 pm v23 consumed input2 input3);
       with v' . assert (pts_to_serialized s input2 #pm v');
@@ -1591,11 +1591,11 @@ fn l2r_write_copy
   let length = S.len x.v;
   let sp1 = S.split out offset;
   match sp1 {
-    S.SlicePair sp11 sp12 -> {
+    Mktuple2 sp11 sp12 -> {
       with v12 . assert (pts_to sp12 v12);
       let sp2 = S.split sp12 length;
       match sp2 {
-        S.SlicePair sp21 sp22 -> {
+        Mktuple2 sp21 sp22 -> {
           S.pts_to_len sp21;
           S.copy sp21 x.v;
           S.join sp21 sp22 sp12;

diff --git a/src/lowparse/pulse/LowParse.Pulse.Combinators.fst b/src/lowparse/pulse/LowParse.Pulse.Combinators.fst
@@ -762,9 +762,9 @@ let split_dtuple2_post
   (input: slice byte)
   (pm: perm)
   (v: Ghost.erased (dtuple2 t1 t2))
-  (res: slice_pair byte)
+  (res: (slice byte & slice byte))
 : Tot slprop
-= let (SlicePair left right) = res in
+= let (left, right) = res in
   split_dtuple2_post' s1 s2 input pm v left right
 
 inline_for_extraction
@@ -783,7 +783,7 @@ fn split_dtuple2
   (#pm: perm)
   (#v: Ghost.erased (dtuple2 t1 t2))
   requires pts_to_serialized (serialize_dtuple2 s1 s2) input #pm v
-  returns res: slice_pair byte
+  returns res: (slice byte & slice byte)
   ensures split_dtuple2_post s1 s2 input pm v res
 {
   serialize_dtuple2_eq s1 s2 v;
@@ -794,15 +794,15 @@ fn split_dtuple2
   let i = j1 input 0sz;
   let res = append_split_trade input i;
   match res {
-    SlicePair input1 input2 -> {
+    Mktuple2 input1 input2 -> {
       Trade.trans (_ ** _) _ _;
       pts_to_serialized_intro_trade s1 input1 (dfst v);
       pts_to_serialized_intro_trade (s2 (dfst v)) input2 (dsnd v);
       Trade.prod (pts_to_serialized s1 input1 #pm _) (pts_to input1 #pm _) (pts_to_serialized (s2 (dfst v)) input2 #pm _) (pts_to input2 #pm _);
       Trade.trans (pts_to_serialized s1 input1 #pm _ ** pts_to_serialized (s2 (dfst v)) input2 #pm _) (pts_to input1 #pm _ ** pts_to input2 #pm _) _;
       fold (split_dtuple2_post' s1 s2 input pm v input1 input2);
-      fold (split_dtuple2_post s1 s2 input pm v (input1 `SlicePair` input2));
-      (input1 `SlicePair` input2)
+      fold (split_dtuple2_post s1 s2 input pm v (input1, input2));
+      (input1, input2)
     }
   }
 }
@@ -829,7 +829,7 @@ fn dtuple2_dfst
     trade (pts_to_serialized s1 res #pm (dfst v)) (pts_to_serialized (serialize_dtuple2 s1 s2) input #pm v)
 {
   let spl = split_dtuple2 s1 j1 s2 input;
-  match spl { SlicePair input1 input2 -> {
+  match spl { Mktuple2 input1 input2 -> {
     unfold (split_dtuple2_post s1 s2 input pm v spl);
     unfold (split_dtuple2_post' s1 s2 input pm v input1 input2);
     Trade.elim_hyp_r _ _ _;
@@ -859,7 +859,7 @@ fn dtuple2_dsnd
     trade (pts_to_serialized (s2 (dfst v)) res #pm (dsnd v)) (pts_to_serialized (serialize_dtuple2 s1 s2) input #pm v)
 {
   let spl = split_dtuple2 s1 j1 s2 input;
-  match spl { SlicePair input1 input2 -> {
+  match spl { Mktuple2 input1 input2 -> {
     unfold (split_dtuple2_post s1 s2 input pm v spl);
     unfold (split_dtuple2_post' s1 s2 input pm v input1 input2);
     Trade.elim_hyp_l _ _ _;
@@ -898,9 +898,9 @@ let split_nondep_then_post
   (input: slice byte)
   (pm: perm)
   (v: Ghost.erased (t1 & t2))
-  (res: slice_pair byte)
+  (res: (slice byte & slice byte))
 : Tot slprop
-= let (SlicePair left right) = res in
+= let (left, right) = res in
   split_nondep_then_post' s1 s2 input pm v left right
 
 #set-options "--print_implicits"
@@ -944,7 +944,7 @@ fn split_nondep_then
   (#pm: perm)
   (#v: Ghost.erased (t1 & t2))
   requires pts_to_serialized (serialize_nondep_then s1 s2) input #pm v
-  returns res: slice_pair byte
+  returns res: (slice byte & slice byte)
   ensures split_nondep_then_post s1 s2 input pm v res
 {
   pts_to_serialized_ext_trade'
@@ -965,13 +965,13 @@ fn split_nondep_then
     input;
   Trade.trans (pts_to_serialized (serialize_dtuple2 s1 #k2 #(const_fun t2) #(const_fun p2) (const_fun s2)) _ #pm _) _ _;
   let res = split_dtuple2 #t1 #(const_fun t2) s1 j1 #_ #(const_fun p2) (const_fun s2) input;
-  match res { SlicePair input1 input2 -> {
+  match res { Mktuple2 input1 input2 -> {
     unfold (split_dtuple2_post #t1 #(const_fun t2) s1 #k2 #(const_fun p2) (const_fun s2) input pm (dtuple2_of_pair v) res);
     unfold (split_dtuple2_post' #t1 #(const_fun t2) s1 #_ #(const_fun p2) (const_fun s2) input pm (dtuple2_of_pair v) input1 input2);
     Trade.trans (_ ** _) _ _;
     fold (split_nondep_then_post' s1 s2 input pm v input1 input2);
-    fold (split_nondep_then_post s1 s2 input pm v (input1 `SlicePair` input2));
-    (input1 `SlicePair` input2)
+    fold (split_nondep_then_post s1 s2 input pm v (input1, input2));
+    (input1, input2)
   }}
 }
 ```
@@ -996,7 +996,7 @@ fn nondep_then_fst
     trade (pts_to_serialized s1 res #pm (fst v)) (pts_to_serialized (serialize_nondep_then s1 s2) input #pm v)
 {
   let spl = split_nondep_then s1 j1 s2 input;
-  match spl { SlicePair input1 input2 -> {
+  match spl { Mktuple2 input1 input2 -> {
     unfold (split_nondep_then_post s1 s2 input pm v spl);
     unfold (split_nondep_then_post' s1 s2 input pm v input1 input2);
     Trade.elim_hyp_r _ _ _;
@@ -1025,7 +1025,7 @@ fn nondep_then_snd
     trade (pts_to_serialized s2 res #pm (snd v)) (pts_to_serialized (serialize_nondep_then s1 s2) input #pm v)
 {
   let spl = split_nondep_then s1 j1 s2 input;
-  match spl { SlicePair input1 input2 -> {
+  match spl { Mktuple2 input1 input2 -> {
     unfold (split_nondep_then_post s1 s2 input pm v spl);
     unfold (split_nondep_then_post' s1 s2 input pm v input1 input2);
     Trade.elim_hyp_l _ _ _;
@@ -1057,7 +1057,7 @@ fn read_dtuple2
   (f: _)
 {
   let split12 = split_dtuple2 s1 j1 s2 input;
-  match split12 { SlicePair input1 input2 -> {
+  match split12 { Mktuple2 input1 input2 -> {
     unfold (split_dtuple2_post s1 s2 input pm v split12);
     unfold (split_dtuple2_post' s1 s2 input pm v input1 input2);
     let x1 = leaf_reader_of_reader r1 input1;

diff --git a/src/lowparse/pulse/LowParse.Pulse.SeqBytes.fst b/src/lowparse/pulse/LowParse.Pulse.SeqBytes.fst
@@ -63,11 +63,11 @@ fn l2r_write_lseq_bytes_copy
   let length = S.len x'.v;
   let sp1 = S.split out offset;
   match sp1 {
-    SlicePair sp11 sp12 -> {
+    Mktuple2 sp11 sp12 -> {
       with v12 . assert (pts_to sp12 v12);
       let sp2 = S.split sp12 length;
       match sp2 {
-        SlicePair sp21 sp22 -> {
+        Mktuple2 sp21 sp22 -> {
           pts_to_len sp21;
           S.copy sp21 x'.v;
           fold (pts_to_seqbytes n x' x);

diff --git a/src/lowparse/pulse/LowParse.Pulse.VCList.fst b/src/lowparse/pulse/LowParse.Pulse.VCList.fst
@@ -147,9 +147,9 @@ let nlist_hd_tl_post
   (input: slice byte)
   (pm: perm)
   (v: (nlist n t))
-  (hd_tl: (slice_pair byte))
+  (hd_tl: (slice byte & slice byte))
 : slprop
-= nlist_hd_tl_post' s sq n input pm v (hd_tl.fst) (hd_tl.snd)
+= nlist_hd_tl_post' s sq n input pm v (fst hd_tl) (snd hd_tl)
 
 inline_for_extraction
 ```pulse
@@ -166,15 +166,15 @@ fn nlist_hd_tl
   (#v: Ghost.erased (nlist n t))
 requires
   pts_to_serialized (serialize_nlist n s) input #pm v
-returns res : slice_pair byte
+returns res : (slice byte & slice byte)
 ensures
   nlist_hd_tl_post s sq n input pm v res
 {
   nlist_cons_as_nondep_then s n input;
   with v' . assert (pts_to_serialized (serialize_nondep_then s (serialize_nlist (n - 1) s)) input #pm v');
   let res = split_nondep_then #_ #(nlist (n - 1) t) s j #(parse_nlist_kind (n - 1) k) #(coerce_eq () (parse_nlist (n - 1) p)) (coerce_eq () (serialize_nlist (n - 1) s <: serializer (parse_nlist (n - 1) p))) input; // FIXME: same as above
   match res {
-    SlicePair s1 s2 -> {
+    Mktuple2 s1 s2 -> {
       unfold (split_nondep_then_post s (serialize_nlist (n - 1) s) input pm v' res);
       unfold (split_nondep_then_post' s (serialize_nlist (n - 1) s) input pm v' s1 s2);
       Trade.trans _ _ (pts_to_serialized (serialize_nlist n s) input #pm v);
@@ -349,7 +349,7 @@ ensures
   } else {
     let pl = nlist_hd_tl s sq j (SZ.v n) a;
     match pl {
-      SlicePair s1 s2 -> {
+      Mktuple2 s1 s2 -> {
         unfold (nlist_hd_tl_post s sq (SZ.v n) a pm v pl);
         unfold (nlist_hd_tl_post' s sq (SZ.v n) a pm v s1 s2);
         let mut phd = s1;
@@ -382,7 +382,7 @@ ensures
           with tl . assert (pts_to_serialized (serialize_nlist (SZ.v gi) s) stl #pm tl);
           let pl = nlist_hd_tl s sq j (SZ.v gi) stl;
           match pl {
-            SlicePair s1 s2 -> {
+            Mktuple2 s1 s2 -> {
               unfold (nlist_hd_tl_post s sq (SZ.v gi) stl pm tl pl);
               unfold (nlist_hd_tl_post' s sq (SZ.v gi) stl pm tl s1 s2);
               let shd = !phd;