Thv/degree lowering hardening

[Sword-Smith]

Add tests that degree lowering and code generator for constraint evaluation is deterministic and does not change unintentionally.

[jan-ferdinand]

Passing three things of the same type is bad design. It is very easy to mess up the order of the arguments, which will lead to runtime failures or – worse – erroneous behavior, where instead the compiler could highlight incorrect use of the function. Introduce a new type instead (or use an existing one should one fit).

[aszepieniec]

66b8225 Introduces type aliases EvolvingMainConstraintsNumber and EvolvingAuxConstraintsNumber for the second two counts.

Personally, I think this change degrades code quality. Having the commit as part of the PR is the fastest way forward, because it either earns your checkmark directly or else contributes to convincing you to reject it.

My position, in case you are interested:

• Types used once are mis-used.
• The function is called in one place only, not counting the test. It is conceptually part of that same function; the only reason why it is factored out is to test it in isolation.
• The counts serve to derive indices of new columns and are thus inherently usizes. Declaring another type for these variables suggests a different context applies, but I don't think it does. The reader's attention is diverted towards finding this missing context.
• Messing up the order of the arguments is still possible. (If due to too-weak introduced types, please show by example how it ought to be done.)
• Why not declare a new type for every argument in every function interface? I do think that's the logical conclusion of your train of thought; if not I wonder where it stops.
• All of the above being said, I do think that NodeId could be a useful type but a) that doesn't resolve the problem completely; and b) that refactor is out of the scope of this PR.

[jan-ferdinand]

Type aliases don't do what you suggest they do in 66b8225 – that's newtypes.

Taking position:

Types used once are mis-used.

I see help from the type system to write correct programs as beneficial in all cases.¹

The function is called in one place only […].

I don't see how this justifies bad design.

[…] the […] reason why it is factored out is to test it in isolation.

Which is laudable and a decision I fully support.

The counts […] are […] inherently usizes.

Consider:

let _ = PrintConfig::new(true, true, false);
let _ = PrintConfig::new(Sided::Single, Colored::Colored, PrintSpeed::Slow);

Even though (for arguments sake) all these enums have only two variants, and are thus inherently bools, I strongly prefer the second version.² In my opinion, the argument extends to numerical types.

Why not declare a new type for every argument in every function interface?

The concrete contract of a function as well the number of arguments it takes make a huge difference. In my_vec.remove(i), there's no room for screwing up the argument order.³ The same holds for my_vec.swap(i, j), and so having two arguments of the same type does not influence the method's usability. I don't have a hard-and-fast rule at hand as to where it is beneficial to introduce new types.

I do think that NodeId could be a useful type

Sounds like a good idea. I agree with it being out of scope for this PR.

---

All that said, I think testability completely justifies factoring out the function. I also think that you have inherited design decisions (and, worse, accidental design) that would require a ton of work to improve.⁴ We can write the argument sublist usize, usize, usize off as being part of overall improvable design, improving which is left as future work. One might argue that this constitutes building up technical debt,⁵ but I think an equally valid argument is that factoring out the method only highlights existing technical debt.

In my opinion, introducing a type like NumConstraints slightly mitigates the issues I have with the same-type arguments. Fully resolving all pain points I see would probably require a more fundamental redesign.

Footnotes

1. Yes, I'm looking forward to your counter argument after having made such an absolute claim. ↩

2. Other designs than a function new() taking many arguments should be considered were PrintConfig actually being added. The types' names would need a rework, too. ↩

3. Technically, it's possible: Vec::remove(i, &mut my_vec). However, (a) the type checker will stop you, and (b) why would you write that, apart from trying to prove a point, which, fair enough. ↩

4. One strong indicator of this is that the two arguments in question are essentially internal tracking information. The function should not have to rely on externally supplied information for this. ↩

5. I'm sure you won't be surprised to hear that I'm not a fan of building up technical debt, and even less of doing it consciously. ↩

[aszepieniec]

I modified 66b8225 (now 14a0572) to use newtypes instead of type aliases. Thanks for the reference. Let's proceed with this.

I see help from the type system to write correct programs as beneficial in all cases.1

You already read a few general counter-arguments in my bullet point list. In response to this particular phrasing: in the eyes of one person, "help from the type system to write correct programs" is "having to fight the type system to write anything at all in exchange for a marginal assurance of correctness" in the eyes of another. There are programming languages whose type systems are powerful enough to produce a formal computer-verifiable proof of programs' correctness. If rust's type system had this feature, would you recommend using it everywhere and always? The alternative would be to find an optimum on the tradeoff curve interpolating between (a) getting stuff done and (b) correctness.

The function is called in one place only […].

I don't see how this justifies bad design.

