PLT-7098 Adapt Determinism proof to SOPs (#5582)

Extends the determinism proof of the reduction semantics to handle SOPs. Makes SOPs variable naming more uniform.
IntersectMBO · Oct 19, 2023 · 802e9c7 · 802e9c7
1 parent 056383e
commit 802e9c7
Show file tree

Hide file tree

Showing 28 changed files with 911 additions and 473 deletions.
diff --git a/plutus-metatheory/src/Algorithmic.lagda b/plutus-metatheory/src/Algorithmic.lagda
@@ -240,27 +240,30 @@ data _⊢_ (Γ : Ctx Φ) : Φ ⊢Nf⋆ * → Set where
     → Γ ⊢ C
 
   constr : ∀{n}
-      → (i : Fin n)                   -- The tag
+      → (i : Fin n)                     -- The tag
 
-      → (A : Vec (List (Φ ⊢Nf⋆ *)) n) -- The sum of products. We make it a Vector
-                                      -- of lists, so that the tag is statically correct.
+      → (Tss : Vec (List (Φ ⊢Nf⋆ *)) n) -- The types of the sum of products. 
+                                        -- We make it a Vector of lists, so that 
+                                        -- the tag is statically correct.
+                                        -- We use the name `Tss` as it stands for a 
+                                        -- a container of containers of types.
 
-      → ∀ {ts} → ts ≡ lookup A i      -- The reason to define it like this, rather than
-      → ConstrArgs Γ ts               -- simply ConstrArgs Γ (lookup A e) 
-                                      -- is so that it is easier to construct terms (avoids using subst)
-                                      -- as often the result of a function will not match definitionally
-                                      -- with (lookup A e) but only propositionally.
+      → ∀ {ts} → ts ≡ lookup Tss i      -- The reason to define it like this, rather than
+      → ConstrArgs Γ ts                 -- simply ConstrArgs Γ (lookup Tss i) is so that it 
+                                        -- is easier to construct terms (helps to avoid the use of subst)
+                                        -- as often the result of a function will not match definitionally
+                                        -- with (lookup Tss i) but only propositionally.
         --------------------------------------
-      → Γ ⊢ SOP A
+      → Γ ⊢ SOP Tss
 
-  case : ∀{n}{tss : Vec _ n}{A : Φ ⊢Nf⋆ *}
-      → (t : Γ ⊢ SOP tss)
-      → (cases : Cases Γ A tss)
+  case : ∀{n}{Tss : Vec _ n}{A : Φ ⊢Nf⋆ *}
+      → (t : Γ ⊢ SOP Tss)               -- The term we case on
+      → (cases : Cases Γ A Tss)
         --------------------------
-      → Γ ⊢ A  
+      → Γ ⊢ A
 
   con : ∀{A : ∅ ⊢Nf⋆ ♯}{B}
-    → ⟦ A ⟧ 
+    → ⟦ A ⟧
     → B ≡ subNf∅ A
       ---------------------
     → Γ ⊢ con B
@@ -276,17 +279,18 @@ data _⊢_ (Γ : Ctx Φ) : Φ ⊢Nf⋆ * → Set where
       --------------
     → Γ ⊢ A
 
+-- The type of arguments to a `constr` constructor
 ConstrArgs Γ = IList (Γ ⊢_)
 
 -- Cases is indexed by a vector 
 -- so it can't be an IList
 data Cases Γ B where 
    []  : Cases Γ B []
-   _∷_ : ∀{n}{AS}{ASS : Vec _ n}(
-         c : Γ ⊢ (mkCaseType B AS)) 
-       → (cs : Cases Γ B ASS)
+   _∷_ : ∀{n}{Ts}{Tss : Vec _ n}(
+         c : Γ ⊢ (mkCaseType B Ts)) 
+       → (cs : Cases Γ B Tss)
          --------------------- 
-       → Cases Γ B (AS ∷ ASS) 
+       → Cases Γ B (Ts ∷ Tss) 
 \end{code}
 
 Utility functions
@@ -306,21 +310,21 @@ conv⊢ : ∀ {Γ Γ'}{A A' : Φ ⊢Nf⋆ *}
  → Γ' ⊢ A'
 conv⊢ refl refl t = t
 
-lookupCase : ∀{n Φ}{Γ : Ctx Φ}{B}{TSS : Vec _ n} → (i : Fin n) → Cases Γ B TSS → Γ ⊢ mkCaseType B (Vec.lookup TSS i)
+lookupCase : ∀{n Φ}{Γ : Ctx Φ}{A}{Tss : Vec _ n} → (i : Fin n) → Cases Γ A Tss → Γ ⊢ mkCaseType A (Vec.lookup Tss i)
 lookupCase Fin.zero (c ∷ cs) = c
 lookupCase (Fin.suc i) (c ∷ cs) = lookupCase i cs
 
 bwdMkCaseType : ∀{Φ} → Bwd (Φ ⊢Nf⋆ *) → (A : Φ ⊢Nf⋆ *) → Φ ⊢Nf⋆ *
 bwdMkCaseType bs A = bwd-foldr _⇒_ A bs
 
-lemma-bwdfwdfunction' : ∀{Φ} {B : Φ ⊢Nf⋆ *} TS → mkCaseType B TS ≡ bwdMkCaseType ([] <>< TS) B
-lemma-bwdfwdfunction' {B = B} TS = trans (cong (mkCaseType B) (sym (lemma<>1 [] TS))) (lemma-bwd-foldr _⇒_ B ([] <>< TS))         
+lemma-bwdfwdfunction' : ∀{Φ} {B : Φ ⊢Nf⋆ *} Ts → mkCaseType B Ts ≡ bwdMkCaseType ([] <>< Ts) B
+lemma-bwdfwdfunction' {B = B} Ts = trans (cong (mkCaseType B) (sym (lemma<>1 [] Ts))) (lemma-bwd-foldr _⇒_ B ([] <>< Ts))         
 
-constr-cong :  ∀{Γ : Ctx Φ}{n}{i : Fin n}{A : Vec (List (Φ ⊢Nf⋆ *)) n}{ts} 
-            → (p : ts ≡ lookup A i)
+constr-cong :  ∀{Γ : Ctx Φ}{n}{i : Fin n}{Tss : Vec (List (Φ ⊢Nf⋆ *)) n}{ts} 
+            → (p : ts ≡ lookup Tss i)
             → {cs : ConstrArgs Γ ts}
-            → {cs' : ConstrArgs Γ (lookup A i)}
+            → {cs' : ConstrArgs Γ (lookup Tss i)}
             → (q : cs' ≡ subst (IList (Γ ⊢_)) p cs)
-            → constr i A refl cs' ≡ constr i A p cs
+            → constr i Tss refl cs' ≡ constr i Tss p cs
 constr-cong refl refl = refl
 \end{code}
diff --git a/plutus-metatheory/src/Algorithmic/CC.lagda.md b/plutus-metatheory/src/Algorithmic/CC.lagda.md
@@ -51,9 +51,9 @@ dissect (wrap E) with dissect E
 dissect (unwrap E / refl) with dissect E
 ... | inj₁ refl           = inj₂ (_ ,, [] ,, unwrap-)
 ... | inj₂ (C ,, E' ,, F) = inj₂ (C ,, unwrap E' / refl ,, F)
-dissect (constr i TSS p {tidx} vs ts E) with dissect E 
-... | inj₁ refl           = inj₂ (_ ,, ([] ,, (constr- i TSS p {tidx} vs ts)))
-... | inj₂ (C ,, E' ,, F) = inj₂ (_ ,, ((constr i TSS p {tidx} vs ts E') ,, F))
+dissect (constr i Tss p {tidx} vs ts E) with dissect E 
+... | inj₁ refl           = inj₂ (_ ,, ([] ,, (constr- i Tss p {tidx} vs ts)))
+... | inj₂ (C ,, E' ,, F) = inj₂ (_ ,, ((constr i Tss p {tidx} vs ts E') ,, F))
 dissect (case cs E)  with dissect E 
 ... | inj₁ refl           = inj₂ (_ ,, ([] ,, (case- cs)))
 ... | inj₂ (C ,, E' ,, F) = inj₂ (_ ,, ((case cs E') ,, F))
