Issue #124 details the Lair-side changes that are necessary to support Loam. We also need some Loam-side changes in order to integrate with Lair.
[ ] Trace generation to produce the partial witnesses needed by Lair for proving (a.k.a. the QueryRecords)
[ ] Extending the loam! macro to generate Lair code, or more directly a Lair AST.
I think we can expect trace generation to be fairly straightforward to implement.
For more on the second point: Given #124, i.e. if we have the provide and require opcodes, we can directly translate the relation clauses in each rule. The other conditional causes need to be arithmetized into Lair, which can also happen directly with some modification to ascent!, e.g. allowing the user to embed any Lair syntax into the rules, which we can paste into the generated Lair function. Finally, as discussed with @wwared and @gabriel-barrett, Loam chips and Lair functions aren't exactly semantically the same, so some coordination has to happen on this boundary for a complete integration.
Issue #124 details the Lair-side changes that are necessary to support Loam. We also need some Loam-side changes in order to integrate with Lair.
QueryRecords)loam!macro to generate Lair code, or more directly a Lair AST.I think we can expect trace generation to be fairly straightforward to implement.
For more on the second point: Given #124, i.e. if we have the
provideandrequireopcodes, we can directly translate the relation clauses in each rule. The other conditional causes need to be arithmetized into Lair, which can also happen directly with some modification toascent!, e.g. allowing the user to embed any Lair syntax into the rules, which we can paste into the generated Lair function. Finally, as discussed with @wwared and @gabriel-barrett, Loam chips and Lair functions aren't exactly semantically the same, so some coordination has to happen on this boundary for a complete integration.