IntersectMBO / IntersectMBO/plutus
[Epic] Compiler Certification Semantic Equivalence Proofs
- Dominant language
- Haskell
- Stars
- 1.6k
- Forks
- 508
- Avg merge
- 3d 10h
- Merged PRs (30d)
- 22
Description
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
Contributor guide
Assessment
This issue has not been assessed yet.