Clean up some unused functions.

src/encoding.rs

@@ -27,7 +27,6 @@ pub struct Chunk {
     pub data: [u8; 32],
 }
 
-
 #[hax_lib::attributes]
 pub trait Encoder {
     #[hax_lib::requires(true)]
@@ -35,7 +34,6 @@ pub trait Encoder {
     where
         Self: Sized;
     fn next_chunk(&mut self) -> Chunk;
-    fn data(&self) -> &Vec<u8>;
 }
 
 #[hax_lib::attributes]
@@ -46,8 +44,6 @@ pub trait Decoder {
         Self: Sized;
     fn add_chunk(&mut self, chunk: &Chunk);
     fn decoded_message(&self) -> Option<Vec<u8>>;
-    //fn take_decoded_message(&mut self) -> Option<Vec<u8>>;
-    fn is_complete(&self) -> bool;
 }
 
 // XXX: For ease of formal verification with hax, we avoid using
@@ -73,15 +69,6 @@ impl<T: Encoder> Encoder for Option<T> {
         *self = Some(tmp);
         chunk
     }
-
-    #[hax_lib::requires(self.is_some())]
-    fn data(&self) -> &Vec<u8> {
-        let value = self.as_ref().unwrap();
-        hax_lib::fstar!(
-            "Hax_lib.v_assume (f_data_pre #v_T #FStar.Tactics.Typeclasses.solve value)"
-        );
-        T::data(value)
-    }
 }
 
 #[hax_lib::attributes]
@@ -111,20 +98,4 @@ impl<T: Decoder> Decoder for Option<T> {
         );
         T::decoded_message(value)
     }
-
-    /* fn take_decoded_message(&mut self) -> Option<Vec<u8>> {
-        let mut tmp = self.take().unwrap();
-        let result = T::take_decoded_message(&mut tmp);
-        *self = Some(tmp);
-        result
-    } */
-
-    #[hax_lib::requires(self.is_some())]
-    fn is_complete(&self) -> bool {
-        let value = self.as_ref().unwrap();
-        hax_lib::fstar!(
-            "Hax_lib.v_assume (f_is_complete_pre #v_T #FStar.Tactics.Typeclasses.solve value)"
-        );
-        T::is_complete(value)
-    }
 }

src/encoding/gf.rs

@@ -582,7 +582,6 @@ impl GF16 {
         }
         out
     }
-
 }
 
 #[cfg(test)]
@@ -619,7 +618,7 @@ mod test {
             assert_eq!(a, b);
         }
     }
-    
+
     #[test]
     fn div() {
         let mut rng = rand::rng();

src/encoding/polynomial.rs

@@ -559,7 +559,9 @@ impl PolyEncoder {
         out
     }
 
-    pub(crate) fn from_pb(pb: proto::pq_ratchet::PolynomialEncoder) -> Result<Self, PolynomialError> {
+    pub(crate) fn from_pb(
+        pb: proto::pq_ratchet::PolynomialEncoder,
+    ) -> Result<Self, PolynomialError> {
         let s = if !pb.pts.is_empty() {
             if !pb.polys.is_empty() {
                 return Err(PolynomialError::SerializationInvalid);
@@ -711,11 +713,6 @@ impl Encoder for PolyEncoder {
         self.idx = self.idx.wrapping_add(1);
         out
     }
-
-    #[hax_lib::requires(false)]
-    fn data(&self) -> &Vec<u8> {
-        todo!()
-    }
 }
 
 #[derive(Clone)]
@@ -789,7 +786,9 @@ impl PolyDecoder {
         out
     }
 
-    pub(crate) fn from_pb(pb: proto::pq_ratchet::PolynomialDecoder) -> Result<Self, PolynomialError> {
+    pub(crate) fn from_pb(
+        pb: proto::pq_ratchet::PolynomialDecoder,
+    ) -> Result<Self, PolynomialError> {
         if pb.pts.len() != 16 {
             return Err(PolynomialError::SerializationInvalid);
         }
@@ -906,10 +905,6 @@ impl Decoder for PolyDecoder {
         }
         Some(out)
     }
-
-    fn is_complete(&self) -> bool {
-        self.is_complete
-    }
 }
 
 #[cfg(test)]

src/encoding/round_robin.rs

@@ -39,10 +39,6 @@ impl Encoder for RoundRobinEncoder {
         self.next_idx += 1;
         self.chunk_at(index)
     }
-
-    fn data(&self) -> &Vec<u8> {
-        &self.data
-    }
 }
 
 type ChunkData = [u8; 32];
@@ -92,16 +88,4 @@ impl Decoder for RoundRobinDecoder {
             None
         }
     }
-
-    /* fn take_decoded_message(&mut self) -> Option<Vec<u8>> {
-        let data = self.decoded_message();
-        if data.is_some() {
-            self.is_complete = true;
-        }
-        data
-    } */
-
-    fn is_complete(&self) -> bool {
-        self.is_complete
-    }
 }