Table of Contents for Programming Languages: a survey

https://en.bitcoin.it/wiki/Script

" Disabled opcodes. Bitcoin used to support a wider range of Script opcodes than exist now. Many were disabled for security reasons in 2010, and require a hard fork to re-enable them. Some of them had significant risks (unbounded memory usage), but not all of them. Alpha reintroduces these safe but disabled opcodes. They include string concatenation and substrings, integer shifts, and several bitwise operations. " -- https://github.com/ElementsProject/elementsproject.github.io

Proposal to re-enable some of those:

" ...

- re-enable CAT, SUBSTR, LEFT, RIGHT, INVERT, AND, OR, XOR, LSHIFT, and RSHIFT;
- introduce new opcodes: DUPTOALTSTACK (0xba), DUPFROMALTSTACK (0xbb), SWAPSTACK (0xbc), SWAPCAT (0xbd), and RESIZE (0xbe); ... In the following, xn represents the top-n item on the stack. For example, x1 is the top stack item, and x2 is the second-to-top item.

CAT and SWAPCAT will remove the top two stack items and push the concantenated string onto the stack. If x2 is "abcd" and x1 is "efgh", CAT will return "abcdefgh" while SWAPCAT will return "efghabcd". The script will fail if the stack has less than two items or the total size of the concantenated string is bigger than TBD bytes.

SUBSTR will remove the top three stack items and push a substring of x3 onto the stack, with x2 as the starting position, and x1 as the length of the substring. For example, if x3 is "abcdefghij", x2 is 3 and x1 is 4, the returned string is "defg". The script will fail if the stack has less then three items, x2 or x3 is negative, x2 is not smaller than the size of x1, and x2 + x3 is bigger than the size of x1.

LEFT will remove the top two stack items and push the x1 leftmost characters of x2 onto the stack. For example, if x2 is "abcdefghij" and x1 is 6, the returned string is "abcdef". An empty vector is returned if x1 is 0, and x2 is returned if x1 is not smaller than the size of x2. The script will fail if the stack has less than two items or x1 is negative.

RIGHT will remove the top two stack items and push the x2 with the x1 leftmost characters removed onto the stack. For example, if x2 is "abcdefghij" and x1 is 6, the returned string is "ghij". x2 is returned if x1 is 0, and an empty vector is returned if x1 is not smaller than the size of x2. The script will fail if the stack has less than two items or x1 is negative.

INVERT will flip the bits of the top stack item. For example, 0xbeef (0b1011111011101111) will become 0x4110 (0b0100000100010000). The script will fail if the stack is empty.

AND, OR, XOR will remove the top two stack items and push the boolean and, or, xor of the two values onto the stack, respectively. For example, if the values are 0xdead (0b1101111010101101) and 0xbeef (0b1011111011101111):

ANDwill return 0x9ead (0b1001111010101101), ORwill return 0xfeef (0b1111111011101111), XORwill return 0x6042 (0b0110000001000010).

The script will fail if the stack has less then two items or the size of the top two items are not the same.

LSHIFT will remove the top two stack items. The x2, interpreted as a little-endian string, will be left-shifted by x1 bits and the result (with most significant zero bytes removed) is pushed onto the stack. For example, if x2 is 0xbeef00 (0b101111101110111100000000) and x1 is 11, the result is 0x00f07d07 (0b00000000111100000111110100000111). The script will fail if the stack has less then two items, or x1 is negative, or size of the result is potentially larger than TBD bytes.

RSHIFT will remove the top two stack items. The x2, interpreted as a little-endian string, will be right-shifted by x1 bits and the result (with most significant zero bytes removed) is pushed onto the stack. For example, if x2 is 0xbeef00 (0b101111101110111100000000) and x1 is 11, the result is 0x1d (0b00011101). The script will fail if the stack has less then two items or x1 is negative.

