Change query function and set_hint function by more flexible "hint" code block

[chriseth]

We should not tie the hint function that tightly to specific columns. This way, it will be easier to share computed values between different columns and we could e.g. create all values for a full block in a block machine in one go.

Proposed syntax:

hint |row_index| {
  // replacement for the "hint" query alternative
  std::prover::set_value(column, row_index, value);
  std::prover::output("string");
  let x = std::prover::input(1, 2);
};

One problem is that we should specify somehow when to run the hint. For set_value, it is probably important that some other value of a witness column is known. For output, we should not run it multiple times per row, same for input.

We currently run the hints as long as the value for the associated column is not known. We could either model that explicitly in the hint:

hint (col1, col2) |row_index| { ... }

or in the code:

hint |row_index| { if std::prover::value_known(col1, row_index) { ... } }

Once we implement this, we should remove std::prover::set_hint / std::prelude::set_hint and all related mechanisms.

Related: https://github.com/powdr-labs/powdr/issues/1365

[chriseth]

I think we also considered in the past just calling this section prover { ... }

[chriseth]

Oh and this statement would be valid at statement level and inside constr functions.

[chriseth]

Another question to answer is how the hint/prover blocks are handled by the machine extractor. If we list columns whose known-ness trigger the hint, then this could be used. We could also collect references, but that might fail to work if we call another function (unless we follow the function call...).

Once we have proof objects, this might become easier...

[georgwiese]

Cool! I don't think I really have answers to your questions, but a few thoughts.

I think what we want is for the user to be able to provide some callback that is called by the solver for each row until success. Maybe we can have the callback return whether it succeeded? This way, a hint that has a side effect (e.g. one calling std::prover::output) can make sure that it only ran once, and a hint that set all values successfully can mark itself as complete, so it doesn't need to be run again. Each hint should be written such that it is idempotent if it returns Status::Incomplete, and should have side effects only before returning Status::Complete.

We currently run the hints as long as the value for the associated column is not known. We could either model that explicitly in the hint:

hint (col1, col2) |row_index| { ... }

or in the code:

hint |row_index| { if std::prover::value_known(col1, row_index) { ... } }

In the first approach, does it mean that both col1 and col2 need to be known, or that the hint is run if at least one of them is unknown? I think both would be useful. And are we talking about the current row?

I think the first approach allows us to optimize performance a lot better (no need to run the PIL evaluator if the conditions are not met) and helps with machine detection, as you mentioned. On the other hand, the second approach is more general and doesn't require the user to know some special syntax to answer the questions I have with the first approach...

[chriseth]

I actually think that for now, we can ignore most of these questions. std::prover::eval can fail and if it fails, the prover section is re-executed at a later point. If the prover section can be executed without error, it is not re-run for the same row. I think that should work for most of our use-cases for now. If we need it, we can add the status return value, that's a good idea.

Also I think that instead of set_value we should name that function provide_value, since this sounds more like a "hint".

[chriseth]

Interesting. There might be a way to implement this with rather small changes to the parser and even condenser:

At statement level (everywhere where we allow constraints), we allow lambda functions of query kind. We rename "query" to "prover".

Then it looks exactly like proposed above:

let x;
let y;
prover |i| {
  std::prover::provide_value(x, i, std::prover::eval_at(x, i));
};

The side-effect checker already works properly. And then the condenser collects those prover functions and stores them in Analyzed.

[chriseth]

This has been implemented in #1717