Intro
UPD: I’ve added proof sketches in comments down below. I would suggest to refer to definitions there as a main source (some notation is better, and also I’ve fixed stuff here and there, the main post still has mistakes).
Hello everyone. Throughout the recent few days, I’ve discussed with different people a variety of things related to lookups, Nova, and other stuff. It seems I have now something to tell back. It will be a long post, and mostly it will consist of constructions, not security proofs. I expect this to be possible roadmap to realizing zkproofs of very large circuits.
Logically, it is split into two independent parts (three, if we include preliminaries). I am sort of convinced that the first part works, and feel shaky but excited about the second.
First part is devoted to adding permutation argument to Nova (/ Sangria, they are not that different). This, potentially, means memory accesses between the steps, or even copy constraints between the steps. It seems to be different from Origami and Nico’s approach (communicated to me in private)  which are approaches focused on separate lookups on each step instance. The advantage of my approach is the fact that (1) it removes the need of keeping the lookup table in each instance (2) it allows us to do interesting crossstep interactions. Generally, it leads to folding of arbitrary unstructured circuits, completely superseding SuperNova. Disadvantage is the fact that it is not really incremental  the whole batch of steps needs to be known beforehand. However, I believe this should be, generally, an effective and manageable approach to very big circuits.
Second part is concerned with using Nova over integer coefficients by using Pedersen commitments in RSA group.
Acknowledgements
I would like to thank everyone who communicated with me and shared ideas through the last few days. @barryWhiteHat asked me about lookups / challenge oracle in Nova, and we have came up with ~ the approach I’m now going to tell you. Lucas Meier @cronokirby was the one who gave me the initial push. We had extensive discussion with @nico_mnbl, and some parts of what I will be telling you are influenced by him. Thanks to @aard_k_vark and @krzhang who created Origami and talked about it with me, and thanks to @kobi, @portport255 and Yar for listening to my incoherent ramblings.
Onwards.
Preliminaries
Before we start, let’s, as a short warmup, recall how Nova works. I will consider a slightly more general case, so Sangria is also subsumed by it.
Our instance is a polynomial equation system \forall i : P^{i}(x_0, ..., x_n) = 0, with some subset of variables called “fixed” (or “instance” variables, or “public inputs”). We also assume that x_0 is fixed and equals 1. For convenience, lets split each polynomial into homogeneous parts, i.e. P^i(\bar x) = \underset{0 < k < d_i}\sum P^i_k (\bar x).
Then, the system can be rewritten into homogeneous system: P^i_{\text{new}} \overset{\text{def}}= \sum P_k^i(\bar x)x_0^{dk}. In what follows, I will always assume w.l.o.g. that this system is homogeneous. //in Nova paper x_0 = u.
I will also denote \bar x = (\bar p, \bar q) the splitting of the vector x on instance and witness parts.
Now, let’s also create relaxed version of a system, namely \forall i: P^i(\bar x) = E^i. The vector \bar E also sort of counts as instance vector (and is called error term). We will use some linearly homomorphic vector commitment system, and commitment to a vector \bar v will be denoted [\bar v]. The committed relaxed instance is [\bar p, \bar E], and committed witness is [\bar q].
Now, given two (committed relaxed) instances of the system, the following protocol allows to prove we have solutions to both of them:

The prover sends to the verifier [\bar q_1], [\bar q_2] and the following crossterms: [C_k] = [\bar P (x_1 + t x_2) _{t^k}] \quad \forall \quad 0<k<d. Here, P_{t^k} \overset{def}= \frac{1}{k!}(\frac{\partial}{\partial t})^k P _{t=0}.

Verifier samples random \lambda, and gives it back to prover.

Prover now only needs to prove it knows a solution \bar q_1 + \lambda \bar q_2 to the instance [\bar p_1 + \lambda \bar p_2, \bar E_1 + \lambda^d \bar E_2  \underset{0<k<d}\sum \lambda^k C_k]  it can do it by directly revealing all the commitments, or use the obtained relaxed committed instance to fold it again and again.
I will frequently assume that the system of equations was quadratic (because it might be simpler to write formulas this way), but actually it is not necessary. Before describing how Nova works, let’s consider the following simple protocol:

Prover commits to n “step instances + step witnesses”, called u_1 ... u_n. Each instance has parts of the fixed values called “input” and “output”, and we also require that \text{in}_{i+1} = \text{out}_i.

Prover also folds everything (i.e. shows all the commitments to the occuring crossterms in the incremental folding process), and then reveals the witnessinstance pair of the resulting folded instance (it could also publish a SNARK of it, but let’s just ignore it for a moment).
This protocol, on paper, takes O(n) verification time, but even this is already quite powerful. Imagine, for example, that it was actually a repeated computation of length N, split into batches of length n = \sqrt{N}, corresponding to each step.
Then, apparently, it takes O(\sqrt{N}) time  because we have \sqrt{N} folds, followed by reading witness of size O(\sqrt{N}).
High level idea of Nova approach is by modifying the steppredicate in such a way that it “remembers” previous steps, and so prover does not need to publish all the step commitments. Let’s recall how it works:
Denote the original step predicate F. Our new, modified step predicate F' takes all inputs as nondeterministic advice, except of 1 called h, which will be used to keep our running instance in. Denote the values obtained by applying F z_i = F^i(z_0).
Denote u_b, w_b the trivial instancewitness pair with both error term and public input being 0,
In the base case i=0 the predicate F' should just output h = H(vk, z_0, F(z_0), 1, u_b).
Now, for the step i>0:
 Get a nondeterministic advice U_i, u_i where U_i represents the running instance and u_i the current instance, and also z_0, z_i, i.
 Unpack the hash: H(vk, z_0, z_i, i, U_i) = u_i.h
 Calculate F(z_i) = z_{i+1}
 Check that u_i is wellformed, i.e. its error term is 0 and u_i.x_0 = 1
 Fold U_i and u_i to obtain U_{i+1}
 Set h = H(vk, z_0, z_{i+1}, i+1, U_{i+1})
