Skip to content

Commit e2a5ffd

Browse files
DavePearceDavePearce
authored
feat: tweaking stdlib (#775)
* strengthen type of or! This strengthens the type of logical or to require that its parameters having loobean type. That just forces greater structure on the constraints. * fix benchmark tests Some of the benchmark tests needed to be updated in accordance with the stricter rules required by go-corset.
1 parent e7d3217 commit e2a5ffd

File tree

14 files changed

+171
-176
lines changed

14 files changed

+171
-176
lines changed

‎pkg/corset/ast/type.go‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -214,7 +214,7 @@ func (p *NativeType) AsUnderlying() sc.Type {
214214
func (p *NativeType) SubtypeOf(other Type) bool {
215215
if o, ok := other.(*NativeType); ok && p.datatype.SubtypeOf(o.datatype) {
216216
// An interpreted type can flow into an uninterpreted type.
217-
return (!o.loobean && !o.boolean) || p == o
217+
return (!o.loobean && !o.boolean) || (p.loobean == o.loobean && p.boolean == o.boolean)
218218
}
219219
//
220220
return false

‎pkg/corset/compiler/typing.go‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -373,7 +373,7 @@ func (p *typeChecker) typeCheckInvokeInModule(expr *ast.Invoke) (ast.Type, []Syn
373373
}
374374
// TODO: this is potentially expensive, and it would likely be good if we
375375
// could avoid it.
376-
body := signature.Apply(expr.Args, nil)
376+
body := signature.Apply(expr.Args, p.srcmap)
377377
// Dig out the type
378378
return p.typeCheckExpressionInModule(body)
379379
}

‎pkg/corset/stdlib.lisp‎

Lines changed: 5 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -13,10 +13,10 @@
1313
(defpurefun (if-zero cond then) (if (vanishes! cond) then))
1414
(defpurefun (if-zero cond then else) (if (vanishes! cond) then else))
1515

16-
(defpurefun (if-not-zero cond then) (if (force-bool cond) then))
17-
(defpurefun (if-not-zero cond then else) (if (force-bool cond) then else))
16+
(defpurefun (if-not-zero cond then) (if (as-bool cond) then))
17+
(defpurefun (if-not-zero cond then else) (if (as-bool cond) then else))
1818

19-
(defpurefun ((force-bool :𝔽@bool :force) x) x)
19+
(defpurefun ((as-bool :𝔽@bool :force) x) x)
2020
(defpurefun ((is-binary :𝔽@loob :force) e0) (* e0 (- 1 e0)))
2121

2222
(defpurefun ((force-bin :binary :force) x) x)
@@ -27,20 +27,16 @@
2727
;; !-suffix denotes loobean algebra (i.e. 0 == true)
2828
;; ~-prefix denotes normalized-functions (i.e. output is 0/1)
2929
(defpurefun (and a b) (* a b))
30-
(defpurefun ((or! :𝔽@loob) a b) (* a b))
30+
(defpurefun ((or! :𝔽@loob) (a :𝔽@loob) (b :𝔽@loob)) (* a b))
31+
(defpurefun ((or! :𝔽@loob) (a :𝔽@loob) (b :𝔽@loob) (c :𝔽@loob)) (* a b c))
3132
(defpurefun ((not :binary@bool :force) (x :binary)) (- 1 x))
3233

3334
(defpurefun ((eq! :𝔽@loob) x y) (- x y))
3435
(defpurefun ((neq! :binary@loob :force) x y) (not (~ (eq! x y))))
35-
(defunalias = eq!)
3636

3737
(defpurefun ((eq :binary@bool :force) x y) (- 1 (~ (eq! x y))))
3838
(defpurefun ((neq :𝔽@bool) x y) (- x y))
3939

40-
;; Variadic variations on and/or
41-
(defunalias any! *)
42-
(defunalias all *)
43-
4440
;; Boolean functions
4541
(defpurefun ((is-not-zero :binary@bool) x) (~ x))
4642
(defpurefun ((is-not-zero! :binary@loob :force) x) (- 1 (is-not-zero x)))

‎testdata/gas.lisp‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,7 @@
4848

4949
;; 2
5050
(defconstraint iomf-increments ()
51-
(any! (will-remain-constant! IOMF) (will-inc! IOMF 1)))
51+
(or! (will-remain-constant! IOMF) (will-inc! IOMF 1)))
5252

5353
;; 3
5454
(defconstraint iomf-vanishing-values ()

‎testdata/mmio.lisp‎

Lines changed: 22 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -179,30 +179,30 @@
179179
(eq! MMIO_INSTRUCTION (mmio_inst_weight)))
180180

181181
(defun (fast-op-flag-sum)
182-
(force-bool (+ IS_LIMB_VANISHES
183-
IS_LIMB_TO_RAM_TRANSPLANT
184-
IS_RAM_TO_LIMB_TRANSPLANT
185-
IS_RAM_TO_RAM_TRANSPLANT
186-
IS_RAM_VANISHES)))
182+
(+ IS_LIMB_VANISHES
183+
IS_LIMB_TO_RAM_TRANSPLANT
184+
IS_RAM_TO_LIMB_TRANSPLANT
185+
IS_RAM_TO_RAM_TRANSPLANT
186+
IS_RAM_VANISHES))
187187

