From 982e49b806e356df10249f5816d3d0bb94d8c384 Mon Sep 17 00:00:00 2001
From: Matthew Fernandez <matthew.fernandez@gmail.com>
Date: Sun, 13 Sep 2026 18:49:37 -0700
Subject: [PATCH] release v2026.09.13

---
 CHANGELOG.rst           |  28 +++++
 share/CMakeLists.txt    |   3 +
 share/v2026.09.13/_list | 232 ++++++++++++++++++++++++++++++++++++++++
 share/v2026.09.13/_set  | 100 +++++++++++++++++
 4 files changed, 363 insertions(+)
 create mode 100644 share/v2026.09.13/_list
 create mode 100644 share/v2026.09.13/_set

diff --git a/CHANGELOG.rst b/CHANGELOG.rst
index 1ec4ca9c..e68b7674 100644
--- a/CHANGELOG.rst
+++ b/CHANGELOG.rst
@@ -1,6 +1,34 @@
 Change log
 ==========
 
+v2026.09.13
+-----------
+
+User-facing changes
+~~~~~~~~~~~~~~~~~~~
+* Bug fix: compilation of the generated checker when using the x32 ABI has been
+  repaired. This bug was introduced in v2026.08.30 (commits
+  9bd4c196af6aa3fefeacab0a828ec7abd8ac24b7,
+  dfe5f5b98ff04ab496e83ac3281bcd442566f8c1).
+* The auxiliary tools ``murphi2c``, ``murphi2murphi``, ``murphi2smv``,
+  ``murphi2uclid``, and ``murphi2xml`` now print their error messages including
+  context and colouring for ease of reading (commits
+  bb728dd1052cb2605b04a78f4a776be2bba864ce,
+  4b6bd3d668057601cad0cdb4751bfb33305f126b,
+  35f0f7f388b227bf07431dfb1ff599c660b6f9f5,
+  c0c3e715a0d6e79da0425b4db3a64e9ea928fbb5,
+  d98255a32cf957b0f9b0d8700741fd010cf9f376,
+  3f466fe3ccd670cb97f369985c179b6e939f0099).
+
+Internal changes
+~~~~~~~~~~~~~~~~
+* The type of a numeric literal (``Number::type()``) is now a range that
+  contains only its exact value, rather than an infinite range. I.e. ``42``
+  would previously be considered to have a type ``-∞..∞`` whereas it now has the
+  type ``42..42`` (commit d6d5bc93ee6ec12292cf440972de05eae28c254f).
+* Reproducible builds of Rumur should now be possible without patching the build
+  system (commit 3d0e63d8d5b5622d5d198e3b70363743e9089179).
+
 v2026.08.30
 -----------
 
