diff --git a/ec_data/columns.lisp b/ec_data/columns.lisp index 6b98946a..0610ed7c 100644 --- a/ec_data/columns.lisp +++ b/ec_data/columns.lisp @@ -1,56 +1,47 @@ (module ec_data) -(defcolumns - STAMP - INDEX - CT_MIN - LIMB +(defcolumns + STAMP + INDEX + CT_MIN + LIMB + TYPE + (EC_RECOVER :binary) + (EC_ADD :binary) + (EC_MUL :binary) + (EC_PAIRING :binary) + TOTAL_PAIRINGS + ACC_PAIRINGS + (COMPARISONS :binary) + (EQUALITIES :binary) + (HURDLE :binary) + (PRELIMINARY_CHECKS_PASSED :binary) + (ALL_CHECKS_PASSED :binary) + SQUARE + CUBE + (BYTE_DELTA :byte) + ACC_DELTA + WCP_ARG1_HI + WCP_ARG1_LO + WCP_ARG2_HI + WCP_ARG2_LO + (WCP_INST :byte :display :opcode) + (WCP_RES :binary) + EXT_ARG1_HI + EXT_ARG1_LO + EXT_ARG2_HI + EXT_ARG2_LO + EXT_ARG3_HI + EXT_ARG3_LO + EXT_INST + EXT_RES_LO + EXT_RES_HI + (THIS_IS_NOT_ON_G2 :binary) + (THIS_IS_NOT_ON_G2_ACC :binary) + (SOMETHING_WASNT_ON_G2 :binary)) - TYPE - (EC_RECOVER :binary) - (EC_ADD :binary) - (EC_MUL :binary) - (EC_PAIRING :binary) - - TOTAL_PAIRINGS - ACC_PAIRINGS - - (COMPARISONS :binary) - (EQUALITIES :binary) - - (HURDLE :binary) - (PRELIMINARY_CHECKS_PASSED :binary) - (ALL_CHECKS_PASSED :binary) - - SQUARE - CUBE - - (BYTE_DELTA :byte) - ACC_DELTA - - WCP_ARG1_HI - WCP_ARG1_LO - WCP_ARG2_HI - WCP_ARG2_LO - WCP_INST - WCP_RES - - EXT_ARG1_HI - EXT_ARG1_LO - EXT_ARG2_HI - EXT_ARG2_LO - EXT_ARG3_HI - EXT_ARG3_LO - EXT_INST - EXT_RES_LO - EXT_RES_HI +;; aliases +(defalias + PCP PRELIMINARY_CHECKS_PASSED) - (THIS_IS_NOT_ON_G2 :binary) - (THIS_IS_NOT_ON_G2_ACC :binary) - (SOMETHING_WASNT_ON_G2 :binary) -) -;; aliases -(defalias - PCP PRELIMINARY_CHECKS_PASSED -) \ No newline at end of file diff --git a/ec_data/ecdata_into_wcp.lisp b/ec_data/ecdata_into_wcp.lisp index 628b886a..72f6558c 100644 --- a/ec_data/ecdata_into_wcp.lisp +++ b/ec_data/ecdata_into_wcp.lisp @@ -1,20 +1,22 @@ -(deflookup lookup-ec_data-into-wcp - ; target columns - ( - wcp.ARGUMENT_1_HI - wcp.ARGUMENT_1_LO - wcp.ARGUMENT_2_HI - wcp.ARGUMENT_2_LO - wcp.INST - wcp.RESULT_LO - ) - ; source columns - ( - ec_data.WCP_ARG1_HI - ec_data.WCP_ARG1_LO - ec_data.WCP_ARG2_HI - ec_data.WCP_ARG2_LO - ec_data.WCP_INST - ec_data.WCP_RES - ) -) +(deflookup + lookup-ec_data-into-wcp + ; target columns + ( + wcp.ARGUMENT_1_HI + wcp.ARGUMENT_1_LO + wcp.ARGUMENT_2_HI + wcp.ARGUMENT_2_LO + wcp.INST + wcp.RESULT + ) + ; source columns + ( + ec_data.WCP_ARG1_HI + ec_data.WCP_ARG1_LO + ec_data.WCP_ARG2_HI + ec_data.WCP_ARG2_LO + ec_data.WCP_INST + ec_data.WCP_RES + )) + + diff --git a/stp/lookups/stp_into_wcp.lisp b/stp/lookups/stp_into_wcp.lisp index 9bdd0bda..7d66e002 100644 --- a/stp/lookups/stp_into_wcp.lisp +++ b/stp/lookups/stp_into_wcp.lisp @@ -6,8 +6,7 @@ wcp.ARG_1_LO wcp.ARG_2_HI wcp.ARG_2_LO - wcp.RES_HI - wcp.RES_LO + wcp.RES wcp.INST ) ; source columns (in STP) @@ -16,7 +15,6 @@ (* stp.ARG_1_LO stp.WCP_FLAG) 0 (* stp.ARG_2_LO stp.WCP_FLAG) - 0 (* stp.RES_LO stp.WCP_FLAG) (* stp.EXO_INST stp.WCP_FLAG) )) diff --git a/txn_data/columns.lisp b/txn_data/columns.lisp index b2209c8c..83e8fbf9 100644 --- a/txn_data/columns.lisp +++ b/txn_data/columns.lisp @@ -41,7 +41,7 @@ OUTGOING_RLP_TXNRCPT WCP_ARG_ONE_LO WCP_ARG_TWO_LO - (WCP_RES_LO :binary) + (WCP_RES :binary) (WCP_INST :byte :display :opcode)) (defalias diff --git a/txn_data/constraints.lisp b/txn_data/constraints.lisp index 173b76b7..8360911a 100644 --- a/txn_data/constraints.lisp +++ b/txn_data/constraints.lisp @@ -284,7 +284,7 @@ (= WCP_ARG_TWO_LO (+ (value) (* (max_fee) (gas_limit)))) (= WCP_INST LT) - (vanishes! WCP_RES_LO))) + (vanishes! WCP_RES))) (defun (upfront_gas_cost_of_transaction) (if-not-zero TYPE0 @@ -302,7 +302,7 @@ (begin (= (shift WCP_ARG_ONE_LO 1) (gas_limit)) (= (shift WCP_ARG_TWO_LO 1) (upfront_gas_cost_of_transaction)) (= (shift WCP_INST 1) LT) - (vanishes! (shift WCP_RES_LO 1)))) + (vanishes! (shift WCP_RES 1)))) ;; epsilon is the remainder in the euclidean division of [T_g - g'] by 2 (defun (epsilon) @@ -315,7 +315,7 @@ (begin (= (shift WCP_ARG_ONE_LO 2) (- (gas_limit) LEFTOVER_GAS)) ;; (= (shift WCP_ARG_TWO_LO 2) ???) ;; unknown (= (shift WCP_INST 2) LT) - (vanishes! (shift WCP_RES_LO 2)) + (vanishes! (shift WCP_RES 2)) (is-binary (epsilon)))) ;; row i + 3 @@ -323,7 +323,7 @@ (begin (= (shift WCP_ARG_ONE_LO 3) REF_CNT) (= (shift WCP_ARG_TWO_LO 3) (shift WCP_ARG_TWO_LO 2)) (= (shift WCP_INST 3) LT) - ;; (= (shift WCP_RES_LO 3) ???) ;; unknown + ;; (= (shift WCP_RES 3) ???) ;; unknown )) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -334,21 +334,21 @@ (begin (= (shift WCP_ARG_ONE_LO 4) (max_fee)) (= (shift WCP_ARG_TWO_LO 4) BASEFEE) (= (shift WCP_INST 4) LT) - (= (shift WCP_RES_LO 4) 0))) + (= (shift WCP_RES 4) 0))) ;; row i + 5 (defun (type_2_comparing_max_fee_and_max_priority_fee) (begin (= (shift WCP_ARG_ONE_LO 5) (max_fee)) (= (shift WCP_ARG_TWO_LO 5) (max_priority_fee)) (= (shift WCP_INST 5) LT) - (= (shift WCP_RES_LO 5) 0))) + (= (shift WCP_RES 5) 0))) ;; row i + 6 (defun (type_2_computing_the_effective_gas_price) (begin (= (shift WCP_ARG_ONE_LO 6) (max_fee)) (= (shift WCP_ARG_TWO_LO 6) (+ (max_priority_fee) BASEFEE)) (= (shift WCP_INST 6) LT) - ;; (= (shift WCP_RES_LO 6) ???) ;; unknown + ;; (= (shift WCP_RES 6) ???) ;; unknown )) (defconstraint comparisons (:guard (first-row-trigger)) @@ -371,14 +371,14 @@ (= IGAS (- (gas_limit) (shift WCP_ARG_TWO_LO 1))) ;; constraining REFUND_AMOUNT - (if-zero (shift WCP_RES_LO 3) + (if-zero (shift WCP_RES 3) (= REF_AMT (+ LEFTOVER_GAS (shift WCP_ARG_TWO_LO 2))) (= REF_AMT (+ LEFTOVER_GAS REF_CNT))) ;; constraining GAS_PRICE (if-zero TYPE2 (= GAS_PRICE (gas_price)) - (if-zero (shift WCP_RES_LO 6) + (if-zero (shift WCP_RES 6) (= GAS_PRICE (+ (max_priority_fee) BASEFEE)) (= GAS_PRICE (max_fee)))))) diff --git a/txn_data/lookups/into_wcp.lisp b/txn_data/lookups/into_wcp.lisp index eefbf872..3464e726 100644 --- a/txn_data/lookups/into_wcp.lisp +++ b/txn_data/lookups/into_wcp.lisp @@ -6,8 +6,7 @@ wcp.ARGUMENT_1_LO wcp.ARGUMENT_2_HI wcp.ARGUMENT_2_LO - wcp.RESULT_HI - wcp.RESULT_LO + wcp.RESULT wcp.INST ) ; source columns @@ -16,8 +15,7 @@ txnData.WCP_ARG_ONE_LO 0 txnData.WCP_ARG_TWO_LO - 0 - txnData.WCP_RES_LO + txnData.WCP_RES txnData.WCP_INST )) diff --git a/wcp/columns.lisp b/wcp/columns.lisp index 4162ccfc..7056535c 100644 --- a/wcp/columns.lisp +++ b/wcp/columns.lisp @@ -2,15 +2,24 @@ (defcolumns WORD_COMPARISON_STAMP - (ONE_LINE_INSTRUCTION :binary) - COUNTER - (INST :display :opcode) + (COUNTER :byte) + (CT_MAX :byte) + (INST :byte :display :opcode) ARGUMENT_1_HI ARGUMENT_1_LO ARGUMENT_2_HI ARGUMENT_2_LO - RESULT_HI - RESULT_LO + (RESULT :binary) + (IS_LT :binary) + (IS_GT :binary) + (IS_SLT :binary) + (IS_SGT :binary) + (IS_EQ :binary) + (IS_ISZERO :binary) + (IS_GEQ :binary) + (IS_LEQ :binary) + (ONE_LINE_INSTRUCTION :binary) + (VARIABLE_LENGTH_INSTRUCTION :binary) (BITS :binary) (NEG_1 :binary) (NEG_2 :binary) @@ -35,12 +44,12 @@ (defalias STAMP WORD_COMPARISON_STAMP OLI ONE_LINE_INSTRUCTION + VLI VARIABLE_LENGTH_INSTRUCTION CT COUNTER ARG_1_HI ARGUMENT_1_HI ARG_1_LO ARGUMENT_1_LO ARG_2_HI ARGUMENT_2_HI ARG_2_LO ARGUMENT_2_LO - RES_HI RESULT_HI - RES_LO RESULT_LO) + RES RESULT) diff --git a/wcp/constraints.lisp b/wcp/constraints.lisp index 01f4fffb..945b59e0 100644 --- a/wcp/constraints.lisp +++ b/wcp/constraints.lisp @@ -1,244 +1,213 @@ (module wcp) +(defpurefun (if-eq-else A B then else) + (if-zero (- A B) + then + else)) + ;; opcode values -(defconst - LT 16 - GT 17 - SLT 18 - SGT 19 - EQ_ 20 - ISZERO 21 - LIMB_SIZE 16 - LIMB_SIZE_MINUS_ONE 15) - - -;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 2.1 heartbeat ;; -;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;; - - -;; 2.1.1) -(defconstraint forst-row (:domain {0}) (vanishes! STAMP)) - -;; 2.1.2) -(defconstraint stampIncrements () - (any! (will-inc! STAMP 0) - (will-inc! STAMP 1))) - -;; 2.1.3) -(defconstraint zeroRow (:guard (is-zero STAMP)) - (begin - (vanishes! OLI) - (vanishes! CT))) - -;; 2.1.4) -(defconstraint counterReset () +(defconst + LEQ 0x0E + GEQ 0x0F + LT 16 + GT 17 + SLT 18 + SGT 19 + EQ_ 20 + ISZERO 21 + LLARGE 16 + LLARGEMO 15) + +(defconstraint binarities () + (begin (is-binary NEG_1) + (is-binary NEG_2) + (is-binary RES) + (is-binary BITS) + (is-binary BIT_1) + (is-binary BIT_2) + (is-binary BIT_3) + (is-binary BIT_4) + (is-binary IS_ISZERO) + (is-binary IS_EQ) + (is-binary IS_LT) + (is-binary IS_GT) + (is-binary IS_LEQ) + (is-binary IS_GEQ) + (is-binary IS_SLT) + (is-binary IS_SGT))) + +(defun (flag-sum) + (+ (one-line-inst) (variable-length-inst))) + +(defun (weight-sum) + (+ (* LT IS_LT) + (* GT IS_GT) + (* SLT IS_SLT) + (* SGT IS_SGT) + (* EQ_ IS_EQ) + (* ISZERO IS_ISZERO) + (* GEQ IS_GEQ) + (* LEQ IS_LEQ))) + +(defun (one-line-inst) + (+ IS_EQ IS_ISZERO)) + +(defun (variable-length-inst) + (+ IS_LT IS_GT IS_LEQ IS_GEQ IS_SLT IS_SGT)) + +(defconstraint inst-decoding () + (if-zero STAMP + (vanishes! (flag-sum)) + (eq! (flag-sum) 1))) + +(defconstraint setting-flag () + (begin (eq! INST (weight-sum)) + (eq! OLI (one-line-inst)) + (eq! VLI (variable-length-inst)))) + +(defconstraint counter-constancies () + (begin (counter-constancy CT ARG_1_HI) + (counter-constancy CT ARG_1_LO) + (counter-constancy CT ARG_2_HI) + (counter-constancy CT ARG_2_LO) + (counter-constancy CT RES) + (counter-constancy CT INST) + (counter-constancy CT CT_MAX) + (counter-constancy CT BIT_3) + (counter-constancy CT BIT_4) + (counter-constancy CT NEG_1) + (counter-constancy CT NEG_2))) + +(defconstraint first-row (:domain {0}) + (vanishes! STAMP)) + +(defconstraint stamp-increments () + (any! (will-remain-constant! STAMP) (will-inc! STAMP 1))) + +(defconstraint counter-reset () (if-not-zero (will-remain-constant! STAMP) (vanishes! (next CT)))) -;; 2.1.5) +(defconstraint setting-ct-max () + (if-eq OLI 1 (vanishes! CT_MAX))) + (defconstraint heartbeat (:guard STAMP) - (if-zero OLI - ;; 2.1.5.a) - ;; If OLI == 0 - (if-eq-else CT LIMB_SIZE_MINUS_ONE - ;; 2.1.5.a).(ii) - ;; If CT == LIMB_SIZE_MINUS_ONE (i.e. 15) - (will-inc! STAMP 1) - ;; 2.1.5.a).(ii) - ;; If CT != LIMB_SIZE_MINUS_ONE (i.e. 15) - (begin (will-inc! CT 1) - (vanishes! (shift OLI 1)))) - ;; 2.1.5.a) - ;; If OLI == 1 - (will-inc! STAMP 1))) -;; 2.1.6) -(defconstraint lastRow (:domain {-1} :guard STAMP) - (if-zero OLI - (eq! CT LIMB_SIZE_MINUS_ONE))) - -;; stamp constancies -(defconstraint stamp-constancies () - (begin - (stamp-constancy STAMP ARG_1_HI) - (stamp-constancy STAMP ARG_1_LO) - (stamp-constancy STAMP ARG_2_HI) - (stamp-constancy STAMP ARG_2_LO) - (stamp-constancy STAMP RES_HI) - (stamp-constancy STAMP RES_LO) - (stamp-constancy STAMP INST))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 2.2 counter constancy ;; -;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + (if-eq-else CT CT_MAX (will-inc! STAMP 1) (will-inc! CT 1))) +(defconstraint ct-upper-bond () + (eq! (~ (- LLARGE CT)) + 1)) -(defconstraint counter-constancies () - (begin - (counter-constancy CT BIT_1) - (counter-constancy CT BIT_2) - (counter-constancy CT BIT_3) - (counter-constancy CT BIT_4) - (counter-constancy CT NEG_1) - (counter-constancy CT NEG_2))) - +(defconstraint lastRow (:domain {-1}) + (eq! CT CT_MAX)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; -;; 2.3 byte decompositions ;; +;; 2.6 byte decompositions ;; ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - - ;; byte decompositions (defconstraint byte_decompositions () - (begin - (byte-decomposition CT ACC_1 BYTE_1) - (byte-decomposition CT ACC_2 BYTE_2) - (byte-decomposition CT ACC_3 BYTE_3) - (byte-decomposition CT ACC_4 BYTE_4) - (byte-decomposition CT ACC_5 BYTE_5) - (byte-decomposition CT ACC_6 BYTE_6))) - -;; binary constraints -(defconstraint binary_constraints () - (begin - (is-binary BIT_1) - (is-binary BIT_2) - (is-binary BIT_3) - (is-binary BIT_4) - (is-binary BITS) - (is-binary NEG_1) - (is-binary NEG_2))) - -;; bytehood constraints: TODO - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; ;; -;; 2.4 ONE_LINE_INSTRUCTION constraints ;; -;; ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - - -;; 2.4.1), 2), 3) and 4) -(defconstraint oli-constraints () - (begin - (is-binary OLI) - (if-eq INST EQ_ (= OLI 1)) - (if-eq INST ISZERO (= OLI 1)) - (if-not-zero (* (- INST EQ_) (- INST ISZERO)) - (vanishes! OLI)))) - + (begin (byte-decomposition CT ACC_1 BYTE_1) + (byte-decomposition CT ACC_2 BYTE_2) + (byte-decomposition CT ACC_3 BYTE_3) + (byte-decomposition CT ACC_4 BYTE_4) + (byte-decomposition CT ACC_5 BYTE_5) + (byte-decomposition CT ACC_6 BYTE_6))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; -;; 2.5 BITS and sign bit constraints ;; +;; 2.7 BITS and sign bit constraints ;; ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - - -;; 2.5.1 DONE -;; 2.5.2 DONE -;; 2.5.3 -(defconstraint bits_and_negs (:guard STAMP) - (if-zero OLI - (if-zero CT - (begin - (= BYTE_1 (first-eight-bits-bit-dec)) - (= BYTE_3 (last-eight-bits-bit-dec)) - (= NEG_1 BITS) - (= NEG_2 (shift BITS 8)))))) +(defconstraint bits-and-negs (:guard (+ IS_SLT IS_SGT)) + (if-eq CT LLARGEMO + (begin (eq! (shift BYTE_1 (- 0 LLARGEMO)) + (first-eight-bits-bit-dec)) + (eq! (shift BYTE_3 (- 0 LLARGEMO)) + (last-eight-bits-bit-dec)) + (eq! NEG_1 + (shift BITS (- 0 LLARGEMO))) + (eq! NEG_2 + (shift BITS (- 0 7)))))) + +(defconstraint no-neg-if-small () + (if-not-zero (- CT_MAX LLARGEMO) + (begin (vanishes! NEG_1) + (vanishes! NEG_2)))) (defun (first-eight-bits-bit-dec) - (+ (* 128 BITS) - (* 64 (shift BITS 1)) - (* 32 (shift BITS 2)) - (* 16 (shift BITS 3)) - (* 8 (shift BITS 4)) - (* 4 (shift BITS 5)) - (* 2 (shift BITS 6)) - (shift BITS 7))) + (reduce + + (for i + [0 :7] + (* (^ 2 i) + (shift BITS + (- 0 (+ i 8))))))) (defun (last-eight-bits-bit-dec) - (+ (* 128 (shift BITS 8)) - (* 64 (shift BITS 9)) - (* 32 (shift BITS 10)) - (* 16 (shift BITS 11)) - (* 8 (shift BITS 12)) - (* 4 (shift BITS 13)) - (* 2 (shift BITS 14)) - (shift BITS 15))) - + (reduce + + (for i + [0 :7] + (* (^ 2 i) + (shift BITS (- 0 i)))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; ;; 2.6 target constraints ;; ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - - (defconstraint target-constraints () - (begin - (if-not-zero STAMP - (begin (if-eq-else ARG_1_HI ARG_2_HI - (= BIT_1 1) - (= BIT_1 0)) - (if-eq-else ARG_1_LO ARG_2_LO - (= BIT_2 1) - (= BIT_2 0)))) - (if-eq CT LIMB_SIZE_MINUS_ONE - (begin (= ACC_1 ARG_1_HI) - (= ACC_2 ARG_1_LO) - (= ACC_3 ARG_2_HI) - (= ACC_4 ARG_2_LO) - (= ACC_5 - (- (* (- (* 2 BIT_3) 1)(- ARG_1_HI ARG_2_HI)) - BIT_3)) - (= ACC_6 - (- (* (- (* 2 BIT_4) 1) - (- ARG_1_LO ARG_2_LO)) - BIT_4)))))) - + (begin (if-not-zero STAMP + (begin (if-eq-else ARG_1_HI ARG_2_HI (eq! BIT_1 1) (vanishes! BIT_1)) + (if-eq-else ARG_1_LO ARG_2_LO (eq! BIT_2 1) (vanishes! BIT_2)))) + (if-eq VLI 1 + (if-eq CT CT_MAX + (begin (eq! ACC_1 ARG_1_HI) + (eq! ACC_2 ARG_1_LO) + (eq! ACC_3 ARG_2_HI) + (eq! ACC_4 ARG_2_LO) + (eq! ACC_5 + (- (* (- (* 2 BIT_3) 1) + (- ARG_1_HI ARG_2_HI)) + BIT_3)) + (eq! ACC_6 + (- (* (- (* 2 BIT_4) 1) + (- ARG_1_LO ARG_2_LO)) + BIT_4))))) + (debug (if-eq IS_ISZERO 1 + (begin (vanishes! ARG_2_HI) + (vanishes! ARG_2_LO)))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; ;; 2.7 result constraints ;; ;; ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - ;; eq_ = [[1]] . [[2]] ;; gt_ = [[3]] + [[1]] . [[4]] ;; lt_ = 1 - eq - gt -(defun (eq_) (* BIT_1 BIT_2)) -(defun (gt_) (+ BIT_3 (* BIT_1 BIT_4))) -(defun (lt_) (- 1 (eq_) (gt_))) +(defun (eq_) + (* BIT_1 BIT_2)) +(defun (gt_) + (+ BIT_3 (* BIT_1 BIT_4))) -;; 2.7.1 -(defconstraint result_hi () (vanishes! RES_HI)) +(defun (lt_) + (- 1 (eq_) (gt_))) ;; 2.7.2 -(defconstraint result_lo (:guard STAMP) - (if-zero OLI - ;; 2.7.2.(b) - ;; If OLI == 0 - (begin (if-eq INST LT - (= RES_LO (lt_))) - (if-eq INST GT - (= RES_LO (gt_))) - (if-eq INST SLT - (if-eq-else NEG_1 NEG_2 - (= RES_LO (lt_)) - (= RES_LO NEG_1))) - (if-eq INST SGT - (if-eq-else NEG_1 NEG_2 - (= RES_LO (gt_)) - (= RES_LO NEG_2)))) - ;; 2.7.2.(a) - ;; If OLI == 1 - (= RES_LO (eq_)))) +(defconstraint result () + (begin (if-eq OLI 1 (eq! RES (eq_))) + (if-eq IS_LT 1 (eq! RES (lt_))) + (if-eq IS_GT 1 (eq! RES (gt_))) + (if-eq IS_LEQ 1 + (eq! RES (+ (lt_) (eq_)))) + (if-eq IS_GEQ 1 + (eq! RES (+ (gt_) (eq_)))) + (if-eq IS_LT 1 (eq! RES (lt_))) + (if-eq IS_SLT 1 + (if-eq-else NEG_1 NEG_2 (eq! RES (lt_)) (eq! RES NEG_1))) + (if-eq IS_SGT 1 + (if-eq-else NEG_1 NEG_2 (eq! RES (gt_)) (eq! RES NEG_2))))) + +