RESIZE will remove the top two stack items. The x2 will be resized to x1 bytes and pushed onto the stack. Zero-padding or truncation will be made at the right hand side. For example, if x2 is 0xdeadbeef, x1 = 6 will return 0xdeadbeef0000, x1 = 4 will return 0xdeadbeef, x1 = 2 will return 0xdead, and x1 = 0 will return an empty vector. The script will fail if the stack has less than two items, or x1 is negative, or x1 is greater than TBD.

DUPTOALTSTACK will copy the top main stack item onto the top of the alt stack. The main stack is not modified.

DUPFROMALTSTACK will copy the top alt stack item onto the top of the main stack. The alt stack is not modified.

SWAPSTACK will swap main stack and alt stack. ... " -- [1]

https://cardanodocs.com/technical/plutus/introduction/ https://cardanodocs.com/technical/plutus/types/ https://cardanodocs.com/technical/plutus/examples/

intended to be used in place of things like Bitcoin script, for the cryptocurrency Cardano.

" The Plutus language is a variant of the λ calculus with functions and user-defined recursive data types, as well as a variety of build-in functions for cryptographic calculations.

...

a strictly-typed, parametrically polymorphic language similar to Haskell and ML.

...

Tm ::=

- x (variable)
- n (declared name)
- m : t (type annotation)
- let { tmd ∗ } in m (local declarations)
- λx → m λ * (abstraction)
- mm (function application)
- n m ∗ (constructed data)
- case m ∗ of { c ∗ } (case)
- success m (success)
- failure failure)
- do { x ← m ; m } (do notation)
- !n m ∗ (built-in function)

Cl ::=

- p ∗ → m (case clause)

Pat ::=

- x (variable pattern)
- n p ∗ (constructor pattern)

Prg ::=

- d ∗ (programs)

Dec ::=

- tyd (type declaration)
- tmd (term declaration)

TyDec? ::=

- data n α ∗ = tyc ∗ (type declaration)

TyCl? ::=

- n t ∗ type (alternative clause)

Ty ::=

- α (type variable)
- n t ∗ (type constructor)
- t → t (function type)
- ∀α. t (polymorphic quantifier)
- Comp t (computations)

TmDec? ::=

- n : t { tmc ∗ } (term declaration)

TmCl? ::=

- n p ∗ = m (term clause) " -- [2]

(i think that the following quote is obsoleted by the quotes given afterwards from 'Rev 12'?)

"Plutus Core is an untyped λ calculus...we have variables, λ abstractions, and application. In addition to this, there are also local let bindings, data constructors which have arguments, case terms which match on lists of terms, declared names, success and failure terms, and built-in functions. Terms live within a top level program which consists of some declarations.

...

Tm m ::=

- x (variable)
- decname[n] (declared name)
- let(m;x.m) (local declaration)
- λ(x.m) λ (abstraction)
- app(m;m) (function application)
- con[n](m ∗ ) (constructed data)
- case(m ∗ ;c ∗ ) (case)
- success(m) (success)
- failure (failure)
- bind(m;x.m) (computation bind)
- builtin[n](m ∗ ) (built-in function)

c ::=

- cl(p ∗ ;m) (case clause)

p ::=

- x (variable pattern)
- con[n](p ∗ ) (constructor pattern)

g ::=

- program(d ∗ ) (program)

d ::=

- dec(n;m) (name declaration)

" -- [3]

" Plutus Core is a typed, strict, eagerly-reduced λ-calculus design to run as a transaction validation scripting language on blockchain systems. It’s designed to be simple and easy to reason about using mechanized proof assistants and automated theorem provers.... As is standard in λ-calculi, we have variables, λ-abstractions, and application. In addition to this, there are also polymorphic and instantiation, data constructors, case expressions, declared names, computational primitives, primitive values, and built- in functions. Terms live within top-level declarations, which can also consist of data and type declarations as well as type signature declarations. Declarations themselves reside within modules, and a program is a collection of such modules.

...

