Zulip Chat Archive

Stream: general

Topic: Discussion: RISC-V verification


Alok Singh (Feb 20 2025 at 06:33):

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 (Feb 20 2025 at 06:59):

@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 (Feb 20 2025 at 07:00):

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

Patrick Massot (Feb 20 2025 at 08:36):

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

Alok Singh (Feb 20 2025 at 21:13):

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


Last updated: May 02 2025 at 03:31 UTC