[Epic] Compiler Certification Semantic Equivalence Proofs

[ramsay-t]

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 will need some formalisations of notions of equivalence and some modules with useful lemmas etc.
  • [x] https://github.com/IntersectMBO/plutus-private/issues/1488
  • [ ] UPLC Reduction Semantics Determinism Proofs: Proof of ⟶-det and related lemmas in the metatheory.
  • [ ] Reduction Semantics Determinism Proofs: 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 do not ever reduce.
  • [ ] Contextual equivalence framework - functions, operators, etc.
• [ ] Semantic Equivalence proofs for UPLC Phases
  • [ ] UCSE Semantic Equivalence proof
  • [ ] UCaseOfCase Semantic Equivalence proof
  • [ ] UCaseReduce Semantic Equivalence proof
  • [ ] UFloatDelay Semantic Equivalence proof
  • [ ] UForceDelay Semantic Equivalence proof
  • [ ] UntypedTranslation Semantic Equivalence proof
  • [ ] UntypedViews Semantic Equivalence proof

[effectfully]

I've now made it a single Epic issue instead of 1 Epic + God knows how many individual issues. You can spin off new issues once you start working on them or just add PRs to the sprint like I do.