To the extent that the partially elided sentence justifies deviating from your standards (I would obviously not use the B-word) the point is not so much that the function is used in a small number of places and therefore unimpactful; instead, the point made by the elided part is that the function is conceptually and semantically, inseparably part of the of the function that calls it. This relation makes the maintenance of a succinct and misuse-resistant interface moot at best and counter-productive at worst -- because if the algorithm changes then the "interface" will have to adapt.

Consider:

let _ = PrintConfig::new(true, true, false);
let _ = PrintConfig::new(Sided::Single, Colored::Colored, PrintSpeed::Slow);

Even though (for arguments sake) all these enums have only two variants, and are thus inherently bools, I strongly prefer the second version.2 In my opinion, the argument extends to numerical types.

There is no natural mapping from Single-Sided/Double-Sided or Colored/Monochrome or Slow/Fast to true/false. You can define a mapping and call it canonical but it would still be an arbitrary choice that preserves no structure. So I disagree with the position that these enums "are inherently bools" and would even argue that the second line is preferable to the first.

To bolster my position that the counts in question are inherently usizes, consider the necessary boilerplate following the definition of EvolvingMainConstraintNumber:

struct EvolvingMainConstraintsNumber(usize);
impl From<EvolvingMainConstraintsNumber> for usize {
    fn from(value: EvolvingMainConstraintsNumber) -> Self {
        value.0
    }
}

In fact, the counts are not used except through this from method. The type is not used in any algebraic sense.

Maybe that's the point and the essence of our difference. I want types to semantically reflect the underlying maths; whereas you want types to constrain control flow and interfaces.

In my_vec.remove(i), there's no room for screwing up the argument order.3 The same holds for my_vec.swap(i, j), and so having two arguments of the same type does not influence the method's usability.

There is no room for screwing up the argument order (footnote notwithstanding) but there is room for making the wrong selection from the variables of type usize that live in scope. In this case, binding the interface through custom defined types gives the false impression of correctness, which is worse than no impression at all.

[aszepieniec]

Something funky is happening with the test table::master_table::tests::air_constraints_evaluators_have_not_changed which I can't explain. CI is failing with

expected: (03756754445351585926·x² + 06769459618545093804·x + 09140558386905394900)
observed: (14714205515170095309·x² + 13661591558076455036·x + 14115119063754412580)

whereas on my desktop computer I get

expected: (03756754445351585926·x² + 06769459618545093804·x + 09140558386905394900)
observed: (03346962278739234229·x² + 12572006219868624302·x + 10286558549229477187)

and both are obviously different from my laptop which produced the expected value. Any ideas as to what might cause this?

[Sword-Smith]

On my desktop at home, I get the same as the CI machine observed:

expected: (03756754445351585926·x² + 06769459618545093804·x + 09140558386905394900)
observed: (14714205515170095309·x² + 13661591558076455036·x + 14115119063754412580)

[Sword-Smith]

Would it make sense to also add a proptest like node_substitution_is_complete_and_sound for a DualRowIndicator type?

[aszepieniec]

Correction: on my laptop I get this failure:

exoected: (03756754445351585926·x² + 06769459618545093804·x + 09140558386905394900)
observed: (03346962278739234229·x² + 12572006219868624302·x + 10286558549229477187)

which agrees with my desktop.

After rebasing in @Sword-Smith's faster compilation changes, I get this failure

expected: (03756754445351585926·x² + 06769459618545093804·x + 09140558386905394900)
observed: (14714205515170095309·x² + 13661591558076455036·x + 14115119063754412580)

which agrees with CI and @Sword-Smith's machine.

[aszepieniec]

For the record, applying just the first commit (9e5db866063a6527366be62616611d74db1ef416) of setting opt-level=3 generates this failure:

expected: (03756754445351585926·x² + 06769459618545093804·x + 09140558386905394900)
observed: (03346962278739234229·x² + 12572006219868624302·x + 10286558549229477187)

which agrees with the failure before setting the opt-level. So this compiler optimization does not seem to change anything.

[aszepieniec]

@jan-ferdinand: All checks pass. Any further requested changes?

[aszepieniec]

BTW: I can confirm that all tests pass on my desktop machine as well.

[jan-ferdinand]

The test's top-level comment is very helpful to understand why the test is doing what it is doing, and why it is meaningful to have the test. The test itself is a very good addition.

[aszepieniec]

All comments are resolved now (I think).

[jan-ferdinand]

All comments are resolved now (I think).

I'm still wondering about the following points:

• Can the code in the various num_ functions be de-duplicated? (review comment)
• Is there a copy-paste error in the docstring for num_nodes? (review comment)
• Is the method how the various num_ things are computed relevant enough to be mentioned in the docstring? (review comment)
• Can the hidden relationship between node types in the multicircuit strategy be removed by changing which node types are supplied? (review comment)

[aszepieniec]

I think I've answered all your questions. Any further remarks / requests?

[jan-ferdinand]

No further requests. Happy to have this test in. 👍