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