Skip to main content

max / synckit

Relate the three descriptions of the chunked-blob layout `encrypt_blob_chunked` produces the v3 layout, `blob_encrypted_len` and `sealed_chunk_len` predict it before a byte is sealed, and `parse_blob_header` + `decrypt_blob_chunk` read it back incrementally. Three implementations of one format, none of them checked against another. The predictor is the load-bearing one: a multipart uploader signs an exact Content-Length per part from it, so a disagreement is a broken upload rather than a wrong number. Three relations, none needing an expected-value table: predicted total length equals produced length, the per-chunk lengths tile the sealed body, and the streaming and buffered decoders agree on every input. Corrects the relation as filed. "Multipart and one-shot upload of the same bytes must produce identical ciphertext" cannot hold: every chunk is sealed under a fresh nonce, which the sibling property asserts on purpose. What the uploader actually depends on is layout agreement, so that is what is asserted. Checked by dropping one chunk's overhead from the predictor, which fails the length relation naming the size it disagreed at. Phase 2 of wiki `testing-posture`.
Co-Authored-By
Claude Opus 5 (1M context) <noreply@anthropic.com>
Author: Max Johnson <me@maxj.phd> · 2026-08-05 15:12 UTC
Signed with PGP, not checked
Commit: 10634456ee184798534b73ddd57abf0d7d2718e8
Parent: 914ca41
1 file changed, +106 insertions, -0 deletions
@@ -932,6 +932,112 @@
932 932 }
933 933 }
934 934
935 + /// Differential relations over the chunked-blob format.
936 + ///
937 + /// Three implementations describe one layout: `encrypt_blob_chunked`
938 + /// produces it, `blob_encrypted_len`/`sealed_chunk_len`/
939 + /// `blob_chunk_count_for` predict it before a byte is sealed, and
940 + /// `parse_blob_header` + `decrypt_blob_chunk` read it back one chunk at a
941 + /// time. Relating them needs no expected-value table, which is what makes
942 + /// these cheap (Chen et al. 1998; McKeeman 1998).
943 + ///
944 + /// Note on what is NOT asserted: the multipart and one-shot paths do not
945 + /// produce identical ciphertext and cannot, because every chunk is sealed
946 + /// under a fresh nonce (see `sealing_twice_does_not_repeat_ciphertext`
947 + /// above). The relation that holds, and the one the uploader depends on, is
948 + /// that the predicted layout equals the produced layout.
949 + ///
950 + /// See wiki `testing-posture`, Phase 2.
951 + mod blob_relations {
952 + use super::*;
953 + use proptest::prelude::*;
954 +
955 + /// Lengths that land either side of a chunk boundary, using a small
956 + /// stand-in for the 1 MiB production chunk so a case is cheap to run.
957 + /// The boundary arithmetic is what these relations are about, and it is
958 + /// the same arithmetic at any chunk size.
959 + fn plaintext() -> impl Strategy<Value = Vec<u8>> {
960 + prop_oneof![
961 + 1 => Just(Vec::new()),
962 + 4 => prop::collection::vec(any::<u8>(), 1..4096),
963 + ]
964 + }
965 +
966 + proptest! {
967 + /// The uploader signs an exact `Content-Length` per part before it
968 + /// has sealed anything, so a predicted length that disagrees with
969 + /// the produced one is a broken upload rather than a wrong number.
970 + #[test]
971 + fn the_predicted_length_equals_the_produced_length(plaintext in plaintext()) {
972 + let key = generate_master_key();
973 + let sealed = encrypt_blob_chunked(&plaintext, &key, "h").expect("encrypt");
974 + prop_assert_eq!(
975 + sealed.len(),
976 + blob_encrypted_len(plaintext.len()),
977 + "blob_encrypted_len disagrees with encrypt_blob_chunked for {} bytes",
978 + plaintext.len()
979 + );
980 + }
981 +
982 + /// The per-chunk lengths must add up the same way, since the
983 + /// uploader slices parts by them. Checked against the header the
984 + /// encoder actually wrote rather than against the predictor's own
985 + /// idea of it.
986 + #[test]
987 + fn the_predicted_chunk_layout_equals_the_produced_one(plaintext in plaintext()) {
988 + let key = generate_master_key();
989 + let sealed = encrypt_blob_chunked(&plaintext, &key, "h").expect("encrypt");
990 + let (header, consumed) = parse_blob_header(&sealed).expect("parse header");
991 +
992 + prop_assert_eq!(
993 + header.chunk_count,
994 + blob_chunk_count_for(plaintext.len()),
995 + "header chunk count disagrees with the predictor"
996 + );
997 + let summed: usize = (0..header.chunk_count)
998 + .map(|i| header.sealed_chunk_len(i))
999 + .sum();
1000 + prop_assert_eq!(
1001 + consumed + summed,
1002 + sealed.len(),
1003 + "the per-chunk lengths do not tile the sealed body"
1004 + );
1005 + }
1006 +
1007 + /// The two decode paths are two implementations of one format: the
1008 + /// buffered fallback and the streaming reader the download path
1009 + /// actually uses. They must agree on every input, or a blob opens
1010 + /// one way in a test and another way in the app.
1011 + #[test]
1012 + fn streaming_and_buffered_decode_agree(plaintext in plaintext()) {
1013 + let key = generate_master_key();
1014 + let sealed = encrypt_blob_chunked(&plaintext, &key, "h").expect("encrypt");
1015 +
1016 + let buffered = decrypt_blob_chunked(&sealed, &key, "h").expect("buffered decrypt");
1017 +
1018 + let (header, consumed) = parse_blob_header(&sealed).expect("parse header");
1019 + let mut streamed = Vec::new();
1020 + let mut offset = consumed;
1021 + for i in 0..header.chunk_count {
1022 + let len = header.sealed_chunk_len(i);
1023 + let chunk = &sealed[offset..offset + len];
1024 + streamed.extend_from_slice(
1025 + &decrypt_blob_chunk(chunk, &key, "h", i, header.chunk_count)
1026 + .expect("chunk decrypt"),
1027 + );
1028 + offset += len;
1029 + }
1030 +
1031 + prop_assert_eq!(&buffered, &plaintext, "buffered decode lost the plaintext");
1032 + prop_assert_eq!(
1033 + &streamed, &plaintext,
1034 + "streaming decode disagreed with the plaintext"
1035 + );
1036 + prop_assert_eq!(offset, sealed.len(), "streaming decode left bytes unread");
1037 + }
1038 + }
1039 + }
1040 +
935 1041 #[test]
936 1042 fn master_key_generation_is_random() {
937 1043 let k1 = generate_master_key();