diff --git a/share/CMakeLists.txt b/share/CMakeLists.txt
index 0a22ce89..fa336b39 100644
--- a/share/CMakeLists.txt
+++ b/share/CMakeLists.txt
@@ -23,3 +23,6 @@ install(DIRECTORY v2026.03.11
 install(DIRECTORY v2026.08.30
   DESTINATION ${CMAKE_INSTALL_DATAROOTDIR}/rumur/lib
 )
+install(DIRECTORY v2026.09.13
+  DESTINATION ${CMAKE_INSTALL_DATAROOTDIR}/rumur/lib
+)
diff --git a/share/v2026.09.13/_list b/share/v2026.09.13/_list
new file mode 100644
index 00000000..fa7115ae
--- /dev/null
+++ b/share/v2026.09.13/_list
@@ -0,0 +1,232 @@
+dnl template for a statically sized list/queue/stack
+dnl
+dnl This file defines, as an M4¹ template, a type-generic Murphi list data
+dnl structure. To use this, include the template and then call the macro "_list"
+dnl with 4 parameters:
+dnl   • "name" – a prefix for the generated list data structure and its
+dnl     supporting functions
+dnl   • "index_t" – a Murphi type for indexing the list
+dnl   • "elem_t" – a Murphi type for the elements of the list
+dnl   • "size" – one more than the number of elements in type "index_t",
+dnl     defaulting to 2³¹-1 (see discussion of this below)
+dnl E.g.:
+dnl
+dnl   include(`_list')dnl
+dnl
+dnl   type
+dnl     int: 0..32;
+dnl
+dnl   _list(`ints', `0..10', `int')dnl
+dnl
+dnl Pre-process your model with M4:
+dnl
+dnl   $ m4 --include=/path/to/rumur/install/share/rumur/lib model.m >out.m
+dnl
+dnl This generates a type and some supporting functions:
+dnl
+dnl   type
+dnl     ints_t: …
+dnl
+dnl   function ints_is_empty(list_: ints_t): boolean;
+dnl   function ints_is_full(list_: ints_t): boolean;
+dnl   function ints_size(list_: ints_t): 0..2147483647;
+dnl   procedure ints_push_back(var list_: ints_t; elem_: int);
+dnl   function ints_try_push_back(var list_: ints_t; elem_: int): boolean;
+dnl   function ints_pop_front(var list_: ints_t): int;
+dnl   function ints_pop_back(var list_: ints_t): int;
+dnl
+dnl You can then go on to use the "ints_t" type in your handwritten model code.
+dnl
+dnl "index_t" can be an arbitrary type; the only requirement is that it is
+dnl iterable. It can be a previously defined type or a type literal. The
+dnl underlying type could be boolean, a range, a scalarset, or an enum. Though
+dnl it is unlikely anything except a range makes sense.
+dnl
+dnl "elem_t" can be an arbitrary type. It can be a previously defined type or a
+dnl type literal, though you probably want to name it in order to more easily
+dnl use the push and pop functions.
+dnl
+dnl "size" does not need to be supplied unless (a) your indexing type "index_t"
+dnl has more than 2³¹-2 elements or (b) you are trying to optimise your model by
+dnl using a value type narrower than "int32_t". In either case, you still do not
+dnl need to supply "size" if you never call the "*_size()" function; it is not
+dnl used internally within this template. If you call "*_size()" and your usage
+dnl falls into the (a) or (b) cases above, supply a "size" that is the number of
+dnl elements in "index_t" plus 1. Note that, e.g. if your indexing type is
+dnl "0..255", your size will need to be ≥ 256, preventing you using the value
+dnl type "uint8_t" which is not large enough to hold the value 256.
+dnl
+dnl This template is in the public domain. You may use it for any purpose and
+dnl its inclusion in a model does not affect the legal status of that model.
+dnl
+dnl ¹ https://en.wikipedia.org/wiki/M4_(computer_language)
+dnl
+define(`_list', `dnl
+-------------------------------------------------------------------------------
+-- interface for $1_t, a list of $3 values indexed by $2
+-------------------------------------------------------------------------------
+
+type
+  $1_t: array[$2] of record
+    -- Does this slot hold an item? The type 1..1 is used to model a boolean
+    -- without incurring an extra bit for the undefined value. I.e.
+    --   false = isundefined(is_populated_)
+    --   true = !isundefined(is_populated_)
+    is_populated_: 1..1;
+    -- the contents of the slot, if !isundefined(is_populated_)
+    value_: $3;
+  end;
+
+function $1_is_empty(list_: $1_t): boolean;
+begin
+  -- use a single-iteration loop to check the first element to avoid assuming
+  -- the lower bound of type $2
+  for i_: $2 do
+    if !isundefined(list_[i_].is_populated_) then
+      return false;
+    else
+      return true;
+    end;
+  end;
+  -- in the edge case where $2 is an empty type, consider the list always empty
+  return true;
+end;
+
+-- get the number of elements present in a list
+function $1_size(list_: $1_t): 0..ifelse(`$4', `', `2147483647', `$4');
+  var count_: 0..ifelse(`$4', `', `2147483647', `$4');
+begin
+  -- We have no easy way of checking the number of members in the type $2 at
+  -- generation time. So we use a runtime sanity check here that our return type
+  -- is large enough to represent the maximum size. A decent compiler will
+  -- constant fold and eliminate this in the common case where the type is
+  -- indeed large enough.
+  count_ := 0;
+  for i_: $2 do
+    assert
+      "0..ifelse(`$4', `', `2147483647', `$4') too small to represent $1_t size"
+      count_ < ifelse(`$4', `', `2147483647', `$4');
+    count_ := count_ + 1;
+  end;
+
+  count_ := 0;
+  for i_: $2 do
+    if !isundefined(list_[i_].is_populated_) then
+      count_ := count_ + 1;
+    end;
+  end;
+  return count_;
+end;
+
+function $1_is_full(list_: $1_t): boolean;
+begin
+  -- use a loop to check the last element to avoid assuming the upper bound of
+  -- type $2
+  for i_: $2 do
+    if isundefined(list_[i_].is_populated_) then
+      return false;
+    end;
+  end;
+  return true;
+end;
+
+-- Treating a $1_t as a first-in-first-out queue, enqueue an item. Or
+-- equivalently, treating a $1_t as a last-in-first-out stack, stack an item.
+procedure $1_push_back(var list_: $1_t; elem_: $3);
+begin
+  assert "attempting to push into a full $1_t" !$1_is_full(list_);
+  -- use a loop to find the first empty slot to avoid assuming the upper bound
+  -- of type $2
+  for i_: $2 do
+    if isundefined(list_[i_].is_populated_) then
+      list_[i_].value_ := elem_;
+      list_[i_].is_populated_ := 1;
+      return;
+    end;
+  end;
+  assert "unreachable code executed" false;
+end;
+
+-- Treating a $1_t as a first-in-first-out queue, enqueue an item and return
+-- true if possible. Or equivalently, treating a $1_t as a last-in-first-out
+-- stack, stack an item and return true if possible. If it is not possible to
+-- insert the new item, do nothing and return false.
+function $1_try_push_back(var list_: $1_t; elem_: $3): boolean;
+begin
+  if $1_is_full(list_) then
+    return false;
+  end;
+  $1_push_back(list_, elem_);
+  return true;
+end;
+
+-- treating a $1_t as a first-in-first-out queue, dequeue an item
+function $1_pop_front(var list_: $1_t): $3;
+var
+  first_: $3;
+  successor_: boolean;
+begin
+  assert "attempting to pop from an empty $1_t" !$1_is_empty(list_);
+  for i_: $2 do
+
+    -- extract the first element
+    assert "corrupted list" !isundefined(list_[i_].is_populated_);
+    first_ := list_[i_].value_;
+
+    -- Shuffle the remaining elements forwards. We do this with an unorthodox
+    -- double loop to avoid assuming anything about the bounds of $2 or
+    -- even whether its members are orderable.
+    for j_: $2 do
+      undefine list_[j_];
+      successor_ := false;
+      for k_: $2 do
+        if j_ = k_ then
+          assert "incorrect shuffle logic" !successor_;
+          successor_ := true;
+        elsif successor_ then
+          list_[j_] := list_[k_];
+          successor_ := false;
+        end;
+      end;
+    end;
+
+    return first_;
+  end;
+end;
+
+-- treating a $1_t as a last-in-first-out stack, unstack an item
+function $1_pop_back(var list_: $1_t): $3;
+var
+  last_: $3;
+  has_successor_: boolean;
+  successor_: boolean;
+begin
+  assert "attempting to pop from an empty $1_t" !$1_is_empty(list_);
+  for i_: $2 do
+
+    -- Is this element the last? We do this with an unorthodox loop to avoid
+    -- assuming anything about the bounds of $2 or even whether its members
+    -- are orderable.
+    has_successor_ := false;
+    for j_: $2 do
+      if i_ = j_ then
+        successor_ := true;
+      elsif successor_ then
+        has_successor_ := !isundefined(list_[j_].is_populated_);
+        successor_ := false;
+      end;
+    end;
+
+    -- if this is the last element, extract and return it
+    if !has_successor_ then
+      last_ := list_[i_].value_;
+      undefine list_[i_];
+      return last_;
+    end;
+  end;
+end;
+
+-------------------------------------------------------------------------------
+-- end interface for $1_t
+-------------------------------------------------------------------------------
+')dnl
diff --git a/share/v2026.09.13/_set b/share/v2026.09.13/_set
new file mode 100644
index 00000000..85749ed1
--- /dev/null
+++ b/share/v2026.09.13/_set
@@ -0,0 +1,100 @@
+dnl template for an unordered set
+dnl
+dnl This file defines, as an M4¹ template, a type-generic Murphi set data
+dnl structure. To use this, include the template and then call the macro "_set"
+dnl with 2 parameters:
+dnl   • "name" – a prefix for the generated set data structure and its
+dnl     supporting functions
+dnl   • "elem_t" – a Murphi type for the elements of the set
+dnl E.g.:
+dnl
+dnl   include(`_set')dnl
+dnl
+dnl   type
+dnl     int: 0..32;
+dnl
+dnl   _set(`ints', `int')dnl
+dnl
+dnl Pre-process your model with M4:
+dnl
+dnl   $ m4 --include=/path/to/rumur/install/share/rumur/lib model.m >out.m
+dnl
+dnl This generates a type and some supporting functions:
+dnl
+dnl   type
+dnl     ints_t: …
+dnl
+dnl   function ints_is_empty(set_: ints_t): boolean;
+dnl   function ints_is_full(set_: ints_t): boolean;
+dnl   function ints_add(var set_: ints_t; elem_: int): boolean;
+dnl   function ints_remove(var set_: ints_t; elem_: int): boolean;
+dnl   function ints_contains(set_: ints_t; elem_: int): boolean;
+dnl
+dnl You can then go on to use the "ints_t" type in your handwritten model code.
+dnl
+dnl "elem_t" can be an arbitrary scalar type. It can be a previously defined
+dnl type or a type literal.
+dnl
+dnl This template is in the public domain. You may use it for any purpose and
+dnl its inclusion in a model does not affect the legal status of that model.
+dnl
+dnl ¹ https://en.wikipedia.org/wiki/M4_(computer_language)
+dnl
+define(`_set', `dnl
+-------------------------------------------------------------------------------
+-- interface for $1_t, a set of $2
+-------------------------------------------------------------------------------
+
+type
+  $1_t: array[$2] of 1..1;
+
+function $1_is_empty(set_: $1_t): boolean;
+begin
+  for i_: $2 do
+    if !isundefined(set_[i_]) then
+      return false;
+    end;
+  end;
+  return true;
+end;
+
+function $1_is_full(set_: $1_t): boolean;
+begin
+  for i_: $2 do
+    if isundefined(set_[i_]) then
+      return false;
+    end;
+  end;
+  return true;
+end;
+
+-- insert a value into the set, returning true if it was already present
+function $1_add(var set_: $1_t; elem_: $2): boolean;
+var
+  rc_: boolean;
+begin
+  rc_ := !isundefined(set_[elem_]);
+  set_[elem_] := 1;
+  return rc_;
+end;
+
+-- remove a value from the set, returning true if it was present
+function $1_remove(var set_: $1_t; elem_: $2): boolean;
+var
+  rc_: boolean;
+begin
+  rc_ := !isundefined(set_[elem_]);
+  undefine set_[elem_];
+  return rc_;
+end;
+
+-- test the existence of an element in the set
+function $1_contains(set_: $1_t; elem_: $2): boolean;
+begin
+  return !isundefined(set_[elem_]);
+end;
+
+-------------------------------------------------------------------------------
+-- end interface for $1_t
+-------------------------------------------------------------------------------
+')dnl