Write Hash Chiplet constraints in AirScript #215

Fumuran · 2023-03-13T12:14:26Z

Addressing: #202
This PR adds Hash Chiplet constraints.

tohrnii

Thank you @Overcastan. I left a few comments.

I am wondering if we should allow logical operators in intermediate variables and for intermediate variables? For e.g., should the following be valid?:

let a = s0 & !s1
let b = !a

tohrnii · 2023-03-13T13:19:52Z

constraints/miden-vm/hash.air

+ev hash_chiplet(main: [s[3], r, h[12], i]):
+
+    ## Instruction flags ##
+    let f_rpr = 1 - k0


Should we refactor this as:
let f_rpr = !k0

tohrnii · 2023-03-13T13:20:37Z

constraints/miden-vm/hash.air

+
+    ## Instruction flags ##
+    let f_rpr = 1 - k0
+    let f_bp = k2 * s[0] * (1 - s[1]) * (1 - s[2])


Should we rewrite this as:
let f_bp = k2 & s[0] & !s[1] & !s[2]

Should we declare an intermediate variable for k2 & s[0]?

As noted, I think we shouldn't make this change to variables yet, even though I like it. Instead, maybe we should add a binary_not helper function for now, like we have in Rust.

If we're doing this change, we should also define an intermediate variable for k0 * (1 - s[0]), and we should make sure there's a good comment with each variable definition.

Also, I think it would probably be really helpful to add a one line comment above each instruction flag definition.

I'm not sure why should we create intermediate variables for the k0 * (1 - s[0]) and similar expressions. I think in this case readability will be decreased since every row is described with set of selector values (e.g. # this flag is set to 1 when flags are (i, j, k) and ... ) and in this case it will be more difficult to keep track of the value of the first flag

I think you're imagining this in a different way from what we intended. If you were to follow this suggestion, it would be given a meaningful name, so we would have something like the following:

let last_row_and_s0 = k0 * s[0] let first_row_and_s0 = k2 * s[0]

But looking at this, I wonder if the most readable thing to do would actually be to rename the periodic columns like:

periodic_columns: cycle_row_7: [0, 0, 0, 0, 0, 0, 0, 1] cycle_row_6: [0, 0, 0, 0, 0, 0, 1, 0] cycle_row_0: [1, 0, 0, 0, 0, 0, 0, 0]

tohrnii · 2023-03-13T13:22:04Z

constraints/miden-vm/hash.air

+    let f_sout = k0 * (1 - s[0]) * (1 - s[1]) * s[2]
+    let f_out = k0 * (1 - s[0]) * (1 - s[1])
+    let f_out_next = k1 * (1 - s[0]') * (1 - s[1]')
+    let f_abp = k0 * s[0] * (1 - s[1]) * (1 - s[2])


Should we declare an intermediate variable for k0 & s[0]?

tohrnii · 2023-03-13T13:22:44Z

constraints/miden-vm/hash.air

+    let f_hout = k0 * (1 - s[0]) * (1 - s[1]) * (1 - s[2])
+    let f_sout = k0 * (1 - s[0]) * (1 - s[1]) * s[2]
+    let f_out = k0 * (1 - s[0]) * (1 - s[1])
+    let f_out_next = k1 * (1 - s[0]') * (1 - s[1]')


Should we rewrite this as:
let f_out_next = k1 & !s[0]' & !s[1]'

tohrnii · 2023-03-13T13:24:00Z

constraints/miden-vm/hash.air