188188
(defconstraint fast-op ()
189189
(eq! FAST (fast-op-flag-sum)))
190190

191191
(defun (slow-op-flag-sum)
192-
(force-bool (+ IS_LIMB_TO_RAM_ONE_TARGET
193-
IS_LIMB_TO_RAM_TWO_TARGET
194-
IS_RAM_TO_LIMB_ONE_SOURCE
195-
IS_RAM_TO_LIMB_TWO_SOURCE
196-
IS_RAM_TO_RAM_PARTIAL
197-
IS_RAM_TO_RAM_TWO_TARGET
198-
IS_RAM_TO_RAM_TWO_SOURCE
199-
IS_RAM_EXCISION)))
192+
(+ IS_LIMB_TO_RAM_ONE_TARGET
193+
IS_LIMB_TO_RAM_TWO_TARGET
194+
IS_RAM_TO_LIMB_ONE_SOURCE
195+
IS_RAM_TO_LIMB_TWO_SOURCE
196+
IS_RAM_TO_RAM_PARTIAL
197+
IS_RAM_TO_RAM_TWO_TARGET
198+
IS_RAM_TO_RAM_TWO_SOURCE
199+
IS_RAM_EXCISION))
200200

201201
(defconstraint slow-op ()
202202
(eq! SLOW (slow-op-flag-sum)))
203203

204204
(defun (op-flag-sum)
205-
(force-bool (+ (fast-op-flag-sum) (slow-op-flag-sum))))
205+
(+ (fast-op-flag-sum) (slow-op-flag-sum)))
206206

207207
(defconstraint no-stamp-no-op ()
208208
(eq! (op-flag-sum) (~ STAMP)))
@@ -220,13 +220,13 @@
220220
(eq! (weighted-exo-sum) (* (instruction-may-provide-exo-sum) EXO_SUM)))
221221

222222
(defun (instruction-may-provide-exo-sum)
223-
(force-bool (+ IS_LIMB_VANISHES
224-
IS_LIMB_TO_RAM_TRANSPLANT
225-
IS_LIMB_TO_RAM_ONE_TARGET
226-
IS_LIMB_TO_RAM_TWO_TARGET
227-
IS_RAM_TO_LIMB_TRANSPLANT
228-
IS_RAM_TO_LIMB_ONE_SOURCE
229-
IS_RAM_TO_LIMB_TWO_SOURCE)))
223+
(+ IS_LIMB_VANISHES
224+
IS_LIMB_TO_RAM_TRANSPLANT
225+
IS_LIMB_TO_RAM_ONE_TARGET
226+
IS_LIMB_TO_RAM_TWO_TARGET
227+
IS_RAM_TO_LIMB_TRANSPLANT
228+
IS_RAM_TO_LIMB_ONE_SOURCE
229+
IS_RAM_TO_LIMB_TWO_SOURCE))
230230

231231
;;
232232
;; Heartbeat
@@ -235,7 +235,7 @@
235235
(vanishes! MMIO_STAMP))
236236

237237
(defconstraint stamp-increment ()
238-
(any! (will-remain-constant! STAMP) (will-inc! STAMP 1)))
238+
(or! (will-remain-constant! STAMP) (will-inc! STAMP 1)))
239239

