From f33be724318bfed8d9d7856d38667669926006b3 Mon Sep 17 00:00:00 2001 From: Ana Pantilie Date: Tue, 26 May 2026 18:51:42 +0300 Subject: [PATCH 1/3] WIP: contextual semantics --- .../src/Untyped/ContextualSemantics.lagda.md | 135 ++++++++++++++++++ 1 file changed, 135 insertions(+) create mode 100644 plutus-metatheory/src/Untyped/ContextualSemantics.lagda.md diff --git a/plutus-metatheory/src/Untyped/ContextualSemantics.lagda.md b/plutus-metatheory/src/Untyped/ContextualSemantics.lagda.md new file mode 100644 index 00000000000..855f7ba4357 --- /dev/null +++ b/plutus-metatheory/src/Untyped/ContextualSemantics.lagda.md @@ -0,0 +1,135 @@ +--- +title: Contextual Semantics +layout: page +--- + +``` +module Untyped.ContextualSemantics where +``` + +## Imports + +``` +open import Untyped +open import Data.Nat using (ℕ; suc; _+_; _<_; _≤_) +open import Data.List using (List; _++_) +import Data.List as List +open import Data.List.Relation.Unary.All using (All) +open import Builtin +open import Builtin.Signature using (args♯; Sig) +open import Untyped.RenamingSubstitution using (_[_]) +open import Data.Vec using (Vec) +import Data.List.NonEmpty as NE +import Data.Vec as Vec +import Data.Fin as Fin +open import Relation.Binary.PropositionalEquality using (_≡_) + +``` + +## TODO + +``` +variable + n : ℕ + +data B : n ⊢ → Set +data Value : n ⊢ → Set +data A : {X : n ⊢} → B X → Set + +data B where + builtinB + : (b : Builtin) + → B {n} (builtin b) + appB + : {t₁ t₂ : n ⊢} + → B t₁ + → Value t₂ + → B (t₁ · t₂) + forceB + : {t : n ⊢} + → B t + → B (force t) + +β : {X : n ⊢} → B X → Builtin +β (builtinB b) = b +β (appB b v) = β b +β (forceB b) = β b + +||_|| : {X : n ⊢} → B X → ℕ +||_|| (builtinB b) = 0 +||_|| (appB b v) = 1 + || b || +||_|| (forceB b) = 1 + || b || + +data A where + builtinA + : {b : Builtin} + → A {n} (builtinB b) + appA + : {t₁ t₂ : n ⊢} (b : B (t₁ · t₂)) + → || b || < args♯ (signature (β b)) + -- TODO: quantification? + → A {n} b + forceA + : {t : n ⊢} (b : B (force t)) + → || b || < 1 -- TODO: we don't formalize quantifications, in practice I've only seen them applied directly to 'builtin b', but this should be fixed separately + → A {n} b + +data Value where + conᵥ : (t : TmCon) → Value {n} (con t) + delayᵥ : (t : n ⊢) → Value (delay t) + ƛᵥ : (t : suc n ⊢) → Value (ƛ t) + constrᵥ : (i : ℕ) (ts : List (n ⊢)) → All Value ts → Value (constr i ts) + bAppᵥ : {t : n ⊢} {b : B t} → A b → Value t + +data Frame : n ⊢ → Set where + □ + : {t : n ⊢} + → Frame t + _ᶠ·_ + : {t₁ : n ⊢} + → Frame t₁ + → (t₂ : n ⊢) + → Frame (t₁ · t₂) + _·ᶠ_ + : {t₁ t₂ : n ⊢} + → Value t₁ + → Frame t₂ + → Frame (t₁ · t₂) + forceᶠ + : {t : n ⊢} + → Frame t + → Frame (force t) + constrᶠ + : {f : n ⊢} {vs : List (n ⊢)} + → (i : ℕ) + → All Value vs + → Frame f + → (ts : List (n ⊢)) + → Frame (constr i (vs ++ List.[ f ] ++ ts)) + caseᶠ + : {f : n ⊢} + → Frame f + → (ts : List (n ⊢)) + → Frame (case f ts) + +-- TODO: implement +postulate + multiApp : {t : n ⊢} → Value t → List (n ⊢) → n ⊢ + +-- TODO: rename constructors +data _⟶_ : n ⊢ → n ⊢ → Set where + lamapp + : {t₁ : suc n ⊢} {t₂ : n ⊢} + → Value t₂ + → (ƛ t₁ · t₂) ⟶ (t₁ [ t₂ ]) + forcedelay + : {t : n ⊢} + → (force (delay t)) ⟶ t + caseconstr + : {i l : ℕ} {vs ts : List (n ⊢)} {f : n ⊢} + → All Value vs + -- TODO: lookup i in ts, we need to deal with empty ts's and index out of bounds + → (case (constr i vs) ts) ⟶ (multiApp {! !} vs) + + +``` \ No newline at end of file From 272db9e199c1a4680f437e1e10d9e0a086188671 Mon Sep 17 00:00:00 2001 From: Ana Pantilie Date: Tue, 30 Jun 2026 22:39:28 +0300 Subject: [PATCH 2/3] WIP: finish formalization for partial buultin applications --- .../src/Untyped/ContextualSemantics.lagda.md | 69 ++++++++++++++++--- 1 file changed, 60 insertions(+), 9 deletions(-) diff --git a/plutus-metatheory/src/Untyped/ContextualSemantics.lagda.md b/plutus-metatheory/src/Untyped/ContextualSemantics.lagda.md index 855f7ba4357..383e80e7fed 100644 --- a/plutus-metatheory/src/Untyped/ContextualSemantics.lagda.md +++ b/plutus-metatheory/src/Untyped/ContextualSemantics.lagda.md @@ -11,14 +11,17 @@ module Untyped.ContextualSemantics where ``` open import Untyped -open import Data.Nat using (ℕ; suc; _+_; _<_; _≤_) +open import Data.Nat using (ℕ; suc; _+_; _<_; _≤_; _≤ᵇ_) open import Data.List using (List; _++_) import Data.List as List open import Data.List.Relation.Unary.All using (All) open import Builtin -open import Builtin.Signature using (args♯; Sig) +open import Builtin.Signature using (_/_⊢⋆; args♯; Sig; fv) open import Untyped.RenamingSubstitution using (_[_]) open import Data.Vec using (Vec) +open import Data.Maybe using (Maybe; just; nothing) +open import Data.Bool using (if_then_else_) +import Data.List.NonEmpty as List⁺ import Data.List.NonEmpty as NE import Data.Vec as Vec import Data.Fin as Fin @@ -60,20 +63,68 @@ data B where ||_|| (appB b v) = 1 + || b || ||_|| (forceB b) = 1 + || b || +||_||ₐ : {X : n ⊢} → B X → ℕ +||_||ₐ (builtinB b) = 0 +||_||ₐ (appB b v) = 1 + || b || +||_||ₐ (forceB b) = || b || + +||_||ᶠ : {X : n ⊢} → B X → ℕ +||_||ᶠ (builtinB b) = 0 +||_||ᶠ (appB b v) = || b || +||_||ᶠ (forceB b) = 1 + || b || + data A where builtinA - : {b : Builtin} - → A {n} (builtinB b) + : {t : Builtin} + → (b : B {n} (builtin t)) + → A {n} b appA - : {t₁ t₂ : n ⊢} (b : B (t₁ · t₂)) - → || b || < args♯ (signature (β b)) - -- TODO: quantification? + : {t₁ t₂ : n ⊢} + → (b : B (t₁ · t₂)) + -- we may apply app a number of times equal to the number of term arguments it has + → || b ||ₐ ≤ args♯ (signature (β b)) + -- check that the builtin is not fully saturated + → || b || < args♯ (signature (β b)) + fv (signature (β b)) → A {n} b forceA - : {t : n ⊢} (b : B (force t)) - → || b || < 1 -- TODO: we don't formalize quantifications, in practice I've only seen them applied directly to 'builtin b', but this should be fixed separately + : {t : n ⊢} + → (b : B (force t)) + -- a builtin may be forced the number of times equal to the number of type arguments it has + → || b ||ᶠ ≤ fv (signature (β b)) + -- check that the builtin is not fully saturated + → || b || < args♯ (signature (β b)) + fv (signature (β b)) → A {n} b +βᴬ : {t : n ⊢} {b : B t} → A b → Builtin +βᴬ (builtinA b) = β b +βᴬ (appA b x x₁) = β b +βᴬ (forceA b x x₁) = β b + +||_||ᴬ : {t : n ⊢} {b : B t} → A b → ℕ +||_||ᴬ (builtinA b) = || b || +||_||ᴬ (appA b x x₁) = || b || +||_||ᴬ (forceA b x x₁) = || b || + +||_||ᶠᴬ : {t : n ⊢} {b : B t} → A b → ℕ +||_||ᶠᴬ (builtinA b) = || b ||ᶠ +||_||ᶠᴬ (appA b x x₁) = || b ||ᶠ +||_||ᶠᴬ (forceA b x x₁) = || b ||ᶠ + +-- this doesn't typecheck because i need to use the information +-- that a is a partial application in order to lookup the next argument; +-- that means that the x is always smaller than the total number of args +-- and i should know that from the fact that a is a partial application +nextᴬ + : {n : ℕ} {t : n ⊢} {b : B t} + → (a : A b) + → Maybe (Sig.fv⋆ (signature (βᴬ a)) / Sig.fv♯ (signature (βᴬ a)) ⊢⋆) +nextᴬ a with || a ||ᴬ +... | 0 = + if ( || a ||ᶠᴬ ≤ᵇ fv (signature (βᴬ a)) ) + then nothing + else (just (List⁺.head (Sig.args (signature (βᴬ a))))) +... | x = just (Vec.lookup (List⁺.toVec (Sig.args (signature (βᴬ a)))) {! Fin.fromℕ x !}) + data Value where conᵥ : (t : TmCon) → Value {n} (con t) delayᵥ : (t : n ⊢) → Value (delay t) From 4be3034bf15f549d97337d35f6171d43b6ab84dd Mon Sep 17 00:00:00 2001 From: Ana Pantilie Date: Tue, 7 Jul 2026 18:52:07 +0300 Subject: [PATCH 3/3] Keep track of forces and arguments in well-defined partial applications --- .../src/Untyped/ContextualSemantics.lagda.md | 120 +++++++++--------- 1 file changed, 59 insertions(+), 61 deletions(-) diff --git a/plutus-metatheory/src/Untyped/ContextualSemantics.lagda.md b/plutus-metatheory/src/Untyped/ContextualSemantics.lagda.md index 383e80e7fed..380ebd359bd 100644 --- a/plutus-metatheory/src/Untyped/ContextualSemantics.lagda.md +++ b/plutus-metatheory/src/Untyped/ContextualSemantics.lagda.md @@ -11,7 +11,7 @@ module Untyped.ContextualSemantics where ``` open import Untyped -open import Data.Nat using (ℕ; suc; _+_; _<_; _≤_; _≤ᵇ_) +open import Data.Nat using (ℕ; zero; suc; _+_; _∸_; _<_; _≤_; _≤ᵇ_) open import Data.List using (List; _++_) import Data.List as List open import Data.List.Relation.Unary.All using (All) @@ -37,7 +37,12 @@ variable data B : n ⊢ → Set data Value : n ⊢ → Set -data A : {X : n ⊢} → B X → Set +β : {X : n ⊢} → B X → Builtin +-- the signature of the builtin underlying the spine 'b' +sigOf : {X : n ⊢} → B X → Sig +-- the type of a term argument expected by the 'b' builtin +ArgTy : {X : n ⊢} → B X → Set +data A : {X : n ⊢} → (b : B X) → ℕ → NE.List⁺ (ArgTy b) → Set data B where builtinB @@ -53,84 +58,77 @@ data B where → B t → B (force t) -β : {X : n ⊢} → B X → Builtin β (builtinB b) = b β (appB b v) = β b β (forceB b) = β b +sigOf b = signature (β b) + +ArgTy b = Sig.fv⋆ (sigOf b) / Sig.fv♯ (sigOf b) ⊢⋆ + ||_|| : {X : n ⊢} → B X → ℕ ||_|| (builtinB b) = 0 ||_|| (appB b v) = 1 + || b || ||_|| (forceB b) = 1 + || b || -||_||ₐ : {X : n ⊢} → B X → ℕ -||_||ₐ (builtinB b) = 0 -||_||ₐ (appB b v) = 1 + || b || -||_||ₐ (forceB b) = || b || - -||_||ᶠ : {X : n ⊢} → B X → ℕ -||_||ᶠ (builtinB b) = 0 -||_||ᶠ (appB b v) = || b || -||_||ᶠ (forceB b) = 1 + || b || - data A where builtinA - : {t : Builtin} - → (b : B {n} (builtin t)) - → A {n} b - appA - : {t₁ t₂ : n ⊢} - → (b : B (t₁ · t₂)) - -- we may apply app a number of times equal to the number of term arguments it has - → || b ||ₐ ≤ args♯ (signature (β b)) - -- check that the builtin is not fully saturated - → || b || < args♯ (signature (β b)) + fv (signature (β b)) - → A {n} b + : (b : Builtin) + → A (builtinB {n} b) (fv (signature b)) (Sig.args (signature b)) forceA - : {t : n ⊢} - → (b : B (force t)) - -- a builtin may be forced the number of times equal to the number of type arguments it has - → || b ||ᶠ ≤ fv (signature (β b)) - -- check that the builtin is not fully saturated - → || b || < args♯ (signature (β b)) + fv (signature (β b)) - → A {n} b - -βᴬ : {t : n ⊢} {b : B t} → A b → Builtin -βᴬ (builtinA b) = β b -βᴬ (appA b x x₁) = β b -βᴬ (forceA b x x₁) = β b - -||_||ᴬ : {t : n ⊢} {b : B t} → A b → ℕ -||_||ᴬ (builtinA b) = || b || -||_||ᴬ (appA b x x₁) = || b || -||_||ᴬ (forceA b x x₁) = || b || - -||_||ᶠᴬ : {t : n ⊢} {b : B t} → A b → ℕ -||_||ᶠᴬ (builtinA b) = || b ||ᶠ -||_||ᶠᴬ (appA b x x₁) = || b ||ᶠ -||_||ᶠᴬ (forceA b x x₁) = || b ||ᶠ - --- this doesn't typecheck because i need to use the information --- that a is a partial application in order to lookup the next argument; --- that means that the x is always smaller than the total number of args --- and i should know that from the fact that a is a partial application + : {t : n ⊢} {b : B t} {fl : ℕ} + {al : NE.List⁺ (ArgTy b)} + -- a force is still expected: consume it, leaving the argument list suffix untouched + → A b (suc fl) al + → A (forceB b) fl al + appA + : {t₁ t₂ : n ⊢} {b : B t₁} + {τ : ArgTy b} + {as : NE.List⁺ (ArgTy b)} + -- all forces done: consume the head argument τ, non-empty suffix 'as' remains + → A b zero (τ NE.∷⁺ as) + → (v : Value t₂) + → A (appB b v) zero as + +βᴬ : {t : n ⊢} {b : B t} {fl : ℕ} + {al : NE.List⁺ (ArgTy b)} + → A b fl al → Builtin +βᴬ {b = b} _ = β b + +-- number of forces performed so far: total type variables minus those still expected +||_||ᶠᴬ + : {t : n ⊢} {b : B t} {fl : ℕ} {al : NE.List⁺ (ArgTy b)} + → A b fl al + → ℕ +||_||ᶠᴬ {b = b} {fl = fl} _ = fv (sigOf b) ∸ fl + +-- number of forces + applications performed so far +||_||ᴬ + : {t : n ⊢} {b : B t} {fl : ℕ} {al : NE.List⁺ (ArgTy b)} + → A b fl al + → ℕ +||_||ᴬ {b = b} {fl = fl} {al = al} a = + || a ||ᶠᴬ + (args♯ (sigOf b) ∸ NE.length al) + +-- The type of the next argument the partial application expects: +-- - nothing if the next expected argument is a type argument (a force) +-- - just τ if the next expected argument is a term argument of type τ nextᴬ - : {n : ℕ} {t : n ⊢} {b : B t} - → (a : A b) - → Maybe (Sig.fv⋆ (signature (βᴬ a)) / Sig.fv♯ (signature (βᴬ a)) ⊢⋆) -nextᴬ a with || a ||ᴬ -... | 0 = - if ( || a ||ᶠᴬ ≤ᵇ fv (signature (βᴬ a)) ) - then nothing - else (just (List⁺.head (Sig.args (signature (βᴬ a))))) -... | x = just (Vec.lookup (List⁺.toVec (Sig.args (signature (βᴬ a)))) {! Fin.fromℕ x !}) + : {t : n ⊢} {b : B t} {fl : ℕ} {al : NE.List⁺ (ArgTy b)} + → A b fl al + → Maybe (ArgTy b) +nextᴬ {fl = suc _} _ = nothing +nextᴬ {fl = zero} {al = al} _ = just (NE.head al) data Value where conᵥ : (t : TmCon) → Value {n} (con t) delayᵥ : (t : n ⊢) → Value (delay t) ƛᵥ : (t : suc n ⊢) → Value (ƛ t) constrᵥ : (i : ℕ) (ts : List (n ⊢)) → All Value ts → Value (constr i ts) - bAppᵥ : {t : n ⊢} {b : B t} → A b → Value t + bAppᵥ + : {t : n ⊢} {b : B t} {fl : ℕ} {al : NE.List⁺ (ArgTy b)} + → A b fl al + → Value t data Frame : n ⊢ → Set where □