Write semantics for all builtins (there are many more than listed in the spec)

[SchmErik]

https://github.com/input-output-hk/plutus/pull/4281 adds an option to the uplc program to dump all builtins and there are many more builtins than listed in the spec. Here's the output from this proposed option mentioned in the pull request:

$ cabal exec uplc print-builtin-types
addInteger               : { (con integer), (con integer) } -> (con integer)
subtractInteger          : { (con integer), (con integer) } -> (con integer)
multiplyInteger          : { (con integer), (con integer) } -> (con integer)
divideInteger            : { (con integer), (con integer) } -> (con integer)
quotientInteger          : { (con integer), (con integer) } -> (con integer)
remainderInteger         : { (con integer), (con integer) } -> (con integer)
modInteger               : { (con integer), (con integer) } -> (con integer)
equalsInteger            : { (con integer), (con integer) } -> (con bool)
lessThanInteger          : { (con integer), (con integer) } -> (con bool)
lessThanEqualsInteger    : { (con integer), (con integer) } -> (con bool)
appendByteString         : { (con bytestring), (con bytestring) } -> (con bytestring)
consByteString           : { (con integer), (con bytestring) } -> (con bytestring)
sliceByteString          : { (con integer), (con integer), (con bytestring) } -> (con bytestring)
lengthOfByteString       : { (con bytestring) } -> (con integer)
indexByteString          : { (con bytestring), (con integer) } -> (con integer)
equalsByteString         : { (con bytestring), (con bytestring) } -> (con bool)
lessThanByteString       : { (con bytestring), (con bytestring) } -> (con bool)
lessThanEqualsByteString : { (con bytestring), (con bytestring) } -> (con bool)
sha2_256                 : { (con bytestring) } -> (con bytestring)
sha3_256                 : { (con bytestring) } -> (con bytestring)
blake2b_256              : { (con bytestring) } -> (con bytestring)
verifySignature          : { (con bytestring), (con bytestring), (con bytestring) } -> (con bool)
appendString             : { (con string), (con string) } -> (con string)
equalsString             : { (con string), (con string) } -> (con bool)
encodeUtf8               : { (con string) } -> (con bytestring)
decodeUtf8               : { (con bytestring) } -> (con string)
ifThenElse               : { forall a, (con bool), a, a } -> a
chooseUnit               : { forall a, (con unit), a } -> a
trace                    : { forall a, (con string), a } -> a
fstPair                  : { forall a, forall b, [ [ (con pair) a ] b ] } -> a
sndPair                  : { forall a, forall b, [ [ (con pair) a ] b ] } -> b
chooseList               : { forall a, forall b, [ (con list) a ], b, b } -> b
mkCons                   : { forall a, a, [ (con list) a ] } -> [ (con list) a ]
headList                 : { forall a, [ (con list) a ] } -> a
tailList                 : { forall a, [ (con list) a ] } -> [ (con list) a ]
nullList                 : { forall a, [ (con list) a ] } -> (con bool)
chooseData               : { forall a, (con data), a, a, a, a, a } -> a
constrData               : { (con integer), (con list (data)) } -> (con data)
mapData                  : { (con list (pair (data) (data))) } -> (con data)
listData                 : { (con list (data)) } -> (con data)
iData                    : { (con integer) } -> (con data)
bData                    : { (con bytestring) } -> (con data)
unConstrData             : { (con data) } -> (con pair (integer) (list (data)))
unMapData                : { (con data) } -> (con list (pair (data) (data)))
unListData               : { (con data) } -> (con list (data))
unIData                  : { (con data) } -> (con integer)
unBData                  : { (con data) } -> (con bytestring)
equalsData               : { (con data), (con data) } -> (con bool)
mkPairData               : { (con data), (con data) } -> (con pair (data) (data))
mkNilData                : { (con unit) } -> (con list (data))
mkNilPairData            : { (con unit) } -> (con list (pair (data) (data)))

[kwxm]

We (IOHK) are working on a revised version of the specification at the moment and hope to have a preliminary public version available in a week or two. That will add a generic specification for built-in functions and explain the semantics of the current set of builtins in detail.

[SchmErik]

Hi @kwxm thanks for your response! For some reason, I didn't see your response until now. Do you have any updates on a preliminary version of the specification?

[kwxm]

Hi @kwxm thanks for your response! For some reason, I didn't see your response until now. Do you have any updates on a preliminary version of the specification?

I hope that we should be able to give you something early next week. It'll still be kind of rough, but having feedback from formalisers could be very helpful.

[SchmErik]

Ok, here's the situation on our side: we found several missing pieces that are blocking us from completing the flat format parser and the semantics as well as a few other corrections. Some of these issues may be resolved in this new format but I'll open bugs against them now and check the new version to see if they've been addressed. We're Looking forward to seeing the new version!