feat: support assembly implementation of euc

DavePearce · DavePearce · commit 585202344d07 · 2025-11-14T13:54:26.000+13:00
This puts in place an assembly implementation of the euc module, thereby
replacing the original.
diff --git a/Makefile b/Makefile
@@ -34,7 +34,7 @@ EC_DATA_LONDON := ecdata/london
 
 EC_DATA_OSAKA := ecdata/osaka
 
-EUC := euc
+EUC := euc/euc.zkasm
 
 EXP := exp/exp.zkasm
 
diff --git a/blockdata/cancun/lookups/blockdata_into_euc.lisp b/blockdata/cancun/lookups/blockdata_into_euc.lisp
@@ -4,7 +4,6 @@
   (blockdata-into-euc :unchecked)
   ;; target columns
   (
-    euc.IOMF
     euc.DIVIDEND
     euc.DIVISOR
     euc.QUOTIENT
@@ -13,7 +12,6 @@
   (blockdata-into-euc-selector)
   ;; source columns
   (
-    1
     blockdata.ARG_1_LO
     blockdata.ARG_2_LO
     blockdata.RES
diff --git a/blockdata/london/lookups/blockdata_into_euc.lisp b/blockdata/london/lookups/blockdata_into_euc.lisp
@@ -4,7 +4,6 @@
   (blockdata-into-euc :unchecked)
   ;; target columns
   (
-    euc.IOMF
     euc.DIVIDEND
     euc.DIVISOR
     euc.QUOTIENT
@@ -13,7 +12,6 @@
   (blockdata-into-euc-selector)
   ;; source columns
   (
-    1
     blockdata.ARG_1_LO
     blockdata.ARG_2_LO
     blockdata.RES
diff --git a/blockdata/paris/lookups/blockdata_into_euc.lisp b/blockdata/paris/lookups/blockdata_into_euc.lisp
@@ -4,7 +4,6 @@
   (blockdata-into-euc :unchecked)
   ;; target columns
   (
-    euc.IOMF
     euc.DIVIDEND
     euc.DIVISOR
     euc.QUOTIENT
@@ -13,7 +12,6 @@
   (blockdata-into-euc-selector)
   ;; source columns
   (
-    1
     blockdata.ARG_1_LO
     blockdata.ARG_2_LO
     blockdata.RES
diff --git a/euc/columns.lisp b/euc/columns.lisp
diff --git a/euc/constraints.lisp b/euc/constraints.lisp
diff --git a/euc/euc.zkasm b/euc/euc.zkasm
@@ -0,0 +1,30 @@
+;; The Tiny Euclidean Division Module (EUC) is used for checking small
+;; (64-bit) divisions are correct.  In addition, the function computes
+;; a ceiling for the quotient.  NOTE: the function does not permit a
+;; zero divisor
+fn euc(DIVIDEND u64, DIVISOR=1 u64, QUOTIENT u64, REMAINDER u64) -> (CEIL u64)
+;; PRE: DIVISOR!=0
+{
+   var val_hi, val_lo u64
+   var tmp u64
+   var b, c u1
+   ;; assert divisor is non-zero
+   if DIVISOR == 0 goto exit_f
+   ;; reconstruct value from quotient / remainder
+   val_hi,val_lo = (QUOTIENT * DIVISOR) + REMAINDER
+   ;; assert value is consistent
+   if val_hi != 0 goto exit_f
+   if val_lo != DIVIDEND goto exit_f
+   ;; assert remainder < divisor
+   b, tmp = DIVISOR - REMAINDER - 1
+   if b == 1 goto exit_f
+   ;; Compute ceiling
+   if REMAINDER == 0 goto exit_0
+   c, CEIL = QUOTIENT + 1
+   return
+exit_0:
+   CEIL = QUOTIENT
+   return
+exit_f:
+   fail
+}
diff --git a/euc/lookups/euc_into_wcp.lisp b/euc/lookups/euc_into_wcp.lisp
diff --git a/mmu/london/lookups/mmu_into_euc.lisp b/mmu/london/lookups/mmu_into_euc.lisp
@@ -10,7 +10,6 @@
     euc.QUOTIENT
     euc.REMAINDER
     euc.CEIL
-    euc.DONE
   )
   ;; source selector
   (mmu-to-euc-selector)
@@ -21,7 +20,6 @@
     mmu.prprc/EUC_QUOT
     mmu.prprc/EUC_REM
     mmu.prprc/EUC_CEIL
-    1
   ))
 
 
diff --git a/mmu/osaka/lookups/mmu_into_euc.lisp b/mmu/osaka/lookups/mmu_into_euc.lisp
@@ -10,7 +10,6 @@
     euc.QUOTIENT
     euc.REMAINDER
     euc.CEIL
-    euc.DONE
   )
   ;; source selector
   (mmu-to-euc-selector)
@@ -21,7 +20,6 @@
     mmu.prprc/EUC_QUOT
     mmu.prprc/EUC_REM
     mmu.prprc/EUC_CEIL
-    1
   ))
 
 
