I wrote some code to extract the axioms from Strata.Boogie code (see Strata/Languages/Boogie/Examples/DDMAxiomExtractionExample.lean).
I cannot just call that in the Factory.lean as this creates a cycle in the imports.
However, we can at least copy/paste them, which is cleaner and less error prone. This could be automated via a script I guess.

For that to work though, the update and select functions must be typed, so I modified the translation to add the types.

The axiom generation should probably be elsewhere, any suggestion?

The CI fails because the Lambda translation now adds type information to applications of update and select, which change the guard messsages.

I'm inclined to merge this as-is because it provides functionality we really want and will serve as a regular reminder to encourage us to implement a way to write the axioms more concisely. :)

I'm just waiting on Shilpi's PR to be merged to un comment the concise version that is working :)

I'm inclined to merge this as-is because it provides functionality we really want and will serve as a regular reminder to encourage us to implement a way to write the axioms more concisely. :)

I'm just waiting on Shilpi's PR to be merged to un comment the concise version that is working :)

Ah, nice! In that case, let's wait for that PR.

There you go @atomb :)