@@ -65,7 +65,7 @@ compEC (VM ·r E) E' = VM ·r compEC E E'
 compEC (E ·⋆ A / refl) E' = compEC E E' ·⋆ A / refl
 compEC (wrap E) E' = wrap (compEC E E')
 compEC (unwrap E / refl) E' = unwrap (compEC E E') / refl
-compEC (constr i TSS p {tidx} vs ts E) E' = constr i TSS p {tidx} vs ts (compEC E E')
+compEC (constr i Tss p {tidx} vs ts E) E' = constr i Tss p {tidx} vs ts (compEC E E')
 compEC (case cs E) E' = case cs (compEC E E')
 
 extEC : ∀{A B C}(E : EC A B)(F : Frame B C) → EC A C
@@ -75,7 +75,7 @@ extEC [] (VM ·-) = VM ·r []
 extEC [] (-·⋆ A) = [] ·⋆ A / refl
 extEC [] wrap- = wrap []
 extEC [] unwrap- = unwrap [] / refl
-extEC [] (constr- i TSS p {tidx} vs ts) = constr i TSS p {tidx} vs ts []
+extEC [] (constr- i Tss p {tidx} vs ts) = constr i Tss p {tidx} vs ts []
 extEC [] (case- cs) = case cs []
 extEC (E l· M') F = extEC E F l· M'
 extEC (VM ·r E) F = VM ·r extEC E F
@@ -96,7 +96,7 @@ data State (T : ∅ ⊢Nf⋆ *) : Set where
   □  : {t : ∅ ⊢ T} →  Value t → State T
   ◆   : (A : ∅ ⊢Nf⋆ *)  →  State T
 
-extValueFrames : ∀{T H BS XS} → EC T H → {xs : IBwd (∅ ⊢_) BS} → VList xs → XS ≡ bwdMkCaseType BS H → EC T XS
+extValueFrames : ∀{T H Bs Xs} → EC T H → {xs : IBwd (∅ ⊢_) Bs} → VList xs → Xs ≡ bwdMkCaseType Bs H → EC T Xs
 extValueFrames E [] refl = E
 extValueFrames E (vs :< v) refl = extValueFrames (extEC E (-·v v)) vs refl
 
@@ -116,15 +116,15 @@ stepV (V-IΠ b  {σA = σ} q) (inj₂ (_ ,, E ,, -·⋆ A)) =
           E ◅ V-I b (step⋆ q refl {σ [ A ]SigTy})
 stepV V (inj₂ (_ ,, E ,, wrap-)) = E ◅ V-wrap V
 stepV (V-wrap V) (inj₂ (_ ,, E ,, unwrap-)) = E ▻ deval V -- E ◅ V
-stepV V (inj₂ (_ ,, E ,, constr- i A p vs ts)) with Vec.lookup A i in eq  
+stepV V (inj₂ (_ ,, E ,, constr- i Tss p vs ts)) with Vec.lookup Tss i in eq  
 stepV V (inj₂ (_ ,, E ,, constr- i _ refl {tidx} vs ts)) | [] with no-empty-≣-<>> tidx 
 ... | ()
-stepV V (inj₂ (_ ,, E ,, constr- {VS = VS} {H} i _ refl {r}{tidx} vs [])) | _ ∷ _  = 
-     E ◅ V-constr i _ (sym eq) (sym (trans (cong ([] <><_) (lem-≣-<>> r)) (lemma<>2 VS (H ∷ [])))) (vs :< V) refl
-stepV V (inj₂ (_ ,, E ,, constr- {VS = VS} i A refl {r} vs (t ∷ ts))) | _ ∷ _  
+stepV V (inj₂ (_ ,, E ,, constr- {Vs = Vs} {H} i _ refl {r}{tidx} vs [])) | _ ∷ _  = 
+     E ◅ V-constr i _ (sym eq) (sym (trans (cong ([] <><_) (lem-≣-<>> r)) (lemma<>2 Vs (H ∷ [])))) (vs :< V) refl
+stepV V (inj₂ (_ ,, E ,, constr- {Vs = Vs} i A refl {r} vs (t ∷ ts))) | _ ∷ _  
     = extEC E (constr- i A (sym eq) {bubble r} (vs :< V) ts) ▻ t
-stepV (V-constr e A refl refl vs x) (inj₂ (_ ,, E ,, case- cs)) = 
-    extValueFrames E vs (lemma-bwdfwdfunction' (Vec.lookup A e)) ▻ lookupCase e cs
+stepV (V-constr e Tss refl refl vs x) (inj₂ (_ ,, E ,, case- cs)) = 
+    extValueFrames E vs (lemma-bwdfwdfunction' (Vec.lookup Tss e)) ▻ lookupCase e cs
 
 stepT : ∀{A} → State A → State A
 stepT (E ▻ ƛ M) = E ◅ V-ƛ M
@@ -133,10 +133,10 @@ stepT (E ▻ Λ M) = E ◅ V-Λ M
 stepT (E ▻ (M ·⋆ A / refl)) = extEC E (-·⋆ A) ▻ M
 stepT (E ▻ wrap A B M) = extEC E wrap- ▻ M
 stepT (E ▻ unwrap M refl) = extEC E unwrap- ▻ M
-stepT (E ▻ constr e A refl z)  with Vec.lookup A e in eq  
-stepT (E ▻ constr e A refl []) | [] = E ◅ V-constr e A (sym eq) refl [] refl
-stepT (E ▻ constr e A refl (x ∷ xs)) | a ∷ as = 
-        extEC E (constr- e A (sym eq) {start} [] xs) ▻  x
+stepT (E ▻ constr e Tss refl z)  with Vec.lookup Tss e in eq  
+stepT (E ▻ constr e Tss refl []) | [] = E ◅ V-constr e Tss (sym eq) refl [] refl
+stepT (E ▻ constr e Tss refl (x ∷ xs)) | a ∷ as = 
+        extEC E (constr- e Tss (sym eq) {start} [] xs) ▻  x
 stepT (E ▻ case M cases) = extEC E (case- cases) ▻ M
 stepT (E ▻ con c refl) = E ◅ V-con c
 stepT (E ▻ (builtin b / refl)) = E ◅ ival b

diff --git a/plutus-metatheory/src/Algorithmic/CEK.lagda.md b/plutus-metatheory/src/Algorithmic/CEK.lagda.md
@@ -93,7 +93,7 @@ data Value where
        → {σB : SigTy (bubble pt) pa B}
        → BApp b (Π B) (sucΠ σB)
        → Value (Π B)
-  V-constr : ∀{n}(e : Fin n) A {ts} (vs : VList ts) → ts ≡ [] <>< Vec.lookup A e → Value (SOP A)
+  V-constr : ∀{n}(e : Fin n) Tss {ts} (vs : VList ts) → ts ≡ [] <>< Vec.lookup Tss e → Value (SOP Tss)
 
 data BApp b where
   base : BApp b (sig2type (signature b)) (sig2SigTy (signature b))
@@ -172,7 +172,7 @@ dischargeStack-aux : ∀{A B C} → (s : VList A) → IList (∅ ⊢_) B → A <
 dischargeStack-aux [] a refl = a
 dischargeStack-aux (s :< x) a refl = dischargeStack-aux s (discharge x ∷ a) refl
 
-dischargeStack : ∀{TS} → IBwd Value ([] <>< TS) → IList (_⊢_ ∅) TS
+dischargeStack : ∀{Ts} → IBwd Value ([] <>< Ts) → IList (_⊢_ ∅) Ts
 dischargeStack bs = dischargeStack-aux bs [] (lemma<>1 [] _)
 
 discharge (V-ƛ M ρ)  = ƛ (dischargeBody M ρ)
@@ -181,7 +181,7 @@ discharge (V-wrap V) = wrap _ _ (discharge V)
 discharge (V-con c)  = con c refl
 discharge (V-I⇒ b bt) = dischargeB bt
 discharge (V-IΠ b bt) = dischargeB bt 
-discharge (V-constr i A s refl) = constr i A refl (dischargeStack s) 
+discharge (V-constr i Tss s refl) = constr i Tss refl (dischargeStack s) 
 ```
 
 ## Builtin Semantics
@@ -357,14 +357,14 @@ data Frame : (T : ∅ ⊢Nf⋆ *) → (H : ∅ ⊢Nf⋆ *) → Set where
   unwrap- : ∀{K}{A : ∅ ⊢Nf⋆ (K ⇒ *) ⇒ K ⇒ *}{B : ∅ ⊢Nf⋆ K}
     → Frame (nf (embNf A · ƛ (μ (embNf (weakenNf A)) (` Z)) · embNf B))
             (μ A B)