240240
(defconstraint stamp-reset-ct ()
241241
(if-not-zero (- STAMP (prev STAMP))

‎testdata/mmu.lisp‎

Lines changed: 18 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -256,7 +256,7 @@
256256
(defun (stamp-decrementing X)
257257
(if-not-zero (- STAMP
258258
(+ (prev STAMP) 1))
259-
(any! (remained-constant! X) (did-dec! X 1))))
259+
(or! (remained-constant! X) (did-dec! X 1))))
260260

261261
(defconstraint stamp-decrementings ()
262262
(begin (stamp-decrementing TOT)
@@ -307,22 +307,22 @@
307307
(* 13 IS_BLAKE)))
308308

309309
(defun (is-any-to-ram-with-padding)
310-
(force-bool (+ IS_ANY_TO_RAM_WITH_PADDING_SOME_DATA
311-
IS_ANY_TO_RAM_WITH_PADDING_PURE_PADDING)))
310+
(+ IS_ANY_TO_RAM_WITH_PADDING_SOME_DATA
311+
IS_ANY_TO_RAM_WITH_PADDING_PURE_PADDING))
312312

313313
(defun (inst-flag-sum)
314-
(force-bool (+ IS_MLOAD
315-
IS_MSTORE
316-
IS_MSTORE8
317-
IS_INVALID_CODE_PREFIX
318-
IS_RIGHT_PADDED_WORD_EXTRACTION
319-
IS_RAM_TO_EXO_WITH_PADDING
320-
IS_EXO_TO_RAM_TRANSPLANTS
321-
IS_RAM_TO_RAM_SANS_PADDING
322-
(is-any-to-ram-with-padding)
323-
IS_MODEXP_ZERO
324-
IS_MODEXP_DATA
325-
IS_BLAKE)))
314+
(+ IS_MLOAD
315+
IS_MSTORE
316+
IS_MSTORE8
317+
IS_INVALID_CODE_PREFIX
318+
IS_RIGHT_PADDED_WORD_EXTRACTION
319+
IS_RAM_TO_EXO_WITH_PADDING
320+
IS_EXO_TO_RAM_TRANSPLANTS
321+
IS_RAM_TO_RAM_SANS_PADDING
322+
(is-any-to-ram-with-padding)
323+
IS_MODEXP_ZERO
324+
IS_MODEXP_DATA
325+
IS_BLAKE))
326326

327327
(defun (weight-flag-sum)
328328
(+ (* MMU_INST_MLOAD IS_MLOAD)
@@ -348,9 +348,9 @@
348348
;; Micro Instruction writing row types
349349
;;
350350

351-
(defun (ntrv-row) (force-bool (+ NT_ONLY NT_FIRST NT_MDDL NT_LAST)))
352-
(defun (rzro-row) (force-bool (+ RZ_ONLY RZ_FIRST RZ_MDDL RZ_LAST)))
353-
(defun (zero-row) (force-bool (+ LZRO (rzro-row))))
351+
(defun (ntrv-row) (+ NT_ONLY NT_FIRST NT_MDDL NT_LAST))
352+
(defun (rzro-row) (+ RZ_ONLY RZ_FIRST RZ_MDDL RZ_LAST))
353+
(defun (zero-row) (+ LZRO (rzro-row)))
354354

355355
(defconstraint sum-row-flag ()
356356
(eq! (+ LZRO (ntrv-row) (rzro-row)) MICRO))

‎testdata/mod.lisp‎

Lines changed: 18 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -164,9 +164,9 @@
164164
(* THETA2 (beta))))
165165

166166
;; alisases for decoding inst
167-
(defun (flag_sum) (force-bool (+ IS_SMOD IS_MOD IS_SDIV IS_DIV)))
167+
(defun (flag_sum) (+ IS_SMOD IS_MOD IS_SDIV IS_DIV))
168168
(defun (weight_sum) (+ (* EVM_INST_SMOD IS_SMOD) (* EVM_INST_MOD IS_MOD) (* EVM_INST_SDIV IS_SDIV) (* EVM_INST_DIV IS_DIV)))
169-
(defun (signed_inst) (force-bool (+ IS_SMOD IS_SDIV)))
169+
(defun (signed_inst) (+ IS_SMOD IS_SDIV))
170170

