Add array axiomatization as a standalone SMT-IR transformation

[abdoo8080]

Issue #, if available:

N/A

Description of changes:

Add a shallow Lean model of the SMT-LIB ArraysEx theory so the metaverifier can denote Map programs under array theory, and route the useArrayTheory flag through the proof path so the generated Lean goals actually land on it.

Key changes:

• New Strata/DL/SMT/SmtArray.lean: SmtArray α β is the total function space α → β, exposed only through select, store, const, and the SMT-LIB array axioms (select_const, select_store_self, select_store_of_ne, ext). The constructor and underlying projection are private so downstream code can only use the axiomatic API.
• Strata/DL/SMT/Translate.lean and Strata/DL/SMT/Denote.lean: translate the SMT-IR Array A B sort to SmtArray A B, and select/store array-theory terms to SmtArray.select/SmtArray.store. Adds the supporting denoteSortArray_* lemmas.
• Strata/MetaVerifier.lean: genCoreVCs now sets useArrayTheory := true for each dialect's proof path (Core, C_Simp, Boole), and Core.ProofObligation.toSMTObligation passes that flag through to Core.ProofObligation.toSMTTerms so it actually reaches the encoder. Without this, the encoder defaulted to false and the proof goals came out using an abstract Map-sort + uninterpreted select UF instead of SmtArray + .select/.store.
• Boole proof updates: widening_casts.lean and map_extensionality.lean gen_smt_vcs proofs now intro fewer binders (no abstract Map/select sort/UF) and close against the new SmtArray goal — exact hNonneg (v.select i) / exact hPointwise i.

Read-over-write semantics under useArrayTheory = false is left unchanged: the SMT encoder's generic factory handler already instantiates Core.mapUpdateFunc.axioms at each update call site. Under useArrayTheory = true the encoder's select/update special case short-circuits before that handler, so those axioms aren't added — which is what we want, because array theory provides r-o-w natively.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

🤖 Generated with Claude Code

Co-Authored-By: Claude Opus 4.7 (1M context) noreply@anthropic.com
Co-Authored-By: Claude Fable 5 noreply@anthropic.com

[atomb]

This PR in and of itself looks pretty good. However, I wonder whether it would make more sense to do this axiomatization as a Core -> Core transformation. That is, the SMT backend would always use the Array theory for the Map type, but the Core -> Core transformation could replace Map with another type that came along with some uninterpreted functions and axioms. There would be several reasons to do this:

• Other proof engines that don't use SMT could make use of the axioms.
• We could add models for the axioms in Lean, to ensure that they're consistent. Fully connecting these to the axioms would require denotations for Lambda expressions (coming soon!), but there's an example of a (currently not connected) model of Sequence in terms of List here: https://github.com/strata-org/Strata/blob/main/Strata/Languages/Core/SeqModel.lean

[abdoo8080]