In this grammar, we have multi-argument application, both in types ([T T + ]) and in terms ([M M + ]). This is to be understood as a convenient form of syntactic sugar for iterated binary application associated to the left, and the formal rules treat only the binary case.

...

As an example, consider the program in Figure 3, which defines the type of natural numbers as well as lists, and the factorial and map functions. This program is not the most read- able, which is to be expected from a representation intended for machine interpretation rather than human interpretation, but it does make explicit precisely what the roles are of the various parts.

Fig. 3. Example with Fibonacci and Map

(program (data Nat () (Zero) (Suc (con Nat))) (data List ((a (type))) (Nil) (Cons a (con List a))) (declare fibonacci (fun (con Nat) (con Nat))) (define fibonacci (lam n (case (builtin equalsInteger n 0) (True () 1) (False () (builtin multiplyInteger n [fibonacci (builtin subtractInteger n 1)]))))) (declare map (forall a (type) (forall b (type) (fun (fun a b) (fun (con List a) (con List b)))))) (define map (abs a (abs b (lam f (lam xs (case xs (Nil () (con N il)) (Cons (x xs 0 ) (con Cons [f x] [(inst (inst map a) b) f xs 0 ])))))))))

...

Fig. 1. Grammar of Plutus Core

Term M,N ::=

- x (variable)
- n (declared name)
- (isa T M ) (type annotation)
- (letrec T (D ∗ ) M ) (letrec)
- (abs α M ) (type abstraction)
- (inst M T ) (type instantiation)
- (lam x M ) (λ abstraction)
- [M M + ] (function application)
- (con c M ∗ ) (constructed data)
- (case M C ∗ ) (case)
- (success M ) (success)
- (failure) (failure)
- (compbuiltin cbi) (computation builtin)
- (bind M x M ) (computation bind)
- i (primitive integer)
- f (primitive float)
- b (primitive bytestring)
- (builtin bi M ∗ ) (built-in function)

Clause C ::=

- (c (x ∗ ) M ) (case clause)

Declaration D ::=

- dd (data decl.)
- td (type decl.)
- md (term decl.)
- df (term defn.)

Type R,S,T ::=

- α (type variable)
- ν (declared type name)
- (fun T T ) (function type)
- (con κ T ∗ ) (type constructor)
- (comp T ) (computation type)
- (forall α K T ) (polymorphic type)
- (bytestring) (bytestring)
- (integer) (integer)
- (float) (float)
- (lam α K T ) (type abstraction)
- [T T + ] (type application)

Kind J,K ::=

- (type) (type kind)
- (fun K K) (arrow kind)

Data Declaration dd ::=

- (data κ (ks ∗ ) alt ∗ ) (data decl.)

Type Declaration td ::=

- (type ν T ) (type decl.)

Kind Signature ks ::=

- (α K) (kind signature)

Alternative alt ::=

- (c T ∗ ) (alternative)

Term Declaration md ::=

- (declare n T ) (term decl.)

Term Definition df ::=

- (define n M ) (name definition)

...

Fig. 22. Builtin Types and Reductions ((excerpted))

- addInteger
- subtractInteger
- multiplyInteger
- divideInteger
- remainderInteger
- lessThanInteger
- lessThanEqualsInteger
- greaterThanInteger
- greaterThanEqualsInteger
- equalsInteger
- intToFloat
- intToByteString
- addFloat
- subtractFloat
- multiplyFloat
- divideFloat
- lessThanFloat
- lessThanEqualsFloat
- greaterThanFloat
- greaterThanEqualsFloat
- equalsFloat
- ceil
- floor
- round
- concatenate
- takeByteString
- dropByteString
- sha2 256
- sha3 256
- equalsByteString

...

Fig. 23. Comp Builtin Types

- txhash
- blocknum
- blocktime

" -- [4]

https://en.wikipedia.org/wiki/LOOP_%28programming_language%29 , http://www.lacl.fr/valarcher/Publi/fi2011.pdf http://web.archive.org/web/20120311032544/http://loopgotowhile.eugenkiss.com/