Constraint linearity in the resource machine

[degregat]

@cwgoes

So-called intent resources are just ephemeral resources (scoped to the lifetime of a single transaction), which have regular resource logics (which, in the transparent case, could indeed be Nockma). Is that what you have in mind here (or sufficient to implement it)?

Yes, that should be sufficient to implement it!

@cwgoes

Now, it may be difficult to translate arbitrary resource logics (e.g. in Nockma) to CSPs, so we might want to think about what subset we can easily translate, and what kind of structure might be necessary in a resource logic VM in order for it to be easily translatable

Most conjunctives should be fine, but yes we could to a survey, or maybe @AHart might chime in and explain which constructions should be easy to translate. I don’t assume any constraints or invariants developers might need should be too hard to come by, from what I understand.

@cwgoes

I don’t think we need any fancy annotations here, just the transaction function and a transaction data structure which allows for an order of the resource logic arguments to be clearly specified should be sufficient. The transaction data structure should not require running Nockma code to evaluate, though, apart from any resource logics written in Nockma (not sure if you meant to imply that other Nockma code is required or not).

That sounds good to me! And no, I did not mean to imply that extra nockma code is needed here.

@cwgoes

we have a deterministic procedure to evaluate transaction validity, I see no reason to implement that procedure in Nockma or any VM

Then we can just continue using that. Is that specified somewhere already?

@cwgoes

I’m fine with the “stack machine evaluation” as a mental model for how transactions are evaluated, or even as a formal model if we need one for some reason, but I don’t think there’s much benefit in actually implementing it, apart from as a tool for understanding.

If the above model is already specified, we can also transition to using this for intuition, as that removes one layer of indirection.

[cwgoes]

@degregat

Most conjunctives should be fine, but yes we could to a survey, or maybe @AHart might chime in and explain which constructions should be easy to translate. I don’t assume any constraints or invariants developers might need should be too hard to come by, from what I understand.

I think this is worth further investigating. Most VMs we have considered so far (Nockma, Cairo, RISC5) are built for evaluation, not CSP analysis. It might be possible to find something considerably more suitable for automatic CSP translation - and it might also be possible to translate these VMs reasonably easily - I’m not sure yet, but we should investigate.

@degregat

Then we can just continue using that. Is that specified somewhere already?

Yes - it’s specified in the RMv2 report (will soon be ported to the specs as well) - the report does not yet include the modifications I proposed above to enforce the kind of linearity it seems that we want, but they will be added soon.

[degregat]

@cwgoes

I think this is worth further investigating. Most VMs we have considered so far (Nockma, Cairo, RISC5) are built for evaluation, not CSP analysis. It might be possible to find something considerably more suitable for automatic CSP translation - and it might also be possible to translate these VMs reasonably easily - I’m not sure yet, but we should investigate.

Agreed. Maybe a discussion with @AHart, @mariari, @xuyang and/or @camofu in the next week(s) would be good?

@cwgoes

Yes - it’s specified in the RMv2 report (will soon be ported to the specs as well) - the report does not yet include the modifications I proposed above to enforce the kind of linearity it seems that we want, but they will be added soon.

Perfect! That, together with ordered resource logic arguments in the TX data structure should be enought to make the stack based model obsolete, even for reasoning.