From b296494c6567b44d24b2b74072bdb37fd3f7c11a Mon Sep 17 00:00:00 2001
From: Will Bradley <68962413+a2435191@users.noreply.github.com>
Date: Sun, 17 May 2026 04:16:56 -0400
Subject: [PATCH 1/2] Merge parts of branch 'bugfix-experiments' into
 nary-arity-bug-fix

---
 harmony_model_checker/charm/ops.c    |  6 ++++++
 harmony_model_checker/harmony/ast.py | 10 ++++++++++
 harmony_model_checker/harmony/ops.py |  5 +++++
 3 files changed, 21 insertions(+)

diff --git a/harmony_model_checker/charm/ops.c b/harmony_model_checker/charm/ops.c
index b0e1a6ae..c644881d 100644
--- a/harmony_model_checker/charm/ops.c
+++ b/harmony_model_checker/charm/ops.c
@@ -2477,6 +2477,7 @@ void op_Nary(const void *env, struct state *state, struct step *step){
             }
         }
     }
+    assert(en->arity <= MAX_ARITY); 
     for (unsigned int i = 0; i < en->arity; i++) {
         args[i] = ctx_pop(step->ctx);
         if (step->keep_callstack) {
@@ -2493,6 +2494,7 @@ void op_Nary(const void *env, struct state *state, struct step *step){
             strbuf_printf(&step->explain, "); ");
         }
     }
+    debug("Nary: Executing %d-ary %s\n", en->arity, en->fi->name);
     hvalue_t result = (*en->fi->f)(state, step, args, en->arity);
     if (!step->ctx->failed) {
         if (step->keep_callstack) {
@@ -3422,6 +3424,10 @@ void *init_Nary(struct dict *map, struct allocator *allocator){
     copy[arity->u.atom.len] = 0;
     env->arity = atoi(copy);
     free(copy);
+    if (env->arity > MAX_ARITY) {
+        fprintf(stderr, "Nary: arity %u is too large (> %u)\n", env->arity, MAX_ARITY);
+        exit(1);
+    }
 
     struct json_value *op = dict_lookup(map, "value", 5);
     assert(op->type == JV_ATOM);
diff --git a/harmony_model_checker/harmony/ast.py b/harmony_model_checker/harmony/ast.py
index 3e953b08..a43467f4 100644
--- a/harmony_model_checker/harmony/ast.py
+++ b/harmony_model_checker/harmony/ast.py
@@ -666,6 +666,16 @@ def gencode(self, scope, code, stmt):
         else:
             for i in range(n):
                 self.args[i].compile(scope, code, stmt)
+            # TODO: in the future maybe split into chunks of smaller arity
+            if n > NaryOp.MAX_ARITY:
+                lexeme, file, line, column = self.endtoken # end token looks better imo
+                raise HarmonyCompilerError(
+                    message="Arity %d exceeds max arity %d" % (n, NaryOp.MAX_ARITY),
+                    filename=file,
+                    line=line,
+                    column=column,
+                    lexeme=lexeme
+                )
             code.append(NaryOp(self.op, n), self.token, self.endtoken, stmt=stmt)
 
     def getLabels(self):
diff --git a/harmony_model_checker/harmony/ops.py b/harmony_model_checker/harmony/ops.py
index 7e129ac4..7ebbe29c 100644
--- a/harmony_model_checker/harmony/ops.py
+++ b/harmony_model_checker/harmony/ops.py
@@ -1260,8 +1260,13 @@ def substitute(self, map):
             self.pc = map[self.pc].pc
 
 class NaryOp(Op):
+    # See MAX_ARITY in `ops.c`
+    MAX_ARITY = 16
+    
     def __init__(self, op, n):
+        """Caller should check that n <= MAX_ARITY"""
         self.op = op
+        assert n <= self.MAX_ARITY
         self.n = n
 
     def __repr__(self):

From dcbe524bc6caf3016663f033aec996ef49b69d72 Mon Sep 17 00:00:00 2001
From: Will Bradley <68962413+a2435191@users.noreply.github.com>
Date: Sun, 17 May 2026 04:37:02 -0400
Subject: [PATCH 2/2] Remove extraneous `debug` call from bugfix-experiments
 branch

---
 harmony_model_checker/charm/ops.c | 1 -
 1 file changed, 1 deletion(-)

diff --git a/harmony_model_checker/charm/ops.c b/harmony_model_checker/charm/ops.c
index c644881d..b6724c38 100644
--- a/harmony_model_checker/charm/ops.c
+++ b/harmony_model_checker/charm/ops.c
@@ -2494,7 +2494,6 @@ void op_Nary(const void *env, struct state *state, struct step *step){
             strbuf_printf(&step->explain, "); ");
         }
     }
-    debug("Nary: Executing %d-ary %s\n", en->arity, en->fi->name);
     hvalue_t result = (*en->fi->f)(state, step, args, en->arity);
     if (!step->ctx->failed) {
         if (step->keep_callstack) {