From 8fe4970f5f3cef84231768aa6f5acbb38796d663 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Tue, 29 Oct 2024 17:26:55 -0700 Subject: [PATCH] SlicePair -> Mktuple2 --- src/cbor/pulse/raw/CBOR.Pulse.Raw.Iterator.fst | 2 +- .../pulse/raw/everparse/CBOR.Pulse.Raw.EverParse.Format.fst | 6 +++--- .../raw/everparse/CBOR.Pulse.Raw.EverParse.Iterator.fst | 2 +- .../pulse/raw/everparse/CBOR.Pulse.Raw.Format.Parse.fst | 2 +- .../raw/everparse/CBOR.Pulse.Raw.Format.Serialized.fst | 2 +- src/lowparse/pulse/LowParse.Pulse.Recursive.fst | 2 +- 6 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/cbor/pulse/raw/CBOR.Pulse.Raw.Iterator.fst b/src/cbor/pulse/raw/CBOR.Pulse.Raw.Iterator.fst index 361d6f3d..4c30ee29 100644 --- 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 index a49bef6f..83931aae 100644 --- 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 index 4ac826f4..eb342578 100644 --- 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 index dcb9a899..9aa17825 100644 --- 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 index 47a63478..67a45939 100644 --- 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 index ccaf6cf8..45abdc53 100644 --- 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