IMPL6.md (1582B)
1 # IMPL6: Add property-based tests 2 3 ## Goal 4 Add a small set of QuickCheck properties to complement spec vectors and 5 negative tests. 6 7 ## Constraints 8 - Use tasty-quickcheck only in the test suite. 9 - Keep generators small and deterministic enough for CI. 10 - No new dependencies beyond QuickCheck (already permitted for tests). 11 12 ## Properties 13 1) Handshake round-trip: 14 - For random static keys and fixed entropy for ephemeral keys, 15 a full handshake succeeds and the derived sessions are consistent: 16 initiator send key == responder recv key, and vice versa. 17 2) Encrypt/decrypt round-trip: 18 - For random payloads of size 0..256 bytes, encrypt then decrypt 19 yields the original payload and advances sessions. 20 3) Framing: 21 - For random payloads, decrypt_frame consumes exactly one frame and 22 returns the remainder when concatenated with a second frame. 23 - decrypt_frame_partial returns NeedMore when given a prefix shorter 24 than 18 bytes, and FrameOk when given a full frame. 25 26 ## Implementation notes 27 - Add small helpers to generate valid Sec/Pub pairs from 32-byte 28 entropy (filter invalid scalars). 29 - Use fixed ephemeral entropy in properties for determinism, or 30 generate both static and ephemeral keys while rejecting invalid input. 31 - Add QuickCheck size limits to keep runtime fast. 32 33 ## Steps 34 1) Add tasty-quickcheck dependency to test-suite if not already present. 35 2) Implement generators for 32-byte entropy and payload ByteStrings. 36 3) Add property tests to `test/Main.hs` under a new test group. 37 4) Run `cabal test` to confirm runtime and determinism.