Discussion: RISC-V verification

Stream: general

[Alok Singh]

woah.

big ask: could you comment up some of the elab rules for MLIR? MLIR is something i've wanted to try out for ages and this would be a big help

[Andrés Goens]

@Alok Singh not sure if I know what you mean by elab rules, but if you mean it as in the lean elaborator, (with @Siddharth Bhat and @Alex Keizer) we built an elaboration of MLIR into a typed Lean representation that we can give denotational semantics in https://github.com/opencompl/lean-mlir it's an active project and people are building denotational semantics for more dialects, etc

[Andrés Goens]

(this should probably be moved into a discussion thread by the way, I don't have Zulip permissions to do so)

[Patrick Massot]

This is the discussion thread about #announce > RSIC Zero's zk circuit for RISC-V verification @ 💬

[Alok Singh]

Andrés Goens said:

Alok Singh not sure if I know what you mean by elab rules, but if you mean it as in the lean elaborator, (with Siddharth Bhat and Alex Keizer) we built an elaboration of MLIR into a typed Lean representation that we can give denotational semantics in https://github.com/opencompl/lean-mlir it's an active project and people are building denotational semantics for more dialects, etc

This file https://github.com/NethermindEth/risczero-fv/blob/main/Risc0/MlirTactics.lean