wire_test.cpp
1 // Cornell Wire Format Tests 2 // Property tests validating C++ implementation against Lean4 specification 3 // 4 // These tests are generated from Cornell/Extract.lean and verify: 5 // 1. Roundtrip: parse(serialize(x)) == x 6 // 2. Consumption: parse(serialize(x) ++ extra) leaves extra untouched 7 // 3. Constants: Magic numbers match Lean definitions 8 9 #include "cornell/wire.hpp" 10 #include <cassert> 11 #include <cstdio> 12 #include <cstdlib> 13 14 using namespace cornell; 15 16 // ═══════════════════════════════════════════════════════════════════════════════ 17 // Test Helpers 18 // ═══════════════════════════════════════════════════════════════════════════════ 19 20 #define TEST(name) void test_##name() 21 #define RUN_TEST(name) do { \ 22 printf(" %s...", #name); \ 23 test_##name(); \ 24 printf(" OK\n"); \ 25 } while(0) 26 27 // ═══════════════════════════════════════════════════════════════════════════════ 28 // Primitive Roundtrip Tests 29 // PROOF: Cornell.u8.roundtrip, Cornell.u64le.roundtrip, etc. 30 // ═══════════════════════════════════════════════════════════════════════════════ 31 32 TEST(u8_roundtrip) { 33 for (uint8_t v = 0; v < 255; ++v) { 34 Bytes buf; 35 serialize_u8(v, buf); 36 auto r = parse_u8(ByteSpan(buf)); 37 assert(r.has_value()); 38 assert(r->value == v); 39 assert(r->remaining.empty()); 40 } 41 } 42 43 TEST(u64le_roundtrip) { 44 uint64_t test_values[] = { 45 0, 1, 255, 256, 65535, 65536, 46 0xFFFFFFFF, 0x100000000ULL, 47 0xFFFFFFFFFFFFFFFFULL, 48 WORKER_MAGIC_1, 49 WORKER_MAGIC_2, 50 0x126, // Protocol 1.38 51 }; 52 53 for (uint64_t v : test_values) { 54 Bytes buf; 55 serialize_u64le(v, buf); 56 assert(buf.size() == 8); 57 58 auto r = parse_u64le(ByteSpan(buf)); 59 assert(r.has_value()); 60 assert(r->value == v); 61 assert(r->remaining.empty()); 62 } 63 } 64 65 TEST(bool64_roundtrip) { 66 for (bool b : {false, true}) { 67 Bytes buf; 68 serialize_bool64(b, buf); 69 assert(buf.size() == 8); 70 71 auto r = parse_bool64(ByteSpan(buf)); 72 assert(r.has_value()); 73 assert(r->value == b); 74 assert(r->remaining.empty()); 75 } 76 } 77 78 // ═══════════════════════════════════════════════════════════════════════════════ 79 // Consumption Tests 80 // PROOF: Cornell.u64le.consumption, Cornell.Nix.nixString.consumption 81 // ═══════════════════════════════════════════════════════════════════════════════ 82 83 TEST(u64le_consumption) { 84 // Serialize a value, append extra bytes, verify they're left untouched 85 Bytes buf; 86 serialize_u64le(0x12345678, buf); 87 buf.push_back(0xAA); 88 buf.push_back(0xBB); 89 buf.push_back(0xCC); 90 91 auto r = parse_u64le(ByteSpan(buf)); 92 assert(r.has_value()); 93 assert(r->value == 0x12345678); 94 assert(r->remaining.size() == 3); 95 assert(r->remaining[0] == 0xAA); 96 assert(r->remaining[1] == 0xBB); 97 assert(r->remaining[2] == 0xCC); 98 } 99 100 // ═══════════════════════════════════════════════════════════════════════════════ 101 // Nix String Tests 102 // PROOF: Cornell.Nix.nixString.roundtrip, Cornell.Nix.nixString.consumption 103 // ═══════════════════════════════════════════════════════════════════════════════ 104 105 TEST(nix_string_roundtrip) { 106 std::string test_strings[] = { 107 "", 108 "a", 109 "hello", 110 "1234567", // 7 bytes -> 1 byte padding 111 "12345678", // 8 bytes -> 0 byte padding 112 "/nix/store/abc123-hello", 113 "/nix/store/03r3ipfa69l8nla101khyw3g67j24357-bash-5.3p9.drv", 114 }; 115 116 for (const auto& s : test_strings) { 117 Bytes buf; 118 serialize_nix_string(s, buf); 119 120 // Check size: 8 (length) + len + padding 121 size_t expected = 8 + s.size() + pad_size(s.size()); 122 assert(buf.size() == expected); 123 124 auto r = parse_nix_string(ByteSpan(buf)); 125 assert(r.has_value()); 126 assert(r->value == s); 127 assert(r->remaining.empty()); 128 } 129 } 130 131 TEST(nix_string_consumption) { 132 Bytes buf; 133 serialize_nix_string("hello", buf); 134 buf.push_back(0xFF); 135 buf.push_back(0xFE); 136 137 auto r = parse_nix_string(ByteSpan(buf)); 138 assert(r.has_value()); 139 assert(r->value == "hello"); 140 assert(r->remaining.size() == 2); 141 assert(r->remaining[0] == 0xFF); 142 assert(r->remaining[1] == 0xFE); 143 } 144 145 // ═══════════════════════════════════════════════════════════════════════════════ 146 // Protocol Constants Tests 147 // PROOF: Cornell.Nix.WORKER_MAGIC_1, etc. 148 // ═══════════════════════════════════════════════════════════════════════════════ 149 150 TEST(protocol_constants) { 151 // Test WORKER_MAGIC_1: "cxin" in little-endian 152 { 153 uint8_t magic1_bytes[] = {0x63, 0x78, 0x69, 0x6e, 0x00, 0x00, 0x00, 0x00}; 154 auto r = parse_u64le(ByteSpan(magic1_bytes, 8)); 155 assert(r.has_value()); 156 assert(r->value == WORKER_MAGIC_1); 157 } 158 159 // Test WORKER_MAGIC_2: "oixd" in little-endian 160 { 161 uint8_t magic2_bytes[] = {0x6f, 0x69, 0x78, 0x64, 0x00, 0x00, 0x00, 0x00}; 162 auto r = parse_u64le(ByteSpan(magic2_bytes, 8)); 163 assert(r.has_value()); 164 assert(r->value == WORKER_MAGIC_2); 165 } 166 } 167 168 // ═══════════════════════════════════════════════════════════════════════════════ 169 // List Tests 170 // PROOF: Cornell.parseList, Cornell.serializeList 171 // ═══════════════════════════════════════════════════════════════════════════════ 172 173 TEST(string_list_roundtrip) { 174 std::vector<std::string> test_lists[] = { 175 {}, 176 {"hello"}, 177 {"a", "bb", "ccc"}, 178 {"/nix/store/abc", "/nix/store/def", "/nix/store/ghi"}, 179 }; 180 181 for (const auto& list : test_lists) { 182 Bytes buf; 183 serialize_string_list(list, buf); 184 185 auto r = parse_string_list(ByteSpan(buf)); 186 assert(r.has_value()); 187 assert(r->value.size() == list.size()); 188 for (size_t i = 0; i < list.size(); ++i) { 189 assert(r->value[i] == list[i]); 190 } 191 assert(r->remaining.empty()); 192 } 193 } 194 195 // ═══════════════════════════════════════════════════════════════════════════════ 196 // Binary Capture Tests 197 // Validates against actual Nix daemon protocol captures 198 // ═══════════════════════════════════════════════════════════════════════════════ 199 200 TEST(client_hello_capture) { 201 // From captures/client_hello.bin: 202 // 63 78 69 6e 00 00 00 00 26 01 00 00 00 00 00 00 203 uint8_t data[] = { 204 0x63, 0x78, 0x69, 0x6e, 0x00, 0x00, 0x00, 0x00, // magic1 205 0x26, 0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, // version 1.38 206 }; 207 208 ByteSpan bs(data, sizeof(data)); 209 210 // Parse magic 211 auto magic = parse_u64le(bs); 212 assert(magic.has_value()); 213 assert(magic->value == WORKER_MAGIC_1); 214 215 // Parse version 216 auto version = parse_u64le(magic->remaining); 217 assert(version.has_value()); 218 assert(version->value == 0x126); // 1.38 219 assert(version->remaining.empty()); 220 } 221 222 TEST(isvalidpath_request_capture) { 223 // From captures/isvalidpath_request.bin (minus op code): 224 // 3a 00 00 00 00 00 00 00 = length 58 225 // /nix/store/03r3ipfa69l8nla101khyw3g67j24357-bash-5.3p9.drv 226 // + 6 bytes padding 227 uint8_t data[] = { 228 0x3a, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 229 0x2f, 0x6e, 0x69, 0x78, 0x2f, 0x73, 0x74, 0x6f, 230 0x72, 0x65, 0x2f, 0x30, 0x33, 0x72, 0x33, 0x69, 231 0x70, 0x66, 0x61, 0x36, 0x39, 0x6c, 0x38, 0x6e, 232 0x6c, 0x61, 0x31, 0x30, 0x31, 0x6b, 0x68, 0x79, 233 0x77, 0x33, 0x67, 0x36, 0x37, 0x6a, 0x32, 0x34, 234 0x33, 0x35, 0x37, 0x2d, 0x62, 0x61, 0x73, 0x68, 235 0x2d, 0x35, 0x2e, 0x33, 0x70, 0x39, 0x2e, 0x64, 236 0x72, 0x76, 237 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, // padding 238 }; 239 240 auto r = parse_nix_string(ByteSpan(data, sizeof(data))); 241 assert(r.has_value()); 242 assert(r->value == "/nix/store/03r3ipfa69l8nla101khyw3g67j24357-bash-5.3p9.drv"); 243 assert(r->remaining.empty()); 244 } 245 246 // ═══════════════════════════════════════════════════════════════════════════════ 247 // FFI Tests 248 // ═══════════════════════════════════════════════════════════════════════════════ 249 250 TEST(ffi_parse_u64le) { 251 uint8_t data[] = {0x26, 0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00}; 252 uint64_t value = 0; 253 size_t consumed = cornell_parse_u64le(data, sizeof(data), &value); 254 assert(consumed == 8); 255 assert(value == 0x126); 256 } 257 258 TEST(ffi_serialize_u64le) { 259 uint8_t buf[8] = {0}; 260 size_t written = cornell_serialize_u64le(0x126, buf, sizeof(buf)); 261 assert(written == 8); 262 assert(buf[0] == 0x26); 263 assert(buf[1] == 0x01); 264 for (int i = 2; i < 8; ++i) assert(buf[i] == 0); 265 } 266 267 // ═══════════════════════════════════════════════════════════════════════════════ 268 // Main 269 // ═══════════════════════════════════════════════════════════════════════════════ 270 271 int main() { 272 printf("Cornell Wire Format Tests\n"); 273 printf("=========================\n\n"); 274 275 printf("Primitive Roundtrip:\n"); 276 RUN_TEST(u8_roundtrip); 277 RUN_TEST(u64le_roundtrip); 278 RUN_TEST(bool64_roundtrip); 279 280 printf("\nConsumption:\n"); 281 RUN_TEST(u64le_consumption); 282 283 printf("\nNix String:\n"); 284 RUN_TEST(nix_string_roundtrip); 285 RUN_TEST(nix_string_consumption); 286 287 printf("\nProtocol Constants:\n"); 288 RUN_TEST(protocol_constants); 289 290 printf("\nList:\n"); 291 RUN_TEST(string_list_roundtrip); 292 293 printf("\nBinary Captures:\n"); 294 RUN_TEST(client_hello_capture); 295 RUN_TEST(isvalidpath_request_capture); 296 297 printf("\nFFI:\n"); 298 RUN_TEST(ffi_parse_u64le); 299 RUN_TEST(ffi_serialize_u64le); 300 301 printf("\n=========================\n"); 302 printf("All tests passed!\n"); 303 304 return 0; 305 }