Adding random values to IR #134

Fumuran · 2023-02-02T15:51:50Z

Partly addressing #86.

Added support for random values in IR.
Added indexed access to random values by custom name.
Added integration test for random values.

grjte

Looks great, thank you @Overcastan! I left several comments inline, but it's all small stuff

air-script/tests/aux_trace/aux_trace.air

air-script/tests/random_values/random_values.air

air-script/tests/main.rs

air-script/tests/random_values/random_values_simple.air

ir/src/symbol_table.rs

ir/src/constraints/graph.rs

tohrnii

Thank you @Overcastan, looks good to me. I just left a few small nits inline.

ir/src/constraints/graph.rs

ir/src/symbol_table.rs

tohrnii · 2023-02-03T12:13:10Z

ir/src/symbol_table.rs

@@ -20,6 +20,9 @@ pub(super) enum IdentifierType {
    PeriodicColumn(usize, usize),
    /// an identifier for an integrity variable, containing its name and value
    IntegrityVariable(Variable),
+    /// an identifier for random value, containing its index in the random values array and its
+    /// length if this value is an array. For non-array random values second parameter is always 1.
+    RandomValue(usize, usize),


nit: If this can represent an array, should this be called RandomValues instead?

The problem is that we have a main array of random values (rand: [a, b, c, ... ]), so calling it RandomValues can be confusing, it will be unclear whether we mean the main array or its element, which is represented by an array. I agree with you that it would be better to rename it somehow, but I don't know yet which name would be better. Perhaps RandomValuesElement, but this name also does not reflect that this element can be an array.

It could be RandomValuesBinding again, to be somewhat consistent with the AST?

What about RandomValuesGroup?

ir/src/constraints/graph.rs

tohrnii

Thank you @Overcastan, looks good to me. I just left very minor things inline. One question is if we should handle #46 in this PR and the check that you suggested regarding returning an error if there are no aux trace columns but random values section is declared or if we should leave it for the next PR.

tohrnii · 2023-02-04T02:29:26Z

ir/src/tests/mod.rs

+
+    let parsed = parse(source).expect("Parsing failed");
+    let result = AirIR::from_source(&parsed);
+    assert!(result.is_ok());
+}
+
+#[test]
+fn random_values_custom_name() {
+    let source = "
+    trace_columns:
+        main: [a, b[12]]
+    public_inputs:
+        stack_inputs: [16]
+    random_values:
+        alphas: [16]
+    integrity_constraints:
+        enf a' = $alphas[3] + 1
+    boundary_constraints:
+        enf a.first = $alphas[10] * 2
+        enf a.last = 1";
+
+    let parsed = parse(source).expect("Parsing failed");
+    let result = AirIR::from_source(&parsed);
+    assert!(result.is_ok());
+}
+
+#[test]
+fn random_values_ident_vector() {
+    let source = "
+    trace_columns:
+        main: [a, b[12]]
+    public_inputs:
+        stack_inputs: [16]
+    random_values:
+        rand: [c, d[4]]
+    integrity_constraints:
+        enf a' = c + d[2] + $rand[1]
+    boundary_constraints:
+        enf a.first = (d[1] - $rand[0]) * 2
+        enf a.last = c";
+
+    let parsed = parse(source).expect("Parsing failed");
+    let result = AirIR::from_source(&parsed);
+    assert!(result.is_ok());
+}
+
+#[test]
+fn error_random_values_out_of_bounds() {
+    let source_fixed_list = "
+    trace_columns:
+        main: [a, b[12]]
+    public_inputs:
+        stack_inputs: [16]
+    random_values:
+        rand: [4]
+    integrity_constraints:
+        enf a' = $rand[4] + 1
+    boundary_constraints:
+        enf a.first = $rand[10] * 2
+        enf a.last = 1";
+
+    let parsed = parse(source_fixed_list).expect("Parsing failed");
+    let result = AirIR::from_source(&parsed);
+    assert!(result.is_err());
+
+    let source_ident_vector_sub_vec = "
+    trace_columns:
+        main: [a, b[12]]
+    public_inputs:
+        stack_inputs: [16]
+    random_values:
+        rand: [c, d[4]]
+    integrity_constraints:
+        enf a' = c + 1
+    boundary_constraints:
+        enf a.first = d[5] * 2
+        enf a.last = 1";
+
+    let parsed = parse(source_ident_vector_sub_vec).expect("Parsing failed");
+    let result = AirIR::from_source(&parsed);
+    assert!(result.is_err());
+
+    let source_ident_vector_index = "
+    trace_columns:
+        main: [a, b[12]]
+    public_inputs:
+        stack_inputs: [16]
+    random_values:
+        rand: [c, d[4]]
+    integrity_constraints:
+        enf a' = c + 1
+    boundary_constraints:
+        enf a.first = $rand[10] * 2
+        enf a.last = 1";
+
+    let parsed = parse(source_ident_vector_index).expect("Parsing failed");
+    let result = AirIR::from_source(&parsed);
+    assert!(result.is_err());
+}
+


