Skip to content

Commit

Permalink
feat: spec update
Browse files Browse the repository at this point in the history
  • Loading branch information
@letypequividelespoubelles
letypequividelespoubelles committed Dec 27, 2023
1 parent 12ed0a8 commit e3b72b3
Show file tree
Hide file tree
Showing 2 changed files with 177 additions and 148 deletions.
18 changes: 16 additions & 2 deletions wcp/columns.lisp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,14 +2,25 @@

(defcolumns
WORD_COMPARISON_STAMP
(ONE_LINE_INSTRUCTION :binary)
(COUNTER :byte)
(CT_MAX :byte)
(INST :display :opcode)
ARGUMENT_1_HI
ARGUMENT_1_LO
ARGUMENT_2_HI
ARGUMENT_2_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)
(MULTI_LINE_INSTRUCTION :binary)
(VARIABLE_LENGTH_INSTRUCTION :binary)
(BITS :binary)
(NEG_1 :binary)
(NEG_2 :binary)
Expand All @@ -28,12 +39,15 @@
(BIT_1 :binary)
(BIT_2 :binary)
(BIT_3 :binary)
(BIT_4 :binary))
(BIT_4 :binary)
WITNESS)

;; aliases
(defalias
STAMP WORD_COMPARISON_STAMP
OLI ONE_LINE_INSTRUCTION
MLI MULTI_LINE_INSTRUCTION
VLI VARIABLE_LENGTH_INSTRUCTION
CT COUNTER
ARG_1_HI ARGUMENT_1_HI
ARG_1_LO ARGUMENT_1_LO
Expand Down
307 changes: 161 additions & 146 deletions wcp/constraints.lisp
View file
Original file line number Diff line number Diff line change
@@ -1,86 +1,112 @@
(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))
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)
(+ IS_LT IS_GT IS_SLT IS_SGT IS_EQ IS_ISZERO IS_GEQ IS_LEQ))

(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 (multi-line-inst)
(+ IS_SLT IS_SGT))

(defun (variable-length-inst)
(+ IS_LT IS_GT IS_LEQ IS_GEQ))

(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! MLI (multi-line-inst))
(eq! VLI (variable-length-inst))))

;; 2.1.2)
(defconstraint stampIncrements ()
(any! (will-inc! STAMP 0) (will-inc! STAMP 1)))
(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))

;; 2.1.3)
(defconstraint zeroRow (:guard (is-zero STAMP))
(begin (vanishes! OLI)
(vanishes! CT)))
(defconstraint stamp-increments ()
(any! (will-remain-constant! STAMP) (will-inc! STAMP 1)))

;; 2.1.4)
(defconstraint counterReset ()
(defconstraint counter-reset ()
(if-not-zero (will-remain-constant! STAMP)
(vanishes! (next CT))))

;; 2.1.5)
(defconstraint setting-ct-max ()
(begin (if-eq OLI 1 (vanishes! CT_MAX))
(if-eq MLI 1 (eq! CT_MAX LLARGEMO))))

(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)
(stamp-constancy STAMP INST)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; 2.2 counter constancy ;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(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)))
(begin (if-eq-else CT CT_MAX (will-inc! STAMP 1) (will-inc! CT 1))
(eq! (* WITNESS (- LLARGE CT))
1)))

(defconstraint lastRow (:domain {-1})
(eq! CT CT_MAX))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; 2.3 byte decompositions ;;
;; 2.6 byte decompositions ;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; byte decompositions
Expand All @@ -92,65 +118,53 @@
(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))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; 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 MLI)
(if-eq CT CT_MAX
(begin (eq! BYTE_1 (first-eight-bits-bit-dec))
(eq! BYTE_3 (last-eight-bits-bit-dec))
(eq! NEG_1
(shift BITS (- LLARGEMO)))
(eq! NEG_2
(shift BITS (- 8))))))

(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)))
(+ (* 128
(shift BITS (- 15)))
(* 64
(shift BITS (- 14)))
(* 32
(shift BITS (- 13)))
(* 16
(shift BITS (- 12)))
(* 8
(shift BITS (- 11)))
(* 4
(shift BITS (- 10)))
(* 2
(shift BITS (- 9)))
(shift BITS (- 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)))
(+ (* 128
(shift BITS (- 7)))
(* 64
(shift BITS (- 6)))
(* 32
(shift BITS (- 5)))
(* 16
(shift BITS (- 4)))
(* 8
(shift BITS (- 3)))
(* 4
(shift BITS (- 2)))
(* 2
(shift BITS (- 1)))
BITS))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
Expand All @@ -161,19 +175,20 @@
(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))))))
(if-eq (+ MLI VLI) 1
(if-eq CT CT_MAX
(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)))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
Expand All @@ -193,18 +208,18 @@
(- 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 (lt_)))
(if-eq INST GT (= RES (gt_)))
(if-eq INST SLT
(if-eq-else NEG_1 NEG_2 (= RES (lt_)) (= RES NEG_1)))
(if-eq INST SGT
(if-eq-else NEG_1 NEG_2 (= RES (gt_)) (= RES NEG_2))))
;; 2.7.2.(a)
;; If OLI == 1
(= RES (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 (+ (lt_) (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 (lt_)) (eq! RES NEG_1)))))


0 comments on commit e3b72b3

Please sign in to comment.