SlicePair -> Mktuple2

project-everest · Oct 30, 2024 · 8fe4970 · 8fe4970
1 parent 94ee2db
commit 8fe4970
Show file tree

Hide file tree

Showing 6 changed files with 8 additions and 8 deletions.
diff --git a/src/cbor/pulse/raw/CBOR.Pulse.Raw.Iterator.fst b/src/cbor/pulse/raw/CBOR.Pulse.Raw.Iterator.fst
@@ -245,7 +245,7 @@ fn slice_split_right (#t: Type0) (s: S.slice t) (#p: perm) (#v: Ghost.erased (Se
 {
   let sp = S.split s i;
   match sp {
-    S.SlicePair s1 s2 -> {
+    Mktuple2 s1 s2 -> {
       with v1 . assert (pts_to s1 #p v1);
       with v2 . assert (pts_to s2 #p v2);
       let sq : squash (Ghost.reveal v == v1 `Seq.append` v2) = Seq.lemma_split v (SZ.v i);

diff --git a/src/cbor/pulse/raw/everparse/CBOR.Pulse.Raw.EverParse.Format.fst b/src/cbor/pulse/raw/everparse/CBOR.Pulse.Raw.EverParse.Format.fst
@@ -755,7 +755,7 @@ fn validate_recursive_step_count_leaf (_: squash SZ.fits_u64) :
     (serialize_dtuple2 serialize_header serialize_leaf_content)
     a;
   let spl = split_dtuple2 serialize_header (jump_header ()) serialize_leaf_content a;
-  match spl { S.SlicePair input1 input2 -> {
+  match spl { Mktuple2 input1 input2 -> {
     unfold (split_dtuple2_post serialize_header serialize_leaf_content a pm va spl);
     unfold (split_dtuple2_post' serialize_header serialize_leaf_content a pm va input1 input2);
     let h = read_header () input1;
@@ -807,7 +807,7 @@ fn jump_recursive_step_count_leaf (_: squash SZ.fits_u64) :
     (serialize_dtuple2 serialize_header serialize_leaf_content)
     a;
   let spl = split_dtuple2 serialize_header (jump_header ()) serialize_leaf_content a;
-  match spl { S.SlicePair input1 input2 -> {
+  match spl { Mktuple2 input1 input2 -> {
     unfold (split_dtuple2_post serialize_header serialize_leaf_content a pm va spl);
     unfold (split_dtuple2_post' serialize_header serialize_leaf_content a pm va input1 input2);
     let h = read_header () input1;
@@ -905,7 +905,7 @@ fn get_header_and_contents
   Trade.trans _ _ (pts_to_serialized serialize_raw_data_item input #pm v);
   with v' . assert (pts_to_serialized (serialize_dtuple2 serialize_header serialize_content) input #pm v');
   let spl = split_dtuple2 serialize_header (jump_header ()) serialize_content input;
-  match spl { S.SlicePair ph outc -> {
+  match spl { Mktuple2 ph outc -> {
     unfold (split_dtuple2_post serialize_header serialize_content input pm v' spl);
     unfold (split_dtuple2_post' serialize_header serialize_content input pm v' ph outc);
     Trade.trans _ _ (pts_to_serialized serialize_raw_data_item input #pm v);

diff --git a/src/cbor/pulse/raw/everparse/CBOR.Pulse.Raw.EverParse.Iterator.fst b/src/cbor/pulse/raw/everparse/CBOR.Pulse.Raw.EverParse.Iterator.fst
@@ -188,7 +188,7 @@ fn cbor_raw_serialized_iterator_next
     s'
     i.s;
   match sp {
-    SlicePair s1 s2 -> {
+    Mktuple2 s1 s2 -> {
       unfold (LPC.split_nondep_then_post s s' i.s pm v' sp);
       unfold (LPC.split_nondep_then_post' s s' i.s pm v' s1 s2);
       Trade.trans _ _ (cbor_raw_serialized_iterator_match s pm i l);

diff --git a/src/cbor/pulse/raw/everparse/CBOR.Pulse.Raw.Format.Parse.fst b/src/cbor/pulse/raw/everparse/CBOR.Pulse.Raw.Format.Parse.fst
@@ -225,7 +225,7 @@ fn cbor_raw_sorted (sq: squash SZ.fits_u64) : LowParse.Pulse.Recursive.impl_pred
   with va' . assert (pts_to_serialized (LowParse.Spec.Combinators.serialize_dtuple2 serialize_header serialize_content) a #pm va');
   let spl = LowParse.Pulse.Combinators.split_dtuple2 serialize_header (jump_header ()) serialize_content a;
   match spl {
-    SlicePair ah ap -> {
+    Mktuple2 ah ap -> {
       unfold (LowParse.Pulse.Combinators.split_dtuple2_post serialize_header serialize_content a pm va' spl);
       unfold (LowParse.Pulse.Combinators.split_dtuple2_post' serialize_header serialize_content a pm va' ah ap);
       Trade.trans _ _ (pts_to_serialized serialize_raw_data_item a #pm va);

diff --git a/src/cbor/pulse/raw/everparse/CBOR.Pulse.Raw.Format.Serialized.fst b/src/cbor/pulse/raw/everparse/CBOR.Pulse.Raw.Format.Serialized.fst
@@ -251,7 +251,7 @@ fn cbor_serialized_map_iterator_next_cont (sq: squash SZ.fits_u64)
     serialize_raw_data_item
     x;
   match sp {
-    SlicePair s1 s2 -> {
+    Mktuple2 s1 s2 -> {
       unfold (LPC.split_nondep_then_post serialize_raw_data_item serialize_raw_data_item x pm v sp);
       unfold (LPC.split_nondep_then_post' serialize_raw_data_item serialize_raw_data_item x pm v s1 s2);
       with v1 . assert (pts_to_serialized serialize_raw_data_item s1 #pm v1);

diff --git a/src/lowparse/pulse/LowParse.Pulse.Recursive.fst b/src/lowparse/pulse/LowParse.Pulse.Recursive.fst
@@ -664,7 +664,7 @@ fn impl_nlist_forall_pred_recursive
         j
         (serialize_nlist_recursive_cons_payload s (SZ.v n))
         pi;
-      match spl { S.SlicePair ph pc -> {
+      match spl { Mktuple2 ph pc -> {
         unfold (C.split_dtuple2_post (serializer_of_tot_serializer s.serialize_header) (serialize_nlist_recursive_cons_payload s (SZ.v n)) pi pm vi spl);
         unfold (C.split_dtuple2_post' (serializer_of_tot_serializer s.serialize_header) (serialize_nlist_recursive_cons_payload s (SZ.v n)) pi pm vi ph pc);
         Trade.trans