AVM: Add a lot of type annotations to opcodes (algorand#5902)

data/transactions/logic/README.md

@@ -52,9 +52,6 @@ assembly time to do type checking and to provide more informative error messages
 
 | Name | Bound | AVM Type |
 | ---- | ---- | -------- |
-| [32]byte | len(x) == 32 | []byte |
-| [64]byte | len(x) == 64 | []byte |
-| [80]byte | len(x) == 80 | []byte |
 | []byte | len(x) <= 4096 | []byte |
 | address | len(x) == 32 | []byte |
 | any |  | any |

data/transactions/logic/TEAL_opcodes_v1.md

@@ -133,7 +133,7 @@ Overflow is an error condition which halts execution and fails the transaction.
 ## itob
 
 - Bytecode: 0x16
-- Stack: ..., A: uint64 → ..., []byte
+- Stack: ..., A: uint64 → ..., [8]byte
 - converts uint64 A to big-endian byte array, always of length 8
 
 ## btoi

data/transactions/logic/TEAL_opcodes_v10.md

@@ -43,7 +43,7 @@ The 32 byte public key is the last element on the stack, preceded by the 64 byte
 
 - Syntax: `ecdsa_verify V` where V: [ECDSA](#field-group-ecdsa)
 - Bytecode: 0x05 {uint8}
-- Stack: ..., A: [32]byte, B: []byte, C: []byte, D: []byte, E: []byte → ..., bool
+- Stack: ..., A: [32]byte, B: [32]byte, C: [32]byte, D: [32]byte, E: [32]byte → ..., bool
 - for (data A, signature B, C and pubkey D, E) verify the signature of the data against the pubkey => {0 or 1}
 - **Cost**: Secp256k1=1700; Secp256r1=2500
 - Availability: v5
@@ -64,7 +64,7 @@ The 32 byte Y-component of a public key is the last element on the stack, preced
 
 - Syntax: `ecdsa_pk_decompress V` where V: [ECDSA](#field-group-ecdsa)
 - Bytecode: 0x06 {uint8}
-- Stack: ..., A: []byte → ..., X: []byte, Y: []byte
+- Stack: ..., A: [33]byte → ..., X: [32]byte, Y: [32]byte
 - decompress pubkey A into components X, Y
 - **Cost**: Secp256k1=650; Secp256r1=2400
 - Availability: v5
@@ -75,7 +75,7 @@ The 33 byte public key in a compressed form to be decompressed into X and Y (top
 
 - Syntax: `ecdsa_pk_recover V` where V: [ECDSA](#field-group-ecdsa)
 - Bytecode: 0x07 {uint8}
-- Stack: ..., A: [32]byte, B: uint64, C: [32]byte, D: [32]byte → ..., X: []byte, Y: []byte
+- Stack: ..., A: [32]byte, B: uint64, C: [32]byte, D: [32]byte → ..., X: [32]byte, Y: [32]byte
 - for (data A, recovery id B, signature C, D) recover a public key
 - **Cost**: 2000
 - Availability: v5
@@ -175,7 +175,7 @@ Overflow is an error condition which halts execution and fails the transaction.
 ## itob
 
 - Bytecode: 0x16
-- Stack: ..., A: uint64 → ..., []byte
+- Stack: ..., A: uint64 → ..., [8]byte
 - converts uint64 A to big-endian byte array, always of length 8
 
 ## btoi
@@ -896,7 +896,7 @@ params: Txn.Accounts offset (or, since v4, an _available_ account address), _ava
 ## app_local_get
 
 - Bytecode: 0x62
-- Stack: ..., A, B: []byte → ..., any
+- Stack: ..., A, B: stateKey → ..., any
 - local state of the key B in the current application in account A
 - Availability: v2
 - Mode: Application
@@ -906,7 +906,7 @@ params: Txn.Accounts offset (or, since v4, an _available_ account address), stat
 ## app_local_get_ex
 
 - Bytecode: 0x63
-- Stack: ..., A, B: uint64, C: []byte → ..., X: any, Y: bool
+- Stack: ..., A, B: uint64, C: stateKey → ..., X: any, Y: bool
 - X is the local state of application B, key C in account A. Y is 1 if key existed, else 0
 - Availability: v2
 - Mode: Application
@@ -916,7 +916,7 @@ params: Txn.Accounts offset (or, since v4, an _available_ account address), _ava
 ## app_global_get
 
 - Bytecode: 0x64
-- Stack: ..., A: []byte → ..., any
+- Stack: ..., A: stateKey → ..., any
 - global state of the key A in the current application
 - Availability: v2
 - Mode: Application
@@ -926,7 +926,7 @@ params: state key. Return: value. The value is zero (of type uint64) if the key
 ## app_global_get_ex
 
 - Bytecode: 0x65
-- Stack: ..., A: uint64, B: []byte → ..., X: any, Y: bool
+- Stack: ..., A: uint64, B: stateKey → ..., X: any, Y: bool
 - X is the global state of application A, key B. Y is 1 if key existed, else 0
 - Availability: v2
 - Mode: Application
@@ -936,7 +936,7 @@ params: Txn.ForeignApps offset (or, since v4, an _available_ application id), st
 ## app_local_put
 
 - Bytecode: 0x66
-- Stack: ..., A, B: []byte, C → ...
+- Stack: ..., A, B: stateKey, C → ...
 - write C to key B in account A's local state of the current application
 - Availability: v2
 - Mode: Application
@@ -946,15 +946,15 @@ params: Txn.Accounts offset (or, since v4, an _available_ account address), stat
 ## app_global_put
 
 - Bytecode: 0x67
-- Stack: ..., A: []byte, B → ...
+- Stack: ..., A: stateKey, B → ...
 - write B to key A in the global state of the current application
 - Availability: v2
 - Mode: Application
 
 ## app_local_del
 
 - Bytecode: 0x68
-- Stack: ..., A, B: []byte → ...
+- Stack: ..., A, B: stateKey → ...
 - delete key B from account A's local state of the current application
 - Availability: v2
 - Mode: Application
@@ -966,7 +966,7 @@ Deleting a key which is already absent has no effect on the application local st
 ## app_global_del
 
 - Bytecode: 0x69
-- Stack: ..., A: []byte → ...
+- Stack: ..., A: stateKey → ...
 - delete key A from the global state of the current application
 - Availability: v2
 - Mode: Application
@@ -1254,7 +1254,7 @@ bitlen interprets arrays as big-endian integers, unlike setbit/getbit
 ## bsqrt
 
 - Bytecode: 0x96
-- Stack: ..., A: []byte → ..., []byte
+- Stack: ..., A: bigint → ..., bigint
 - The largest integer I such that I^2 <= A. A and I are interpreted as big-endian unsigned integers
 - **Cost**: 40
 - Availability: v6
@@ -1271,7 +1271,7 @@ The notation A,B indicates that A and B are interpreted as a uint128 value, with
 ## sha3_256
 
 - Bytecode: 0x98
-- Stack: ..., A: []byte &rarr; ..., []byte
+- Stack: ..., A: []byte &rarr; ..., [32]byte
 - SHA3_256 hash of value A, yields [32]byte
 - **Cost**: 130
 - Availability: v7
@@ -1353,7 +1353,7 @@ The notation A,B indicates that A and B are interpreted as a uint128 value, with
 ## b%
 
 - Bytecode: 0xaa
-- Stack: ..., A: []byte, B: []byte &rarr; ..., []byte
+- Stack: ..., A: bigint, B: bigint &rarr; ..., bigint
 - A modulo B. A and B are interpreted as big-endian unsigned integers. Fail if B is zero.
 - **Cost**: 20
 - Availability: v4
@@ -1608,7 +1608,7 @@ For boxes that exceed 4,096 bytes, consider `box_create`, `box_extract`, and `bo
 
 - Syntax: `vrf_verify S` where S: [vrf_verify](#field-group-vrf_verify)
 - Bytecode: 0xd0 {uint8}
-- Stack: ..., A: []byte, B: [80]byte, C: [32]byte &rarr; ..., X: []byte, Y: bool
+- Stack: ..., A: []byte, B: [80]byte, C: [32]byte &rarr; ..., X: [64]byte, Y: bool
 - Verify the proof B of message A against pubkey C. Returns vrf output and verification flag.
 - **Cost**: 5700
 - Availability: v7

data/transactions/logic/TEAL_opcodes_v2.md

@@ -133,7 +133,7 @@ Overflow is an error condition which halts execution and fails the transaction.
 ## itob
 
 - Bytecode: 0x16
-- Stack: ..., A: uint64 → ..., []byte
+- Stack: ..., A: uint64 → ..., [8]byte
 - converts uint64 A to big-endian byte array, always of length 8
 
 ## btoi
@@ -540,7 +540,7 @@ params: Txn.Accounts offset (or, since v4, an _available_ account address), _ava
 ## app_local_get
 
 - Bytecode: 0x62
-- Stack: ..., A: uint64, B: []byte → ..., any
+- Stack: ..., A: uint64, B: stateKey → ..., any
 - local state of the key B in the current application in account A
 - Availability: v2
 - Mode: Application
@@ -550,7 +550,7 @@ params: Txn.Accounts offset (or, since v4, an _available_ account address), stat
 ## app_local_get_ex
 
 - Bytecode: 0x63
-- Stack: ..., A: uint64, B: uint64, C: []byte → ..., X: any, Y: bool
+- Stack: ..., A: uint64, B: uint64, C: stateKey → ..., X: any, Y: bool
 - X is the local state of application B, key C in account A. Y is 1 if key existed, else 0
 - Availability: v2
 - Mode: Application
@@ -560,7 +560,7 @@ params: Txn.Accounts offset (or, since v4, an _available_ account address), _ava
 ## app_global_get
 
 - Bytecode: 0x64
-- Stack: ..., A: []byte → ..., any
+- Stack: ..., A: stateKey → ..., any
 - global state of the key A in the current application
 - Availability: v2
 - Mode: Application
@@ -570,7 +570,7 @@ params: state key. Return: value. The value is zero (of type uint64) if the key
 ## app_global_get_ex
 
 - Bytecode: 0x65
-- Stack: ..., A: uint64, B: []byte → ..., X: any, Y: bool
+- Stack: ..., A: uint64, B: stateKey → ..., X: any, Y: bool
 - X is the global state of application A, key B. Y is 1 if key existed, else 0
 - Availability: v2
 - Mode: Application
@@ -580,7 +580,7 @@ params: Txn.ForeignApps offset (or, since v4, an _available_ application id), st
 ## app_local_put
 
 - Bytecode: 0x66
-- Stack: ..., A: uint64, B: []byte, C → ...
+- Stack: ..., A: uint64, B: stateKey, C → ...
 - write C to key B in account A's local state of the current application
 - Availability: v2
 - Mode: Application
@@ -590,15 +590,15 @@ params: Txn.Accounts offset (or, since v4, an _available_ account address), stat
 ## app_global_put
 
 - Bytecode: 0x67
-- Stack: ..., A: []byte, B → ...
+- Stack: ..., A: stateKey, B → ...
 - write B to key A in the global state of the current application
 - Availability: v2
 - Mode: Application
 
 ## app_local_del
 
 - Bytecode: 0x68
-- Stack: ..., A: uint64, B: []byte → ...
+- Stack: ..., A: uint64, B: stateKey → ...
 - delete key B from account A's local state of the current application
 - Availability: v2
 - Mode: Application
@@ -610,7 +610,7 @@ Deleting a key which is already absent has no effect on the application local st
 ## app_global_del
 
 - Bytecode: 0x69
-- Stack: ..., A: []byte → ...
+- Stack: ..., A: stateKey → ...
 - delete key A from the global state of the current application
 - Availability: v2
 - Mode: Application

data/transactions/logic/TEAL_opcodes_v3.md

@@ -133,7 +133,7 @@ Overflow is an error condition which halts execution and fails the transaction.
 ## itob
 
 - Bytecode: 0x16
-- Stack: ..., A: uint64 → ..., []byte
+- Stack: ..., A: uint64 → ..., [8]byte
 - converts uint64 A to big-endian byte array, always of length 8
 
 ## btoi
@@ -628,7 +628,7 @@ params: Txn.Accounts offset (or, since v4, an _available_ account address), _ava
 ## app_local_get
 
 - Bytecode: 0x62
-- Stack: ..., A: uint64, B: []byte → ..., any
+- Stack: ..., A: uint64, B: stateKey → ..., any
 - local state of the key B in the current application in account A
 - Availability: v2
 - Mode: Application
@@ -638,7 +638,7 @@ params: Txn.Accounts offset (or, since v4, an _available_ account address), stat
 ## app_local_get_ex
 
 - Bytecode: 0x63
-- Stack: ..., A: uint64, B: uint64, C: []byte → ..., X: any, Y: bool
+- Stack: ..., A: uint64, B: uint64, C: stateKey → ..., X: any, Y: bool
 - X is the local state of application B, key C in account A. Y is 1 if key existed, else 0
 - Availability: v2
 - Mode: Application
@@ -648,7 +648,7 @@ params: Txn.Accounts offset (or, since v4, an _available_ account address), _ava
 ## app_global_get
 
 - Bytecode: 0x64
-- Stack: ..., A: []byte → ..., any
+- Stack: ..., A: stateKey → ..., any
 - global state of the key A in the current application
 - Availability: v2
 - Mode: Application
@@ -658,7 +658,7 @@ params: state key. Return: value. The value is zero (of type uint64) if the key
 ## app_global_get_ex
 
 - Bytecode: 0x65
-- Stack: ..., A: uint64, B: []byte → ..., X: any, Y: bool
+- Stack: ..., A: uint64, B: stateKey → ..., X: any, Y: bool
 - X is the global state of application A, key B. Y is 1 if key existed, else 0
 - Availability: v2
 - Mode: Application
@@ -668,7 +668,7 @@ params: Txn.ForeignApps offset (or, since v4, an _available_ application id), st
 ## app_local_put
 
 - Bytecode: 0x66
-- Stack: ..., A: uint64, B: []byte, C → ...
+- Stack: ..., A: uint64, B: stateKey, C → ...
 - write C to key B in account A's local state of the current application
 - Availability: v2
 - Mode: Application
@@ -678,15 +678,15 @@ params: Txn.Accounts offset (or, since v4, an _available_ account address), stat
 ## app_global_put
 
 - Bytecode: 0x67
-- Stack: ..., A: []byte, B → ...
+- Stack: ..., A: stateKey, B → ...
 - write B to key A in the global state of the current application
 - Availability: v2
 - Mode: Application
 
 ## app_local_del
 
 - Bytecode: 0x68
-- Stack: ..., A: uint64, B: []byte → ...
+- Stack: ..., A: uint64, B: stateKey → ...
 - delete key B from account A's local state of the current application
 - Availability: v2
 - Mode: Application
@@ -698,7 +698,7 @@ Deleting a key which is already absent has no effect on the application local st
 ## app_global_del
 
 - Bytecode: 0x69
-- Stack: ..., A: []byte → ...
+- Stack: ..., A: stateKey → ...
 - delete key A from the global state of the current application
 - Availability: v2
 - Mode: Application