Arithmic/word address

[arithmic-ASHISH]

No description provided.

[moodlezoup]

still reviewing, but leaving some initial feedback here

[moodlezoup]

nit: delete

[moodlezoup]

use resize instead

[moodlezoup]

I think something like this should work

Suggested change

	let input_vector_word: Vec<Vec<u64>> = (0..WORD_BYTES)
	.map(|i| word_vector.iter().map(|row| row.bytes[i]).collect())
	.collect();
	let mut output_array: [Vec<u64>; WORD_BYTES] = Default::default();
	for (i, row) in input_vector_word.iter().enumerate() {
	output_array[i] = row.clone();
	}
	output_array
	std::array::from_fn(|i| word_vector.iter().map(|row| row.bytes[i]).collect())

[moodlezoup]

Similar to how we handle [ a_ram, v_write_rd, v_init_reg, v_final_reg, t_final_reg, t_final_ram ] above

Suggested change

	|| map_to_polys(&[t_read_ram.clone()])[0].clone(),
	|| map_to_polys(&[t_write_ram])[0].clone(),
	|| map_to_polys(&[remainder_vec])[0].clone()
	|| map_to_polys(&[t_read_ram, t_write_ram, remainder_vec]),

[moodlezoup]

unnecessary take I think

[moodlezoup]

delete

[moodlezoup]

we can just directly return the result of the batch_verify

[sragss]

A few syntax comments.

[sragss]

You can simplify all these now thanks to the implementation of std::ops::{add, mul, sub, neg} for most of the things that Impl<Into<LC>>

For example: let remainder: LC<JoltIn> = JoltIn::Remainder - 2;

I won't drop comments on all of the lines below but this lets you remove ConstraintSystem::{create_term, create_term_with_constant_variable}, LC::{sum2, sum3, sum_any}

[moodlezoup]

Also, I think it's more efficient to do 2 - remainder rather than remainder - 2 (same with remainder - 1 and remainder - 3)

[arithmic-ASHISH]

LC::sub2(JoltIn::RAM_Write_Byte0, JoltIn::LookupOutput),
@moodlezoup Is this the right way to handle the above statement?

let byte0: LC<JoltIn> = JoltIn::RAM_Write_Byte0.into();
let lookup_output: LC<JoltIn> = JoltIn::LookupOutput.into();
byte0 - lookup_output,

[sragss]

For these you can use let term: Term<JoltIn> = JoltIn::RAM_Read_Byte0 * (1<<8);

[sragss]

This and following uses of constrain prod seem to conditionally check that term0 is 0.

I think it would be clearer to use cs.constrain_eq_conditional(JoltIn::OpFlags_X, term, 0)

Note, again you can just inline the 0 term here rather than LC::zero() because i64 impl Into<LC>.

[sragss]

We should make a cs.constrain_pack_be_conditional so the format would look as follows.

cs.constrain_pack_be_conditional(JoltIn::OpFlags_IsSw, input_range!(JoltIn::RAM_Write_Byte0, JoltIn::RAM_Write_Byte3), packed_query, 8)

There's a TODO(sragss) above to do this. I can add, leave this comment open.

[sragss]

For this constraint: (LB_flag + LBU_flag + SB_flag) [remainder*(remainder -1)*(remainder -2)*(remainder-3)] + (LH_flag + LHU_flag + SH_flag) [remainder*(remainder -2)] + (LW_flag + SW_flag)*remainder = 0

Isn't the first term guaranteed to be zero? [remainder*(remainder -1)*(remainder -2)*(remainder-3)] == 0 remainder \in {0,1,2,3} If the goal is just to check that remainder is in fact {0,1,2,3} then we can get rid of the flat term out front.

For (LH_flag + LHU_flag + SH_flag) [remainder*(remainder -2)] I believe it would be clearer to structure it as:

let is_half_mem = JoltIn::IF_LH + JoltIn::IF_LHU + JoltIn::IF_SH`;
let remainder_is_0_or_2 = cs.allocate_prod(JoltIn::remainder, JoltIn::remainder - 2);
cs.constrain_eq_conditional(half_mem, remainder_is_0_or_2, 0);

[vineet-n]

For this constraint: (LB_flag + LBU_flag + SB_flag) [remainder*(remainder -1)*(remainder -2)*(remainder-3)] + (LH_flag + LHU_flag + SH_flag) [remainder*(remainder -2)] + (LW_flag + SW_flag)*remainder = 0

Isn't the first term guaranteed to be zero? [remainder*(remainder -1)*(remainder -2)*(remainder-3)] == 0 remainder \in {0,1,2,3} If the goal is just to check that remainder is in fact {0,1,2,3} then we can get rid of the flat term out front.

Not sure how we can remove it.
The first term ensures that the remainder is in {0,1,2,3} when the instruction is LB, LBU, or SB. For example if the instruction is LB and remainder is 5 then constraint is non-zero, and hence an invalid execution. This cannot be captured if we remove this term.