Thanks for the feedback! I have the same intention but at the SMT level. This PR is mainly to get initial feedback before doing the same for more complex theories like sequences and datatypes (which many performant solvers like Bitwuzla don't support), so the design matters more for those cases than for arrays specifically.

The reason I chose the SMT IR layer over Core IR is that other higher-level IRs that don't go through Core can also make use of these passes, and the SMT IR is a simpler language, so the rewriting is more straightforward. I can also add denotational semantics for the new theories on top of the already existing SMT IR semantics, which gives a path to proving the axiomatizations sound at that level.

That said, I do see the appeal of a Core-to-Core pass, especially for non-SMT backends and for connecting axiom models in Lean. I'm fine with either approach as long as I can:

• Axiomatize theories selectively (e.g., axiomatize datatypes but not sequences).
• Extend the SMT IR with richer theories (e.g., sequences) even if they aren't used by default, since those are needed as targets for the Lean backend.

Happy to contribute to either or both! Would it make sense to discuss which theories belong at which layer?

P.S. I wonder if Sequence in Core IR corresponds better to Lean's Array than to Lean's List, given that Array is accessed by index while List is typically eliminated via its constructors. Note that SMT-LIB's theory of arrays is a different concept with no direct Lean counterpart.

[atomb]

In general, the hope is that every high-level IR can go through Core on the path to some form of analysis. But you're very right that a Core -> Core pass wouldn't do much good for a pipeline that didn't go through Core!

Both of your bullets are things I think would be good, too.

Given that there's already a denotational semantics for SMT in the codebase, and that such semantics for Lambda are still to come, what would you think of taking a stab at coming up with a model for the Array theory and linking it to the axioms your current code generates? If we had that, I think I'd be happy, even if we do ultimately wind up doing the translation at the Core level.

As far as how to construct that model, I don't think it matters as long as it satisfies the axioms and therefore shows them to be consistent. I suspect functions would work as a model for Map. As you point out, Array would work as a model for Sequence. But List also has the associated operations, and I think it largely doesn't matter what model we use as long as it has no assumptions.

[abdoo8080]

Sounds good! SmtArray.lean contains a model for SMT arrays using functions as you suggested.

Two theorems correspond directly to the axioms in the transformation pass and Core's functions factory. The third theorem corresponds to the SMT-LIB extensionality axiom, which is (surprisingly?) missing from Core's functions factory (and, therefore, missing from the axiomatization pass). I added it as a theorem regardless since it's part of the SMT-LIB standard axioms. Should I add it to the axiomatization pass as well?

The last theorem corresponds to the SMT-LIB store preservation axiom. It looks slightly different from the axiom in Core's functions factory, though it's still equivalent: j ≠ i → (a.store i v).select j = a.select j vs. if j = i then true else (a.store i v).select j = a.select j.

[abdoo8080]

what would you think of taking a stab at coming up with a model for the Array theory and linking it to the axioms your current code generates?

The Lean backend now makes use of SmtArray when generating Lean goals. Proving that the array axiomatization pass preserves SMT-LIB semantics will be quite challenging (and probably impossible without the extensionality axiom). The 4 theorems do seem to be sufficient for grind to discharge the generated VCs with the axiomatization pass disabled though (e.g., find_max.lean).

[kondylidou]

@abdoo8080 I'm fixing the merge coflicts. Please have a look at my changes to see if they are ok

[atomb]

The Lean backend now makes use of SmtArray when generating Lean goals. Proving that the array axiomatization pass preserves SMT-LIB semantics will be quite challenging (and probably impossible without the extensionality axiom). The 4 theorems do seem to be sufficient for grind to discharge the generated VCs with the axiomatization pass disabled though (e.g., find_max.lean).

Yeah, I think that proving that the pass preserves semantics isn't needed for now (though the rest of the Strata team may work on it at some point this year). Having a model for the axioms is the key thing, and the one you've added looks very nice.

My one option question: is the proof of find_max using grind without the axiomatization pass the one that's happening in CI now, or is that something you just tried out-of-band? And if it's not in CI yet, could you add it?

[abdoo8080]

My one option question: is the proof of find_max using grind without the axiomatization pass the one that's happening in CI now, or is that something you just tried out-of-band? And if it's not in CI yet, could you add it?

Yes. SmtArray is now used for the Lean backend. It's why I added the grind attributes to the theorems. Some of the theorems are needed for grind to prove the correctness of VCs generated for find_max.

[atomb]

Thanks for contributing this!

[abdoo8080]

Could you please make a plan on the feasibility of migrating your code to a Core to Core transformation? I'm still inclined to go that route even if it means contributing to this PR or fixing other issues before so that this PR can be migrated to Core.

@MikaelMayer, after thinking about it for a while, I decided to reduce the scope of this PR to just add a model SMT-LIB arrays (SmtArray) which treats them as functions (there are other more permissive interpretations).

The reason I'm comfortable shrinking it: the factory's Core.mapUpdateFunc.axioms already give us "use by default, drop when array theory is on" without any Core pass. Under useArrayTheory = false the SMT encoder's generic factory handler instantiates those axioms at every update call site; under useArrayTheory = true the select/update special case short-circuits before that handler, so the axioms aren't asserted (which is what we want: array theory provides read-over-write natively). I had a Core-IR ArrayElim pass that just re-emitted the same instantiated axioms as Decl.ax, but it turned out to be entirely redundant with what the encoder is already doing, so I dropped it.

If you still want an ArrayElim pass or prefer it over the factory's axioms. I can go ahead and add it. However, I do not need it for the Lean backend.

[aqjune-aws]

Hi Abdal, Mikael is on vacation in this summer. I can volunteer as another reviewer.

One question is about the support of datatype in denotational semantics of SMT-LIB, because this is adding the array theory to the semantics. The extension of the semantics to support arrays is welcome, but I wonder what's your thought about extending it to generic datatypes in SMT-LIB - will it be a significant challenge compared to a lightweight, special coding for arrays?

[abdoo8080]

Hello @aqjune-aws, thanks for volunteering!

Short answer to your question: generic datatypes will be a bigger lift than the lightweight array coding, but I don't think we want to special-case them.

I initially wanted to denote inductive datatypes via W-types in Lean. However, @joscoh managed to convince me that an axiomatization of datatypes could be a better option. His reasoning, backed by previous experience, is that even though W-types work as a denotation of inductive types, they're very painful to work with once you get to denoting recursive functions. IIUC, his idea is to encapsulate the properties of an inductive datatype and its constructors inside a type-class and then instantiate those properties with native Lean datatypes at VC-gen time via the meta framework. Since the type is universally quantified in this approach, we also need to show that any two types instantiating the same SMT datatype are isomorphic (which is really just the soundness condition that the class actually pins the datatype down). Honestly, this doesn't seem any easier than the W-types approach (the opposite is probably true). But it doesn't prevent the use of W-types, which naturally instantiate the type-class, and it lets us use native datatypes, which Clark has been saying we should do!

BTW this somewhat relates to the PR: I model SMT-LIB arrays with a concrete SmtArray wrapper over functions, which works fine. But the same trick would let us depend on an IsSmtArray type-class instead and instantiate it with whatever type we want.

[aqjune-aws]

IIUC, his idea is to encapsulate the properties of an inductive datatype and its constructors inside a type-class and then instantiate those properties with native Lean datatypes at VC-gen time via the meta framework. Since the type is universally quantified in this approach, we also need to show that any two types instantiating the same SMT datatype are isomorphic (which is really just the soundness condition that the class actually pins the datatype down). Honestly, this doesn't seem any easier than the W-types approach (the opposite is probably true). But it doesn't prevent the use of W-types, which naturally instantiate the type-class, and it lets us use native datatypes, which Clark has been saying we should do!

It is really great to have this kind of discussion in this project. Looking forward to the general support for datatype.

Since the scope of general support for datatypes will be much larger and take a long time whereas the primary support of array will already unlock many interesting cases, I am fine with going through adding a support for array first (hence the scope of this PR is fine with me).
The internship scope of @amanda-zx in this summer will be showing that lowering Lambda to SMT-LIB is correct w.r.t denotational semantics of Lambda and SMT-LIB.
Another question what is the relation between generic support for datatype and #1273 ?

[abdoo8080]

Another question what is the relation between generic support for datatype and #1273?

#1273 is an attempt to eliminate datatypes by asserting only some of their axioms. Since implementing a full denotation of datatypes is quite involved, it's a way to support them in the Lean backend without a denotation.

The internship scope of @amanda-zx in this summer will be showing that lowering Lambda to SMT-LIB is correct w.r.t denotational semantics of Lambda and SMT-LIB.

The current denotation of the SMT IR is hacky and probably not good for verification imo (improvements are welcome!). Happy to meet with both of you to explain how it works! There were some discussions to lift the SMT IR on top of Lambda and make use of Josh's denotation (in which case lowering wouldn't be necessary), but it appears this is just a discussion, with no plans to go ahead so far.

[aqjune-aws]

Happy to meet with both of you to explain how it works! There were some discussions to lift the SMT IR on top of Lambda and make use of Josh's denotation (in which case lowering wouldn't be necessary), but it appears this is just a discussion, with no plans to go ahead so far.

OK, let us set up a meeting soon. :)

[atomb]

This has evolved into an elegant solution for a slice of the problem. Nice work! And I'm sure it can be followed up with other threads of exciting work based on the discussion in the comments.