1  /* Cornell FFI - C interface for Haskell bindings
  2   *
  3   * This header provides a pure C interface to the Cornell wire format
  4   * primitives. The C++ implementation is compiled into a shared library
  5   * that Haskell can link against via FFI.
  6   *
  7   * PROOF CERTIFICATES:
  8   * Each function corresponds to verified Lean4 code in Cornell/Basic.lean
  9   * and Cornell/Nix.lean. The C++ implementation is validated against
 10   * Lean-generated test properties.
 11   */
 12  
 13  #ifndef CORNELL_FFI_H
 14  #define CORNELL_FFI_H
 15  
 16  #include <stdint.h>
 17  #include <stddef.h>
 18  
 19  #ifdef __cplusplus
 20  extern "C" {
 21  #endif
 22  
 23  /* ═══════════════════════════════════════════════════════════════════════════
 24   * Parse results
 25   * 
 26   * Functions return the number of bytes consumed, or 0 on failure.
 27   * Parsed values are written to output pointers.
 28   * ═══════════════════════════════════════════════════════════════════════════ */
 29  
 30  /* Parse u64le from bytes
 31   * Returns: bytes consumed (8 on success, 0 on failure)
 32   * PROOF: Cornell.u64le.roundtrip, Cornell.u64le.consumption
 33   */
 34  size_t cornell_parse_u64le(
 35      const uint8_t* data, 
 36      size_t len, 
 37      uint64_t* out_value
 38  );
 39  
 40  /* Serialize u64le to buffer
 41   * Returns: bytes written (8 on success, 0 if buffer too small)
 42   * PROOF: Cornell.u64le.roundtrip
 43   */
 44  size_t cornell_serialize_u64le(
 45      uint64_t value, 
 46      uint8_t* out, 
 47      size_t out_len
 48  );
 49  
 50  /* Parse bool64 from bytes
 51   * Returns: bytes consumed (8 on success, 0 on failure)
 52   * PROOF: Cornell.bool64.roundtrip, Cornell.bool64.consumption
 53   */
 54  size_t cornell_parse_bool64(
 55      const uint8_t* data,
 56      size_t len,
 57      int* out_value  /* 0 = false, nonzero = true */
 58  );
 59  
 60  /* Serialize bool64 to buffer
 61   * Returns: bytes written (8 on success, 0 if buffer too small)
 62   */
 63  size_t cornell_serialize_bool64(
 64      int value,
 65      uint8_t* out,
 66      size_t out_len
 67  );
 68  
 69  /* Parse NixString from bytes
 70   * Returns: bytes consumed (>0 on success, 0 on failure)
 71   * String is written to out_str (up to out_str_len bytes)
 72   * Actual string length written to out_actual_len
 73   * PROOF: Cornell.Nix.nixString.roundtrip, Cornell.Nix.nixString.consumption
 74   */
 75  size_t cornell_parse_nix_string(
 76      const uint8_t* data,
 77      size_t len,
 78      char* out_str,
 79      size_t out_str_len,
 80      size_t* out_actual_len
 81  );
 82  
 83  /* Calculate serialized size of NixString
 84   * Returns: total wire size (8 + len + padding)
 85   */
 86  size_t cornell_nix_string_wire_size(size_t str_len);
 87  
 88  /* Serialize NixString to buffer
 89   * Returns: bytes written (>0 on success, 0 if buffer too small)
 90   */
 91  size_t cornell_serialize_nix_string(
 92      const char* str,
 93      size_t str_len,
 94      uint8_t* out,
 95      size_t out_len
 96  );
 97  
 98  /* ═══════════════════════════════════════════════════════════════════════════
 99   * Protocol constants
100   * ═══════════════════════════════════════════════════════════════════════════ */
101  
102  #define CORNELL_WORKER_MAGIC_1 0x6e697863ULL
103  #define CORNELL_WORKER_MAGIC_2 0x6478696fULL
104  
105  #define CORNELL_STDERR_NEXT  0x6f6c6d67ULL
106  #define CORNELL_STDERR_READ  0x64617461ULL
107  #define CORNELL_STDERR_WRITE 0x64617416ULL
108  #define CORNELL_STDERR_LAST  0x616c7473ULL
109  #define CORNELL_STDERR_ERROR 0x63787470ULL
110  
111  #ifdef __cplusplus
112  }
113  #endif
114  
115  #endif /* CORNELL_FFI_H */