Ramsay Taylor

Add arrays to metatheory

1

Fixes https://github.com/IntersectMBO/plutus-private/issues/1465

Fixes https://github.com/IntersectMBO/plutus-private/issues/1600 Fixes https://github.com/IntersectMBO/plutus/issues/6529

Proof of ⟶-det and related lemmas in the metatheory. ⟶-det is the proof that reduction is deterministic, and it depends on the value-¬⟶ and ⟶-¬value lemmas that show that Values...

Proof of ⟶-det and related lemmas in the metatheory.

There is a disagreement between the simplifier and the certifier about the inline phase. This is probably a bug in the certifier's `UInline` decision procedure. First we need to identify...

[Epic] Compiler Certification Semantic Equivalence Proofs

1

This will need a number of stages: - [x] #6612 - [x] #6613 - [ ] To produce Semantic Equivalence proofs in "Semantic Equivalence proofs for UPLC Phases" below we...

Semantic Equivalence proof support modules

1

To produce Semantic Equivalence proofs in #6615 we will need some formalisations of notions of _equivalence_ and some modules with useful lemmas etc. - [ ] #7008 - [ ]...