-  constr- : ∀{Γ n VS H TS} 
+  constr- : ∀{Γ n Vs H Ts} 
           → (i : Fin n) 
-          → (TSS : Vec _ n) 
+          → (Tss : Vec _ n) 
           → Env Γ 
-          → ∀{XS} → (XS ≡ Vec.lookup TSS i)
-          → {tidx : XS ≣ VS <>> (H ∷ TS)} → VList VS → ConstrArgs Γ TS
-          → Frame (SOP TSS) H
-  case- : ∀{Γ A n}{TSS : Vec _ n} → (ρ : Env Γ) → Cases Γ A TSS → Frame A (SOP TSS)
+          → ∀{Xs} → (Xs ≡ Vec.lookup Tss i)
+          → {tidx : Xs ≣ Vs <>> (H ∷ Ts)} → VList Vs → ConstrArgs Γ Ts
+          → Frame (SOP Tss) H
+  case- : ∀{Γ A n}{Tss : Vec _ n} → (ρ : Env Γ) → Cases Γ A Tss → Frame A (SOP Tss)
 
 data Stack (T : ∅ ⊢Nf⋆ *) : (H : ∅ ⊢Nf⋆ *) → Set where
   ε   : Stack T T
@@ -379,7 +379,7 @@ data State (T : ∅ ⊢Nf⋆ *) : Set where
 ival : ∀(b : Builtin) → Value (btype b)
 ival b = V-I b base 
 
