Skip to content

Use reflection to generate injectivity proof for builtins #7746

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
ana-pantilie wants to merge 2 commits into
base: master
Choose a base branch
from
Draft

Use reflection to generate injectivity proof for builtins #7746

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
cb6f81e
WIP: use reflection to generate injectivity proof for builtins
ana-pantilie Apr 28, 2026
6d4db58
Tmp
ana-pantilie Apr 29, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
29 changes: 24 additions & 5 deletions plutus-metatheory/src/Builtin.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@ open _⊢♯ renaming (pair to bpair; list to blist; array to barray)
open _/_⊢⋆
open import Builtin.Constant.AtomicType

open import Utils.Reflection using (defDec;defShow;defEnum;defListConstructors)
open import Utils.Reflection using (defDec;defShow;defEnum;defFromEnum;defListConstructors)
```

## Built-in functions
Expand Down Expand Up @@ -688,15 +688,34 @@ Equality of Builtins is decidable. In order to prove equality we would have to p
enumBuiltin : Builtin → ℕ
unquoteDef enumBuiltin = defEnum (quote Builtin) enumBuiltin

fromEnumBuiltin : ℕ → Maybe Builtin
unquoteDef fromEnumBuiltin = defFromEnum (quote Builtin) fromEnumBuiltin

open import Agda.Builtin.Equality using (_≡_)
open import Agda.Builtin.TrustMe using (primTrustMe)
open import Relation.Binary.PropositionalEquality using (cong)
open import Relation.Binary.PropositionalEquality using (cong; sym)
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Data.Maybe.Properties using (just-injective)
open import Relation.Binary.Reasoning.Syntax
open import Function.Base using (id; _∘_)
open import Relation.Binary.PropositionalEquality.Core
using (_≡_; cong; refl; subst; trans; sym; subst₂; cong₂)

-- TODO: this should be generated
decode-encode : ∀ x → fromEnumBuiltin (enumBuiltin x) ≡ just x
unquoteDef decode-encode = defDecodeEncode (quote Builtin) decode-encode

-- TODO: this should be safe since enumBuiltin is generated; can it be proven without having to
-- explicitly match on all n² cases?
enumBuiltin-injective : (b1 b2 : Builtin) → enumBuiltin b1 ≡ enumBuiltin b2 → b1 ≡ b2
enumBuiltin-injective b1 b2 b1≡b2 = primTrustMe
enumBuiltin-injective x y p = just-injective (
begin
just x ≡⟨ sym (decode-encode x) ⟩
fromEnumBuiltin (enumBuiltin x) ≡⟨ cong fromEnumBuiltin p ⟩
fromEnumBuiltin (enumBuiltin y) ≡⟨ decode-encode y ⟩
just y
∎)
where
open Relation.Binary.PropositionalEquality.≡-Reasoning


decBuiltin : DecidableEquality Builtin
decBuiltin b1 b2 with (enumBuiltin b1) Data.Nat.≟ (enumBuiltin b2)
Expand Down
Loading
Loading