diff --git a/src/geb/geb.lisp b/src/geb/geb.lisp
index a33a9b71c..a600c541a 100644
--- a/src/geb/geb.lisp
+++ b/src/geb/geb.lisp
@@ -97,7 +97,8 @@
          nat-sub
          nat-mult
          nat-div
-         nat-const)
+         nat-const
+         nat-mod)
      (nat-width (num x)))
     (otherwise
      (subclass-responsibility x))))
@@ -492,6 +493,7 @@ GEB> (gapply geb-bool:and
     (nat-sub   (- (car object) (cadr object)))
     (nat-div   (multiple-value-bind (q)
                    (floor (car object) (cadr object)) q))
+    (nat-mod   (mod (car object) (cadr object)))
     (nat-const  (pos morph))
     (nat-inj    object)
     (nat-concat  (+ (* (expt 2 (num-right morph)) (car object)) (cadr object)))
diff --git a/src/geb/trans.lisp b/src/geb/trans.lisp
index a0fbfdd10..ba0792d32 100644
--- a/src/geb/trans.lisp
+++ b/src/geb/trans.lisp
@@ -328,6 +328,10 @@ get ((A x B) + (A x C)) as times appends sequences"
   "Division is interpreted as divition"
   (seqn-divide (geb.extension.spec:num obj)))
 
+(defmethod to-seqn ((obj geb.extension.spec:nat-mod))
+  "Modulo is interpreted as modulo"
+  (seqn-mod (geb.extension.spec:num obj)))
+
 (defmethod to-seqn ((obj geb.extension.spec:nat-const))
   "A choice of a natural number is the same exact choice in SeqN"
   (seqn-nat (geb.extension.spec:num obj) (geb.extension.spec:pos obj)))
diff --git a/src/lambda/lambda.lisp b/src/lambda/lambda.lisp
index f3dadd793..9bb6ae092 100644
--- a/src/lambda/lambda.lisp
+++ b/src/lambda/lambda.lisp
@@ -158,8 +158,12 @@ the context on the left as well. For more info check [LAMB][class]"))
                                             (ann-term1 ctx rtm)
                                             :ttype (coprod so1 so1)))
         ((lamb-lt ltm rtm)         (lamb-lt (ann-term1 ctx ltm)
+                                            (ann-term1 ctx rtm)
+                                            :ttype (coprod so1 so1)))
+        ((modulo ltm rtm)          (let ((ant (ann-term1 ctx ltm)))
+                                     (modulo ant
                                              (ann-term1 ctx rtm)
-                                             :ttype (coprod so1 so1)))
+                                             :ttype (ttype ant))))
         ((case-on on ltm rtm)
          (let* ((ann-on     (ann-term1 ctx on))
                 (type-of-on (ttype ann-on))
@@ -231,6 +235,7 @@ occurences - re-annotates the term and its subterms with actual
          times
          minus
          divide
+         modulo
          bit-choice
          lamb-eq
          lamb-lt)
@@ -319,13 +324,16 @@ nil"))
                                                    (mapcar #'ttype term)
                                                    :from-end t)
                                            (ttype tterm)))))
-               ((or (plus ltm rtm)
-                    (minus ltm rtm)
-                    (times ltm rtm)
-                    (divide ltm rtm)
-                    (lamb-eq ltm rtm)
-                    (lamb-lt ltm rtm))
-                (obj-equalp (ttype ltm) (ttype rtm)))
+               ((or plus
+                    minus
+                    divide
+                    times
+                    modulo)
+                (obj-equalp (ttype (ltm tterm))
+                            (ttype (rtm tterm))))
+               ((or lamb-eq
+                    lamb-lt)
+                t)
                (index t)
                (unit t)
                (err t)