-pushValueFrames : ∀{T H BS XS} → Stack T H → VList BS → XS ≡ bwdMkCaseType BS H → Stack T XS
+pushValueFrames : ∀{T H Bs Xs} → Stack T H → VList Bs → Xs ≡ bwdMkCaseType Bs H → Stack T Xs
 pushValueFrames s [] refl = s
 pushValueFrames s (vs :< v) refl = pushValueFrames (s , -·v v) vs refl
 
@@ -394,9 +394,9 @@ step (s ; ρ ▻ unwrap L refl) = (s , unwrap-) ; ρ ▻ L
 step (s ; ρ ▻ con c refl) = s ◅ V-con c
 step (s ; ρ ▻ (builtin b / refl)) = s ◅ ival b
 step (s ; ρ ▻ error A) = ◆ A
-step (s ; ρ ▻ constr e A refl as) with Vec.lookup A e in eq 
-step (s ; ρ ▻ constr e A refl []) | []  = s ◅ V-constr e A [] (cong ([] <><_) (sym eq))
-step (_;_▻_ {Γ} s ρ (constr e A refl (_∷_ {xty} {xsty} x xs))) | _ ∷ _ = (s , constr- e A ρ (sym eq) {start} [] xs) ; ρ ▻ x
+step (s ; ρ ▻ constr e Tss refl as) with Vec.lookup Tss e in eq 
+step (s ; ρ ▻ constr e Tss refl []) | []  = s ◅ V-constr e Tss [] (cong ([] <><_) (sym eq))
+step (_;_▻_ {Γ} s ρ (constr e Tss refl (_∷_ {xty} {xsty} x xs))) | _ ∷ _ = (s , constr- e Tss ρ (sym eq) {start} [] xs) ; ρ ▻ x
 step (s ; ρ ▻ case t ts) = (s , case- ρ ts) ; ρ ▻ t
 step (ε ◅ V) = □ V
 step ((s , -· M ρ') ◅ V) = (s , V ·-) ; ρ' ▻ M
@@ -408,14 +408,14 @@ step ((s , -·⋆ A) ◅ V-Λ M ρ) = s ; ρ ▻ (M [ A ]⋆)
 step ((s , -·⋆ A) ◅ V-IΠ b {σB = σ} bapp) = s ◅ V-I b (_$$_ bapp refl {σ [ A ]SigTy})
 step ((s , wrap-) ◅ V) = s ◅ V-wrap V
 step ((s , unwrap-) ◅ V-wrap V) = s ◅ V
-step ((s , constr- i TSS ρ refl {tidx} vs ts) ◅ v) 
-    with Vec.lookup TSS i in eq
+step ((s , constr- i Tss ρ refl {tidx} vs ts) ◅ v) 
+    with Vec.lookup Tss i in eq
 ... | [] with no-empty-≣-<>> tidx
 ... | ()
-step ((s , constr- i TSS ρ refl {r} vs []) ◅ v) | A ∷ AS  = s ◅ V-constr i TSS (vs :< v) 
+step ((s , constr- i Tss ρ refl {r} vs []) ◅ v) | A ∷ As  = s ◅ V-constr i Tss (vs :< v) 
                  (sym (trans (cong ([] <><_) (trans eq (lem-≣-<>> r))) (lemma<>2 _ (_ ∷ []))))
-step ((s , constr- i TSS ρ refl {r} vs (t ∷ ts)) ◅ v) | A ∷ AS = (s , constr- i TSS ρ (sym eq) {bubble r} (vs :< v) ts) ; ρ ▻ t 
-step {t} ((s , case- ρ cases) ◅ V-constr e TSS vs refl) = pushValueFrames s vs (lemma-bwdfwdfunction' (Vec.lookup TSS e)) ; ρ ▻ (lookupCase e cases) 
+step ((s , constr- i Tss ρ refl {r} vs (t ∷ ts)) ◅ v) | A ∷ As = (s , constr- i Tss ρ (sym eq) {bubble r} (vs :< v) ts) ; ρ ▻ t 
+step {t} ((s , case- ρ cases) ◅ V-constr e Tss vs refl) = pushValueFrames s vs (lemma-bwdfwdfunction' (Vec.lookup Tss e)) ; ρ ▻ (lookupCase e cases) 
 step (□ V) = □ V
 step (◆ A) = ◆ A
 

diff --git a/plutus-metatheory/src/Algorithmic/CK.lagda.md b/plutus-metatheory/src/Algorithmic/CK.lagda.md
@@ -66,7 +66,7 @@ closeState (◆ A)             = error _
 discharge : ∀{A : ∅ ⊢Nf⋆ *}{t : ∅ ⊢ A} → Value t → ∅ ⊢ A
 discharge {t = t} _ = t
 
-pushValueFrames : ∀{T H BS XS} → Stack T H → {xs : IBwd (∅ ⊢_) BS} → VList xs → XS ≡ bwdMkCaseType BS H → Stack T XS
+pushValueFrames : ∀{T H Bs Xs} → Stack T H → {xs : IBwd (∅ ⊢_) Bs} → VList xs → Xs ≡ bwdMkCaseType Bs H → Stack T Xs
 pushValueFrames s [] refl = s
 pushValueFrames s (vs :< v) refl = pushValueFrames (s , -·v v) vs refl
 
@@ -78,9 +78,9 @@ step (s ▻ (L ·⋆ A / refl))                    = (s , -·⋆ A) ▻ L
 step (s ▻ wrap A B L)                         = (s , wrap-) ▻ L
 step (s ▻ unwrap L refl)                      = (s , unwrap-) ▻ L
 step (s ▻ con cn refl)                        = s ◅ V-con cn
-step (s ▻ constr e A refl xs) with Vec.lookup A e in eq 
-step (s ▻ constr e TSS refl []) | []          = s ◅ V-constr e TSS (sym eq) refl [] refl
-step (s ▻ constr e TSS refl (x ∷ xs)) | _ ∷ _ = (s , constr- e TSS (sym eq) {tidx = start} [] xs) ▻ x
+step (s ▻ constr e Tss refl xs) with Vec.lookup Tss e in eq 
+step (s ▻ constr e Tss refl []) | []          = s ◅ V-constr e Tss (sym eq) refl [] refl
+step (s ▻ constr e Tss refl (x ∷ xs)) | _ ∷ _ = (s , constr- e Tss (sym eq) {tidx = start} [] xs) ▻ x
 step (s ▻ case t ts)                          = (s , case- ts) ▻ t
 step (s ▻ error A)                            = ◆ A
 step (ε ◅ V)                                  = □ V
@@ -90,19 +90,19 @@ step ((s , (V-ƛ t ·-)) ◅ V)                   = s ▻ (t [ discharge V ])
 step ((s , (-·⋆ A)) ◅ V-Λ t)                  = s ▻ (t [ A ]⋆)
 step ((s , wrap-) ◅ V)                        = s ◅ (V-wrap V)
 step ((s , unwrap-) ◅ V-wrap V)               = s ▻ deval V
-step ((s , constr- i TSS refl {tidx} vs ts) ◅ v) with Vec.lookup TSS i in eq 
+step ((s , constr- i Tss refl {tidx} vs ts) ◅ v) with Vec.lookup Tss i in eq 
 ... | []   with no-empty-≣-<>> tidx 
 ...      | () 
-step ((s , constr- {n} {VS} {H} i TSS refl {tidx}{tvs} vs []) ◅ v) | _ ∷ _  = s ◅  
-   V-constr i TSS
+step ((s , constr- {n} {Vs} {H} i Tss refl {tidx}{tvs} vs []) ◅ v) | _ ∷ _  = s ◅  
+   V-constr i Tss
             (sym eq) 
-            (trans (sym (lemma<>2 VS (H ∷ []))) (sym (cong ([] <><_) (lem-≣-<>> tidx))))
+            (trans (sym (lemma<>2 Vs (H ∷ []))) (sym (cong ([] <><_) (lem-≣-<>> tidx))))
             {tvs :< deval v} 
             (vs :< v)
             refl
-step ((s , constr- i TSS refl {r} vs (t ∷ ts)) ◅ v) | _ ∷ _ = 
-      (s , constr- i TSS (sym eq) {bubble r} (vs :< v) ts) ▻ t
-step ((s , case- cs) ◅ V-constr e TSS refl refl vs x) = pushValueFrames s vs (lemma-bwdfwdfunction' (Vec.lookup TSS e)) ▻ lookupCase e cs
+step ((s , constr- i Tss refl {r} vs (t ∷ ts)) ◅ v) | _ ∷ _ = 
+      (s , constr- i Tss (sym eq) {bubble r} (vs :< v) ts) ▻ t
+step ((s , case- cs) ◅ V-constr e Tss refl refl vs x) = pushValueFrames s vs (lemma-bwdfwdfunction' (Vec.lookup Tss e)) ▻ lookupCase e cs
 step (s ▻ (builtin b / refl))                 = s ◅ ival b
 step ((s , (V-I⇒ b {am = 0}     bt ·-)) ◅ vu) = s ▻ BUILTIN' b (app bt vu)
 step ((s , (V-I⇒ b {am = suc _} bt ·-)) ◅ vu) = s ◅ V-I b (app bt vu)