Jcb/ix tests #134
Jcb/ix tests #134
Conversation
- CompileM is now persistent with the filemapped store - constructing evaluation claims is done through MetaM rather than CompileM - CLI now features the Prove command
…sts for new mutdef format
| | _, .none => .error "bad address {meta}" | ||
| let cont <- StoreIO.toIO (Store.readConst c) | ||
| let meta <- StoreIO.toIO (Store.readConst m) | ||
| let ix := Ix.TransportM.rematerialize cont meta |
There was a problem hiding this comment.
Would it make sense to call this just "materialize"? In some cases, one might want to materialize something that was never read from a Lean source, like the result of some reduction by the IxVM.
There was a problem hiding this comment.
the analogy is with the star trek transporter https://en.wikipedia.org/wiki/Transporter_(Star_Trek), which dematerializes in one place and rematerializes somewhere else. Here dematerialization means the transformation from Ix.IR into an Ixon.Const and Ixon.Metadata. The IxVM operates just over the Ixon.Const, since the metadata isn't relevant for proving. In the proving case, we also already know the output from building the claim.
If we wanted to reduce Ix constants in a non-proving context and construct new outputs, then that would need an "Ix Runtime" which should operate over Ix.IR, not Ixon, as you'd want to also transform the metadata so that the output is human readable
big refactor of the ix compiler, the ixon format and implementation of the decompiler
roundtrip compilation/decompilation of Std, Lean and Ix itself now working (modulo Expr.mdata, which is currently not captured by Ixon metadata, but arguably should be)