@@ -627,6 +627,328 @@ impl CursorOp {
627627 }
628628}
629629
630+ // ---------------------------------------------------------------------------
631+ // Stateful version of the same cursor PBT.
632+ // ---------------------------------------------------------------------------
633+
634+ struct CursorStatefulTest < ' a > {
635+ buf_list_cursor : crate :: Cursor < & ' a BufList > ,
636+ oracle_cursor : io:: Cursor < & ' a [ u8 ] > ,
637+ num_bytes : usize ,
638+ }
639+
640+ #[ hegel:: state_machine]
641+ impl CursorStatefulTest < ' _ > {
642+ // -- Position / seek rules -----------------------------------------------
643+
644+ #[ rule]
645+ fn set_position ( & mut self , tc : hegel:: TestCase ) {
646+ // Allow going past the end of the list a bit.
647+ let pos = tc. draw ( generators:: integers :: < usize > ( ) . max_value ( self . num_bytes * 5 / 4 ) ) as u64 ;
648+ self . buf_list_cursor . set_position ( pos) ;
649+ self . oracle_cursor . set_position ( pos) ;
650+ }
651+
652+ #[ rule]
653+ fn seek_start ( & mut self , tc : hegel:: TestCase ) {
654+ let pos = tc. draw ( generators:: integers :: < usize > ( ) . max_value ( self . num_bytes * 5 / 4 ) ) as u64 ;
655+ let style = SeekFrom :: Start ( pos) ;
656+ CursorOp :: assert_io_result_eq (
657+ self . buf_list_cursor . seek ( style) ,
658+ self . oracle_cursor . seek ( style) ,
659+ )
660+ . unwrap ( ) ;
661+ }
662+
663+ #[ rule]
664+ fn seek_end ( & mut self , tc : hegel:: TestCase ) {
665+ // Allow going past the beginning and end of the list a bit.
666+ let raw = tc. draw ( generators:: integers :: < usize > ( ) . max_value ( self . num_bytes * 3 / 2 ) ) ;
667+ let offset = raw as i64 - ( 1 + self . num_bytes * 5 / 4 ) as i64 ;
668+ let style = SeekFrom :: End ( offset) ;
669+ CursorOp :: assert_io_result_eq (
670+ self . buf_list_cursor . seek ( style) ,
671+ self . oracle_cursor . seek ( style) ,
672+ )
673+ . unwrap ( ) ;
674+ }
675+
676+ #[ rule]
677+ fn seek_current ( & mut self , tc : hegel:: TestCase ) {
678+ let raw = tc. draw ( generators:: integers :: < usize > ( ) . max_value ( self . num_bytes * 3 / 2 ) ) ;
679+ // Center the index at roughly 0.
680+ let offset = raw as i64 - ( self . num_bytes * 3 / 4 ) as i64 ;
681+ let style = SeekFrom :: Current ( offset) ;
682+ CursorOp :: assert_io_result_eq (
683+ self . buf_list_cursor . seek ( style) ,
684+ self . oracle_cursor . seek ( style) ,
685+ )
686+ . unwrap ( ) ;
687+ }
688+
689+ // -- Read rules ----------------------------------------------------------
690+
691+ #[ rule]
692+ fn read ( & mut self , tc : hegel:: TestCase ) {
693+ let buf_size = tc. draw ( generators:: integers :: < usize > ( ) . max_value ( self . num_bytes * 5 / 4 ) ) ;
694+ let mut bl_buf = vec ! [ 0u8 ; buf_size] ;
695+ let mut o_buf = vec ! [ 0u8 ; buf_size] ;
696+ CursorOp :: assert_io_result_eq (
697+ self . buf_list_cursor . read ( & mut bl_buf) ,
698+ self . oracle_cursor . read ( & mut o_buf) ,
699+ )
700+ . unwrap ( ) ;
701+ assert_eq ! ( bl_buf, o_buf, "read buffer mismatch" ) ;
702+ }
703+
704+ #[ rule]
705+ fn read_vectored ( & mut self , tc : hegel:: TestCase ) {
706+ let n_bufs = tc. draw ( generators:: integers :: < usize > ( ) . max_value ( 7 ) ) ;
707+ let mut bl_vecs: Vec < Vec < u8 > > = ( 0 ..n_bufs)
708+ . map ( |_| vec ! [ 0u8 ; tc. draw( generators:: integers:: <usize >( ) . max_value( self . num_bytes) ) ] )
709+ . collect ( ) ;
710+ let mut o_vecs = bl_vecs. clone ( ) ;
711+
712+ let mut bl_slices: Vec < _ > = bl_vecs. iter_mut ( ) . map ( |v| IoSliceMut :: new ( v) ) . collect ( ) ;
713+ let mut o_slices: Vec < _ > = o_vecs. iter_mut ( ) . map ( |v| IoSliceMut :: new ( v) ) . collect ( ) ;
714+
715+ CursorOp :: assert_io_result_eq (
716+ self . buf_list_cursor . read_vectored ( & mut bl_slices) ,
717+ self . oracle_cursor . read_vectored ( & mut o_slices) ,
718+ )
719+ . unwrap ( ) ;
720+ assert_eq ! ( bl_vecs, o_vecs, "read_vectored buffer mismatch" ) ;
721+ }
722+
723+ #[ rule]
724+ fn read_exact ( & mut self , tc : hegel:: TestCase ) {
725+ let buf_size = tc. draw ( generators:: integers :: < usize > ( ) . max_value ( self . num_bytes * 5 / 4 ) ) ;
726+ let mut bl_buf = vec ! [ 0u8 ; buf_size] ;
727+ let mut o_buf = vec ! [ 0u8 ; buf_size] ;
728+ CursorOp :: assert_io_result_eq (
729+ self . buf_list_cursor . read_exact ( & mut bl_buf) ,
730+ self . oracle_cursor . read_exact ( & mut o_buf) ,
731+ )
732+ . unwrap ( ) ;
733+ assert_eq ! ( bl_buf, o_buf, "read_exact buffer mismatch" ) ;
734+ }
735+
736+ #[ rule]
737+ fn consume ( & mut self , tc : hegel:: TestCase ) {
738+ let amt = tc. draw ( generators:: integers :: < usize > ( ) . max_value ( self . num_bytes * 5 / 4 ) ) ;
739+ self . buf_list_cursor . consume ( amt) ;
740+ self . oracle_cursor . consume ( amt) ;
741+ }
742+
743+ // -- Buf trait rules -----------------------------------------------------
744+
745+ #[ rule]
746+ fn buf_chunk ( & mut self , _: hegel:: TestCase ) {
747+ let bl_chunk = self . buf_list_cursor . chunk ( ) ;
748+ let o_chunk = self . oracle_cursor . chunk ( ) ;
749+ // BufList returns one segment at a time while oracle returns the entire
750+ // remaining buffer. Verify emptiness matches and that buf_list's chunk
751+ // is a prefix of oracle's.
752+ assert_eq ! (
753+ bl_chunk. is_empty( ) ,
754+ o_chunk. is_empty( ) ,
755+ "chunk emptiness mismatch"
756+ ) ;
757+ if !bl_chunk. is_empty ( ) {
758+ assert ! (
759+ o_chunk. starts_with( bl_chunk) ,
760+ "buf_list chunk is not a prefix of oracle chunk"
761+ ) ;
762+ }
763+ }
764+
765+ #[ rule]
766+ fn buf_advance ( & mut self , tc : hegel:: TestCase ) {
767+ let amt = tc. draw ( generators:: integers :: < usize > ( ) . max_value ( self . num_bytes * 5 / 4 ) ) ;
768+ // Skip if already past the end, as the oracle's Buf impl has a debug
769+ // assertion that checks position even when advancing by 0.
770+ if self . buf_list_cursor . remaining ( ) > 0 || amt == 0 && self . oracle_cursor . remaining ( ) > 0 {
771+ let amt = amt. min ( self . buf_list_cursor . remaining ( ) ) ;
772+ self . buf_list_cursor . advance ( amt) ;
773+ self . oracle_cursor . advance ( amt) ;
774+ }
775+ }
776+
777+ #[ rule]
778+ fn buf_chunks_vectored ( & mut self , tc : hegel:: TestCase ) {
779+ let num_iovs = tc. draw ( generators:: integers :: < usize > ( ) . max_value ( self . num_bytes ) ) ;
780+ let remaining = self . buf_list_cursor . remaining ( ) ;
781+ assert_eq ! (
782+ remaining,
783+ self . oracle_cursor. remaining( ) ,
784+ "remaining mismatch before chunks_vectored"
785+ ) ;
786+
787+ let mut bl_iovs = vec ! [ io:: IoSlice :: new( & [ ] ) ; num_iovs] ;
788+ let mut o_iovs = vec ! [ io:: IoSlice :: new( & [ ] ) ; num_iovs] ;
789+ let bl_filled = self . buf_list_cursor . chunks_vectored ( & mut bl_iovs) ;
790+ let o_filled = self . oracle_cursor . chunks_vectored ( & mut o_iovs) ;
791+
792+ let bl_bytes: Vec < u8 > = bl_iovs[ ..bl_filled]
793+ . iter ( )
794+ . flat_map ( |iov| iov. as_ref ( ) . iter ( ) . copied ( ) )
795+ . collect ( ) ;
796+ let o_bytes: Vec < u8 > = o_iovs[ ..o_filled]
797+ . iter ( )
798+ . flat_map ( |iov| iov. as_ref ( ) . iter ( ) . copied ( ) )
799+ . collect ( ) ;
800+
801+ if remaining > 0 && num_iovs > 0 {
802+ assert ! (
803+ !bl_bytes. is_empty( ) ,
804+ "should return data when remaining > 0"
805+ ) ;
806+ assert ! (
807+ !o_bytes. is_empty( ) ,
808+ "oracle should return data when remaining > 0"
809+ ) ;
810+ assert ! (
811+ o_bytes. starts_with( & bl_bytes) ,
812+ "buf_list data should match beginning of oracle data"
813+ ) ;
814+ for ( i, iov) in bl_iovs[ ..bl_filled] . iter ( ) . enumerate ( ) {
815+ assert ! (
816+ !iov. is_empty( ) ,
817+ "buf_list iov at index {i} should be non-empty"
818+ ) ;
819+ }
820+ } else if remaining == 0 {
821+ assert ! (
822+ bl_bytes. is_empty( ) && o_bytes. is_empty( ) ,
823+ "should return no data when remaining == 0"
824+ ) ;
825+ }
826+ }
827+
828+ #[ rule]
829+ fn buf_copy_to_bytes ( & mut self , tc : hegel:: TestCase ) {
830+ let len = tc. draw ( generators:: integers :: < usize > ( ) . max_value ( self . num_bytes * 5 / 4 ) ) ;
831+ // copy_to_bytes panics if len > remaining, so guard.
832+ if len <= self . buf_list_cursor . remaining ( ) && len <= self . oracle_cursor . remaining ( ) {
833+ let bl_bytes = self . buf_list_cursor . copy_to_bytes ( len) ;
834+ let o_bytes = self . oracle_cursor . copy_to_bytes ( len) ;
835+ assert_eq ! ( bl_bytes, o_bytes, "copy_to_bytes mismatch" ) ;
836+ }
837+ }
838+
839+ #[ rule]
840+ fn buf_get_u8 ( & mut self , _: hegel:: TestCase ) {
841+ if self . buf_list_cursor . remaining ( ) >= 1 && self . oracle_cursor . remaining ( ) >= 1 {
842+ assert_eq ! (
843+ self . buf_list_cursor. get_u8( ) ,
844+ self . oracle_cursor. get_u8( ) ,
845+ "get_u8 mismatch"
846+ ) ;
847+ }
848+ }
849+
850+ #[ rule]
851+ fn buf_get_u64 ( & mut self , _: hegel:: TestCase ) {
852+ if self . buf_list_cursor . remaining ( ) >= 8 && self . oracle_cursor . remaining ( ) >= 8 {
853+ assert_eq ! (
854+ self . buf_list_cursor. get_u64( ) ,
855+ self . oracle_cursor. get_u64( ) ,
856+ "get_u64 mismatch"
857+ ) ;
858+ }
859+ }
860+
861+ #[ rule]
862+ fn buf_get_u64_le ( & mut self , _: hegel:: TestCase ) {
863+ if self . buf_list_cursor . remaining ( ) >= 8 && self . oracle_cursor . remaining ( ) >= 8 {
864+ assert_eq ! (
865+ self . buf_list_cursor. get_u64_le( ) ,
866+ self . oracle_cursor. get_u64_le( ) ,
867+ "get_u64_le mismatch"
868+ ) ;
869+ }
870+ }
871+
872+ // NOTE: poll_read is not included here because #[cfg(feature = "tokio1")]
873+ // on a #[rule] doesn't work: the state_machine macro collects rule names
874+ // before #[cfg] filtering, so the generated StateMachine impl references
875+ // Self::poll_read unconditionally. When tokio1 is off, the method doesn't
876+ // exist and compilation fails. This is a Hegel limitation; the macro would
877+ // need to propagate #[cfg] attributes into the generated rules() vec.
878+ // The non-stateful PBT above still covers poll_read.
879+
880+ // -- Invariant -----------------------------------------------------------
881+
882+ #[ invariant]
883+ fn cursors_agree ( & mut self , _: hegel:: TestCase ) {
884+ assert_eq ! (
885+ self . buf_list_cursor. remaining( ) ,
886+ self . oracle_cursor. remaining( ) ,
887+ "remaining mismatch"
888+ ) ;
889+ assert_eq ! (
890+ self . buf_list_cursor. has_remaining( ) ,
891+ self . oracle_cursor. has_remaining( ) ,
892+ "has_remaining mismatch"
893+ ) ;
894+
895+ let bl_position = self . buf_list_cursor . position ( ) ;
896+ assert_eq ! (
897+ bl_position,
898+ self . oracle_cursor. position( ) ,
899+ "position mismatch"
900+ ) ;
901+ CursorOp :: assert_io_result_eq (
902+ self . buf_list_cursor . stream_position ( ) ,
903+ self . oracle_cursor . stream_position ( ) ,
904+ )
905+ . unwrap ( ) ;
906+
907+ // fill_buf returns an empty slice iff we're at or past the end.
908+ let fill_buf = self
909+ . buf_list_cursor
910+ . fill_buf ( )
911+ . expect ( "fill_buf never errors" ) ;
912+ if bl_position < self . num_bytes as u64 {
913+ assert ! (
914+ !fill_buf. is_empty( ) ,
915+ "fill_buf cannot be empty since position {} < num_bytes {}" ,
916+ bl_position,
917+ self . num_bytes,
918+ ) ;
919+ } else {
920+ assert ! (
921+ fill_buf. is_empty( ) ,
922+ "fill_buf must be empty since position {} >= num_bytes {}" ,
923+ bl_position,
924+ self . num_bytes,
925+ ) ;
926+ }
927+
928+ self . buf_list_cursor
929+ . assert_invariants ( )
930+ . expect ( "internal invariants violated" ) ;
931+ }
932+ }
933+
934+ /// Assert that buf_list's cursor behaves identically to std::io::Cursor
935+ /// (stateful version).
936+ #[ hegel:: test( test_cases = 200 ) ]
937+ fn hegel_cursor_stateful ( tc : hegel:: TestCase ) {
938+ let buf_list = tc. draw ( buf_lists ( ) ) ;
939+ let num_bytes = buf_list. num_bytes ( ) ;
940+ let oracle_data: Vec < u8 > = buf_list
941+ . clone ( )
942+ . copy_to_bytes ( buf_list. remaining ( ) )
943+ . to_vec ( ) ;
944+ let m = CursorStatefulTest {
945+ buf_list_cursor : crate :: Cursor :: new ( & buf_list) ,
946+ oracle_cursor : io:: Cursor :: new ( & oracle_data) ,
947+ num_bytes,
948+ } ;
949+ hegel:: stateful:: run ( m, tc) ;
950+ }
951+
630952#[ test]
631953fn test_cursor_buf_trait ( ) {
632954 // Create a BufList with multiple chunks
0 commit comments