Skip to content

Metatheory: add Value built-in type with postulated functions #7832

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

Open
basetunnel wants to merge 6 commits into
base: master
Choose a base branch
from
Open

Metatheory: add Value built-in type with postulated functions #7832

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
48a9a49
Add Value built-in type and postulated functions to metatheory
basetunnel Sep 18, 2025
6ab5703
Add changelog entry
basetunnel Jul 5, 2026
7edbf50
Restore golden files from haskell conformance tests
basetunnel Jul 9, 2026
23caf7d
Add alternative size measures for Value and Data
basetunnel Jul 9, 2026
e2487fe
Metatheory: use correct measures for args of insertCoin, lookupCoin a…
basetunnel Jul 10, 2026
dac21b8
Simplify runModel
basetunnel Jul 10, 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
143 changes: 0 additions & 143 deletions plutus-conformance/agda/Spec.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -180,60 +180,6 @@ failingEvaluationTests =
, "test-cases/uplc/evaluation/term/constant-case/unit/unit-01"
, "test-cases/uplc/evaluation/term/constant-case/unit/unit-02"
, "test-cases/uplc/evaluation/term/constant-case/unit/unit-03"
, -- The following are failing because the metatheory needs to be updated with
-- Value built-in functions
"test-cases/uplc/evaluation/builtin/constant/value/empty-value"
, "test-cases/uplc/evaluation/builtin/constant/value/max-currencyID-length"
, "test-cases/uplc/evaluation/builtin/constant/value/max-tokenID-length"
, "test-cases/uplc/evaluation/builtin/constant/value/no-overflow"
, "test-cases/uplc/evaluation/builtin/constant/value/no-underflow"
, "test-cases/uplc/evaluation/builtin/constant/value/value-ok-1"
, "test-cases/uplc/evaluation/builtin/constant/value/value-ok-2"
, "test-cases/uplc/evaluation/builtin/semantics/insertCoin/multi-ccy-empty"
, "test-cases/uplc/evaluation/builtin/semantics/insertCoin/multi-ccy-nonempty"
, "test-cases/uplc/evaluation/builtin/semantics/insertCoin/multi-token"
, "test-cases/uplc/evaluation/builtin/semantics/insertCoin/negative-empty"
, "test-cases/uplc/evaluation/builtin/semantics/insertCoin/positive-empty"
, "test-cases/uplc/evaluation/builtin/semantics/insertCoin/positive-nonempty"
, "test-cases/uplc/evaluation/builtin/semantics/insertCoin/zero-positive"
, "test-cases/uplc/evaluation/builtin/semantics/insertCoin/overflow"
, "test-cases/uplc/evaluation/builtin/semantics/insertCoin/no-overflow"
, "test-cases/uplc/evaluation/builtin/semantics/insertCoin/underflow"
, "test-cases/uplc/evaluation/builtin/semantics/insertCoin/no-underflow"
, "test-cases/uplc/evaluation/builtin/semantics/insertCoin/long-key-zero-1"
, "test-cases/uplc/evaluation/builtin/semantics/insertCoin/long-key-zero-2"
, "test-cases/uplc/evaluation/builtin/semantics/insertCoin/key-too-long-1"
, "test-cases/uplc/evaluation/builtin/semantics/insertCoin/key-too-long-2"
, "test-cases/uplc/evaluation/builtin/semantics/lookupCoin/absent"
, "test-cases/uplc/evaluation/builtin/semantics/lookupCoin/present"
, "test-cases/uplc/evaluation/builtin/semantics/unionValue/cancel-01"
, "test-cases/uplc/evaluation/builtin/semantics/unionValue/cancel-02"
, "test-cases/uplc/evaluation/builtin/semantics/unionValue/combine"
, "test-cases/uplc/evaluation/builtin/semantics/unionValue/unitl"
, "test-cases/uplc/evaluation/builtin/semantics/unionValue/unitr"
, "test-cases/uplc/evaluation/builtin/semantics/unionValue/overflow"
, "test-cases/uplc/evaluation/builtin/semantics/unionValue/no-overflow"
, "test-cases/uplc/evaluation/builtin/semantics/unionValue/underflow"
, "test-cases/uplc/evaluation/builtin/semantics/unionValue/no-underflow"
, "test-cases/uplc/evaluation/builtin/semantics/valueContains/ccy-missing"
, "test-cases/uplc/evaluation/builtin/semantics/valueContains/pos-empty"
, "test-cases/uplc/evaluation/builtin/semantics/valueContains/neg-empty"
, "test-cases/uplc/evaluation/builtin/semantics/valueContains/multi-insufficient"
, "test-cases/uplc/evaluation/builtin/semantics/valueContains/multi-sufficient"
, "test-cases/uplc/evaluation/builtin/semantics/valueContains/neg-neg-eq"
, "test-cases/uplc/evaluation/builtin/semantics/valueContains/neg-neg-gt"
, "test-cases/uplc/evaluation/builtin/semantics/valueContains/neg-neg-lt"
, "test-cases/uplc/evaluation/builtin/semantics/valueContains/neg-pos"
, "test-cases/uplc/evaluation/builtin/semantics/valueContains/pos-neg"
, "test-cases/uplc/evaluation/builtin/semantics/valueContains/reflexive"
, "test-cases/uplc/evaluation/builtin/semantics/valueContains/token-missing"
, "test-cases/uplc/evaluation/builtin/semantics/scaleValue/by-zero"
, "test-cases/uplc/evaluation/builtin/semantics/scaleValue/by-pos"
, "test-cases/uplc/evaluation/builtin/semantics/scaleValue/by-neg"
, "test-cases/uplc/evaluation/builtin/semantics/scaleValue/overflow"
, "test-cases/uplc/evaluation/builtin/semantics/scaleValue/underflow"
, "test-cases/uplc/evaluation/builtin/semantics/scaleValue/no-overflow"
, "test-cases/uplc/evaluation/builtin/semantics/scaleValue/no-underflow"
, -- valueData and unValueData builtins
"test-cases/uplc/evaluation/builtin/semantics/valueData/empty"
, "test-cases/uplc/evaluation/builtin/semantics/valueData/single-entry"
Expand Down Expand Up @@ -330,95 +276,6 @@ failingBudgetTests =
, "test-cases/uplc/evaluation/term/constant-case/unit/unit-01"
, "test-cases/uplc/evaluation/term/constant-case/unit/unit-02"
, "test-cases/uplc/evaluation/term/constant-case/unit/unit-03"
, -- The following are failing because the metatheory needs to be updated with
-- Value built-in functions
"test-cases/uplc/evaluation/builtin/constant/value/empty-value"
, "test-cases/uplc/evaluation/builtin/constant/value/max-currencyID-length"
, "test-cases/uplc/evaluation/builtin/constant/value/max-tokenID-length"
, "test-cases/uplc/evaluation/builtin/constant/value/no-overflow"
, "test-cases/uplc/evaluation/builtin/constant/value/no-underflow"
, "test-cases/uplc/evaluation/builtin/constant/value/value-ok-1"
, "test-cases/uplc/evaluation/builtin/constant/value/value-ok-2"
, "test-cases/uplc/evaluation/builtin/semantics/insertCoin/multi-ccy-empty"
, "test-cases/uplc/evaluation/builtin/semantics/insertCoin/multi-ccy-nonempty"
, "test-cases/uplc/evaluation/builtin/semantics/insertCoin/multi-token"
, "test-cases/uplc/evaluation/builtin/semantics/insertCoin/negative-empty"
, "test-cases/uplc/evaluation/builtin/semantics/insertCoin/positive-empty"
, "test-cases/uplc/evaluation/builtin/semantics/insertCoin/positive-nonempty"
, "test-cases/uplc/evaluation/builtin/semantics/insertCoin/zero-positive"
, "test-cases/uplc/evaluation/builtin/semantics/insertCoin/overflow"
, "test-cases/uplc/evaluation/builtin/semantics/insertCoin/no-overflow"
, "test-cases/uplc/evaluation/builtin/semantics/insertCoin/underflow"
, "test-cases/uplc/evaluation/builtin/semantics/insertCoin/no-underflow"
, "test-cases/uplc/evaluation/builtin/semantics/insertCoin/long-key-zero-1"
, "test-cases/uplc/evaluation/builtin/semantics/insertCoin/long-key-zero-2"
, "test-cases/uplc/evaluation/builtin/semantics/insertCoin/key-too-long-1"
, "test-cases/uplc/evaluation/builtin/semantics/insertCoin/key-too-long-2"
, "test-cases/uplc/evaluation/builtin/semantics/lookupCoin/absent"
, "test-cases/uplc/evaluation/builtin/semantics/lookupCoin/present"
, "test-cases/uplc/evaluation/builtin/semantics/unionValue/cancel-01"
, "test-cases/uplc/evaluation/builtin/semantics/unionValue/cancel-02"
, "test-cases/uplc/evaluation/builtin/semantics/unionValue/combine"
, "test-cases/uplc/evaluation/builtin/semantics/unionValue/unitl"
, "test-cases/uplc/evaluation/builtin/semantics/unionValue/unitr"
, "test-cases/uplc/evaluation/builtin/semantics/unionValue/overflow"
, "test-cases/uplc/evaluation/builtin/semantics/unionValue/no-overflow"
, "test-cases/uplc/evaluation/builtin/semantics/unionValue/underflow"
, "test-cases/uplc/evaluation/builtin/semantics/unionValue/no-underflow"
, "test-cases/uplc/evaluation/builtin/semantics/valueContains/ccy-missing"
, "test-cases/uplc/evaluation/builtin/semantics/valueContains/pos-empty"
, "test-cases/uplc/evaluation/builtin/semantics/valueContains/neg-empty"
, "test-cases/uplc/evaluation/builtin/semantics/valueContains/multi-insufficient"
, "test-cases/uplc/evaluation/builtin/semantics/valueContains/multi-sufficient"
, "test-cases/uplc/evaluation/builtin/semantics/valueContains/neg-neg-eq"
, "test-cases/uplc/evaluation/builtin/semantics/valueContains/neg-neg-gt"
, "test-cases/uplc/evaluation/builtin/semantics/valueContains/neg-neg-lt"
, "test-cases/uplc/evaluation/builtin/semantics/valueContains/neg-pos"
, "test-cases/uplc/evaluation/builtin/semantics/valueContains/pos-neg"
, "test-cases/uplc/evaluation/builtin/semantics/valueContains/reflexive"
, "test-cases/uplc/evaluation/builtin/semantics/valueContains/token-missing"
, "test-cases/uplc/evaluation/builtin/semantics/scaleValue/by-zero"
, "test-cases/uplc/evaluation/builtin/semantics/scaleValue/by-pos"
, "test-cases/uplc/evaluation/builtin/semantics/scaleValue/by-neg"
, "test-cases/uplc/evaluation/builtin/semantics/scaleValue/overflow"
, "test-cases/uplc/evaluation/builtin/semantics/scaleValue/underflow"
, "test-cases/uplc/evaluation/builtin/semantics/scaleValue/no-overflow"
, "test-cases/uplc/evaluation/builtin/semantics/scaleValue/no-underflow"
, -- valueData and unValueData builtins
"test-cases/uplc/evaluation/builtin/semantics/valueData/empty"
, "test-cases/uplc/evaluation/builtin/semantics/valueData/single-entry"
, "test-cases/uplc/evaluation/builtin/semantics/valueData/multi-token"
, "test-cases/uplc/evaluation/builtin/semantics/valueData/multi-currency"
, "test-cases/uplc/evaluation/builtin/semantics/valueData/negative-quantity"
, "test-cases/uplc/evaluation/builtin/semantics/valueData/roundtrip-from-value"
, "test-cases/uplc/evaluation/builtin/semantics/unValueData/empty"
, "test-cases/uplc/evaluation/builtin/semantics/unValueData/single-entry"
, "test-cases/uplc/evaluation/builtin/semantics/unValueData/multi-token"
, "test-cases/uplc/evaluation/builtin/semantics/unValueData/multi-currency"
, "test-cases/uplc/evaluation/builtin/semantics/unValueData/negative-quantity"
, "test-cases/uplc/evaluation/builtin/semantics/unValueData/max-key-len"
, "test-cases/uplc/evaluation/builtin/semantics/unValueData/roundtrip-from-data"
, "test-cases/uplc/evaluation/builtin/semantics/unValueData/data-duplicate-tokens"
, "test-cases/uplc/evaluation/builtin/semantics/unValueData/data-duplicate-currencies"
, "test-cases/uplc/evaluation/builtin/semantics/unValueData/data-duplicate-currencies-cancel"
, "test-cases/uplc/evaluation/builtin/semantics/unValueData/data-duplicate-currencies-merge"
, "test-cases/uplc/evaluation/builtin/semantics/unValueData/data-zero-quantity"
, "test-cases/uplc/evaluation/builtin/semantics/unValueData/data-zero-sum"
, "test-cases/uplc/evaluation/builtin/semantics/unValueData/data-empty-tokens"
, "test-cases/uplc/evaluation/builtin/semantics/unValueData/data-unordered-currencies"
, "test-cases/uplc/evaluation/builtin/semantics/unValueData/data-unordered-tokens"
, "test-cases/uplc/evaluation/builtin/semantics/unValueData/non-map-integer"
, "test-cases/uplc/evaluation/builtin/semantics/unValueData/non-map-constr"
, "test-cases/uplc/evaluation/builtin/semantics/unValueData/non-map-list"
, "test-cases/uplc/evaluation/builtin/semantics/unValueData/non-map-bytes"
, "test-cases/uplc/evaluation/builtin/semantics/unValueData/currency-key-too-long"
, "test-cases/uplc/evaluation/builtin/semantics/unValueData/token-key-too-long"
, "test-cases/uplc/evaluation/builtin/semantics/unValueData/quantity-overflow"
, "test-cases/uplc/evaluation/builtin/semantics/unValueData/quantity-underflow"
, "test-cases/uplc/evaluation/builtin/semantics/unValueData/non-bytestring-currency"
, "test-cases/uplc/evaluation/builtin/semantics/unValueData/non-bytestring-token"
, "test-cases/uplc/evaluation/builtin/semantics/unValueData/non-integer-quantity"
, "test-cases/uplc/evaluation/builtin/semantics/unValueData/non-map-tokens"
]