diff --git a/mxp/cancun/lookups/mxp_into_euc.lisp b/mxp/cancun/lookups/mxp_into_euc.lisp
@@ -11,7 +11,6 @@
     euc.DIVISOR
     euc.QUOTIENT
     euc.CEIL
-    euc.DONE
   )
   ;; source selector
   (mxp-to-euc-selector)
@@ -21,5 +20,4 @@
     mxp.computation/ARG_2_LO
     mxp.computation/RES_A
     mxp.computation/RES_B
-    1
   ))
diff --git a/txndata/cancun/lookups/txndata_into_euc.lisp b/txndata/cancun/lookups/txndata_into_euc.lisp
@@ -4,7 +4,6 @@
   (txndata-into-euc :unchecked)
   ; target columns
   (
-   euc.DONE
    euc.DIVIDEND
    euc.DIVISOR
    euc.QUOTIENT
@@ -14,7 +13,6 @@
   (txn-data-into-euc-selector)
   ; source columns
   (
-   1
    txndata.computation/ARG_1_LO
    txndata.computation/ARG_2_LO
    txndata.computation/EUC_QUOTIENT
diff --git a/txndata/london/lookups/txndata_into_euc.lisp b/txndata/london/lookups/txndata_into_euc.lisp
@@ -2,7 +2,6 @@
   (txndata-into-euc :unchecked)
   ; target columns
   (
-    euc.DONE
     euc.DIVIDEND
     euc.DIVISOR
     euc.QUOTIENT
@@ -11,7 +10,6 @@
   txndata.EUC_FLAG
   ; source columns
   (
-    1
     txndata.ARG_ONE_LO
     txndata.ARG_TWO_LO
     txndata.RES
diff --git a/txndata/osaka/lookups/txndata_into_euc.lisp b/txndata/osaka/lookups/txndata_into_euc.lisp
@@ -4,7 +4,6 @@
   (txndata-into-euc :unchecked)
   ; target columns
   (
-   euc.DONE
    euc.DIVIDEND
    euc.DIVISOR
    euc.QUOTIENT
@@ -14,7 +13,6 @@
   (txn-data-into-euc-selector)
   ; source columns
   (
-   1
    txndata.computation/ARG_1_LO
    txndata.computation/ARG_2_LO
    txndata.computation/EUC_QUOTIENT
diff --git a/txndata/prague/lookups/txndata_into_euc.lisp b/txndata/prague/lookups/txndata_into_euc.lisp
@@ -4,7 +4,6 @@
   (txndata-into-euc :unchecked)
   ; target columns
   (
-   euc.DONE
    euc.DIVIDEND
    euc.DIVISOR
    euc.QUOTIENT
@@ -14,7 +13,6 @@
   (txn-data-into-euc-selector)
   ; source columns
   (
-   1
    txndata.computation/ARG_1_LO
    txndata.computation/ARG_2_LO
    txndata.computation/EUC_QUOTIENT
diff --git a/txndata/shanghai/lookups/txndata_into_euc.lisp b/txndata/shanghai/lookups/txndata_into_euc.lisp
@@ -2,7 +2,6 @@
   (txndata-into-euc :unchecked)
   ;; target columns
   (
-    euc.DONE
     euc.DIVIDEND
     euc.DIVISOR
     euc.QUOTIENT
@@ -11,7 +10,6 @@
   txndata.EUC_FLAG
   ;; source columns
   (
-    1
     txndata.ARG_ONE_LO
     txndata.ARG_TWO_LO
     txndata.RES
