diff --git a/hub/constraints/generalities/context.lisp b/hub/constraints/generalities/context.lisp
index 9458b15f..2ada5763 100644
--- a/hub/constraints/generalities/context.lisp
+++ b/hub/constraints/generalities/context.lisp
@@ -14,9 +14,9 @@
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 
-;; (defconstraint setting-the-context-may-change-flag ()
+;; (defconstraint generalities---setting-the-CONTEXT_MAY_CHANGE-flag ()
 ;;                (begin
-;;                  (is-binary                             CMC)
+;;                  (is-binary                             CMC)  ;; column already declared :binary@prove
 ;;                  (hub-stamp-constancy                   CMC)
 ;;                  (if-zero TX_EXEC            (vanishes! CMC))
 ;;                  (if-not-zero PEEK_AT_STACK
diff --git a/hub/constraints/generalities/exceptions.lisp b/hub/constraints/generalities/exceptions.lisp
index 7c46792d..7823f7ee 100644
--- a/hub/constraints/generalities/exceptions.lisp
+++ b/hub/constraints/generalities/exceptions.lisp
@@ -42,28 +42,29 @@
 
 
 
-(defconstraint exception-flags-are-binary (:perspective stack)
-               (begin
-                 (is-binary  SUX     )
-                 (is-binary  SOX     )
-                 (is-binary  MXPX    )
-                 (is-binary  OOGX    )
-                 (is-binary  RDCX    )
-                 (is-binary  JUMPX   )
-                 (is-binary  STATICX )
-                 (is-binary  SSTOREX )
-                 (is-binary  ICPX    )
-                 (is-binary  MAXCSX  )
-                 (is-binary  OPCX    )
-                 ))
+;; ;; These columns are already marked binary@prove in their respective definitions
+;; (defconstraint   generalities---exceptions---stack-exception-flags-are-binary (:perspective stack)
+;;                  (begin
+;;                    (is-binary  SUX     )
+;;                    (is-binary  SOX     )
+;;                    (is-binary  MXPX    )
+;;                    (is-binary  OOGX    )
+;;                    (is-binary  RDCX    )
+;;                    (is-binary  JUMPX   )
+;;                    (is-binary  STATICX )
+;;                    (is-binary  SSTOREX )
+;;                    (is-binary  ICPX    )
+;;                    (is-binary  MAXCSX  )
+;;                    (is-binary  OPCX    )
+;;                    ))
 
 
-(defconstraint exception-flags-are-exclusive (:perspective stack)
-               (is-binary (exception_flag_sum)))
+(defconstraint   generalities---exceptions---stack-exception-flags-are-exclusive (:perspective stack)
+                 (is-binary (exception_flag_sum)))
 
 
-(defconstraint exception-flags-are-stack-constant (:perspective stack)
-               (stack-row-constancy  (weighted_exception_flag_sum)))
+(defconstraint   generalities---exceptions---exception-flags-are-stack-constant (:perspective stack)
+                 (stack-row-constancy  (weighted_exception_flag_sum)))
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -73,15 +74,15 @@
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 
-(defconstraint automatic-exception-flag-vanishing (:perspective stack)
-               (begin
-                 (eq!            INVALID_FLAG                                   OPCX)
-                 (if-zero        MXP_FLAG                                       (vanishes!    MXPX))
-                 (if-zero        JUMP_FLAG                                      (vanishes!    JUMPX))
-                 (if-zero        STATIC_FLAG                                    (vanishes!    STATICX))
-                 (if-not-zero    (-  INSTRUCTION    EVM_INST_RETURNDATACOPY)    (vanishes!    RDCX))
-                 (if-not-zero    (-  INSTRUCTION    EVM_INST_SSTORE)            (vanishes!    SSTOREX))
-                 (if-not-zero    (-  INSTRUCTION    EVM_INST_RETURN)            (vanishes!    (+ ICPX MAXCSX)))))
+(defconstraint   generalities---exceptions---automatic-stack-exception-flag-vanishing (:perspective stack)
+                 (begin
+                   (eq!            INVALID_FLAG                                   OPCX)
+                   (if-zero        MXP_FLAG                                       (vanishes!    MXPX))
+                   (if-zero        JUMP_FLAG                                      (vanishes!    JUMPX))
+                   (if-zero        STATIC_FLAG                                    (vanishes!    STATICX))
+                   (if-not-zero    (-  INSTRUCTION    EVM_INST_RETURNDATACOPY)    (vanishes!    RDCX))
+                   (if-not-zero    (-  INSTRUCTION    EVM_INST_SSTORE)            (vanishes!    SSTOREX))
+                   (if-not-zero    (-  INSTRUCTION    EVM_INST_RETURN)            (vanishes!    (+ ICPX MAXCSX)))))
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -91,11 +92,9 @@
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 ;; we deal with those constraints in context.lisp along side CMC
-
-;; (defconstraint exception_ahoy ()
-;;                (begin
-;;                  (is-binary                             XAHOY)
-;;                  (hub-stamp-constancy                   XAHOY)
-;;                  (if-zero TX_EXEC            (vanishes! XAHOY))
-;;                  (if-not-zero PEEK_AT_STACK
-;;                               (eq! (exception_flag_sum) XAHOY))))
+;; (defconstraint   generalities---exceptions---setting-the-EXCEPTIONS_AHOY-flag ()
+;;                  (begin
+;;                    (is-binary                             XAHOY)  ;; column already declared :binary@prove
+;;                    (hub-stamp-constancy                   XAHOY)
+;;                    (if-zero     TX_EXEC             (eq!  XAHOY  0))
+;;                    (if-not-zero PEEK_AT_STACK       (eq!  XAHOY  (exception_flag_sum)))))
diff --git a/hub/constraints/generalities/program_counter.lisp b/hub/constraints/generalities/program_counter.lisp
index d75b3676..a5b21e9c 100644
--- a/hub/constraints/generalities/program_counter.lisp
+++ b/hub/constraints/generalities/program_counter.lisp
@@ -1,16 +1,16 @@
 (module hub)
 
-(defconstraint PC-stamp-constancy ()
-               (begin
-                 (hub-stamp-constancy PC)
-                 (hub-stamp-constancy PC_NEW)))
+(defconstraint   generalities---program-counter---stamp-constancy ()
+                 (begin
+                   (hub-stamp-constancy PC)
+                   (hub-stamp-constancy PC_NEW)))
 
-(defconstraint PC-automatic-vanishing-outside-of-EXEC-phase ()
-               (if-zero TX_EXEC
-                        (begin
-                          (vanishes! PC)
-                          (vanishes! PC_NEW))))
+(defconstraint   generalities---program-counter---automatic-vanishing-outside-of-EXEC-phase ()
+                 (if-zero TX_EXEC
+                          (begin
+                            (vanishes! PC)
+                            (vanishes! PC_NEW))))
 
-(defconstraint PC-automatic-update (:guard PEEK_AT_STACK)
-               (if-zero (force-bin (+ stack/PUSHPOP_FLAG stack/JUMP_FLAG))
-                        (eq! PC_NEW (+ 1 PC))))
+(defconstraint   generalities---program-counter---automatic-update (:guard PEEK_AT_STACK)
+                 (if-zero (force-bin (+ stack/PUSHPOP_FLAG stack/JUMP_FLAG))
+                          (eq! PC_NEW (+ 1 PC))))