+    # Enforce that when absorbing the next set of elements into the state during linear hash 
+    # computation (i.e. f_abp = 1) the first 4 elements (the capacity portion) are carried over to 
+    # the next row.
+    enf f_abp * (h[j]' - h[j]) for j in 0..4


This doesn't seem correct as there is no rhs?

Good catch! It should be equal 0. Thank you!

Note for the future - it might be nice to be able to combine constraint comprehension with selectors, e.g.

enf is_copied([h[j]]) for j in 0..4 when f_abp

What do you both think? (Or will this already be possible without extra work?)

@grjte I think @bobbinth suggested to write this as

ev foo(main: h[4]): enf is_copied(h) for h in h enf foo(h[4]) when f_abp

instead.

Also, should we write this as:

enf is_copied([h]) for h in h[0..4]

enf is_copied([h]) for h in h[0..4]
Yes, thank you.

ev foo(main: h[4]):
enf is_copied(h) for h in h
enf foo(h[4]) when f_abp

Yep, this is fine

Fumuran · 2023-03-13T13:59:33Z

Allowing logical operators in intermediate variables looks really useful, but won't this complicate the process of parsing and processing expressions?

grjte · 2023-03-13T14:25:29Z

Allowing logical operators in intermediate variables looks really useful, but won't this complicate the process of parsing and processing expressions?

I think this is a good idea and would be useful, but let's not do it now. Can we create an issue and put it in the "Nice to have" section of this tracking issue?

tohrnii · 2023-03-13T15:39:54Z

I think this is a good idea and would be useful, but let's not do it now. Can we create an issue and put it in the "Nice to have" section of this tracking issue?

Added #217

grjte

Looks good, thank you! I left some comments inline about ways to improve readability. I think perhaps we could be using selectors more aggressively

grjte · 2023-03-13T14:29:31Z

constraints/miden-vm/hash.air

+ev is_binary(main: [a]):
+    enf a^2 - a = 0
+
+### Bitwise Chiplet Air Constraints ###############################################################


nit: this should be "Hash Chiplet Air Constraints"

grjte · 2023-03-13T14:43:08Z

constraints/miden-vm/hash.air

@@ -0,0 +1,76 @@
+mod HashAir


nit: maybe this should be HashChipletAir (and in that case the other one should be BitwiseChipletAir). What do you think?

My thought was that this file contains constraints for general hash operations, that's why I thought that it's possible to name it just HashAir, but HashChipletAir better displays the essence of the entire script, so I agree with you, we should rename it to HashChipletAir.

grjte · 2023-03-13T14:47:59Z

constraints/miden-vm/hash.air

+
+    ## Instruction flags ##
+    let f_rpr = 1 - k0
+    let f_bp = k2 * s[0] * (1 - s[1]) * (1 - s[2])


As noted, I think we shouldn't make this change to variables yet, even though I like it. Instead, maybe we should add a binary_not helper function for now, like we have in Rust.

If we're doing this change, we should also define an intermediate variable for k0 * (1 - s[0]), and we should make sure there's a good comment with each variable definition.

Also, I think it would probably be really helpful to add a one line comment above each instruction flag definition.

grjte · 2023-03-13T14:50:57Z

constraints/miden-vm/hash.air

+    # Enforce that selector columns are binary.
+    enf is_binary([s_i]) for s_i in s
+    # Enforce that unless f_out = 1 or f_out' = 1, the values in columns s[1] and s[2] are copied 
+    # over to the nex row.
+    enf (s[1]' - s[1]) * (1 - f_out_next) * (1 - f_out) = 0
+    enf (s[2]' - s[2]) * (1 - f_out_next) * (1 - f_out) = 0
+    # Enforce that if any of f_abp, f_mpa, f_mva, f_mua flags is set to 1, the next value of s[0] 
+    # is 0.
+    enf s[0]' * (f_abp + f_mpa + f_mva + f_mua) = 0
+    # Enforce that no invalid combinations of flags are allowed.
+    enf k0 * (1 - s[0]) * s[1] = 0


Let's put more empty lines here to make it more readable (and do the same thing throughout the rest of the file). I would do it before each comment:

# Enforce that selector columns are binary. enf is_binary([s_i]) for s_i in s # Enforce that unless f_out = 1 or f_out' = 1, the values in columns s[1] and s[2] are copied # over to the nex row. enf (s[1]' - s[1]) * (1 - f_out_next) * (1 - f_out) = 0 enf (s[2]' - s[2]) * (1 - f_out_next) * (1 - f_out) = 0 # Enforce that if any of f_abp, f_mpa, f_mva, f_mua flags is set to 1, the next value of s[0] # is 0. enf s[0]' * (f_abp + f_mpa + f_mva + f_mua) = 0 # Enforce that no invalid combinations of flags are allowed. enf k0 * (1 - s[0]) * s[1] = 0

constraints/miden-vm/hash.air

grjte · 2023-03-13T15:09:18Z

constraints/miden-vm/hash.air

+    enf (s[1]' - s[1]) * (1 - f_out_next) * (1 - f_out) = 0
+    enf (s[2]' - s[2]) * (1 - f_out_next) * (1 - f_out) = 0


Since these are constraints rather than variables, can we make use of selectors to do the following?

enf s[1]' = s[1] when !f_out & !f_out_next enf s[2]' = s[2] when !f_out & !f_out_next

In fact, it might be best to make an is_copied function, because we check for that a lot in this module and you could use it elsewhere as well

enf is_copied([s[1]]) when !f_out & !f_out_next enf is_copied([s[2]]) when !f_out & !f_out_next

constraints/miden-vm/hash.air

grjte · 2023-03-13T15:32:11Z

constraints/miden-vm/hash.air

+    # Enforce that the value in i is copied over to the next row unless we are absorbing a new row 
+    # or the computation is finished.
+    enf (1 - f_an - f_out) * (i' - i) = 0


We could use is_copied and a selector here, which I think improves readability:

enf is_copied([i]) when 1 - f_an - f_out

Currently we only allow identifiers in when statements not expressions like 1 - f_an - f_out. Do you think we should allow expressions? (To me it doesn't look very clean but not a strong opinion). Maybe we could define another intermediate variable for 1 - f_an - f_out and use that.

Maybe we could define another intermediate variable for 1 - f_an - f_out and use that.

yep, I think this would be better

grjte · 2023-03-13T15:34:06Z

constraints/miden-vm/hash.air

+    # Enforce that when absorbing the next set of elements into the state during linear hash 
+    # computation (i.e. f_abp = 1) the first 4 elements (the capacity portion) are carried over to 
+    # the next row.
+    enf f_abp * (h[j]' - h[j]) for j in 0..4


Note for the future - it might be nice to be able to combine constraint comprehension with selectors, e.g.

enf is_copied([h[j]]) for j in 0..4 when f_abp

What do you both think? (Or will this already be possible without extra work?)

grjte · 2023-03-13T15:47:30Z

constraints/miden-vm/hash.air

+    # Enforce that when absorbing the next node during Merkle path computation 
+    # (i.e. f_mp + f_mv + f_mu = 1), the result of the previous hash (h[4], ..., h[7]) are copied 
+    # over either to (h[4]', ..., h[7]') or to (h[8]', ..., h[11]') depending on the value of b.
+    enf (f_mp + f_mv + f_mu) * ((1 - b) * (h[j + 4]' - h[j + 4]) + b * (h[j + 8]' - h[j + 4])) = 0


A few points here:

I think using a selector for the absorption flag would improve readability (when f_mp + f_mv + f_mu)

I think using is_copied would improve readability (e.g. is_copied([h[j+4]]))

I think using selectors for b and !b would improve readability. This would mean splitting it into 2 constraints using a match enf, one of which is enforced when !b & (f_mp + f_mv + f_mu) and the other of which is enforced when b & (f_mp + f_mv + f_mu).

It needs to be applied to the entire digest, but it looks like it's only being applied to the first element of the digest right now

I'm not sure I understand what do you mean by digest in this context. Can you explain in more detail?

The digest is the 4 field elements that make up the hash

tohrnii

Thank you @Overcastan, I just left a few comments. There is a recent change to logical operators and now they can be used in intermediate variables. Can you please refactor the code to incorporate that?

So, for example, something like:

let f_mpa = k0 * s[0] * binary_not(s[1]) * s[2]

can be re-written as

let f_mpa = k0 & s[0] & !s[1] & s[2]

Can you please also check in the memory chiplets PR if these changes need to be made?

tohrnii · 2023-03-16T00:23:04Z

constraints/miden-vm/hash.air

+
+# Enforce selector columns constraints
+ev selector_columns(main: [s[3]]):
+    # Set to 1 when either f_hout = 1 or f_sout = 1 in the current row.


f_hout and f_sout are undefined.

tohrnii · 2023-03-16T00:24:51Z

constraints/miden-vm/hash.air

+ev selector_columns(main: [s[3]]):
+    # Set to 1 when either f_hout = 1 or f_sout = 1 in the current row.
+    let f_out = k0 * binary_not(s[0]) * binary_not(s[1])
+    # Set to 1 when either f_hout = 1 or f_sout = 1 in the next row.


f_hout and f_sout are undefined.

nit: I'd add a blank line. I think by convention we should have a blank line between a constraint and if the next line is a comment. Wdyt?

Yes, I think we should always do this. I left a similar comment previously

My thought was to create some groups of constraints and variables, so it could be easier to determine what this constraint/variable should do by belonging to the certain group. But, I agree, it also decreases readability. I'm not sure what is more important. Your opinion is that we should add blank line every time, right?

tohrnii · 2023-03-16T00:31:28Z

constraints/miden-vm/hash.air

+    # Set to 1 when selector flags are (1,1,1) on rows which are multiples of 8.
+    let f_mu = k2 * s[0] * s[1] * s[2]
+
+    # Set to 1 when either f_hout = 1 or f_sout = 1 in the current row.


f_hout and f_sout are undefined.

grjte

Looks good, thanks @Overcastan. In addition to the things @tohrnii mentioned, I left a few things inline.

Also more generally - the comments on the flags tell when they're set, but it would be really helpful to include the semantic meaning as well.

For example:

    # Set to 1 when selector flags are (1,0,0) on rows which are 1 less than a multiple of 8.
    # Indicates the hash operation is absorption
    let f_abp = k0 * s[0] * binary_not(s[1]) * binary_not(s[2])

If you're not sure of the semantic meaning of the flags, feel free to message me

grjte · 2023-03-16T10:55:46Z

constraints/miden-vm/hash.air

+    return 1 - value
+
+
+# Enforces that value in column is copied over to the nex row.


nit: "next" instead of "nex"

grjte · 2023-03-16T10:57:07Z

constraints/miden-vm/hash.air

+# Enforces that column must be binary.
+ev is_binary(main: [a]):
+    enf a^2 - a = 0
+
+
+# Returns binary negation of the value.
+fn binary_not(value: scalar) -> scalar:
+    return 1 - value


Should we have a convention to group evaluators together and group functions together? I think it might be clearer in the long run. In that case, I would put the functions first, then the evaluators. Maybe we should even have separate headers for them "Helper functions" and "Helper evaluators" (though I'm not as sure about this). What do you think about either of these things?

I agree, I put function on the top in the Memory Chiplet for the same reason. Not sure about additional headers though. On the one hand functions and evaluators are very similar, so this separation is not needed. But on the other hand if we have a lot of functions and evaluators, it will be very convenient to have this separation. I'll make this separation for now, let's see how it will look like.

constraints/miden-vm/hash.air

grjte · 2023-03-16T11:01:05Z

constraints/miden-vm/hash.air

+    # TODO: once the support for combination of constraint comprehension and selectors is 
+    # implemented, update this constraint as:
+    # ```
+    # match enf:
+    #     is_copied(h[j + 4]) for j in 0..4 when !b & f_abs_node
+    #     h[j + 8]' = h[j + 4] for j in 0..4 when b & f_abs_node
+    # ```
+    enf f_abs_node * ((1 - b) * is_copied(h[j + 4]) + b * (h[j + 8]' - h[j + 4])) = 0 for j in 0..4


I don't think we need to wait, since this isn't going into the tests. I would just change this now:

match enf: is_copied(h[j + 4]) for j in 0..4 when !b & f_abs_node h[j + 8]' = h[j + 4] for j in 0..4 when b & f_abs_node

grjte · 2023-03-16T11:08:41Z

constraints/miden-vm/hash.air

+
+    ## Instruction flags ##
+    let f_rpr = 1 - k0
+    let f_bp = k2 * s[0] * (1 - s[1]) * (1 - s[2])


I think you're imagining this in a different way from what we intended. If you were to follow this suggestion, it would be given a meaningful name, so we would have something like the following:

let last_row_and_s0 = k0 * s[0] let first_row_and_s0 = k2 * s[0]

But looking at this, I wonder if the most readable thing to do would actually be to rename the periodic columns like:

periodic_columns: cycle_row_7: [0, 0, 0, 0, 0, 0, 0, 1] cycle_row_6: [0, 0, 0, 0, 0, 0, 1, 0] cycle_row_0: [1, 0, 0, 0, 0, 0, 0, 0]

grjte

Looks good, thank you! Just a couple of final comments about comments for the functions, then it will be ready to merge

grjte · 2023-03-28T09:11:10Z

constraints/miden-vm/hash.air

+    cycle_row_7: [0, 0, 0, 0, 0, 0, 0, 1]
+    cycle_row_6: [0, 0, 0, 0, 0, 0, 1, 0]
+    cycle_row_0: [1, 0, 0, 0, 0, 0, 0, 0]


nit: I would reorder these to put them in numerical order

cycle_row_0: [1, 0, 0, 0, 0, 0, 0, 0] cycle_row_6: [0, 0, 0, 0, 0, 0, 1, 0] cycle_row_7: [0, 0, 0, 0, 0, 0, 0, 1]

grjte · 2023-03-28T09:25:49Z

constraints/miden-vm/hash.air

+    # Flag f_out is set to 1 when either f_hout = 1 or f_sout = 1 in the current row.
+    let f_out = cycle_row_7 * binary_not(s[0]) * binary_not(s[1])
+
+    # Falg f_out_nextet is to 1 when either f_hout = 1 or f_sout = 1 in the next row.


nit: There are typos here. It should be "Flag f_out_next is set to 1..."

grjte · 2023-03-28T09:27:09Z

constraints/miden-vm/hash.air

+    # Set to 1 when selector flags are (1,0,0) on rows which are 1 less than a multiple of 8. This 
+    # is flag of the instruction that absorbs a new set of elements into the hasher state when 
+    # computing a linear hash of many elements.
+    let f_abp = get_f_abp(s)
+
+    # Set to 1 when selector flags are (1,0,1) on rows which are 1 less than a multiple of 8. This 
+    # is flag of the instruction that absorbs the next Merkle path node into the hasher state 
+    # during Merkle path verification computation.
+    let f_mpa = get_f_mpa(s)
+
+    # Set to 1 when selector flags are (1,1,0) on rows which are 1 less than a multiple of 8. This 
+    # is flag of the instruction that absorbs the next Merkle path node into the hasher state 
+    # during Merkle path verification for the "old" node value during Merkle root update 
+    # computation.
+    let f_mva = get_f_mva(s)
+
+    # Set to 1 when selector flags are (1,1,1) on rows which are 1 less than a multiple of 8. This 
+    # is flag of the instruction that absorbs the next Merkle path node into the hasher state 
+    # during Merkle path verification for the "new" node value during Merkle root update 
+    # computation.
+    let f_mua = get_f_mua(s)


Since we now have functions for all of these, can you move the comments about all of these flags to go above the function definitions instead? That will document the functions and also make this evaluator shorter and more readable

grjte · 2023-03-28T09:29:11Z

constraints/miden-vm/hash.air

+    # of the instruction that returns the whole hasher state.
+    #
+    # Flag f_out is set to 1 when either f_hout = 1 or f_sout = 1 in the current row.
+    let f_out = cycle_row_7 * binary_not(s[0]) * binary_not(s[1])


Should we make a helper function for f_out as well? Then this comment can go above the function definition and this evaluator and the ones below can be much smaller

grjte · 2023-03-28T09:30:17Z

constraints/miden-vm/hash.air

+    # Set to 1 when selector flags are (1,0,1) on rows which are multiples of 8. This is flag of 
+    # the instruction that initiates Merkle path verification computation.
+    let f_mp = get_f_mp(s)
+
+    # Set to 1 when selector flags are (1,1,0) on rows which are multiples of 8. This is flag of 
+    # the instruction that initiates Merkle path verification for the "old" node value during 
+    # Merkle root update computation.
+    let f_mv = get_f_mv(s)
+
+    # Set to 1 when selector flags are (1,1,1) on rows which are multiples of 8. This is flag of 
+    # the instruction that initiates Merkle path verification for the "new" node value during
+    # Merkle root update computation.
+    let f_mu = get_f_mu(s)
+
+    # Set to 1 when selector flags are (1,0,1) on rows which are 1 less than a multiple of 8. This 
+    # is flag of the instruction that absorbs the next Merkle path node into the hasher state 
+    # during Merkle path verification computation.
+    let f_mpa = get_f_mpa(s)
+
+    # Set to 1 when selector flags are (1,1,0) on rows which are 1 less than a multiple of 8. This 
+    # is flag of the instruction that absorbs the next Merkle path node into the hasher state 
+    # during Merkle path verification for the "old" node value during Merkle root update 
+    # computation.
+    let f_mva = get_f_mva(s)
+
+    # Set to 1 when selector flags are (1,1,1) on rows which are 1 less than a multiple of 8. This 
+    # is flag of the instruction that absorbs the next Merkle path node into the hasher state 
+    # during Merkle path verification for the "new" node value during Merkle root update 
+    # computation.
+    let f_mua = get_f_mua(s)


Similar to my previous comment - let's put all of these comments above the function definitions and remove them from here. That way this can be just 6 lines and this evaluator will be much easier to read. Let's also do that anywhere else any of these get_f_* functions are called

grjte

Looks good, thank you! Just a couple of final comments about comments for the functions, then it will be ready to merge

grjte

Looks great, thank you! I've left 2 final nits inline that I think it would be great to fix before merging, but they're not blocking. I'll leave it up to you to merge and you can make those updates first if you agree with them

grjte · 2023-03-29T15:44:13Z

constraints/miden-vm/hash.air

+    # path computation.
+    let f_absorb_node = f_mp + f_mv + f_mu
+
+    let f_abp = get_f_abp(s)


nit: I would prefer to move this up a few rows so it's declared with the other flags at the top of the evaluator

grjte · 2023-03-29T15:45:09Z

constraints/miden-vm/hash.air

+# We can define two flags:
+# 1. Flag f_hout = cycle_row_7 * binary_not(s[0]) * binary_not(s[1]) * binary_not(s[2]), 
+# which is set to 1 when selector flags are (0,0,0) on rows which are 1 less than a multiple 
+# of 8. This is flag of the instruction that returns the result of the currently running 
+# computation.
+# 2. Flag f_sout = cycle_row_7 * binary_not(s[0]) * binary_not(s[1]) * s[2], which is set to 1 
+# when selector flags are (0,0,1) on rows which are 1 less than a multiple of 8. This is flag 
+# of the instruction that returns the whole hasher state.
+#


Since we already have this above the get_f_out function, I think we can remove it and just keep the line below

tohrnii

Thank you @Overcastan, looks good to me. I just left one nit to write flag computation in terms of logical operators if you agree with the change.

tohrnii · 2023-04-06T02:14:09Z

constraints/miden-vm/hash.air

+# Set to 1 when selector flags are (1,0,1) on rows which are multiples of 8. This is flag of 
+# the instruction that initiates Merkle path verification computation.
+fn get_f_mp(s: vector[3]) -> scalar:
+    return cycle_row_0 * s[0] * binary_not(s[1]) * s[2]


nit: should we use logical operators here and other flag calculations as well?

Yes, I think we should do that. Thank you!

feat: write constraints for hash chiplet

730691d

Fumuran requested review from Al-Kindi-0, grjte and tohrnii March 13, 2023 12:14

tohrnii suggested changes Mar 13, 2023

View reviewed changes

refactor: add functions

757a6be

grjte suggested changes Mar 13, 2023

View reviewed changes

Fumuran force-pushed the andrew-hash-chiplet-constraints branch 2 times, most recently from 5788e70 to 3caaebc Compare March 15, 2023 22:57

Fumuran requested review from tohrnii and grjte March 15, 2023 23:45

tohrnii suggested changes Mar 16, 2023

View reviewed changes

grjte suggested changes Mar 16, 2023

View reviewed changes

Fumuran force-pushed the andrew-hash-chiplet-constraints branch from 3caaebc to 1366418 Compare March 17, 2023 13:38

Fumuran requested review from tohrnii and grjte March 17, 2023 13:42

grjte suggested changes Mar 28, 2023

View reviewed changes

Fumuran force-pushed the andrew-hash-chiplet-constraints branch from 1366418 to 7a1930b Compare March 28, 2023 19:50

Fumuran requested a review from grjte March 28, 2023 19:50

grjte approved these changes Mar 29, 2023

View reviewed changes

Fumuran force-pushed the andrew-hash-chiplet-constraints branch from 7a1930b to a97a57b Compare March 29, 2023 17:28

tohrnii approved these changes Apr 6, 2023

View reviewed changes

refactor: readability improvement

3bdc0a4

Fumuran force-pushed the andrew-hash-chiplet-constraints branch from a97a57b to 3bdc0a4 Compare April 6, 2023 02:57

Fumuran merged commit 048be9d into next Apr 6, 2023

Fumuran deleted the andrew-hash-chiplet-constraints branch April 6, 2023 03:05

		enf (s[1]' - s[1]) * (1 - f_out_next) * (1 - f_out) = 0
		enf (s[2]' - s[2]) * (1 - f_out_next) * (1 - f_out) = 0

		return 1 - value


		# Enforces that value in column is copied over to the nex row.

Write Hash Chiplet constraints in AirScript #215

Write Hash Chiplet constraints in AirScript #215

Conversation

Fumuran commented Mar 13, 2023

tohrnii left a comment • edited Loading

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

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 14, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Fumuran commented Mar 13, 2023

grjte commented Mar 13, 2023

tohrnii commented Mar 13, 2023

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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tohrnii Mar 13, 2023 • edited Loading

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 left a comment • edited Loading

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

grjte left a comment • edited Loading

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

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

Choose a reason for hiding this comment

grjte left a 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

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 left a comment •

edited

Loading

tohrnii Mar 14, 2023 •

edited

Loading

tohrnii Mar 13, 2023 •

edited

Loading

tohrnii left a comment •

edited

Loading

grjte left a comment •

edited

Loading