-- Run the tests: see Note [Evaluation with and without costing] above.
Expand Down
41 changes: 41 additions & 0 deletions ...s-metatheory/changelog.d/20260705_163047_4022046+basetunnel_metatheory_value.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,41 @@
<!--
A new scriv changelog fragment.

Uncomment the section that is right (remove the HTML comment wrapper).
For top level release notes, leave all the headers commented out.
-->

<!--
### Removed

- A bullet item for the Removed category.

-->
### Added

- Postulated definitions for `Value` and its corresponding built-in functions

<!--
### Changed

- A bullet item for the Changed category.

-->
<!--
### Deprecated

- A bullet item for the Deprecated category.

-->
<!--
### Fixed

- A bullet item for the Fixed category.

-->
<!--
### Security

- A bullet item for the Security category.

-->
1 change: 1 addition & 0 deletions plutus-metatheory/plutus-metatheory.cabal
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -79,6 +79,7 @@ library
, base
, bytestring
, composition-prelude
, containers
, deepseq
, directory
, extra
Expand Down
21 changes: 20 additions & 1 deletion plutus-metatheory/src/Algorithmic/CEK.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ open _⊢_
open _∋_
open import Algorithmic.RenamingSubstitution using (Sub;sub;exts;exts⋆;_[_];_[_]⋆)
open import Builtin
open import Utils hiding (List;length) renaming (_,_ to _,,_)
open import Utils hiding (List;length;Value) renaming (_,_ to _,,_)

