Merge pull request #618 from mir-protocol/asm_assertions

More basic ASM macros

evm/src/cpu/kernel/aggregator.rs

@@ -23,6 +23,7 @@ pub fn evm_constants() -> HashMap<String, U256> {
 #[allow(dead_code)] // TODO: Should be used once witness generation is done.
 pub(crate) fn combined_kernel() -> Kernel {
     let files = vec![
+        // include_str!("asm/assertions.asm"), // TODO: Should work once PR 619 is merged.
         include_str!("asm/basic_macros.asm"),
         include_str!("asm/exp.asm"),
         include_str!("asm/curve_mul.asm"),

evm/src/cpu/kernel/asm/assertions.asm

@@ -0,0 +1,82 @@
+// It is convenient to have a single panic routine, which we can jump to from
+// anywhere.
+global panic:
+    JUMPDEST
+    PANIC
+
+// Consumes the top element and asserts that it is zero.
+%macro assert_zero
+    %jumpi panic
+%endmacro
+
+// Consumes the top element and asserts that it is nonzero.
+%macro assert_nonzero
+    ISZERO
+    %jumpi panic
+%endmacro
+
+%macro assert_eq
+    EQ
+    %assert_nonzero
+%endmacro
+
+%macro assert_lt
+    // %assert_zero is cheaper than %assert_nonzero, so we will leverage the
+    // fact that (x < y) == !(x >= y).
+    GE
+    %assert_zero
+%endmacro
+
+%macro assert_le
+    // %assert_zero is cheaper than %assert_nonzero, so we will leverage the
+    // fact that (x <= y) == !(x > y).
+    GT
+    %assert_zero
+%endmacro
+
+%macro assert_gt
+    // %assert_zero is cheaper than %assert_nonzero, so we will leverage the
+    // fact that (x > y) == !(x <= y).
+    LE
+    %assert_zero
+%endmacro
+
+%macro assert_ge
+    // %assert_zero is cheaper than %assert_nonzero, so we will leverage the
+    // fact that (x >= y) == !(x < y).
+    LT
+    %assert_zero
+%endmacro
+
+%macro assert_eq_const(c)
+    %eq_const(c)
+    %assert_nonzero
+%endmacro
+
+%macro assert_lt_const(c)
+    // %assert_zero is cheaper than %assert_nonzero, so we will leverage the
+    // fact that (x < c) == !(x >= c).
+    %ge_const(c)
+    %assert_zero
+%endmacro
+
+%macro assert_le_const(c)
+    // %assert_zero is cheaper than %assert_nonzero, so we will leverage the
+    // fact that (x <= c) == !(x > c).
+    %gt_const(c)
+    %assert_zero
+%endmacro
+
+%macro assert_gt_const(c)
+    // %assert_zero is cheaper than %assert_nonzero, so we will leverage the
+    // fact that (x > c) == !(x <= c).
+    %le_const(c)
+    %assert_zero
+%endmacro
+
+%macro assert_ge_const(c)
+    // %assert_zero is cheaper than %assert_nonzero, so we will leverage the
+    // fact that (x >= c) == !(x < c).
+    %lt_const(c)
+    %assert_zero
+%endmacro

evm/src/cpu/kernel/asm/basic_macros.asm

@@ -26,6 +26,83 @@
     %endrep
 %endmacro
 
+%macro add_const(c)
+    // stack: input, ...
+    PUSH $c
+    ADD
+    // stack: input + c, ...
+%endmacro
+
+// Slightly inefficient as we need to swap the inputs.
+// Consider avoiding this in performance-critical code.
+%macro sub_const(c)
+    // stack: input, ...
+    PUSH $c
+    // stack: c, input, ...
+    SWAP1
+    // stack: input, c, ...
+    SUB
+    // stack: input - c, ...
+%endmacro
+
+%macro mul_const(c)
+    // stack: input, ...
+    PUSH $c
+    MUL
+    // stack: input * c, ...
+%endmacro
+
+// Slightly inefficient as we need to swap the inputs.
+// Consider avoiding this in performance-critical code.
+%macro div_const(c)
+    // stack: input, ...
+    PUSH $c
+    // stack: c, input, ...
+    SWAP1
+    // stack: input, c, ...
+    SUB
+    // stack: input / c, ...
+%endmacro
+
+%macro eq_const(c)
+    // stack: input, ...
+    PUSH $c
+    EQ
+    // stack: input == c, ...
+%endmacro
+
+%macro lt_const(c)
+    // stack: input, ...
+    PUSH $c
+    // stack: c, input, ...
+    GT // Check it backwards: (input < c) == (c > input)
+    // stack: input <= c, ...
+%endmacro
+
+%macro le_const(c)
+    // stack: input, ...
+    PUSH $c
+    // stack: c, input, ...
+    GE // Check it backwards: (input <= c) == (c >= input)
+    // stack: input <= c, ...
+%endmacro
+
+%macro gt_const(c)
+    // stack: input, ...
+    PUSH $c
+    // stack: c, input, ...
+    LT // Check it backwards: (input > c) == (c < input)
+    // stack: input >= c, ...
+%endmacro
+
+%macro ge_const(c)
+    // stack: input, ...
+    PUSH $c
+    // stack: c, input, ...
+    LE // Check it backwards: (input >= c) == (c <= input)
+    // stack: input >= c, ...
+%endmacro
+
 // If pred is zero, yields z; otherwise, yields nz
 %macro select
     // stack: pred, nz, z