171171
;; bit decompositions of the most significant bytes
172172
(defun (bit-dec-msb1) (+ (* 128 (shift MSB_1 -7))
@@ -189,12 +189,12 @@
189189

190190
(defun (set-negative zHi zLo yHi yLo)
191191
(if-not-zero yLo
192-
(begin (= zHi (- THETA2 yHi 1))
193-
(= zLo (- THETA2 yLo)))
192+
(begin (eq! zHi (- THETA2 yHi 1))
193+
(eq! zLo (- THETA2 yLo)))
194194
(begin (vanishes! zLo)
195195
(if-zero (* yHi (- THETA_SQUARED_OVER_TWO yHi))
196-
(= zHi yHi)
197-
(= zHi (- THETA2 yHi))))))
196+
(eq! zHi yHi)
197+
(eq! zHi (- THETA2 yHi))))))
198198

199199
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
200200
;; ;;
@@ -218,8 +218,7 @@
218218
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
219219

220220
(defconstraint oli-and-mli-exclusivity ()
221-
(eq! (force-bool (+ OLI MLI))
222-
(flag_sum)))
221+
(eq! (+ OLI MLI) (flag_sum)))
223222

224223
(defconstraint set-oli-and-mli (:guard STAMP)
225224
(if-zero ARG_2_HI
@@ -328,17 +327,17 @@
328327

329328
(defconstraint target-constraints (:guard STAMP)
330329
(if-eq CT MMEDIUMMO
331-
(begin (= ARG_1_HI
330+
(begin (eq! ARG_1_HI
332331
(+ (* THETA (ARG1_3)) (ARG1_2)))
333-
(= ARG_2_HI
332+
(eq! ARG_2_HI
334333
(+ (* THETA (ARG2_3)) (ARG2_2)))
335334
;
336-
(= (shift BYTE_1_3 -7) (bit-dec-msb1))
337-
(= (shift BYTE_2_3 -7) (bit-dec-msb2))
335+
(eq! (shift BYTE_1_3 -7) (bit-dec-msb1))
336+
(eq! (shift BYTE_2_3 -7) (bit-dec-msb2))
338337
;
339-
(= (+ (* (B_0) (Q_1)) (* (B_1) (Q_0)))
338+
(eq! (+ (* (B_0) (Q_1)) (* (B_1) (Q_0)))
340339
(+ (* THETA2 (alpha)) (* THETA (H_1)) (H_0)))
341-
(= (+ (* (B_0) (Q_3)) (* (B_1) (Q_2)) (* (B_2) (Q_1)) (* (B_3) (Q_0)))
340+
(eq! (+ (* (B_0) (Q_3)) (* (B_1) (Q_2)) (* (B_2) (Q_1)) (* (B_3) (Q_0)))
342341
(H_2))
343342
(vanishes! (+ (* (B_1) (Q_3))
344343
(* (B_2) (Q_2))
@@ -367,11 +366,11 @@
367366
(eq! (+ (Delta_0) (lt_0))
368367
(* (- (* 2 (lt_0)) 1)
369368
(- (B_0) (R_0))))
370-
(if-eq-else (B_3) (R_3) (= (eq_3) 1) (vanishes! (eq_3)))
371-
(if-eq-else (B_2) (R_2) (= (eq_2) 1) (vanishes! (eq_2)))
372-
(if-eq-else (B_1) (R_1) (= (eq_1) 1) (vanishes! (eq_1)))
373-
(if-eq-else (B_0) (R_0) (= (eq_0) 1) (vanishes! (eq_0)))
374-
(= 1
369+
(if-eq-else (B_3) (R_3) (eq! (eq_3) 1) (vanishes! (eq_3)))
370+
(if-eq-else (B_2) (R_2) (eq! (eq_2) 1) (vanishes! (eq_2)))
371+
(if-eq-else (B_1) (R_1) (eq! (eq_1) 1) (vanishes! (eq_1)))
372+
(if-eq-else (B_0) (R_0) (eq! (eq_0) 1) (vanishes! (eq_0)))
373+
(eq! 1
375374
(+ (lt_3)
376375
(* (eq_3) (lt_2))
377376
(* (eq_3) (eq_2) (lt_1))

0 commit comments

Comments
 (0)