Update bitwise chiplet constraints #180

Fumuran · 2023-02-27T19:25:01Z

Bitwise chiplet constraints have been updated, now they use variables.
Currently this is the only improvement that the syntax allows to make with these constraints.

tohrnii · 2023-02-27T21:59:32Z

@Overcastan I think there are a few more things we can do here. For e.g. since now we have list comprehension, we could redefine the shape of the trace in terms of groups, i.e.,

main: [s, a0, b0, a[4], b[4], zp, z, dummy]

And then we could use list comprehension and list folding to redefine a_aggr, b_aggr, a_and_b and a_xor_b. For e.g.:

let a_aggr = sum([2^i * a for (i, a) in (0..4, a)])
let b_aggr = sum([2^i * b for (i, b) in (0..4, b)])

It would be interesting to explore if there are other ways to make the constraints cleaner using other syntax we have planned for v0.3 as well.

Fumuran · 2023-02-28T00:04:12Z

Ah, indeed! I remembered that we have list comprehension, but I forgot that we also have list folding. Thank you!

Al-Kindi-0

Looks great @Overcastan !
Left just a few minor nits.

Al-Kindi-0 · 2023-02-28T16:15:34Z

air-script/tests/bitwise/bitwise.air

@@ -22,26 +22,28 @@ integrity_constraints:
    enf k1 * (s' - s) = 0

    # Enforce that input is decomposed into valid bits


nit: that the input

Al-Kindi-0 · 2023-02-28T16:17:48Z

air-script/tests/bitwise/bitwise.air

+    enf b_limb[0]^2 - b_limb[0] = 0
+    enf b_limb[1]^2 - b_limb[1] = 0
+    enf b_limb[2]^2 - b_limb[2] = 0
+    enf b_limb[3]^2 - b_limb[3] = 0

    # Enforce that the values in the column a in the first row should be the aggregation of the


nit: in the first row of column a.
I think it should be the first row of the current 8 row cycle, but I think this is probably too verbose.

Al-Kindi-0 · 2023-02-28T16:18:12Z

air-script/tests/bitwise/bitwise.air


    # Enforce that the values in the column a in the first row should be the aggregation of the
    # decomposed bit columns a0..a3.
-    enf k0 * (a - (2^0 * a0 + 2^1 * a1 + 2^2 * a2 + 2^3 * a3)) = 0
+    let a_aggr = sum([2^i * a for (i, a) in (0..4, a_limb)])
+    enf k0 * (a - a_aggr) = 0
    # Enforce that the values in the column b in the first row should be the aggregation of the


Similar comment to the one on a

Al-Kindi-0 · 2023-02-28T16:19:18Z

air-script/tests/bitwise/bitwise.air


    # Enforce that the values in the column a in the first row should be the aggregation of the
    # decomposed bit columns a0..a3.
-    enf k0 * (a - (2^0 * a0 + 2^1 * a1 + 2^2 * a2 + 2^3 * a3)) = 0
+    let a_aggr = sum([2^i * a for (i, a) in (0..4, a_limb)])
+    enf k0 * (a - a_aggr) = 0
    # Enforce that the values in the column b in the first row should be the aggregation of the
    # decomposed bit columns b0..b3.


nit: maybe " columns b" instead of "b0..b3"?

air-script/tests/bitwise/bitwise.air

bobbinth · 2023-03-01T01:58:40Z

air-script/tests/bitwise/bitwise.air

+    enf a_limb[0]^2 - a_limb[0] = 0
+    enf a_limb[1]^2 - a_limb[1] = 0
+    enf a_limb[2]^2 - a_limb[2] = 0
+    enf a_limb[3]^2 - a_limb[3] = 0


Do we not yet support something like this?:

enf a = a^2 for a in a_limb enf b = b^2 for b in b_limb

@bobbinth We don't. I forgot to open an issue for it. We were supposed to add support for this after list comprehension. Do you have a name suggestion for statements like these (maybe something along the lines of list comprehension)?

Could be "ConstraintComprehension" - but looks rather long.

I couldn't think of any better name than ConstraintComprehension either so went with it in the issue description (#187) tentatively.

grjte

Thanks @Overcastan this looks good! I left one minor nit inline.

Also, I think we should keep the old bitwise constraints file for testing purposes. Let's start collecting the vm constraints somewhere new.

Can you please make new top-level directories constraints/miden-vm and put this new bitwise.air file in there? We can collect all Miden VM constraints there for now. That way we can define the VM constraints using all of the syntax that will be implemented in v0.3 instead of being restricted to only what's implemented right now.

grjte · 2023-03-06T12:28:55Z

air-script/tests/bitwise/bitwise.air

+    # the aggregation of the decomposed bit columns `a_limb`.
+    let a_aggr = sum([2^i * a for (i, a) in (0..4, a_limb)])
+    enf k0 * (a - a_aggr) = 0
+    # Enforce that the value in the first row of column `b` of the current 8-row cycle should be 


nit: let's put a blank line above this comment so it's easier to read

tohrnii · 2023-03-07T07:44:22Z

constraints/miden-vm/bitwise.air

+    # indices.
+    let a_and_b = sum([2^i * a * b for (i, a, b) in (0..4, a_limb, b_limb)])
+    let a_xor_b = sum([2^i * (a + b - 2 * a * b) for (i, a, b) in (0..4, a_limb, b_limb)])
+    enf (1 - s) * (z - (zp * 16 + a_and_b)) + s * (z - (zp * 16 + a_xor_b)) = 0


Based on @bobbinth's suggestion in another PR, we could rewrite this as:

match enf: z = zp * 16 + a_and_b when !s z = zp * 16 + a_xor_b when s

Does this seem correct or did I make some mistake here?

Looks correct to me too. I'll update it right away, thank you!

The only thing I'd maybe change here is the order to be more like:

match enf: z = zp * 16 + a_xor_b when s z = zp * 16 + a_and_b when !s

tohrnii

Thank you @Overcastan, looks good to me. I left a few minor nits.

tohrnii · 2023-03-07T15:52:01Z

constraints/miden-vm/bitwise.air

+# Returns value aggregated from limbs
+fn aggregate(limb: vector[4]) -> scalar:
+    let result = sum([2^i * a for (i, a) in (0..4, limb)])
+    result


nit: Return statements would require return keyword. And maybe we can remove the result variable as well.

tohrnii · 2023-03-07T15:54:38Z

constraints/miden-vm/bitwise.air

+    enf check_binary([a_limb[i]]) for i in 0..4
+    enf check_binary([b_limb[i]]) for i in 0..4  


nit: Maybe we can rewrite this as:

enf check_binary([a]) for a in a_limb enf check_binary([b]) for b in b_limb

tohrnii · 2023-03-07T15:56:09Z

constraints/miden-vm/bitwise.air

+    let a_aggr = aggregate([a_limb])
+    enf a = a_aggr when k0


nit: Maybe we can remove a_aggr variable. aggregate([a_limb]) looks concise enough to me. Not a strong opinion though.

tohrnii · 2023-03-07T15:56:21Z

constraints/miden-vm/bitwise.air

+    let b_aggr = aggregate([b_limb])
+    enf b = b_aggr when k0


nit: Maybe we can remove b_aggr variable. aggregate([b_limb]) looks concise enough to me. Not a strong opinion though.

grjte

Thanks @Overcastan! I left one very minor nit inline, but I think things look good now with the use of evaluators and selectors.

One comment - we will probably want to rework this a bit according to the comments in #122 for supporting modularity, but I think we should do that separately in a future PR.

grjte · 2023-03-08T12:47:42Z

constraints/miden-vm/bitwise.air

+    # Enforce that for each row except the last, the aggregated output value must equal the
+    # previous aggregated output value in the next row.
+    enf z = zp' when k1


very minor nit: since constraints on z are written below and this constraint is really about the zp column, I would reverse this to enf zp' = z when k1

tohrnii

Thank you @Overcastan, looks good to me. I left a couple of minor nits.

tohrnii · 2023-03-08T18:05:42Z

constraints/miden-vm/bitwise.air

+
+    # Enforce that the value in the first row of column `a` of the current 8-row cycle should be 
+    # the aggregation of the decomposed bit columns `a_limb`.
+    enf a = aggregate([a_limb]) when k0


minor nit: I think it should be aggregate(a_limb) for functions. Sorry, I missed this last time.

tohrnii · 2023-03-08T18:05:54Z

constraints/miden-vm/bitwise.air

+
+    # Enforce that the value in the first row of column `b` of the current 8-row cycle should be 
+    # the aggregation of the decomposed bit columns `b_limb`.
+    enf b = aggregate([b_limb]) when k0


minor nit: I think it should be aggregate(b_limb) for functions. Sorry, I missed this last time.

Fumuran requested review from Al-Kindi-0, grjte and tohrnii February 27, 2023 19:25

Fumuran linked an issue Feb 27, 2023 that may be closed by this pull request

update MidenVM constraints for the bitwise chiplet (excludes multiset check constraints) #176

Closed

Fumuran force-pushed the andrew-bitwise-constraints branch from 26e933f to 694b0ea Compare February 28, 2023 13:38

Al-Kindi-0 reviewed Feb 28, 2023

View reviewed changes

bobbinth reviewed Mar 1, 2023

View reviewed changes

Fumuran requested review from bobbinth and Al-Kindi-0 March 2, 2023 10:44

grjte suggested changes Mar 6, 2023

View reviewed changes

Fumuran force-pushed the andrew-bitwise-constraints branch 2 times, most recently from 636fdc9 to 4aa1e2b Compare March 6, 2023 18:11

tohrnii reviewed Mar 7, 2023

View reviewed changes

Fumuran force-pushed the andrew-bitwise-constraints branch 2 times, most recently from c860d93 to cf22093 Compare March 7, 2023 15:17

Fumuran requested review from grjte and tohrnii March 7, 2023 15:17

tohrnii suggested changes Mar 7, 2023

View reviewed changes

refactor: update bitwise chiplet constraints

be073ac

Fumuran force-pushed the andrew-bitwise-constraints branch from cf22093 to be073ac Compare March 7, 2023 19:57

Fumuran requested a review from tohrnii March 7, 2023 21:22

grjte approved these changes Mar 8, 2023

View reviewed changes

grjte mentioned this pull request Mar 8, 2023

Bitwise constraints submodule refactor for modularity #213

Merged

tohrnii approved these changes Mar 8, 2023

View reviewed changes

grjte merged commit 3b033c4 into next Mar 9, 2023

grjte deleted the andrew-bitwise-constraints branch March 9, 2023 09:01

grjte mentioned this pull request Mar 9, 2023

Tracking PR for v0.3 release #175

Merged

grjte mentioned this pull request Mar 23, 2023

update MidenVM constraints for the bitwise chiplet (excludes multiset check constraints) #176

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Update bitwise chiplet constraints #180

Update bitwise chiplet constraints #180

Fumuran commented Feb 27, 2023

tohrnii commented Feb 27, 2023

Fumuran commented Feb 28, 2023

Al-Kindi-0 left a comment

Al-Kindi-0 Feb 28, 2023

Al-Kindi-0 Feb 28, 2023

Al-Kindi-0 Feb 28, 2023

Al-Kindi-0 Feb 28, 2023

bobbinth Mar 1, 2023

tohrnii Mar 1, 2023 •

edited

Loading

bobbinth Mar 1, 2023

tohrnii Mar 1, 2023

grjte left a comment

grjte Mar 6, 2023

tohrnii Mar 7, 2023

Fumuran Mar 7, 2023

bobbinth Mar 7, 2023

tohrnii left a comment

tohrnii Mar 7, 2023

tohrnii Mar 7, 2023

tohrnii Mar 7, 2023

tohrnii Mar 7, 2023

grjte left a comment

grjte Mar 8, 2023

tohrnii left a comment

tohrnii Mar 8, 2023

tohrnii Mar 8, 2023

		@@ -22,26 +22,28 @@ integrity_constraints:
		enf k1 * (s' - s) = 0

		# Enforce that input is decomposed into valid bits

		enf check_binary([a_limb[i]]) for i in 0..4
		enf check_binary([b_limb[i]]) for i in 0..4

Update bitwise chiplet constraints #180

Update bitwise chiplet constraints #180

Conversation

Fumuran commented Feb 27, 2023

tohrnii commented Feb 27, 2023

Fumuran commented Feb 28, 2023

Al-Kindi-0 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tohrnii Mar 1, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

grjte left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tohrnii left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

grjte left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tohrnii left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tohrnii Mar 1, 2023 •

edited

Loading