call a perm lemma

project-everest · Feb 1, 2025 · b56c7e0 · b56c7e0
1 parent e5f644a
commit b56c7e0
Showing 1 changed file with 1 addition and 0 deletions.
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
@@ -363,6 +363,7 @@ fn cbor_raw_serialized_iterator_share
 {
   unfold (cbor_raw_serialized_iterator_match s pm c l);
   LP.pts_to_serialized_share (LP.serialize_nlist (c.glen) s) c.s;
+  half_mul_l pm c.p;
   fold (cbor_raw_serialized_iterator_match s (pm /. 2.0R) c l);
   fold (cbor_raw_serialized_iterator_match s (pm /. 2.0R) c l);
 }