open import Builtin.Constant.AtomicType
open import Builtin.Constant.Type using (TyCon)
Expand Down Expand Up @@ -267,6 +267,25 @@ BUILTIN unMapData (base $ V-con _) = inj₁ (con (ne (^ (atomic aData))))
BUILTIN unListData (base $ V-con (ListDATA x)) = inj₂ (V-con x)
BUILTIN unListData (base $ V-con _) = inj₁ (con (ne (^ (atomic aData))))
BUILTIN serialiseData (base $ V-con d) = inj₂ (V-con (serialiseDATA d))
BUILTIN insertCoin (base $ V-con ccy $ V-con tok $ V-con x $ V-con v) with insertCOIN ccy tok x v
... | just v' = inj₂ (V-con v')
... | nothing = inj₁ (con (ne (^ (atomic aValue))))
BUILTIN lookupCoin (base $ V-con ccy $ V-con tok $ V-con v) = inj₂ (V-con (lookupCOIN ccy tok v))
BUILTIN unionValue (base $ V-con v1 $ V-con v2) with unionVALUE v1 v2
... | just v' = inj₂ (V-con v')
... | nothing = inj₁ (con (ne (^ (atomic aValue))))
BUILTIN valueContains (base $ V-con v1 $ V-con v2) with valueCONTAINS v1 v2
... | just b = inj₂ (V-con b)
... | nothing = inj₁ (con (ne (^ (atomic aValue))))
BUILTIN scaleValue (base $ V-con n $ V-con v) with scaleVALUE n v
... | just v' = inj₂ (V-con v')
... | nothing = inj₁ (con (ne (^ (atomic aValue))))
BUILTIN valueData (base $ V-con v) with valueDATA v
... | just d = inj₂ (V-con d)
... | nothing = inj₁ (con (ne (^ (atomic aValue))))
BUILTIN unValueData (base $ V-con d) with unValueDATA d
... | nothing = inj₁ (con (ne (^ (atomic aValue))))
... | just v = inj₂ (V-con v)
BUILTIN mkNilData (base $ V-con _) = inj₂ (V-con [])
BUILTIN mkNilPairData (base $ V-con _) = inj₂ (V-con [])
BUILTIN chooseUnit (Λ̂ A $ x $ V-con _) = inj₂ x
Expand Down
2 changes: 1 addition & 1 deletion plutus-metatheory/src/Algorithmic/ReductionEC.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ open import Relation.Binary.PropositionalEquality
open import Relation.Binary.HeterogeneousEquality
using (_≅_;refl;≅-to-≡)

open import Utils hiding (List;length;map)
open import Utils hiding (List;length;map;Value)
Comment thread
ana-pantilie marked this conversation as resolved.
open import Utils.List
open import Type using (Ctx⋆;∅;_,⋆_;_⊢⋆_;_∋⋆_;Z)
open _⊢⋆_
Expand Down
2 changes: 1 addition & 1 deletion plutus-metatheory/src/Algorithmic/ReductionEC/Determinism.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ open import Relation.Binary.PropositionalEquality
open import Relation.Binary.HeterogeneousEquality
using (_≅_;refl;≅-to-≡)

open import Utils hiding (_×_;List)
open import Utils hiding (_×_;List;Value)
Comment thread
ana-pantilie marked this conversation as resolved.
open import Utils.List
open import Type using (Ctx⋆;∅;_,⋆_;_⊢⋆_;_∋⋆_;Z)
open _⊢⋆_
Expand Down
Loading
Loading