added agda syntax and semantics of serialiseData

IntersectMBO · Mar 4, 2022 · da98594 · da98594
1 parent 798ab1b
commit da98594
Show file tree

Hide file tree

Showing 5 changed files with 24 additions and 0 deletions.
diff --git a/plutus-metatheory/src/Algorithmic.lagda b/plutus-metatheory/src/Algorithmic.lagda
@@ -140,6 +140,7 @@ sig unListData = _ ,, ∅ , con Data ,, con (list (con Data))
 sig unIData = _ ,, ∅ , con Data ,, con integer
 sig unBData = _ ,, ∅ , con Data ,, con bytestring
 sig equalsData = _ ,, ∅ , con Data , con Data ,, con bool
+sig serialiseData = _ ,, ∅ , con Data ,, con bytestring
 sig chooseData =
   _
   ,,

diff --git a/plutus-metatheory/src/Algorithmic/CEKV.lagda.md b/plutus-metatheory/src/Algorithmic/CEKV.lagda.md
@@ -197,6 +197,8 @@ BUILTIN equalsString (app _ (app _ base (V-con (string s))) (V-con (string s')))
 BUILTIN unIData (app _ base (V-con (Data (iDATA i)))) = inj₂ (V-con (integer i))
 BUILTIN unBData (app _ base (V-con (Data (bDATA b)))) =
   inj₂ (V-con (bytestring b))
+BUILTIN serialiseData (app _ base (V-con (Data d))) =
+  inj₂ (V-con (bytestring (serialiseDATA d)))
 BUILTIN _ {A} _ = inj₁ A
   
 convBApp : (b : Builtin) → ∀{az}{as}(p p' : az <>> as ∈ arity b)
@@ -460,6 +462,9 @@ bappTermLem equalsData {as = as} (bubble {as = az} p) q
   with <>>-cancel-both' az _ (([] :< Term) :< Term) as p refl
 bappTermLem equalsData (bubble (start _)) (app _ base _)
   | refl ,, refl ,, refl = _ ,, _ ,, refl
+bappTermLem serialiseData {az = az} {as} p q
+  with <>>-cancel-both az ([] :< Term) as p
+bappTermLem serialiseData (start _) base | refl ,, refl = _ ,, _ ,, refl
 bappTermLem chooseData (bubble (start _)) (app⋆ _ base refl) =
   _ ,, _ ,, refl
 bappTermLem chooseData
@@ -713,6 +718,9 @@ bappTypeLem unBData {az = az} p q
 bappTypeLem equalsData (bubble {as = az} p) _
   with <>>-cancel-both' az _ (([] :< Term) :< Term) _ p refl
 ... | refl ,, refl ,, ()
+bappTypeLem serialiseData {az = az} p q
+  with <>>-cancel-both' az _ ([] :< Term) _ p refl
+... | refl ,, refl ,, ()
 bappTypeLem chooseData (start _) base = _ ,, _ ,, refl
 bappTypeLem chooseData (bubble (bubble (bubble (bubble (bubble (bubble {as = az} p)))))) _
   with <>>-cancel-both' az _ ([] <>< arity chooseData) _ p refl
@@ -855,6 +863,7 @@ ival unListData = V-I⇒ unListData (start _) base
 ival unIData = V-I⇒ unIData (start _) base
 ival unBData = V-I⇒ unBData (start _) base
 ival equalsData = V-I⇒ equalsData (start _) base
+ival serialiseData = V-I⇒ serialiseData (start _) base
 ival chooseData = V-IΠ chooseData (start _) base
 ival chooseUnit = V-IΠ chooseUnit (start _) base
 ival mkPairData = V-I⇒ mkPairData (start _) base

diff --git a/plutus-metatheory/src/Algorithmic/ReductionEC.lagda.md b/plutus-metatheory/src/Algorithmic/ReductionEC.lagda.md
@@ -183,6 +183,7 @@ BUILTIN decodeUtf8 (step _ (base refl) (V-con (bytestring b)))
 ... | just s  = con (string s)
 BUILTIN unIData (step _ (base refl) (V-con (Data (iDATA i)))) = con (integer i)
 BUILTIN unBData (step _ (base refl) (V-con (Data (bDATA b)))) = con (bytestring b)
+BUILTIN serialiseData (step _ (base refl) (V-con (Data d))) = con (bytestring (serialiseDATA d))
 BUILTIN _ _ = error _
 
 
@@ -584,6 +585,9 @@ bappTermLem equalsData {as = as} _ (bubble {as = az} p) q
   with <>>-cancel-both' az _ (([] :< Term) :< Term) as p refl
 bappTermLem equalsData _ (bubble (start _)) (step _ (base refl) _)
   | refl ,, refl ,, refl = _ ,, _ ,, refl
+bappTermLem serialiseData {az = az} {as} M p q
+  with <>>-cancel-both az ([] :< Term) as p
+bappTermLem serialiseData _ (start _) (base refl) | refl ,, refl = _ ,, _ ,, refl
 bappTermLem chooseData _ (bubble (start _)) (step⋆ _ (base refl) refl) =
   _ ,, _ ,, refl
 bappTermLem chooseData
@@ -782,6 +786,9 @@ bappTypeLem unBData {az = az} _ p q
 bappTypeLem equalsData _ (bubble {as = az} p) _
   with <>>-cancel-both' az _ (([] :< Term) :< Term) _ p refl
 ... | refl ,, refl ,, ()
+bappTypeLem serialiseData {az = az} _ p q
+  with <>>-cancel-both' az _ ([] :< Term) _ p refl
+... | refl ,, refl ,, ()
 bappTypeLem chooseData _ (start _) (base refl) = _ ,, _ ,, refl
 bappTypeLem chooseData _ (bubble (bubble (bubble (bubble (bubble (bubble {as = az} p)))))) _
   with <>>-cancel-both' az _ ([] <>< arity chooseData) _ p refl
@@ -913,6 +920,7 @@ ival unListData = V-I _ (start _) (base refl)
 ival unIData = V-I _ (start _) (base refl)
 ival unBData = V-I _ (start _) (base refl)
 ival equalsData = V-I _ (start _) (base refl)
+ival serialiseData = V-I _ (start _) (base refl)
 ival chooseData = V-I _ (start _) (base refl)
 ival chooseUnit = V-I _ (start _) (base refl)
 ival mkPairData = V-I _ (start _) (base refl)

diff --git a/plutus-metatheory/src/Builtin.lagda.md b/plutus-metatheory/src/Builtin.lagda.md
@@ -73,6 +73,7 @@ data Builtin : Set where
   unIData                  : Builtin
   unBData                  : Builtin
   equalsData               : Builtin
+  serialiseData            : Builtin
   -- Misc constructors
   mkPairData               : Builtin
   mkNilData                : Builtin
@@ -127,6 +128,7 @@ data Builtin : Set where
                                           | UnIData
                                           | UnBData
                                           | EqualsData
+                                          | SerialiseData
                                           | MkPairData
                                           | MkNilData
                                           | MkNilPairData
@@ -158,6 +160,7 @@ postulate
   equals    : ByteString → ByteString → Bool
   ENCODEUTF8 : String → ByteString
   DECODEUTF8 : ByteString → Maybe String
+  serialiseDATA : DATA → ByteString
 ```
 
 # What builtin operations should be compiled to if we compile to Haskell

diff --git a/plutus-metatheory/src/Untyped/CEK.lagda.md b/plutus-metatheory/src/Untyped/CEK.lagda.md
@@ -168,6 +168,8 @@ BUILTIN equalsString (app _ (app _ base (V-con (string s))) (V-con (string s')))
 BUILTIN unIData (app _ base (V-con (Data (iDATA i)))) = inj₂ (V-con (integer i))
 BUILTIN unBData (app _ base (V-con (Data (bDATA b)))) =
   inj₂ (V-con (bytestring b))
+BUILTIN serialiseData (app _ base (V-con (Data d))) =
+  inj₂ (V-con (bytestring (serialiseDATA d)))
 BUILTIN _ _ = inj₁ userError
 
 convBApp : (b : Builtin) → ∀{az}{as}(p p' : az <>> as ∈ arity b)
@@ -225,6 +227,7 @@ ival unListData = V-I⇒ unListData (start _) base
 ival unIData = V-I⇒ unIData (start _) base
 ival unBData = V-I⇒ unBData (start _) base
 ival equalsData = V-I⇒ equalsData (start _) base
+ival serialiseData = V-I⇒ serialiseData (start _) base
 ival chooseData = V-IΠ chooseData (start _) base
 ival chooseUnit = V-IΠ chooseUnit (start _) base
 ival mkPairData = V-I⇒ mkPairData (start _) base