Scale of the Extracted MIR

Oct 13, 2025 by wbrum.org 12 views

Feature Overview for Mir-Semantics Applied to p-token

The p-token contract code and its supporting libraries, particularly the pinocchio library, utilize various features from the Mir-semantics framework. In this article, we will provide an overview of the MIR features used in p-token, including the scale of the extracted MIR, base types used, intrinsics called in the p-token code, MIR features, and a summary of other aspects.

Scale of the Extracted MIR

The following table enumerates the MIR features used in the p-token contract code and its supporting libraries:

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

As shown in the table, the p-token contract code and its supporting libraries use a total of 171 MIR features, with 17 unevaluated constants.

Base Types Used

The following base types are used in the p-token contract code and its supporting libraries:

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

The Bool and integral base types are implemented, while the Char type 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

The following intrinsics are 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 ^[1]. We will implement intrinsics on a by-need basis.

MIR Features

Terminator Kinds

The following terminator kinds are used in the p-token contract code and its supporting libraries:

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

The following statement kinds are used in the p-token contract code and its supporting libraries:

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

The following R-value operations are used in the p-token contract code and its supporting libraries:

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

The following type casts are used in the p-token contract code and its supporting libraries:

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.
Q&A: Mir-Semantics Applied to p-token

In our previous article, we provided an overview of the MIR features used in the p-token contract code and its supporting libraries. In this article, we will answer some frequently asked questions about mir-semantics applied to p-token.

Q: What is mir-semantics?

A: Mir-semantics is a framework for representing and analyzing the semantics of Rust programs. It provides a way to model the behavior of Rust code and to reason about its correctness.

Q: What is the purpose of mir-semantics in p-token?

A: The purpose of mir-semantics in p-token is to provide a formal model of the behavior of the contract code and its supporting libraries. This allows us to reason about the correctness of the code and to identify potential issues.

Q: What are the benefits of using mir-semantics in p-token?

A: The benefits of using mir-semantics in p-token include:

Improved code quality: By modeling the behavior of the code, we can identify potential issues and improve the overall quality of the code.
Increased confidence: By using a formal model of the behavior of the code, we can increase our confidence in the correctness of the code.
Better understanding: By analyzing the behavior of the code, we can gain a better understanding of how it works and how it can be improved.

Q: What are the challenges of using mir-semantics in p-token?

A: The challenges of using mir-semantics in p-token include:

Complexity: Mir-semantics can be complex and difficult to understand, especially for those without a background in formal methods.
Time-consuming: Analyzing the behavior of the code using mir-semantics can be time-consuming and require significant resources.
Limited support: Mir-semantics may not be widely supported or adopted, which can make it difficult to find resources or expertise.

Q: How does mir-semantics relate to other formal methods?

A: Mir-semantics is a formal method that can be used in conjunction with other formal methods, such as type systems and proof assistants. It provides a way to model the behavior of Rust code and to reason about its correctness, which can be used in conjunction with other formal methods to provide a more comprehensive understanding of the code.

Q: Can mir-semantics be used in other programming languages?

A: Yes, mir-semantics can be used in other programming languages, including C, C++, and Java. However, the specific implementation and usage of mir-semantics may vary depending on the language and the specific use case.

Q: What is the future of mir-semantics in p-token?

A: The future of mir-semantics in p-token is promising, with ongoing development and improvement of the framework. As the framework continues to evolve, we expect to see increased adoption and use of mir-semantics in p-token and other Rust projects.

Q: How can I get started with mir-semantics in p-token?

A: To get started with mir-semantics in p-token, we recommend the following:

Familiarize yourself with the Rust programming language and the p-token contract code.
Learn about the mir-semantics framework and its usage in p-token.
Experiment with using mir-semantics in your own Rust projects.
Join the Rust community and participate in discussions about mir-semantics and p-token.

We hope this Q&A article has provided helpful information about mir-semantics applied to p-token. If you have any further questions or would like to learn more, please don't hesitate to contact us.

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