I think we should change these so that random values are only used against auxiliary columns. We don't have a check for it yet but we should still have valid tests here for now. Also, do you think we should address #46 here as well or should we do that in another PR?

I think I can do it in this PR, looks like it wouldn't involve a lot of changes. Just one question: should we also throw an error if random values are used against the main trace in integrity constraints?

I don't think so. I think we can have integrity constraints with random values and main trace column access but maybe it should be an error if there are random values but no auxiliary column access in a constraint? I'm not sure, maybe @grjte or @bobbinth could confirm?

Ideally, something like this should be a warning - but since we don't have warnings, I'm not quite sure what's the best approach. Probably having it be an error is better - but if it creates a lot of extra work now, we can do it later too.

ir/src/symbol_table.rs

Fumuran · 2023-02-06T14:15:46Z

I really don't like how I implemented additional checks, but my other ideas didn't work (it's too hard to implement them). Does anyone have suggestions how it can be done better?

grjte

Thanks @Overcastan! I left a few more comments inline. I think we can simplify and leave the validity checks for a future PR, since this one is good overall and I'd rather merge it sooner

ir/src/constraints/graph.rs

ir/src/lib.rs

ir/src/constraints/mod.rs

ir/src/symbol_table.rs

ir/src/tests/mod.rs

tohrnii

Thank you @Overcastan, looks good to me. I just left a few very minor naming related nits but don't have strong opinion on those.

ir/src/symbol_table.rs

tohrnii · 2023-02-06T18:08:48Z

ir/src/tests/mod.rs

@@ -379,6 +379,126 @@ fn transition_constraints_using_parens() {
    assert!(result.is_ok());
 }

+#[test]
+fn random_values_fixed_list() {


nit: Should this be renamed to random_values_indexed_access or something like that?

tohrnii · 2023-02-06T18:09:39Z

ir/src/tests/mod.rs

+}
+
+#[test]
+fn random_values_ident_vector() {


nit: Should this be renamed to random_values_named_access or something similar?

grjte

LGTM! Thanks @Overcastan!

feat: add random values to the IR

1c8675b

Fumuran requested review from Al-Kindi-0, grjte and tohrnii February 2, 2023 15:51

feat: add intergation test

5cb4acc

Fumuran force-pushed the andrew-ir-random-values branch from 8d52e1c to 5cb4acc Compare February 2, 2023 21:35

grjte suggested changes Feb 3, 2023

View reviewed changes

tohrnii suggested changes Feb 3, 2023

View reviewed changes

feat: refactoring

8e31a6b

Fumuran force-pushed the andrew-ir-random-values branch from 873d374 to f4379f5 Compare February 3, 2023 15:56

Fumuran requested review from grjte and tohrnii February 3, 2023 15:58

tohrnii suggested changes Feb 4, 2023

View reviewed changes

Fumuran requested a review from tohrnii February 6, 2023 14:15

grjte suggested changes Feb 6, 2023

View reviewed changes

feat: add indexed access to random values by custom name

a7eb8a3

Fumuran force-pushed the andrew-ir-random-values branch from 83cf6fe to a7eb8a3 Compare February 6, 2023 17:41

Fumuran requested review from grjte and bobbinth February 6, 2023 17:45

tohrnii approved these changes Feb 6, 2023

View reviewed changes

feat: naming improvements

dcaf137

grjte approved these changes Feb 6, 2023

View reviewed changes

tohrnii merged commit 3e541d7 into next Feb 7, 2023

tohrnii deleted the andrew-ir-random-values branch February 7, 2023 07:45

This was referenced Feb 7, 2023

Tracking PR for v0.2 release #79

Merged

Individual section and named access for random values #128

Closed

Add section for random values and allow declaring names for accessing random values #86

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Adding random values to IR #134

Adding random values to IR #134

Fumuran commented Feb 2, 2023 •

edited

Loading

grjte left a comment

tohrnii left a comment

tohrnii Feb 3, 2023

Fumuran Feb 3, 2023 •

edited

Loading

grjte Feb 3, 2023

tohrnii Feb 4, 2023

tohrnii left a comment

tohrnii Feb 4, 2023

Fumuran Feb 6, 2023

tohrnii Feb 6, 2023

bobbinth Feb 6, 2023

Fumuran commented Feb 6, 2023

grjte left a comment

tohrnii left a comment

tohrnii Feb 6, 2023

tohrnii Feb 6, 2023

grjte left a comment

Adding random values to IR #134

Adding random values to IR #134

Conversation

Fumuran commented Feb 2, 2023 • edited Loading

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

Fumuran Feb 3, 2023 • edited Loading

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

Fumuran commented Feb 6, 2023

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

grjte left a comment

Choose a reason for hiding this comment

Fumuran commented Feb 2, 2023 •

edited

Loading

Fumuran Feb 3, 2023 •

edited

Loading