Feature Overview for mir-semantics applied to p-token

[jberthold]

Feature List for mir-semantics applied to p-token

The following tables enumerate MIR features used in the p-token contract code and its supporting libraries, in particular the pinocchio library.

Organised along the essential MIR constructs, we provide indications of what is used in p-token as well as our implementation progress and roadmap towards supporting it.

Scale of the extracted MIR

Crate	Item Count	Unevaluated Constants
five8_const-7a7eaf25d5456ae4.smir.json	17	2
five8_core-d65460d704b16048.smir.json
pinocchio-ceb2bae344bce809.smir.json	18
pinocchio_log-a975bfb56b4a7d15.smir.json
pinocchio_pubkey-ed41f003f12e2219.smir.json
token_interface-780379fb816ad22c.smir.json		2
token_program.smir.json	128	3

Base types used

"Bool"
"Char"
"Float": "F64"
"Int": "I16"
"Int": "I32"
"Int": "I64"
"Int": "I8"
"Int": "Isize"
"Uint": "U16"
"Uint": "U32"
"Uint": "U64"
"Uint": "U8"
"Uint": "Usize"

• Bool and integral base types are implemented.
• Char will be implemented soon.
• The Float type is not supported yet and was previously descoped as high-effort/low-gain.

Intrinsics called in the p-token code

Intrinsic Name	Comment
"assert_inhabited"	either panic or no-op
"black_box"	no-op at runtime, used to prevent optimisations
"cold_path"	compiler hint only
----------------------------	-------------------------------------------------
"compare_bytes"	unsigned-byte comparison
"ctpop"	safe to call in all circumstances
"cttz"	safe to call in all circumstances
"cttz_nonzero"
"exact_div"
----------------------------	-------------------------------------------------
"ptr_offset_from_unsigned"
"raw_eq"
----------------------------	-------------------------------------------------
"saturating_sub"	safe to call in all circumstances
----------------------------	-------------------------------------------------
"simd_and"
"simd_bitmask"
"simd_eq"
"simd_or"
"simd_reduce_all"
"simd_shuffle"
----------------------------	-------------------------------------------------
"size_of_val"
"write_bytes"
----------------------------	-------------------------------------------------

This is a relatively small set compared to the total ¹.
We will implement intrinsics on a by-need basis.

MIR Features

Terminator Kinds

Terminator	Use	Implemented
"Resume"	Unwinding
"Return"	Control flow	✓
"Unreachable"	No-Op	n/a
"Assert"	Runtime Check	✓
"Call"	Control Flow	✓
"Drop"	Memory Mgmt.
"Goto"	Control Flow	✓
"SwitchInt"	Control Flow	✓

Not used:
InlineAsm		not supported
Abort	Unwinding

Statement Kinds

Statement	Use	Implemented
"Assign"	evaluation	✓
"Intrinsic"	safe calls
"StorageDead"	Memory Mgmt.
"StorageLive"	Memory Mgmt.

Not used:
SetDiscriminant
Deinit	Memory Mgmt.
Retag	miri
PlaceMention	technical
FakeRead	technical
AscribeUserType	technical
Coverage	technical
ConstEvalCounter	technical

R-Values

Operation	Use	Implemented
"AddressOf"	pointers
"Aggregate"	ADT/tuples/pointers	✓ (ADTs, tuples)
"BinaryOp"	arith/cmp	✓ (except bit-shifts)
"Cast"	type casts	(see below)
"CheckedBinaryOp"	arithmetic	✓
"Discriminant"
"Len"	arrays/slices
"NullaryOp"	static information
"Ref"	references
"Repeat"	arrays/slices
"UnaryOp"	arith/logic/pointers	✓ (arithmetic/logic)
"Use"	passing values	✓

Not used
CopyForDeref	Memory Mgmt.	Variant of Use
ShallowInitBox	Memory Mgmt.

Type casts

Cast Kind	Implemented
"IntToInt"	✓
"FloatToInt"
"IntToFloat"
"PointerCoercion": "Unsize"
"PointerExposeAddress"
"PointerWithExposedProvenance"
"PtrToPtr"
"Transmute"

Not used:
"DynStar"
"PointerCoercion":
"FloatToFloat"
"FnPtrToPtr"

Summary / Other aspects

Programs with basic numeric types performing arithmetic are supported in the current state. To enable better use of stdlib functions, the next step will be support for references and dereferencing. Support for arrays and slices is also planned to be added next.
Furthermore, function pointers (as arguments) need to be supported, the current semantics only supports named constant functions but stdlib uses function pointers in many places.
More explicit memory management, including dynamic allocation and various pointer operations, follows afterwards. Intrinsics will be implemented on a by-need basis.

Footnotes

1. https://doc.rust-lang.org/std/intrinsics/index.html#functions ↩