feat: module implem

Makefile

@@ -73,6 +73,9 @@ STP := stp/columns.lisp stp/constraints.lisp \
 
 TABLES := $(wildcard lookup_tables/tables/*lisp)
 
+TEUC := teuc/columns.lisp teuc/constraints.lisp #\
+	# lookup
+
 TRM := trm/columns.lisp trm/constraints.lisp
 
 TXN_DATA := txn_data/columns.lisp txn_data/constraints.lisp \
@@ -100,6 +103,7 @@ ZKEVM_MODULES := ${ALU} \
 	${STACK} \
 	${STP} \
 	${TABLES} \
+	${TEUC} \
 	${TRM} \
 	${TXN_DATA} \
 	${WCP}

teuc/columns.lisp

@@ -0,0 +1,18 @@
+(module teuc)
+
+(defcolumns 
+  (IOMF :binary)
+  (CT :byte)
+  (CT_MAX :byte)
+  (DIVIDEND :i8)
+  (DIVISOR :i8)
+  (QUOTIENT :i8)
+  (REST :i8)
+  (CEIL :i8)
+  (DONE :binary)
+  (DIVIDEND_BYTE :byte)
+  (DIVISOR_BYTE :byte)
+  (QUOTIENT_BYTE :byte)
+  (REST_BYTE :byte))
+
+

teuc/constraints.lisp

@@ -0,0 +1,40 @@
+(module teuc)
+
+(defconst 
+  MAX_INPUT_LENGTH 8)
+
+(defconstraint first-row (:domain {0})
+  (vanishes! IOMF))
+
+(defconstraint heartbeat ()
+  (if-zero IOMF
+           (begin (vanishes! DONE)
+                  (vanishes! (next CT)))
+           (begin (eq! (next IOMF) 1)
+                  (if-zero (- CT CT_MAX)
+                           (begin (vanishes! DONE)
+                                  (will-inc! CT 1))
+                           (begin (eq! DONE 1)
+                                  (vanishes! (next CT)))))))
+
+(defconstraint ctmax ()
+  (eq! (~ (- CT MAX_INPUT_LENGTH))
+       1))
+
+(defconstraint last-row (:domain {-1})
+  (eq! DONE 1))
+
+(defconstraint byte-decomposition ()
+  (begin (byte-decomposition CT DIVIDEND DIVIDEND_BYTE)
+         (byte-decomposition CT DIVISOR DIVISOR_BYTE)
+         (byte-decomposition CT QUOTIENT QUOTIENT_BYTE)
+         (byte-decomposition CT REST REST_BYTE)))
+
+(defconstraint result (:guard DONE)
+  (begin (eq! DIVIDEND
+              (+ (* DIVISOR QUOTIENT) REST))
+         (if-zero REST
+                  (eq! CEIL QUOTIENT)
+                  (eq! CEIL (+ QUOTIENT 1)))))
+
+