1  /-
  2    Cornell.ExtractStateMachine - C++ Code Generation for State Machines
  3    
  4    Generates std::variant-based state machine code from the StateMachine DSL.
  5    The generated code matches the structure of handshake.hpp exactly.
  6  -/
  7  
  8  import Cornell.StateMachine
  9  
 10  namespace Cornell.ExtractStateMachine
 11  
 12  open Cornell.StateMachine
 13  
 14  -- ═══════════════════════════════════════════════════════════════════════════════
 15  -- C++ CODE GENERATION - Matching handshake.hpp interface exactly
 16  -- ═══════════════════════════════════════════════════════════════════════════════
 17  
 18  /-- Generate file header -/
 19  def genHeader : String :=
 20  "// ═══════════════════════════════════════════════════════════════════════════════
 21  // GENERATED BY CORNELL - DO NOT EDIT
 22  // Source: Cornell.ExtractStateMachine
 23  // 
 24  // This file is generated from the Lean specification in Cornell.StateMachine.
 25  // The state machine types are extracted automatically via metaprogramming.
 26  // The transition functions are direct translations of the Lean pattern matches.
 27  //
 28  // To regenerate:
 29  //   lake build cornell_sm_gen && lake exe cornell_sm_gen > cpp/include/cornell/handshake.hpp
 30  // ═══════════════════════════════════════════════════════════════════════════════
 31  
 32  #pragma once
 33  
 34  #include \"cornell/protocol.hpp\"
 35  #include <algorithm>
 36  #include <optional>
 37  #include <set>
 38  #include <string>
 39  #include <utility>
 40  #include <variant>
 41  #include <vector>
 42  
 43  namespace cornell {
 44  "
 45  
 46  /-- Generate HandshakeConfig -/
 47  def genHandshakeConfig : String :=
 48  "// ═══════════════════════════════════════════════════════════════════════════════
 49  // HANDSHAKE CONFIGURATION
 50  // Generated from: Cornell.StateMachine.HandshakeConfig
 51  // ═══════════════════════════════════════════════════════════════════════════════
 52  
 53  struct HandshakeConfig {
 54      ProtocolVersion serverVersion = CURRENT_PROTOCOL;
 55      std::set<Feature> serverFeatures = {Feature::ReapiV2, Feature::CasSha256, Feature::StreamingNar};
 56      std::optional<ReapiConfig> reapiConfig;
 57      std::string daemonVersion = \"nix-serve-cas 0.1.0\";
 58      TrustLevel trustLevel = TrustLevel::Trusted;
 59      
 60      static HandshakeConfig default_config() {
 61          HandshakeConfig cfg;
 62          cfg.reapiConfig = ReapiConfig{
 63              \"main\",
 64              DigestFunction::SHA256,
 65              {Capability::CAS, Capability::ActionCache}
 66          };
 67          return cfg;
 68      }
 69  };
 70  "
 71  
 72  /-- Generate ServerState enum -/
 73  def genServerStateEnum : String :=
 74  "// ═══════════════════════════════════════════════════════════════════════════════
 75  // SERVER STATE
 76  // Generated from: Cornell.StateMachine.ServerState
 77  // ═══════════════════════════════════════════════════════════════════════════════
 78  
 79  struct SrvInit {
 80      HandshakeConfig config;
 81  };
 82  struct SrvVersioned {
 83      HandshakeConfig config;
 84      ProtocolVersion negotiated;
 85  };
 86  struct SrvFeatures {
 87      HandshakeConfig config;
 88      ProtocolVersion negotiated;
 89      std::set<Feature> active;
 90  };
 91  struct SrvUpgrading {
 92      HandshakeConfig config;
 93      ProtocolVersion negotiated;
 94      std::set<Feature> active;
 95  };
 96  struct SrvNixReady {
 97      ProtocolVersion version;
 98  };
 99  struct SrvReapiReady {
100      ReapiConfig config;
101  };
102  struct SrvFailed {
103      std::string reason;
104  };
105  
106  using ServerHandshake = std::variant<
107      SrvInit,
108      SrvVersioned,
109      SrvFeatures,
110      SrvUpgrading,
111      SrvNixReady,
112      SrvReapiReady,
113      SrvFailed
114  >;
115  "
116  
117  /-- Generate ServerEvent enum -/
118  def genServerEventEnum : String :=
119  "// ═══════════════════════════════════════════════════════════════════════════════
120  // SERVER EVENTS
121  // Generated from: Cornell.StateMachine.ServerEvent
122  // ═══════════════════════════════════════════════════════════════════════════════
123  
124  struct SrvEvClientHello {
125      ProtocolVersion clientVersion;
126  };
127  struct SrvEvClientLegacy {};
128  struct SrvEvClientFeatures {
129      std::set<Feature> features;
130  };
131  struct SrvEvClientUpgradeResponse {
132      bool accept;
133  };
134  
135  using ServerEvent = std::variant<
136      SrvEvClientHello,
137      SrvEvClientLegacy,
138      SrvEvClientFeatures,
139      SrvEvClientUpgradeResponse
140  >;
141  "
142  
143  /-- Generate ServerAction enum -/
144  def genServerActionEnum : String :=
145  "// ═══════════════════════════════════════════════════════════════════════════════
146  // SERVER ACTIONS
147  // Generated from: Cornell.StateMachine.ServerAction
148  // ═══════════════════════════════════════════════════════════════════════════════
149  
150  struct SrvActSendServerHello {
151      ProtocolVersion version;
152  };
153  struct SrvActSendDaemonVersion {
154      std::string version;
155  };
156  struct SrvActSendTrustLevel {
157      TrustLevel level;
158  };
159  struct SrvActSendFeatures {
160      std::set<Feature> features;
161  };
162  struct SrvActSendUpgradeOffer {};
163  struct SrvActSendReapiConfig {
164      ReapiConfig config;
165  };
166  struct SrvActReady {};
167  struct SrvActFail {
168      std::string reason;
169  };
170  
171  using ServerAction = std::variant<
172      SrvActSendServerHello,
173      SrvActSendDaemonVersion,
174      SrvActSendTrustLevel,
175      SrvActSendFeatures,
176      SrvActSendUpgradeOffer,
177      SrvActSendReapiConfig,
178      SrvActReady,
179      SrvActFail
180  >;
181  "
182  
183  /-- Generate ClientState enum -/
184  def genClientStateEnum : String :=
185  "// ═══════════════════════════════════════════════════════════════════════════════
186  // CLIENT STATE
187  // Generated from: Cornell.StateMachine.ClientState
188  // ═══════════════════════════════════════════════════════════════════════════════
189  
190  struct CliInit {
191      ProtocolVersion clientVersion;
192      std::set<Feature> clientFeatures;
193  };
194  struct CliSentHello {
195      ProtocolVersion clientVersion;
196      std::set<Feature> clientFeatures;
197  };
198  struct CliVersioned {
199      ProtocolVersion negotiated;
200      std::set<Feature> clientFeatures;
201  };
202  struct CliAwaitingUpgrade {
203      ProtocolVersion negotiated;
204  };
205  struct CliNixReady {
206      ProtocolVersion version;
207  };
208  struct CliReapiReady {
209      ReapiConfig config;
210  };
211  struct CliFailed {
212      std::string reason;
213  };
214  
215  using ClientHandshake = std::variant<
216      CliInit,
217      CliSentHello,
218      CliVersioned,
219      CliAwaitingUpgrade,
220      CliNixReady,
221      CliReapiReady,
222      CliFailed
223  >;
224  "
225  
226  /-- Generate ClientEvent enum -/
227  def genClientEventEnum : String :=
228  "// ═══════════════════════════════════════════════════════════════════════════════
229  // CLIENT EVENTS
230  // Generated from: Cornell.StateMachine.ClientEvent
231  // ═══════════════════════════════════════════════════════════════════════════════
232  
233  struct CliEvServerHello {
234      ProtocolVersion version;
235  };
236  struct CliEvDaemonVersion {
237      std::string version;
238  };
239  struct CliEvTrustLevel {
240      TrustLevel level;
241  };
242  struct CliEvServerFeatures {
243      std::set<Feature> features;
244  };
245  struct CliEvUpgradeOffer {};
246  struct CliEvReapiConfig {
247      ReapiConfig config;
248  };
249  
250  using ClientEvent = std::variant<
251      CliEvServerHello,
252      CliEvDaemonVersion,
253      CliEvTrustLevel,
254      CliEvServerFeatures,
255      CliEvUpgradeOffer,
256      CliEvReapiConfig
257  >;
258  "
259  
260  /-- Generate ClientAction enum -/
261  def genClientActionEnum : String :=
262  "// ═══════════════════════════════════════════════════════════════════════════════
263  // CLIENT ACTIONS
264  // Generated from: Cornell.StateMachine.ClientAction
265  // ═══════════════════════════════════════════════════════════════════════════════
266  
267  struct CliActSendClientHello {
268      ProtocolVersion version;
269  };
270  struct CliActSendLegacy {};
271  struct CliActSendFeatures {
272      std::set<Feature> features;
273  };
274  struct CliActSendUpgradeResponse {
275      bool accept;
276  };
277  struct CliActReady {};
278  struct CliActFail {
279      std::string reason;
280  };
281  
282  using ClientAction = std::variant<
283      CliActSendClientHello,
284      CliActSendLegacy,
285      CliActSendFeatures,
286      CliActSendUpgradeResponse,
287      CliActReady,
288      CliActFail
289  >;
290  "
291  
292  /-- Generate server transition function -/
293  def genServerTransition : String :=
294  "// ═══════════════════════════════════════════════════════════════════════════════
295  // SERVER TRANSITION FUNCTION
296  // Generated from: Cornell.StateMachine.serverTransition
297  //
298  // This is a direct translation of the Lean pattern match. Each case corresponds
299  // exactly to a case in the Lean definition.
300  // ═══════════════════════════════════════════════════════════════════════════════
301  
302  inline ServerHandshake init_server_handshake(const HandshakeConfig& config) {
303      return SrvInit{config};
304  }
305  
306  // Helper: compute feature intersection
307  // Generated from: Cornell.StateMachine.featureIntersection
308  inline std::set<Feature> feature_intersection(
309      const std::set<Feature>& server_features,
310      const std::set<Feature>& client_features
311  ) {
312      std::set<Feature> result;
313      for (auto f : server_features) {
314          if (client_features.count(f)) result.insert(f);
315      }
316      return result;
317  }
318  
319  // Helper: check if upgrade should be offered
320  // Generated from: Cornell.StateMachine.shouldOfferUpgrade
321  inline bool should_offer_upgrade(const HandshakeConfig& config, const std::set<Feature>& active) {
322      return active.count(Feature::ReapiV2) && config.reapiConfig.has_value();
323  }
324  
325  inline std::pair<ServerHandshake, std::vector<ServerAction>>
326  server_step(const ServerHandshake& state, const ServerEvent& event) {
327      
328      // Case: .init config, .clientHello clientVer
329      // Lean: | .init config, .clientHello clientVer =>
330      //         let negotiated := if clientVer.value < config.serverVersion.value 
331      //                           then clientVer else config.serverVersion
332      //         { next := .versioned config negotiated
333      //         , actions := [.sendServerHello config.serverVersion] }
334      if (auto* s = std::get_if<SrvInit>(&state)) {
335          if (auto* e = std::get_if<SrvEvClientHello>(&event)) {
336              ProtocolVersion negotiated = (e->clientVersion.value < s->config.serverVersion.value)
337                  ? e->clientVersion
338                  : s->config.serverVersion;
339              return {
340                  SrvVersioned{s->config, negotiated},
341                  {SrvActSendServerHello{s->config.serverVersion}}
342              };
343          }
344      }
345      
346      // Case: .versioned config negotiated, .clientLegacy
347      // Lean: | .versioned config negotiated, .clientLegacy =>
348      //         if negotiated.supports 38 then ... else ...
349      if (auto* s = std::get_if<SrvVersioned>(&state)) {
350          if (std::holds_alternative<SrvEvClientLegacy>(event)) {
351              if (s->negotiated.supports(38)) {
352                  // Version 1.38+: expect features, stay in versioned
353                  std::vector<ServerAction> actions;
354                  if (s->negotiated.supports(33)) {
355                      actions.push_back(SrvActSendDaemonVersion{s->config.daemonVersion});
356                  }
357                  if (s->negotiated.supports(35)) {
358                      actions.push_back(SrvActSendTrustLevel{s->config.trustLevel});
359                  }
360                  return {*s, std::move(actions)};
361              } else {
362                  // Legacy: go straight to ready
363                  std::vector<ServerAction> actions;
364                  if (s->negotiated.supports(33)) {
365                      actions.push_back(SrvActSendDaemonVersion{s->config.daemonVersion});
366                  }
367                  if (s->negotiated.supports(35)) {
368                      actions.push_back(SrvActSendTrustLevel{s->config.trustLevel});
369                  }
370                  actions.push_back(SrvActReady{});
371                  return {SrvNixReady{s->negotiated}, std::move(actions)};
372              }
373          }
374          
375          // Case: .versioned config negotiated, .clientFeatures clientFeatures
376          // Lean: | .versioned config negotiated, .clientFeatures clientFeatures =>
377          //         let active := featureIntersection config.serverFeatures clientFeatures
378          //         if shouldOfferUpgrade config active then ... else ...
379          if (auto* e = std::get_if<SrvEvClientFeatures>(&event)) {
380              auto active = feature_intersection(s->config.serverFeatures, e->features);
381              if (should_offer_upgrade(s->config, active)) {
382                  return {
383                      SrvUpgrading{s->config, s->negotiated, active},
384                      {SrvActSendFeatures{s->config.serverFeatures}, SrvActSendUpgradeOffer{}}
385                  };
386              } else {
387                  return {
388                      SrvNixReady{s->negotiated},
389                      {SrvActSendFeatures{s->config.serverFeatures}, SrvActReady{}}
390                  };
391              }
392          }
393      }
394      
395      // Case: .upgrading config negotiated active, .clientUpgradeResponse accept
396      // Lean: | .upgrading config negotiated active, .clientUpgradeResponse accept =>
397      //         if accept then
398      //           match config.reapiConfig with
399      //           | some rc => ...
400      //           | none => ...
401      //         else ...
402      if (auto* s = std::get_if<SrvUpgrading>(&state)) {
403          if (auto* e = std::get_if<SrvEvClientUpgradeResponse>(&event)) {
404              if (e->accept) {
405                  if (s->config.reapiConfig.has_value()) {
406                      auto rc = *s->config.reapiConfig;
407                      return {
408                          SrvReapiReady{rc},
409                          {SrvActSendReapiConfig{rc}, SrvActReady{}}
410                      };
411                  } else {
412                      return {
413                          SrvFailed{\"REAPI config missing\"},
414                          {SrvActFail{\"REAPI config missing\"}}
415                      };
416                  }
417              } else {
418                  return {SrvNixReady{s->negotiated}, {SrvActReady{}}};
419              }
420          }
421      }
422      
423      // Case: .nixReady _, _ (terminal)
424      // Lean: | .nixReady _, _ => 
425      //         { next := .failed \"Already in terminal state\", actions := [.fail \"Already terminal\"] }
426      if (std::holds_alternative<SrvNixReady>(state)) {
427          return {SrvFailed{\"Already in terminal state\"}, {SrvActFail{\"Already terminal\"}}};
428      }
429      
430      // Case: .reapiReady _, _ (terminal)
431      // Lean: | .reapiReady _, _ => ...
432      if (std::holds_alternative<SrvReapiReady>(state)) {
433          return {SrvFailed{\"Already in terminal state\"}, {SrvActFail{\"Already terminal\"}}};
434      }
435      
436      // Case: .failed reason, _ (absorb)
437      // Lean: | .failed reason, _ => { next := .failed reason, actions := [] }
438      if (auto* s = std::get_if<SrvFailed>(&state)) {
439          return {*s, {}};
440      }
441      
442      // Case: _, _ (invalid transition)
443      // Lean: | s, e => { next := .failed s!\"Invalid event {repr e} in state\"
444      //                 , actions := [.fail \"Invalid transition\"] }
445      return {SrvFailed{\"Invalid transition\"}, {SrvActFail{\"Invalid transition\"}}};
446  }
447  
448  inline bool is_server_terminal(const ServerHandshake& state) {
449      return std::holds_alternative<SrvNixReady>(state) ||
450             std::holds_alternative<SrvReapiReady>(state) ||
451             std::holds_alternative<SrvFailed>(state);
452  }
453  "
454  
455  /-- Generate client transition function -/
456  def genClientTransition : String :=
457  "// ═══════════════════════════════════════════════════════════════════════════════
458  // CLIENT TRANSITION FUNCTION
459  // Generated from: Cornell.StateMachine.clientTransition
460  // ═══════════════════════════════════════════════════════════════════════════════
461  
462  inline std::pair<ClientHandshake, std::vector<ClientAction>>
463  init_client_handshake(ProtocolVersion version, const std::set<Feature>& features) {
464      return {
465          CliSentHello{version, features},
466          {CliActSendClientHello{version}}
467      };
468  }
469  
470  inline std::pair<ClientHandshake, std::vector<ClientAction>>
471  client_step(const ClientHandshake& state, const ClientEvent& event) {
472      
473      // Case: .sentHello clientVersion clientFeatures, .serverHello serverVer
474      // Lean: | .sentHello clientVer clientFeatures, .serverHello serverVer =>
475      //         let negotiated := if clientVer.value < serverVer.value then clientVer else serverVer
476      //         { next := .versioned negotiated clientFeatures
477      //         , actions := [.sendLegacyFields] }
478      if (auto* s = std::get_if<CliSentHello>(&state)) {
479          if (auto* e = std::get_if<CliEvServerHello>(&event)) {
480              ProtocolVersion negotiated = (s->clientVersion.value < e->version.value)
481                  ? s->clientVersion
482                  : e->version;
483              return {
484                  CliVersioned{negotiated, s->clientFeatures},
485                  {CliActSendLegacy{}}
486              };
487          }
488      }
489      
490      // Case: .versioned negotiated features, .serverDaemonVersion _
491      // Lean: | .versioned negotiated features, .serverDaemonVersion _ =>
492      //         { next := .versioned negotiated features, actions := [] }
493      if (auto* s = std::get_if<CliVersioned>(&state)) {
494          if (std::holds_alternative<CliEvDaemonVersion>(event)) {
495              return {*s, {}};
496          }
497      }
498      
499      // Case: .versioned negotiated features, .serverTrustLevel _
500      // Lean: | .versioned negotiated features, .serverTrustLevel _ =>
501      //         { next := .versioned negotiated features, actions := [] }
502      if (auto* s = std::get_if<CliVersioned>(&state)) {
503          if (std::holds_alternative<CliEvTrustLevel>(event)) {
504              return {*s, {}};
505          }
506      }
507      
508      // Case: .versioned negotiated clientFeatures, .serverFeatures serverFeatures
509      // Lean: | .versioned negotiated clientFeatures, .serverFeatures serverFeatures =>
510      //         let active := featureIntersection clientFeatures serverFeatures
511      //         if active.contains .reapiV2 then ... else ...
512      if (auto* s = std::get_if<CliVersioned>(&state)) {
513          if (auto* e = std::get_if<CliEvServerFeatures>(&event)) {
514              auto active = feature_intersection(s->clientFeatures, e->features);
515              std::vector<ClientAction> actions;
516              actions.push_back(CliActSendFeatures{s->clientFeatures});
517              
518              if (active.count(Feature::ReapiV2)) {
519                  return {CliAwaitingUpgrade{s->negotiated}, std::move(actions)};
520              } else {
521                  actions.push_back(CliActReady{});
522                  return {CliNixReady{s->negotiated}, std::move(actions)};
523              }
524          }
525      }
526      
527      // Case: .awaitingUpgrade negotiated, .upgradeOffer
528      // Lean: | .awaitingUpgrade negotiated, .upgradeOffer =>
529      //         { next := .awaitingUpgrade negotiated, actions := [.sendUpgradeResponse true] }
530      if (auto* s = std::get_if<CliAwaitingUpgrade>(&state)) {
531          if (std::holds_alternative<CliEvUpgradeOffer>(event)) {
532              return {*s, {CliActSendUpgradeResponse{true}}};
533          }
534      }
535      
536      // Case: .awaitingUpgrade _, .reapiConfig config
537      // Lean: | .awaitingUpgrade _, .reapiConfig config =>
538      //         { next := .reapiReady config, actions := [.ready] }
539      if (auto* s = std::get_if<CliAwaitingUpgrade>(&state)) {
540          if (auto* e = std::get_if<CliEvReapiConfig>(&event)) {
541              return {CliReapiReady{e->config}, {CliActReady{}}};
542          }
543      }
544      
545      // Terminal states
546      // Lean: | .nixReady _, _ => { next := .failed \"Already terminal\", actions := [] }
547      if (std::holds_alternative<CliNixReady>(state)) {
548          return {CliFailed{\"Already terminal\"}, {}};
549      }
550      
551      // Lean: | .reapiReady _, _ => { next := .failed \"Already terminal\", actions := [] }
552      if (std::holds_alternative<CliReapiReady>(state)) {
553          return {CliFailed{\"Already terminal\"}, {}};
554      }
555      
556      // Lean: | .failed reason, _ => { next := .failed reason, actions := [] }
557      if (auto* s = std::get_if<CliFailed>(&state)) {
558          return {*s, {}};
559      }
560      
561      // Catch-all: invalid transition
562      // Lean: | _, _ => { next := .failed \"Invalid transition\", actions := [.fail \"Invalid transition\"] }
563      return {CliFailed{\"Invalid transition\"}, {CliActFail{\"Invalid transition\"}}};
564  }
565  
566  inline bool is_client_terminal(const ClientHandshake& state) {
567      return std::holds_alternative<CliNixReady>(state) ||
568             std::holds_alternative<CliReapiReady>(state) ||
569             std::holds_alternative<CliFailed>(state);
570  }
571  
572  inline ProtocolVersion negotiate_version(ProtocolVersion client, ProtocolVersion server) {
573      return std::min(client, server);
574  }
575  "
576  
577  /-- Generate complete handshake.hpp -/
578  def genHandshakeHpp : String :=
579    genHeader ++ "\n"
580    ++ genHandshakeConfig ++ "\n"
581    ++ genServerStateEnum ++ "\n"
582    ++ genServerEventEnum ++ "\n"
583    ++ genServerActionEnum ++ "\n"
584    ++ genClientStateEnum ++ "\n"
585    ++ genClientEventEnum ++ "\n"
586    ++ genClientActionEnum ++ "\n"
587    ++ genServerTransition ++ "\n"
588    ++ genClientTransition ++ "\n"
589    ++ "} // namespace cornell\n"
590  
591  -- ═══════════════════════════════════════════════════════════════════════════════
592  -- OUTPUT
593  -- ═══════════════════════════════════════════════════════════════════════════════
594  
595  #eval IO.println genHandshakeHpp
596  
597  end Cornell.ExtractStateMachine
598  
599  -- Main function must be at root scope for executable
600  def main : IO Unit := do
601    IO.println Cornell.ExtractStateMachine.genHandshakeHpp