Add B3 Language Support as Strata Backend Dialect

[MikaelMayer]

Add B3 Language Support as Strata Backend Dialect

This PR adds complete support for the B3 verification language as a new Strata backend dialect.

The implementation successfully parses the entire B3 motivating example as-is.

DDM Definition

Three components:

1. Concrete Syntax Tree (ParseCST.lean) - Defines B3's concrete syntax using DDM

   • Matches B3 language syntax including dots in identifiers (e.g., Map.select)
   • Pipe-delimited identifiers for special cases (e.g., |@0|)

2. Abstract Syntax Tree (DefinitionAST.lean) - Defines B3's abstract syntax for Strata Core

   • De Bruijn indices for variable binding
   • Metadata unwrapping with @[unwrap] to simplify terminal nodes
   • Customizable metadata mapping

3. Bidirectional Conversion (Conversion.lean) - AST ↔ CST conversion

   • Error tracking for unresolved identifiers, out-of-bounds references, and unsupported variable patterns

Technical Highlights

• Inout parameters: Modeled as two values in the context (old and current), enabling old x syntax in procedure bodies and postconditions to reference pre-state values
• Shadowed variables: Proper handling with disambiguation and detection of unsupported middle occurrences

Testing

Tests split across four categories: expressions, statements, declarations, and programs.

Round-trip tests display a formatted and minimal version of the AST in the conversion for better understanding.

Future Work

• Verify B3 text files by invoking the B3 tool from Strata
• Convert Strata Core to B3 AST for backend verification

[atomb]

Why have Expression and Stmt types in here instead of using Lambda.LExpr and Imperative.Stmt? The DDM definition for B3 will allow capturing the exact syntax of B3, but I don't think we need to define it again beyond that.

[MikaelMayer]

Why have Expression and Stmt types in here instead of using Lambda.LExpr and Imperative.Stmt? The DDM definition for B3 will allow capturing the exact syntax of B3, but I don't think we need to define it again beyond that.

If DDM is sufficient for my needs, then yes I'll use it. This is still a work in progress. You commented on this PR just before I enabled the draft mode.

[atomb]

If DDM is sufficient for my needs, then yes I'll use it. This is still a work in progress. You commented on this PR just before I enabled the draft mode.

If the DDM isn't sufficient, we should improve it until it is.

[atomb]

My main reaction to it is the same one as my original comment on the PR. It totally makes sense to have the B3 CST, but I think the B3 AST just duplicates what's in LExpr, Stmt, and Cmd. On the expression side, labeled expressions and let expressions aren't currently in LExpr, but labels to me seem like they should be metadata and let expressions could be either added to LExpr or encoded. I'm undecided which makes more sense.

On the command side, B3 includes check and reach, but we've already decided we'd like to add those to the Cmd type one way or another. On the statement side, B3 includes exit, but we've also already decided to add that to Stmt. The current goto is a stopgap that'll be unnecessary once we have an unstructured representation alongside the structured one. There's a draft PR for that already: #202. Finally, it includes ifcase and choose. We can encode those using other control flow, and I'd argue that that's the right way to do it. Having a non-deterministic choose is useful, but I think it makes sense to represent programs either fully deterministically, like in Stmt, or fully non-deterministically, like in NondetStmt, and to be able to go back and forth. Any given analysis works better if either everything's in one form or everything's in the other form.

Finally, procedure declarations include inout parameters. The procedure notions in Boogie, which should move to Imperative, don't yet include that, but should.