@@ -356,7 +364,8 @@ nil"))
              (typep tterm 'times)
              (typep tterm 'divide)
              (typep tterm 'lamb-eq)
-             (typep tterm 'lamb-lt))
+             (typep tterm 'lamb-lt)
+             (typep tterm 'modulo))
          (or (errorp (ltm tterm))
              (errorp (rtm tterm))))
         (t                        (errorp (term tterm)))))
diff --git a/src/lambda/trans.lisp b/src/lambda/trans.lisp
index ae5d94293..623fe5bfc 100644
--- a/src/lambda/trans.lisp
+++ b/src/lambda/trans.lisp
@@ -83,7 +83,8 @@ error node"
     (times #'nat-mult)
     (divide #'nat-div)
     (lamb-eq #'nat-eq)
-    (lamb-lt #'nat-lt)))
+    (lamb-lt #'nat-lt)
+    (modulo #'nat-mod)))
 
 (defmethod to-cat-err (context (tterm <stlc>))
   "Compiles a checked term with an error term in an appropriate context into the
@@ -257,7 +258,8 @@ This follows from the fact that bool arapped in maybe is 1 + (bool + bool)"
                     times
                     divide
                     lamb-eq
-                    lamb-lt)
+                    lamb-lt
+                    modulo)
                 (let ((tyltm (ttype (ltm tterm))))
                   (labels ((arith (op)
                              (comp (mcase (terminal (prod (maybe tyltm)
@@ -392,7 +394,8 @@ iterated, so is the uncurrying."
                     times
                     divide
                     lamb-eq
-                    lamb-lt)
+                    lamb-lt
+                    modulo)
                 (let ((ltm (ltm tterm)))
                   (labels ((arith (op)
                              (comp (funcall op (num (ttype ltm)))
diff --git a/src/seqn/seqn.lisp b/src/seqn/seqn.lisp
index d034039d1..b4a897ca4 100644
--- a/src/seqn/seqn.lisp
+++ b/src/seqn/seqn.lisp
@@ -84,6 +84,7 @@ For a less formal desription consult the specs file"
     (seqn-subtract    (list (mcar x) (mcar x)))
     (seqn-multiply    (list (mcar x) (mcar x)))
     (seqn-divide      (list (mcar x) (mcar x)))
+    (seqn-mod         (list (mcar x) (mcar x)))
     (seqn-nat         (list 0))
     (seqn-concat      (list (mcar x) (mcadr x)))
     (seqn-decompose   (list (mcar x)))
@@ -119,6 +120,7 @@ For a less formal description consult the specs file"
     (seqn-multiply    (list (mcar x)))
     (seqn-divide      (list (mcar x)))
     (seqn-nat         (list (mcar x)))
+    (seqn-mod         (list (mcar x)))
     (seqn-concat      (list (+ (mcar x) (mcadr x))))
     (seqn-decompose   (list 1 (1- (mcar x))))
     (seqn-eq          (list 1 0))
@@ -167,6 +169,7 @@ is capable of succesfully evaluating all compiled terms"
     (seqn-multiply    (list (* (car vector) (cadr vector))))
     (seqn-divide      (list (multiple-value-bind (q)
                                 (floor (car vector) (cadr vector)) q)))
+    (seqn-mod         (list (mod (car vector) (cadr vector))))
     (seqn-nat         (list (mcadr morphism)))
     (seqn-concat      (list (+ (* (expt 2 (mcadr morphism)) (car vector))
                                (cadr vector))))
@@ -236,6 +239,7 @@ is capable of succesfully evaluating all compiled terms"
          seqn-multiply
          seqn-divide
          seqn-subtract
+         seqn-mod
          seqn-nat
          seqn-concat
          seqn-decompose
diff --git a/src/seqn/trans.lisp b/src/seqn/trans.lisp
index 92bc4f82f..4d24065fe 100644
--- a/src/seqn/trans.lisp
+++ b/src/seqn/trans.lisp
@@ -322,6 +322,15 @@ removed already and hence we cannot count as usual"
                                                     :rhs cadr))
               zero))))
 
+(defmethod to-vampir ((obj seqn-mod) inputs constraints)
+  (declare (ignore constraints))
+  (let ((car (car inputs))
+        (cadr (cadr inputs)))
+    (if (const-check inputs)
+        (list (vamp:make-constant :const (mod (vamp:const car) (vamp:const cadr))))
+        (list (geb.vampir:mod-n (vamp:make-constant :const (mcar obj))
+                                car cadr)))))
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Helpers
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
diff --git a/src/specs/extension.lisp b/src/specs/extension.lisp
index c59d7b01f..4310301d9 100644
--- a/src/specs/extension.lisp
+++ b/src/specs/extension.lisp
@@ -69,7 +69,7 @@ of natural numbers"))
 
 (deftype natmorph ()
   '(or nat-add nat-inj nat-mult nat-sub nat-div nat-const nat-concat
-       one-bit-to-bool nat-decompose nat-eq nat-lt))
+       one-bit-to-bool nat-decompose nat-eq nat-lt nat-mod))
 
 (defclass nat-width (<natobj>)
   ((num :initarg :num
@@ -233,6 +233,14 @@ which evaluated to true iff both inputs are the same"))
   (:documentation "Morphism nat-width n x nat-width n -> bool
 which evaluated to true iff the first input is less than the second"))
 
+(defclass nat-mod (<natmorph>)
+  ((num :initarg :num
+        :accessor num
+        :documentation ""))
+  (:documentation "Morphism nat-width n x nat-width n -> nat-width n
+which takes a modulo of the left projection of a pair by the second
+projection of a pari"))
+
 (defun nat-add (num)
   (values
    (make-instance 'nat-add :num num)))
@@ -284,6 +292,9 @@ which evaluated to true iff the first input is less than the second"))
 (defun nat-lt (num)
   (make-instance 'nat-lt :num num))
 
+(defun nat-mod (num)
+  (make-instance 'nat-mod :num num))
+
 (defgeneric num (obj))
 (defgeneric pos (obj))
 (defgeneric num-left (obj))
diff --git a/src/specs/lambda-printer.lisp b/src/specs/lambda-printer.lisp
index 3ce622c7b..e308742f1 100644
--- a/src/specs/lambda-printer.lisp
+++ b/src/specs/lambda-printer.lisp
@@ -25,3 +25,4 @@
 (easy-printer bit-choice)
 (easy-printer lamb-eq)
 (easy-printer lamb-lt)
+(easy-printer modulo)
diff --git a/src/specs/lambda.lisp b/src/specs/lambda.lisp
index 1f3ed53a0..4dcb321c0 100644
--- a/src/specs/lambda.lisp
+++ b/src/specs/lambda.lisp
@@ -11,7 +11,7 @@ unit types as well as coproduct, product, and function types."))
 which can be filled by auxillary functions or by user. Types are
 represented as [SUBSTOBJ][GEB.SPEC:SUBSTOBJ]."
   '(or absurd unit left right case-on pair fst snd lamb app index err
-    plus times minus divide bit-choice lamb-eq lamb-lt))
+    plus times minus divide bit-choice lamb-eq lamb-lt modulo))
 
 ;; New defgenerics
 
@@ -756,3 +756,33 @@ will be associated with the 0 input and teh second branch with 1."))
 (defun lamb-lt (ltm rtm &key (ttype nil))
   (values
    (make-instance 'lamb-lt :ltm ltm :rtm rtm :ttype ttype)))
+
+(defclass modulo (<stlc>)
+  ((ltm :initarg :ltm
+        :accessor ltm
+        :documentation "")
+   (rtm :initarg :rtm
+        :accessor rtm
+        :documentation "")
+   (ttype :initarg :ttype
+          :initform nil
+          :accessor ttype
+          :documentation ""))
+  (:documentation "A term representing syntactic modulus of the first number
+by the second number. The formal grammar of [MODULO] is
+
+```lisp
+(modulo ltm rtm)
+```
+
+where we can possibly supply typing info by
+
+```lisp
+(modulo ltm rtm :ttype ttype)
+```
+
+meaning that we take ltm mod rtm"))
+
+(defun modulo (ltm rtm &key (ttype nil))
+  (values
+   (make-instance 'modulo :ltm ltm :rtm rtm :ttype ttype)))
diff --git a/src/specs/package.lisp b/src/specs/package.lisp
index b152058fe..feeb96237 100644
--- a/src/specs/package.lisp
+++ b/src/specs/package.lisp
@@ -176,7 +176,8 @@ constructors"
   (seqn-concat      pax:class)
   (seqn-decompose   pax:class)
   (seqn-eq          pax:class)
-  (seqn-lt          pax:class))
+  (seqn-lt          pax:class)
+  (seqn-mod         pax:class))
 
 (pax:defsection @seqn-constructors (:title "Seqn Constructors")
   "Every accessor for each of the classes making up seqn"
@@ -203,7 +204,8 @@ constructors"
   (seqn-concat      pax:function)
   (seqn-decompose   pax:function)
   (seqn-eq          pax:function)
-  (seqn-lt          pax:function))
+  (seqn-lt          pax:function)
+  (seqn-mod         pax:function))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Geb lambda Package Documentation
@@ -237,6 +239,7 @@ constructors"
   (bit-choice pax:class)
   (lamb-eq pax:class)
   (lamb-lt pax:class)
+  (modulo  pax:class)
 
   (absurd pax:function)
   (unit pax:function)
@@ -257,6 +260,7 @@ constructors"
   (bit-choice pax:function)
   (lamb-eq    pax:function)
   (lamb-lt    pax:function)
+  (absurd     pax:function)
   
 
   "Accessors of [ABSURD][class]"
@@ -348,6 +352,11 @@ constructors"
   (rtm   (pax:method () (lamb-lt)))
   (ttype (pax:method () (lamb-lt)))
 
+  "Accessors of [MODULO][class]"
+  (ltm   (pax:method () (modulo)))
+  (rtm   (pax:method () (modulo)))
+  (ttype (pax:method () (modulo)))
+
   (tcod pax:generic-function)
   (tdom pax:generic-function)
   (term pax:generic-function)
@@ -579,6 +588,7 @@ throughout any piece of code"
   (nat-decompose   pax:class)
   (nat-eq          pax:class)
   (nat-lt          pax:class)
+  (nat-mod         pax:class)
 
   (num       (pax:method () (nat-add)))
   (num       (pax:method () (nat-mult)))
@@ -592,6 +602,7 @@ throughout any piece of code"
   (num       (pax:method () (nat-decompose)))
   (num       (pax:method () (nat-eq)))
   (num       (pax:method () (nat-lt)))
+  (num       (pax:method () (nat-mod)))
 
   (nat-add         pax:function)
   (nat-mult        pax:function)
@@ -604,6 +615,7 @@ throughout any piece of code"
   (nat-decompose   pax:function)
   (nat-eq          pax:function)
   (nat-lt          pax:function)
+  (nat-mod         pax:function)
 
   (num          pax:generic-function)
   (pos          pax:generic-function)
diff --git a/src/specs/seqn-printer.lisp b/src/specs/seqn-printer.lisp
index b6b8bcd86..89b12afba 100644
--- a/src/specs/seqn-printer.lisp
+++ b/src/specs/seqn-printer.lisp
@@ -30,3 +30,4 @@
 (easy-printer seqn-decompose)
 (easy-printer seqn-eq)
 (easy-printer seqn-lt)
+(easy-printer seqn-mod)
diff --git a/src/specs/seqn.lisp b/src/specs/seqn.lisp
index a5120b087..28613dd55 100644
--- a/src/specs/seqn.lisp
+++ b/src/specs/seqn.lisp
@@ -4,7 +4,7 @@
   '(or composition id fork-seq drop-nil remove-right remove-left drop-width
     inj-length-left inj-length-right inj-size branch-seq shift-front zero-bit
     one-bit parallel-seq seqn-add seqn-subtract seqn-multiply seqn-divide
-    seqn-nat seqn-concat seqn-decompose seqn-lt seqn-eq))
+    seqn-nat seqn-concat seqn-decompose seqn-lt seqn-eq seqn-mod))
 
 (defclass <seqn> (geb.mixins:direct-pointwise-mixin cat-morph) ()
   (:documentation "Seqn is a category whose objects are finite sequences of natural numbers.
@@ -262,6 +262,15 @@ seqn-eq n : (n, n) -> (1, 0) with the intended semantics being
 that the morphism takes two n-bit integers and produces 1 iff the first
 one is less than the second"))
 
+(defclass seqn-mod (<seqn>)
+  ((mcar :initarg :mcar
+         :accessor mcar
+         :documentation ""))
+  (:documentation " The type signature of the morphism is
+seqn-mod n : (n, n) -> (n) with the intended semantics being
+that the morphism takes two n-bit integers and produces the
+modulo of the first integer by the second"))
+
 (serapeum:-> composition (<seqn> <seqn>) composition)
 (defun composition (mcar mcadr)
   (values
@@ -378,6 +387,11 @@ one is less than the second"))
   (values
    (make-instance 'seqn-lt :mcar mcar)))
 
+(serapeum:-> seqn-mod (fixnum) seqn-mod)
+(defun seqn-mod (mcar)
+  (values
+   (make-instance 'seqn-mod :mcar mcar)))
+
 (make-pattern composition mcar mcadr)
 (make-pattern id mcar)
 (make-pattern fork-seq mcar)
@@ -402,4 +416,5 @@ one is less than the second"))
 (make-pattern seqn-decompose)
 (make-pattern seqn-eq)
 (make-pattern seqn-lt)
+(make-pattern seqn-mod)
 
diff --git a/src/vampir/package.lisp b/src/vampir/package.lisp
index faca31077..c8b70e29b 100644
--- a/src/vampir/package.lisp
+++ b/src/vampir/package.lisp
@@ -103,5 +103,8 @@
     :pwmod32
 
     :*range-n*
-    :range-n)))
+    :range-n
+
+    :*mod-n*
+    :mod-n)))
 
diff --git a/src/vampir/vampir.lisp b/src/vampir/vampir.lisp
index 139b27d3b..81886b92e 100644
--- a/src/vampir/vampir.lisp
+++ b/src/vampir/vampir.lisp
@@ -245,6 +245,74 @@
   (make-application :func :negative
                     :arguments (list n a)))
 
+(defparameter *nonnegative*
+  (make-alias
+   :name :nonnegative
+   :inputs (list :n :a)
+   :body
+   (list (make-infix :op :-
+                     :lhs  (make-constant :const 1)
+                     :rhs (make-application
+                           :func :negative
+                           :arguments (list (make-constant :const :n)
+                                            (make-wire :var :a)))))))
+
+(defun nonnegative (n a)
+  (make-application :func :nonnegative
+                    :arguments (list n a)))
+
+(defparameter *mod-n*
+  (let ((numb   (make-constant :const :n))
+        (a-wire (make-wire :var :a))
+        (b-wire (make-wire :var :b))
+        (q-wire (make-wire :var :q))
+        (r-wire (make-wire :var :r)))
+    (make-alias :name :mod32
+                :inputs (list :n :a :b)
+                :body (list
+                       (make-equality
+                        :lhs (make-application :func :nonnegative
+                                               :arguments (list numb b-wire))
+                        :rhs (make-constant :const 0))
+                       (make-bind
+                        :names (list q-wire)
+                        :value (make-application
+                                :func :fresh
+                                :arguments (list (make-infix :op :/
+                                                             :lhs a-wire
+                                                             :rhs b-wire))))
+                       (make-bind
+                        :names (list r-wire)
+                        :value (make-application
+                                :func :fresh
+                                :arguments (list (make-infix :op :%
+                                                             :lhs a-wire
+                                                             :rhs b-wire))))
+                       (make-equality :lhs (make-application
+                                            :func :nonnegative
+                                            :arguments (list numb r-wire))
+                                      :rhs (make-constant :const :0))
+                       (make-equality :lhs a-wire
+                                      :rhs (make-infix
+                                            :op :+
+                                            :lhs (make-infix :op :*
+                                                             :lhs b-wire
+                                                             :rhs q-wire)
+                                            :rhs q-wire))
+                       (make-equality :lhs (make-application
+                                            :func :negative
+                                            :arguments
+                                            (list numb
+                                                  (make-infix :op :-
+                                                              :lhs r-wire
+                                                              :rhs b-wire)))
+                                      :rhs (make-constant :const 0))
+                       r-wire))))
+
+(defun mod-n (n a b)
+  (make-application :func :mod-n
+                    :arguments (list n a b)))
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Primitive operations with range checks
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -607,7 +675,9 @@
    *take-ind*
    *take*
    *drop-ith-rec*
-   *drop-ith*))
+   *drop-ith*
+   *nonnegative*
+   *mod-n*))
 
 (-> extract (list &optional (or null stream)) (or null stream))
 (defun extract (stmts &optional (stream *standard-output*))