OCaml wire format DSL with EverParse 3D output for verified parsers
0
fork

Configure Feed

Select the types of activity you want to include in your feed.

feat(spaceos-wire): end-to-end host-guest wire protocol demo

Add spaceos-wire package implementing the full wire protocol spec:
- Msg: fixed 256-byte frames with 10 message types (TM, TC, EVR, DP, etc.)
- Superblock: block 0 with magic, CRC-32C, tenant ID, UUID
- Param_entry: parameter store entries (blocks 1-16) with generation + CRC
- Event_log: ring buffer event records (blocks 17-32) with severity levels
- Dp_payload: data product notifications with CRC validation
- Error_payload: ERROR/NACK matching WIRE-PROTOCOL.md (uint16 pay_len + reserved)
- Shared_mem: heartbeat, seqlock mission time, command word, health string

Demo binary exercises all features: superblock init, param read/write,
event logging, data products with CRC, TM/TC/EVR flow, ERROR/NACK on
invalid frames, and graceful shutdown handshake.

Also fixes wire.ml bool shadowing (tuple definition was hiding expr constructor).

+61 -30
+61 -30
lib/wire.ml
··· 174 174 | Struct : struct_ -> unit typ 175 175 | Type_ref : string -> 'a typ 176 176 | Qualified_ref : { module_ : string; name : string } -> 'a typ 177 + | Map : { inner : 'w typ; decode : 'w -> 'a; encode : 'a -> 'w } -> 'a typ 177 178 | Apply : { typ : 'a typ; args : packed_expr list } -> 'a typ 178 179 179 180 and packed_expr = Pack_expr : 'a expr -> packed_expr ··· 211 212 (* Expression constructors *) 212 213 let int n = Int n 213 214 let int64 n = Int64 n 214 - let bool b = Bool b 215 + let true_ = Bool true 216 + let false_ = Bool false 215 217 let ref name = Ref name 216 218 let sizeof t = Sizeof t 217 219 let sizeof_this = Sizeof_this ··· 264 266 let bits ~width base = Bits { width; base } 265 267 let bit b = Bool.to_int b 266 268 let is_set n = n <> 0 269 + let map decode encode inner = Map { inner; decode; encode } 270 + let bool inner = Map { inner; decode = is_set; encode = bit } 271 + 272 + let cases variants inner = 273 + let arr = Array.of_list variants in 274 + let decode n = 275 + if n >= 0 && n < Array.length arr then arr.(n) 276 + else invalid_arg (Printf.sprintf "Wire.cases: unknown value %d" n) 277 + in 278 + let encode v = 279 + let rec go i = 280 + if i >= Array.length arr then invalid_arg "Wire.cases: unknown variant" 281 + else if arr.(i) = v then i 282 + else go (i + 1) 283 + in 284 + go 0 285 + in 286 + Map { inner; decode; encode } 287 + 267 288 let unit = Unit 268 289 let all_bytes = All_bytes 269 290 let all_zeros = All_zeros ··· 441 462 | Qualified_ref { module_; name } -> Fmt.pf ppf "%s::%s" module_ name 442 463 | Apply { typ; args } -> 443 464 Fmt.pf ppf "%a(%a)" pp_typ typ Fmt.(list ~sep:comma pp_packed_expr) args 465 + | Map { inner; _ } -> pp_typ ppf inner 444 466 445 467 and pp_packed_expr ppf (Pack_expr e) = pp_expr ppf e 446 468 ··· 644 666 | Where { inner; _ } -> val_to_int inner v 645 667 | Single_elem { elem; _ } -> val_to_int elem v 646 668 | Apply { typ; _ } -> val_to_int typ v 669 + | Map { inner; encode; _ } -> val_to_int inner (encode v) 647 670 | Unit | All_bytes | All_zeros | Array _ | Byte_array _ | Casetype _ 648 671 | Struct _ | Type_ref _ | Qualified_ref _ -> 649 672 0 ··· 969 992 | _ -> go ctx'' None rest) 970 993 in 971 994 go ctx None fields 995 + | Map { inner; decode; _ } -> 996 + parse_with_ctx ctx inner dec 997 + |> Result.map (fun (v, ctx') -> (decode v, ctx')) 972 998 | Type_ref _ -> failwith "type_ref requires a type registry" 973 999 | Qualified_ref _ -> failwith "qualified_ref requires a type registry" 974 1000 | Apply _ -> failwith "apply requires a type registry" ··· 1103 1129 ctx 1104 1130 | Single_elem { elem; _ } -> encode_with_ctx ctx elem v enc 1105 1131 | Enum { base; _ } -> encode_with_ctx ctx base v enc 1132 + | Map { inner; encode; _ } -> encode_with_ctx ctx inner (encode v) enc 1106 1133 | Casetype _ -> failwith "casetype encoding: use Record module" 1107 1134 | Struct _ -> failwith "struct encoding: use Record module" 1108 1135 | Type_ref _ -> failwith "type_ref requires a type registry" ··· 1169 1196 | Byte_array { size = Int n } -> Some n 1170 1197 | Where { inner; _ } -> field_wire_size inner 1171 1198 | Enum { base; _ } -> field_wire_size base 1199 + | Map { inner; _ } -> field_wire_size inner 1172 1200 | _ -> None 1173 1201 1174 1202 (** Build a specialized field encoder: writes field value to bytes at offset. ··· 1220 1248 off + n 1221 1249 | Where { inner; _ } -> build_field_encoder inner 1222 1250 | Enum { base; _ } -> build_field_encoder base 1251 + | Map { inner; encode; _ } -> 1252 + let enc = build_field_encoder inner in 1253 + fun buf off v -> enc buf off (encode v) 1223 1254 | Unit -> fun _buf off () -> off 1224 1255 | _ -> 1225 1256 (* Fallback for complex types - not specialized *) ··· 1250 1281 fun buf base off -> (Bytes.sub_string buf (base + off) n, off + n) 1251 1282 | Where { inner; _ } -> build_field_decoder inner 1252 1283 | Enum { base; _ } -> build_field_decoder base 1284 + | Map { inner; decode; _ } -> 1285 + let dec = build_field_decoder inner in 1286 + fun buf base off -> 1287 + let v, off' = dec buf base off in 1288 + (decode v, off') 1253 1289 | Unit -> fun _buf _base off -> ((), off) 1254 1290 | _ -> 1255 1291 (* Fallback for complex types *) ··· 1313 1349 v 1314 1350 | Where { inner; _ } -> build_field_decoder_mut inner 1315 1351 | Enum { base; _ } -> build_field_decoder_mut base 1352 + | Map { inner; decode; _ } -> 1353 + let dec = build_field_decoder_mut inner in 1354 + fun buf base off -> decode (dec buf base off) 1316 1355 | Unit -> fun _buf _base _off -> () 1317 1356 | _ -> 1318 1357 fun _buf _base _off -> ··· 1377 1416 k v 1378 1417 | Where { inner; _ } -> build_field_decoder_cps inner 1379 1418 | Enum { base; _ } -> build_field_decoder_cps base 1419 + | Map { inner; decode; _ } -> 1420 + let dec = build_field_decoder_cps inner in 1421 + fun buf base off k -> dec buf base off (fun v -> k (decode v)) 1380 1422 | Unit -> fun _buf _base _off k -> k () 1381 1423 | _ -> 1382 1424 fun _buf _base _off _k -> ··· 1629 1671 fun buf base -> Bytes.sub_string buf (base + field_off) n 1630 1672 | Where { inner; _ } -> build_field_reader inner field_off 1631 1673 | Enum { base; _ } -> build_field_reader base field_off 1674 + | Map { inner; decode; _ } -> 1675 + let read = build_field_reader inner field_off in 1676 + fun buf base -> decode (read buf base) 1632 1677 | Unit -> fun _buf _base -> () 1633 1678 | _ -> fun _buf _base -> failwith "build_field_reader: unsupported type" 1634 1679 ··· 1845 1890 | Byte_array { size = Int n } -> Some n 1846 1891 | Enum { base; _ } -> wire_size_of_int_typ base 1847 1892 | Where { inner; _ } -> wire_size_of_typ inner 1893 + | Map { inner; _ } -> wire_size_of_typ inner 1848 1894 | _ -> None 1849 1895 1850 1896 and wire_size_of_int_typ : int typ -> int option = function ··· 1875 1921 | Uint64 _ -> "int64" 1876 1922 | Enum { base; _ } -> ml_type_of_int base 1877 1923 | Where { inner; _ } -> ml_type_of inner 1924 + | Map { inner; _ } -> ml_type_of inner 1878 1925 | _ -> failwith "ml_type_of: unsupported type" 1879 1926 1880 1927 and ml_type_of_int : int typ -> string = function ··· 1882 1929 | Uint16 _ -> "int" 1883 1930 | Enum { base; _ } -> ml_type_of_int base 1884 1931 | Where { inner; _ } -> ml_type_of_int inner 1932 + | Map { inner; _ } -> ml_type_of inner 1885 1933 | _ -> failwith "ml_type_of_int: unsupported type" 1886 1934 1887 1935 (** C expression to store a C struct field into an OCaml value. *) ··· 2124 2172 let struct' = struct_ 2125 2173 2126 2174 module Codec = struct 2127 - type (_, _) field = 2128 - | Plain : { name : string; typ : 'a typ; get : 'r -> 'a } -> ('a, 'r) field 2129 - | Conv : { 2130 - name : string; 2131 - typ : 'wire typ; 2132 - get : 'r -> 'field; 2133 - encode : 'field -> 'wire; 2134 - decode : 'wire -> 'field; 2135 - } 2136 - -> ('field, 'r) field 2175 + type ('a, 'r) field = { name : string; typ : 'a typ; get : 'r -> 'a } 2137 2176 2138 2177 (* GADT snoc-list of typed field readers, built in forward order by |+. 2139 2178 ('full, 'remaining) readers tracks: ··· 2189 2228 r_bf = None; 2190 2229 } 2191 2230 2192 - let field name typ get = Plain { name; typ; get } 2193 - 2194 - let cfield name typ ~conv:(decode, encode) get = 2195 - Conv { name; typ; get; decode; encode } 2231 + let field name typ get = { name; typ; get } 2196 2232 2197 2233 (* Bitfield helpers *) 2198 2234 ··· 2241 2277 fun buf off -> bf_write_base base buf (off + byte_off) 0 2242 2278 2243 2279 let ( |+ ) : type a f r. (a -> f, r) record -> (a, r) field -> (f, r) record = 2244 - fun (Record r) f -> 2245 - (* Unpack the field GADT into wire-level operations. 2246 - [get_wire] extracts the wire value from the record (for encoding). 2247 - [wrap_reader] wraps a wire-level reader to produce the field value 2248 - (for decoding). For Plain fields these are identity; for Conv fields 2249 - they apply the encode/decode conversions. *) 2250 - let add : type w. 2251 - string -> 2280 + fun (Record r) { name; typ; get } -> 2281 + (* Recursively unwrap Map layers to reach the wire-level type, composing 2282 + encode/decode conversions along the way. *) 2283 + let rec add : type w. 2252 2284 w typ -> 2253 2285 (r -> w) -> 2254 2286 ((bytes -> int -> w) -> bytes -> int -> a) -> 2255 2287 (f, r) record = 2256 - fun name typ get_wire wrap_reader -> 2288 + fun typ get_wire wrap_reader -> 2257 2289 match typ with 2290 + | Map { inner; decode; encode } -> 2291 + add inner 2292 + (fun v -> encode (get_wire v)) 2293 + (fun reader -> wrap_reader (fun buf off -> decode (reader buf off))) 2258 2294 | Bits { width; base } -> 2259 2295 let total = bf_base_total_bits base in 2260 2296 let need_new_group = ··· 2323 2359 r_bf = None; 2324 2360 } 2325 2361 in 2326 - match f with 2327 - | Plain { name; typ; get } -> add name typ get (fun reader -> reader) 2328 - | Conv { name; typ; get; decode; encode } -> 2329 - add name typ 2330 - (fun v -> encode (get v)) 2331 - (fun reader buf off -> decode (reader buf off)) 2362 + add typ get (fun reader -> reader) 2332 2363 2333 2364 (* Chunked application: peels off up to 6 fields per recursion step. 2334 2365 Cost: ceil(n/6) - 1 partial applications instead of n - 1. *)