Now, we are ready to attempt the same trick, but with additional challenge rounds.
Adding the second round  Origami approach ?
Interactive version was initially communicated to me by Nico, who was doing something similar independently, but it seems that these approaches do, in fact, coincide. Maybe this text will still serve as some sort of clarification for the original Origami text; as a guide of turning their argument into noninteractive IVC.
Suppose now, that our step circuit (meaning, witness) is split into two parts, which I call S_0 and S_1. There are also additional public inputs (called “challenge”), which I will denote t_1, ..., t_k, that is not present in any constraints involving S_0.
I will call an algebraic witness to such structure a solution over \mathbb{F}_p(t_1, ..., t_k), such that over S_0 it lives in \mathbb{F_p}. Good example of this is permutation or lookup arguments.
Given the challenge, it produces a normal witness with an overwhelming probability.
Now, this is my interpretation of what I’ve learned from talks with Nico and Origami team. Maybe I’m wrong / interpreting something that was not said explicitly, but for me it looks like the only reasonable way to proceed:
 as before – but also get “partial witness commitments” W^0_i, w^0_i (they mean witnesses for the S_0). Calculate challenge using FiatShamir of w^0_i (here, authors will probably insist that I need to hash the whole transcript, but I claim that in that particular case it is more than enough, but if we need we can use u_i.h, w^0_i).
 Unpack the hash: H(vk, z_0, z_i, i, U_i, W^0_i) = u_i.h
 Calculate F(z_i) = z_{i+1}
 Check that u_i is wellformed, i.e. its error term is 0 and u_i.x_0 = 1
 Fold U_i and u_i to obtain U_{i+1}, fold W^0_i and w^0_i with the same coefficient to obtain W^0_{i+1}
 Set h = H(vk, z_0, z_{i+1}, i+1, U_{i+1}, W^0_{i+1})
The final check should also, in addition, prescribe that the witness corresponding to the first round is exactly the folded W^0. (i.e. if our final check is just “reveal the witness”, then the verifier must also extract W^0_{n+1} and check that it is, indeed, a commitment to its own part of computation of z_{n+1} using F (step 3)).
Why I think it works (totally not a security proof): assume we come up with some fake witnesses. It will, of course, mess up the computation of F^{n+1}(z_0) if we adaptively choose these witnesses, but it will still be correct folding (up to our external check). Moreover, the part of the trace of computation of F that lives over S_0 does not change. I expect it is not possible to choose w_i's adaptively in such a way that its folding would give the folding of the trace of computation of F over S_0.
Adding a second round in a different way  my approach
Now, in the paradigm above, each round has a different challenge. However, it might be reasonable to thrive for a single challenge (in a sense that a commitment to the run over S_0 is obtained, and then commitment over S_1 is produced).
I suggest doing it in a following way. Now, F' will have two running hashes, second one will be called \text{run}.
 Get a nondeterministic advice U_i, u_i, W^0_i, w^0_i, z_0, z_i, i as before.
 Unpack the hash: H(vk, z_0, z_i, i, U_i, W^0_i) = u_i.h
 Guess the challenges \bar t nondeterministically.
 Calculate F(z_i) = z_{i+1}
 Check that u_i is wellformed, i.e. its error term is 0 and u_i.x_0 = 1
 Fold U_i and u_i to obtain U_{i+1}, W^0_i and w^0_i to obtain W^0_{i+1}
 Set h = H(vk, z_0, z_{i+1}, i+1, U_{i+1}, W^0_{i+1}), \text{run} = H(w^0_i, u.\text{run})
After the dust settles, the final verifier performs the check, as before, and also checks that t = \text{run}.
Errata: either we check t*U_{i+1}.x_0 = \text{run}, or we need to constrain t inbetween different steps (say incorporate it in z_i with the rule that t_{i+1} = F(t_i) = t_i). Not sure which one of these approaches is better, both seem to work.
The idea is similar: the witness vector is proposed in each step. It is both folded in, and accumulated into a running hash. The running hash then, retroactively, must be equal to the challenge used at every step, and the folded witness is then used to ensure integrity.
If this works (which I hope it does, but currently this is a mere conjecture), then we would unlock an ability to create copy constraints between different steps. This would allow to fold unstructured circuits, or emulate VM memory accesses using nondeterministic checking of memory access flow.
Integer commitments
Another very fruitful topic is potentially using Pedersen commitments in RSA groups. Nova does not exactly use the fact that it is over a field anywhere. (Here, I’m speaking specifically about groups in which RSA assumption holds. Ideal class groups do not work, because square roots are easy  which could allow rational commitments that become integer after folding, similar to a problem encountered by authors of DARK).
Provided the solution to the integer circuit is relatively tame, the folding can also be made relatively tame  say if r bits is the maximal value of a signal in a circuit, then r+256+\log_2(n) is the total maximal value in the folded circuit.
This unlocks various superpowers that, generally, feel like cheating  starting from dirt cheap range proofs, and ending with dirt cheap circuit for folding itself  expressing RSA in integer arithmetic terms should be very pleasant.
I’m not exactly sure about this part, but I think it is worth researching. Of course even if everything works, we will still need to create trusted setup ceremony, which looks very hard for RSA, but provided this is done we would be able to finally do integer arithmetic normally, which looks like it is worth a shot.
Foreword
If you see any mistakes, inaccuracies, some scheme is clearly broken or you just have valuable input / want to collab on some topic from there  please, reach me out, through twitter or telegram handle levs57. xoxo