From 8890b487bc386ab1853f670b0cec41b4db22e7d4 Mon Sep 17 00:00:00 2001 From: davidsemakula Date: Tue, 12 Nov 2024 12:18:15 +0300 Subject: [PATCH 1/5] pallet-verifier (milestone 1 & 2) --- deliveries/pallet-verifier.md | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 deliveries/pallet-verifier.md diff --git a/deliveries/pallet-verifier.md b/deliveries/pallet-verifier.md new file mode 100644 index 000000000..e50f3b398 --- /dev/null +++ b/deliveries/pallet-verifier.md @@ -0,0 +1,24 @@ +# Milestone Delivery :mailbox: + +**The delivery is according to the official [milestone delivery guidelines](https://github.com/w3f/Grants-Program/blob/master/docs/Support%20Docs/milestone-deliverables-guidelines.md).** + +* **Application Document:** [Pallet Verifier](https://github.com/w3f/Grants-Program/blob/master/applications/pallet-verifier.md) +* **Milestone Number:** 1 & 2 + +**Context** (optional) + +This is a combined delivery for both milestone 1 and 2. + +**Deliverables** + +| Number | Deliverable | Link | Notes | +|---------|---------------------------|--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------| +| **0a.** | License | [MIT](https://github.com/davidsemakula/pallet-verifier/blob/master/LICENSE-MIT) or [Apache 2.0](https://github.com/davidsemakula/pallet-verifier/blob/master/LICENSE-APACHE). | Dual-licensed under either of MIT or Apache 2.0 licenses at the downstream user's option. | +| **0b.** | Documentation | [README](https://github.com/davidsemakula/pallet-verifier/blob/master/README.md) and [Architecture](https://github.com/davidsemakula/pallet-verifier/blob/master/ARCHITECTURE.md) documents on GitHub and extensive inline source documentation. | The README contains instructions for installation and usage. | +| **0c.** | Testing and Testing Guide | [Testing guide](https://github.com/davidsemakula/pallet-verifier/blob/master/README.md#testing). | [UI tests](https://rustc-dev-guide.rust-lang.org/tests/ui.html#introduction) are defined in the [tests/ui](https://github.com/davidsemakula/pallet-verifier/tree/master/tests/ui) directory using the [ui](https://crates.io/crates/ui_test) (also used by [clippy](https://github.com/rust-lang/rust-clippy) and [miri](https://github.com/rust-lang/miri)). Test cases in the [tests/ui/driver](https://github.com/davidsemakula/pallet-verifier/tree/master/tests/ui/driver) and [tests/ui/cargo](https://github.com/davidsemakula/pallet-verifier/tree/master/tests/ui/cargo) subdirectories are essentially minimal sanity checks, while test cases in the [tests/ui/sdk](https://github.com/davidsemakula/pallet-verifier/tree/master/tests/ui/sdk) subdirectory are production pallet tests. The expected output/diagnostics for each test case is defined an `Cargo.stderr` (e.g. [see this](https://github.com/davidsemakula/pallet-verifier/blob/master/tests/ui/sdk/multisig/Cargo.stderr)) - absence of this file implies a test case with no expected diagnostics. | +| 1. | Rust binary crate | [GitHub repository](https://github.com/davidsemakula/pallet-verifier) | | + + +**Additional Information** + +Please use the [master branch](https://github.com/davidsemakula/pallet-verifier/tree/master) for testing. From 0c91f86b84ef2db7e5e24a5bb3220286710cfe12 Mon Sep 17 00:00:00 2001 From: davidsemakula Date: Fri, 15 Nov 2024 00:46:27 +0300 Subject: [PATCH 2/5] update pallet-verifier --- deliveries/pallet-verifier.md | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/deliveries/pallet-verifier.md b/deliveries/pallet-verifier.md index e50f3b398..1fbd76432 100644 --- a/deliveries/pallet-verifier.md +++ b/deliveries/pallet-verifier.md @@ -11,13 +11,15 @@ This is a combined delivery for both milestone 1 and 2. **Deliverables** -| Number | Deliverable | Link | Notes | -|---------|---------------------------|--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------| -| **0a.** | License | [MIT](https://github.com/davidsemakula/pallet-verifier/blob/master/LICENSE-MIT) or [Apache 2.0](https://github.com/davidsemakula/pallet-verifier/blob/master/LICENSE-APACHE). | Dual-licensed under either of MIT or Apache 2.0 licenses at the downstream user's option. | -| **0b.** | Documentation | [README](https://github.com/davidsemakula/pallet-verifier/blob/master/README.md) and [Architecture](https://github.com/davidsemakula/pallet-verifier/blob/master/ARCHITECTURE.md) documents on GitHub and extensive inline source documentation. | The README contains instructions for installation and usage. | -| **0c.** | Testing and Testing Guide | [Testing guide](https://github.com/davidsemakula/pallet-verifier/blob/master/README.md#testing). | [UI tests](https://rustc-dev-guide.rust-lang.org/tests/ui.html#introduction) are defined in the [tests/ui](https://github.com/davidsemakula/pallet-verifier/tree/master/tests/ui) directory using the [ui](https://crates.io/crates/ui_test) (also used by [clippy](https://github.com/rust-lang/rust-clippy) and [miri](https://github.com/rust-lang/miri)). Test cases in the [tests/ui/driver](https://github.com/davidsemakula/pallet-verifier/tree/master/tests/ui/driver) and [tests/ui/cargo](https://github.com/davidsemakula/pallet-verifier/tree/master/tests/ui/cargo) subdirectories are essentially minimal sanity checks, while test cases in the [tests/ui/sdk](https://github.com/davidsemakula/pallet-verifier/tree/master/tests/ui/sdk) subdirectory are production pallet tests. The expected output/diagnostics for each test case is defined an `Cargo.stderr` (e.g. [see this](https://github.com/davidsemakula/pallet-verifier/blob/master/tests/ui/sdk/multisig/Cargo.stderr)) - absence of this file implies a test case with no expected diagnostics. | -| 1. | Rust binary crate | [GitHub repository](https://github.com/davidsemakula/pallet-verifier) | | - +| Number | Deliverable | Link | Notes | +|---------|---------------------------|----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|-----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------| +| **0a.** | License | [MIT](https://github.com/davidsemakula/pallet-verifier/blob/master/LICENSE-MIT) or [Apache 2.0](https://github.com/davidsemakula/pallet-verifier/blob/master/LICENSE-APACHE). | Dual-licensed under either of MIT or Apache 2.0 licenses at the downstream user's option. | +| **0b.** | Documentation | [README](https://github.com/davidsemakula/pallet-verifier/blob/master/README.md) and [Architecture](https://github.com/davidsemakula/pallet-verifier/blob/master/ARCHITECTURE.md) documents. | The [README](https://github.com/davidsemakula/pallet-verifier/blob/master/README.md) contains instructions for installation and usage, the [Architecture document](https://github.com/davidsemakula/pallet-verifier/blob/master/ARCHITECTURE.md) describes how `pallet-verifier` works, while the [source code on GitHub](https://github.com/davidsemakula/pallet-verifier) contains extensive inline documentation. | +| **0c.** | Testing and Testing Guide | [Testing guide](https://github.com/davidsemakula/pallet-verifier/blob/master/TESTING.md). | [UI tests](https://rustc-dev-guide.rust-lang.org/tests/ui.html#introduction) are defined in the [tests/ui](https://github.com/davidsemakula/pallet-verifier/tree/master/tests/ui) directory using the [ui_test framework](https://crates.io/crates/ui_test) (also used by [clippy](https://github.com/rust-lang/rust-clippy) and [miri](https://github.com/rust-lang/miri))
Check out the ["Test Structure" section of the Testing Guide](https://github.com/davidsemakula/pallet-verifier/blob/master/TESTING.md#test-structure) for a detailed description of the purpose of the different test cases and test suites.

For milestone 1: All tests in the [tests/ui/driver](https://github.com/davidsemakula/pallet-verifier/tree/master/tests/ui/driver) and [tests/ui/cargo](https://github.com/davidsemakula/pallet-verifier/tree/master/tests/ui/cargo) subdirectories/ test suites except those related to "integer cast overflow" are relevant (i.e. tests with names that *DON'T* include "int-cast-overflow" suffix).
For milestone 2: Only "integer cast overflow" related tests in [tests/ui/driver](https://github.com/davidsemakula/pallet-verifier/tree/master/tests/ui/driver) and [tests/ui/cargo](https://github.com/davidsemakula/pallet-verifier/tree/master/tests/ui/cargo) are relevant (i.e. tests with names that include "int-cast-overflow" suffix).

Test cases in the [tests/ui/sdk](https://github.com/davidsemakula/pallet-verifier/tree/master/tests/ui/sdk) subdirectory/ test suite are production [FRAME](https://docs.substrate.io/learn/runtime-development/#frame) pallet tests, and include FRAME pallets copied directly from the [Polkadot SDK](https://github.com/paritytech/polkadot-sdk), and as such, apply to both milestones and serve to check the effectiveness of the tool on "real world" production FRAME pallets.

Lastly, the [custom benchmark suite](https://github.com/davidsemakula/pallet-verifier/blob/master/TESTING.md#the-custom-benchmark) is defined in the [benches directory](https://github.com/davidsemakula/pallet-verifier/tree/master/benches). Check out the ["custom benchmark" section of the Testing Guide](https://github.com/davidsemakula/pallet-verifier/blob/master/TESTING.md#the-custom-benchmark) for instructions for running the custom benchmark, and a description of how it works. | +| **0d.** | Docker | N/A | | +| **0e.** | Article | [Article](https://davidsemakula.com/blog/introducing-pallet-verifier) | | +| 1. | Rust binary crate | [GitHub repository](https://github.com/davidsemakula/pallet-verifier) | This includes deliveries for both milestone 1 and 2.

For milestone 1: [custom rustc driver](https://github.com/davidsemakula/pallet-verifier/blob/master/src/driver.rs), [custom cargo subcommand](https://github.com/davidsemakula/pallet-verifier/blob/master/src/main.rs), [MIRAI integration](https://github.com/davidsemakula/pallet-verifier/blob/master/src/callbacks/verifier.rs) ([see also](https://github.com/davidsemakula/pallet-verifier/blob/b8b59354a49432b277c8a311a4a637fc724b08f9/src/driver.rs#L149-L178)) and [automatic tractable entry point generation](https://github.com/davidsemakula/pallet-verifier/blob/master/src/callbacks/entry_points.rs) ([see also](https://github.com/davidsemakula/pallet-verifier/blob/b8b59354a49432b277c8a311a4a637fc724b08f9/src/driver.rs#L126-L147)).
For milestone 2: [adding the `mirai-annotations` crate as a dependency to FRAME pallets without editing `Cargo.toml`](https://github.com/davidsemakula/pallet-verifier/blob/b8b59354a49432b277c8a311a4a637fc724b08f9/src/driver.rs#L50-L70) ([see also](https://github.com/davidsemakula/pallet-verifier/blob/b8b59354a49432b277c8a311a4a637fc724b08f9/src/driver.rs#L199-L251)), [adding MIRAI annotations to MIR, and more specifically to support automatically adding annotations for verifying that integer `as` conversions don't overflow/underflow nor lose precision](https://github.com/davidsemakula/pallet-verifier/blob/master/src/providers/int_cast_overflow.rs).

Check out the [architecture document](https://github.com/davidsemakula/pallet-verifier/blob/master/ARCHITECTURE.md) for a detailed description of how the various components work and fit together. | + **Additional Information** From 68d1b3e2439e0f667efbe7c5dde6cc4ac7039db6 Mon Sep 17 00:00:00 2001 From: davidsemakula Date: Fri, 22 Nov 2024 16:18:02 +0300 Subject: [PATCH 3/5] update pallet-verifier --- deliveries/pallet-verifier.md | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/deliveries/pallet-verifier.md b/deliveries/pallet-verifier.md index 1fbd76432..dfd94e349 100644 --- a/deliveries/pallet-verifier.md +++ b/deliveries/pallet-verifier.md @@ -11,14 +11,14 @@ This is a combined delivery for both milestone 1 and 2. **Deliverables** -| Number | Deliverable | Link | Notes | -|---------|---------------------------|----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|-----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------| -| **0a.** | License | [MIT](https://github.com/davidsemakula/pallet-verifier/blob/master/LICENSE-MIT) or [Apache 2.0](https://github.com/davidsemakula/pallet-verifier/blob/master/LICENSE-APACHE). | Dual-licensed under either of MIT or Apache 2.0 licenses at the downstream user's option. | -| **0b.** | Documentation | [README](https://github.com/davidsemakula/pallet-verifier/blob/master/README.md) and [Architecture](https://github.com/davidsemakula/pallet-verifier/blob/master/ARCHITECTURE.md) documents. | The [README](https://github.com/davidsemakula/pallet-verifier/blob/master/README.md) contains instructions for installation and usage, the [Architecture document](https://github.com/davidsemakula/pallet-verifier/blob/master/ARCHITECTURE.md) describes how `pallet-verifier` works, while the [source code on GitHub](https://github.com/davidsemakula/pallet-verifier) contains extensive inline documentation. | -| **0c.** | Testing and Testing Guide | [Testing guide](https://github.com/davidsemakula/pallet-verifier/blob/master/TESTING.md). | [UI tests](https://rustc-dev-guide.rust-lang.org/tests/ui.html#introduction) are defined in the [tests/ui](https://github.com/davidsemakula/pallet-verifier/tree/master/tests/ui) directory using the [ui_test framework](https://crates.io/crates/ui_test) (also used by [clippy](https://github.com/rust-lang/rust-clippy) and [miri](https://github.com/rust-lang/miri))
Check out the ["Test Structure" section of the Testing Guide](https://github.com/davidsemakula/pallet-verifier/blob/master/TESTING.md#test-structure) for a detailed description of the purpose of the different test cases and test suites.

For milestone 1: All tests in the [tests/ui/driver](https://github.com/davidsemakula/pallet-verifier/tree/master/tests/ui/driver) and [tests/ui/cargo](https://github.com/davidsemakula/pallet-verifier/tree/master/tests/ui/cargo) subdirectories/ test suites except those related to "integer cast overflow" are relevant (i.e. tests with names that *DON'T* include "int-cast-overflow" suffix).
For milestone 2: Only "integer cast overflow" related tests in [tests/ui/driver](https://github.com/davidsemakula/pallet-verifier/tree/master/tests/ui/driver) and [tests/ui/cargo](https://github.com/davidsemakula/pallet-verifier/tree/master/tests/ui/cargo) are relevant (i.e. tests with names that include "int-cast-overflow" suffix).

Test cases in the [tests/ui/sdk](https://github.com/davidsemakula/pallet-verifier/tree/master/tests/ui/sdk) subdirectory/ test suite are production [FRAME](https://docs.substrate.io/learn/runtime-development/#frame) pallet tests, and include FRAME pallets copied directly from the [Polkadot SDK](https://github.com/paritytech/polkadot-sdk), and as such, apply to both milestones and serve to check the effectiveness of the tool on "real world" production FRAME pallets.

Lastly, the [custom benchmark suite](https://github.com/davidsemakula/pallet-verifier/blob/master/TESTING.md#the-custom-benchmark) is defined in the [benches directory](https://github.com/davidsemakula/pallet-verifier/tree/master/benches). Check out the ["custom benchmark" section of the Testing Guide](https://github.com/davidsemakula/pallet-verifier/blob/master/TESTING.md#the-custom-benchmark) for instructions for running the custom benchmark, and a description of how it works. | -| **0d.** | Docker | N/A | | -| **0e.** | Article | [Article](https://davidsemakula.com/blog/introducing-pallet-verifier) | | -| 1. | Rust binary crate | [GitHub repository](https://github.com/davidsemakula/pallet-verifier) | This includes deliveries for both milestone 1 and 2.

For milestone 1: [custom rustc driver](https://github.com/davidsemakula/pallet-verifier/blob/master/src/driver.rs), [custom cargo subcommand](https://github.com/davidsemakula/pallet-verifier/blob/master/src/main.rs), [MIRAI integration](https://github.com/davidsemakula/pallet-verifier/blob/master/src/callbacks/verifier.rs) ([see also](https://github.com/davidsemakula/pallet-verifier/blob/b8b59354a49432b277c8a311a4a637fc724b08f9/src/driver.rs#L149-L178)) and [automatic tractable entry point generation](https://github.com/davidsemakula/pallet-verifier/blob/master/src/callbacks/entry_points.rs) ([see also](https://github.com/davidsemakula/pallet-verifier/blob/b8b59354a49432b277c8a311a4a637fc724b08f9/src/driver.rs#L126-L147)).
For milestone 2: [adding the `mirai-annotations` crate as a dependency to FRAME pallets without editing `Cargo.toml`](https://github.com/davidsemakula/pallet-verifier/blob/b8b59354a49432b277c8a311a4a637fc724b08f9/src/driver.rs#L50-L70) ([see also](https://github.com/davidsemakula/pallet-verifier/blob/b8b59354a49432b277c8a311a4a637fc724b08f9/src/driver.rs#L199-L251)), [adding MIRAI annotations to MIR, and more specifically to support automatically adding annotations for verifying that integer `as` conversions don't overflow/underflow nor lose precision](https://github.com/davidsemakula/pallet-verifier/blob/master/src/providers/int_cast_overflow.rs).

Check out the [architecture document](https://github.com/davidsemakula/pallet-verifier/blob/master/ARCHITECTURE.md) for a detailed description of how the various components work and fit together. | +| Number | Deliverable | Link | Notes | +|---------|---------------------------|----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------| +| **0a.** | License | [MIT](https://github.com/davidsemakula/pallet-verifier/blob/master/LICENSE-MIT) or [Apache 2.0](https://github.com/davidsemakula/pallet-verifier/blob/master/LICENSE-APACHE). | Dual-licensed under either of MIT or Apache 2.0 licenses at the downstream user's option. | +| **0b.** | Documentation | [README](https://github.com/davidsemakula/pallet-verifier/blob/master/README.md) and [Architecture](https://github.com/davidsemakula/pallet-verifier/blob/master/ARCHITECTURE.md) documents. | The [README](https://github.com/davidsemakula/pallet-verifier/blob/master/README.md) contains instructions for installation and usage, the [Architecture document](https://github.com/davidsemakula/pallet-verifier/blob/master/ARCHITECTURE.md) describes how `pallet-verifier` works, while the [source code on GitHub](https://github.com/davidsemakula/pallet-verifier) contains extensive inline documentation. | +| **0c.** | Testing and Testing Guide | [Testing guide](https://github.com/davidsemakula/pallet-verifier/blob/master/TESTING.md). | [UI tests](https://rustc-dev-guide.rust-lang.org/tests/ui.html#introduction) are defined in the [tests/ui](https://github.com/davidsemakula/pallet-verifier/tree/master/tests/ui) directory using the [ui_test framework](https://crates.io/crates/ui_test) (also used by [clippy](https://github.com/rust-lang/rust-clippy) and [miri](https://github.com/rust-lang/miri))
Check out the ["Test Structure" section of the Testing Guide](https://github.com/davidsemakula/pallet-verifier/blob/master/TESTING.md#test-structure) for a detailed description of the purpose of the different test cases and test suites.

For milestone 1: All tests in the [tests/ui/driver](https://github.com/davidsemakula/pallet-verifier/tree/master/tests/ui/driver) and [tests/ui/cargo](https://github.com/davidsemakula/pallet-verifier/tree/master/tests/ui/cargo) subdirectories/ test suites except those related to "integer cast overflow" are relevant (i.e. tests with names that *DON'T* include "int-cast-overflow" suffix).

For milestone 2: Only "integer cast overflow" related tests in [tests/ui/driver](https://github.com/davidsemakula/pallet-verifier/tree/master/tests/ui/driver) and [tests/ui/cargo](https://github.com/davidsemakula/pallet-verifier/tree/master/tests/ui/cargo) are relevant (i.e. tests with names that include "int-cast-overflow" suffix).

Test cases in the [tests/ui/sdk](https://github.com/davidsemakula/pallet-verifier/tree/master/tests/ui/sdk) subdirectory/ test suite are production [FRAME](https://docs.substrate.io/learn/runtime-development/#frame) pallet tests, and include FRAME pallets copied directly from the [Polkadot SDK](https://github.com/paritytech/polkadot-sdk), and as such, apply to both milestones and serve to check the effectiveness of the tool on "real world" production FRAME pallets.

Lastly, the [custom benchmark suite](https://github.com/davidsemakula/pallet-verifier/blob/master/TESTING.md#the-custom-benchmark) is defined in the [benches directory](https://github.com/davidsemakula/pallet-verifier/tree/master/benches). Check out the ["custom benchmark" section of the Testing Guide](https://github.com/davidsemakula/pallet-verifier/blob/master/TESTING.md#the-custom-benchmark) for instructions for running the custom benchmark, and a description of how it works. | +| **0d.** | Docker | N/A | | +| **0e.** | Article | [Article](https://davidsemakula.com/blog/introducing-pallet-verifier) | | +| 1. | Rust binary crate | [GitHub repository](https://github.com/davidsemakula/pallet-verifier) | This includes deliveries for both milestone 1 and 2.

For milestone 1: [custom rustc driver](https://github.com/davidsemakula/pallet-verifier/blob/master/src/driver.rs), [custom cargo subcommand](https://github.com/davidsemakula/pallet-verifier/blob/master/src/main.rs), [MIRAI integration](https://github.com/davidsemakula/pallet-verifier/blob/master/src/callbacks/verifier.rs) ([see also](https://github.com/davidsemakula/pallet-verifier/blob/be0e7ce4d08882cb69f97c67a36091893b2380f4/src/driver.rs#L155-L184)) and [automatic tractable entry point generation](https://github.com/davidsemakula/pallet-verifier/blob/master/src/callbacks/entry_points.rs) ([see also](https://github.com/davidsemakula/pallet-verifier/blob/be0e7ce4d08882cb69f97c67a36091893b2380f4/src/driver.rs#L132-L153)).

For milestone 2: [adding the `mirai-annotations` crate as a dependency to FRAME pallets without editing `Cargo.toml`](https://github.com/davidsemakula/pallet-verifier/blob/be0e7ce4d08882cb69f97c67a36091893b2380f4/src/driver.rs#L56-L76) ([see also](https://github.com/davidsemakula/pallet-verifier/blob/be0e7ce4d08882cb69f97c67a36091893b2380f4/src/driver.rs#L224-L282)), [adding MIRAI annotations to MIR, and more specifically to support automatically adding annotations for verifying that integer `as` conversions don't overflow/underflow nor lose precision](https://github.com/davidsemakula/pallet-verifier/blob/master/src/providers/int_cast_overflow.rs).

Check out the [architecture document](https://github.com/davidsemakula/pallet-verifier/blob/master/ARCHITECTURE.md) for a detailed description of how the various components work and fit together. | **Additional Information** From 17a545fb3354c950993ff4bd0bf20ca0b82a7ec0 Mon Sep 17 00:00:00 2001 From: davidsemakula Date: Tue, 26 Nov 2024 10:22:01 +0300 Subject: [PATCH 4/5] update pallet-verifier --- deliveries/pallet-verifier.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deliveries/pallet-verifier.md b/deliveries/pallet-verifier.md index dfd94e349..dbf8490da 100644 --- a/deliveries/pallet-verifier.md +++ b/deliveries/pallet-verifier.md @@ -18,7 +18,7 @@ This is a combined delivery for both milestone 1 and 2. | **0c.** | Testing and Testing Guide | [Testing guide](https://github.com/davidsemakula/pallet-verifier/blob/master/TESTING.md). | [UI tests](https://rustc-dev-guide.rust-lang.org/tests/ui.html#introduction) are defined in the [tests/ui](https://github.com/davidsemakula/pallet-verifier/tree/master/tests/ui) directory using the [ui_test framework](https://crates.io/crates/ui_test) (also used by [clippy](https://github.com/rust-lang/rust-clippy) and [miri](https://github.com/rust-lang/miri))
Check out the ["Test Structure" section of the Testing Guide](https://github.com/davidsemakula/pallet-verifier/blob/master/TESTING.md#test-structure) for a detailed description of the purpose of the different test cases and test suites.

For milestone 1: All tests in the [tests/ui/driver](https://github.com/davidsemakula/pallet-verifier/tree/master/tests/ui/driver) and [tests/ui/cargo](https://github.com/davidsemakula/pallet-verifier/tree/master/tests/ui/cargo) subdirectories/ test suites except those related to "integer cast overflow" are relevant (i.e. tests with names that *DON'T* include "int-cast-overflow" suffix).

For milestone 2: Only "integer cast overflow" related tests in [tests/ui/driver](https://github.com/davidsemakula/pallet-verifier/tree/master/tests/ui/driver) and [tests/ui/cargo](https://github.com/davidsemakula/pallet-verifier/tree/master/tests/ui/cargo) are relevant (i.e. tests with names that include "int-cast-overflow" suffix).

Test cases in the [tests/ui/sdk](https://github.com/davidsemakula/pallet-verifier/tree/master/tests/ui/sdk) subdirectory/ test suite are production [FRAME](https://docs.substrate.io/learn/runtime-development/#frame) pallet tests, and include FRAME pallets copied directly from the [Polkadot SDK](https://github.com/paritytech/polkadot-sdk), and as such, apply to both milestones and serve to check the effectiveness of the tool on "real world" production FRAME pallets.

Lastly, the [custom benchmark suite](https://github.com/davidsemakula/pallet-verifier/blob/master/TESTING.md#the-custom-benchmark) is defined in the [benches directory](https://github.com/davidsemakula/pallet-verifier/tree/master/benches). Check out the ["custom benchmark" section of the Testing Guide](https://github.com/davidsemakula/pallet-verifier/blob/master/TESTING.md#the-custom-benchmark) for instructions for running the custom benchmark, and a description of how it works. | | **0d.** | Docker | N/A | | | **0e.** | Article | [Article](https://davidsemakula.com/blog/introducing-pallet-verifier) | | -| 1. | Rust binary crate | [GitHub repository](https://github.com/davidsemakula/pallet-verifier) | This includes deliveries for both milestone 1 and 2.

For milestone 1: [custom rustc driver](https://github.com/davidsemakula/pallet-verifier/blob/master/src/driver.rs), [custom cargo subcommand](https://github.com/davidsemakula/pallet-verifier/blob/master/src/main.rs), [MIRAI integration](https://github.com/davidsemakula/pallet-verifier/blob/master/src/callbacks/verifier.rs) ([see also](https://github.com/davidsemakula/pallet-verifier/blob/be0e7ce4d08882cb69f97c67a36091893b2380f4/src/driver.rs#L155-L184)) and [automatic tractable entry point generation](https://github.com/davidsemakula/pallet-verifier/blob/master/src/callbacks/entry_points.rs) ([see also](https://github.com/davidsemakula/pallet-verifier/blob/be0e7ce4d08882cb69f97c67a36091893b2380f4/src/driver.rs#L132-L153)).

For milestone 2: [adding the `mirai-annotations` crate as a dependency to FRAME pallets without editing `Cargo.toml`](https://github.com/davidsemakula/pallet-verifier/blob/be0e7ce4d08882cb69f97c67a36091893b2380f4/src/driver.rs#L56-L76) ([see also](https://github.com/davidsemakula/pallet-verifier/blob/be0e7ce4d08882cb69f97c67a36091893b2380f4/src/driver.rs#L224-L282)), [adding MIRAI annotations to MIR, and more specifically to support automatically adding annotations for verifying that integer `as` conversions don't overflow/underflow nor lose precision](https://github.com/davidsemakula/pallet-verifier/blob/master/src/providers/int_cast_overflow.rs).

Check out the [architecture document](https://github.com/davidsemakula/pallet-verifier/blob/master/ARCHITECTURE.md) for a detailed description of how the various components work and fit together. | +| 1. | Rust binary crate | [GitHub repository](https://github.com/davidsemakula/pallet-verifier) | This includes deliveries for both milestone 1 and 2.

For milestone 1: [custom rustc driver](https://github.com/davidsemakula/pallet-verifier/blob/master/src/driver.rs), [custom cargo subcommand](https://github.com/davidsemakula/pallet-verifier/blob/master/src/main.rs), [MIRAI integration](https://github.com/davidsemakula/pallet-verifier/blob/master/src/callbacks/verifier.rs) ([see also](https://github.com/davidsemakula/pallet-verifier/blob/844a49f85f434442202f724c2b5a8aecd0cf9d84/src/driver.rs#L144-L168)) and [automatic tractable entry point generation](https://github.com/davidsemakula/pallet-verifier/blob/master/src/callbacks/entry_points.rs) ([see also](https://github.com/davidsemakula/pallet-verifier/blob/844a49f85f434442202f724c2b5a8aecd0cf9d84/src/driver.rs#L124-L142)).

For milestone 2: [adding the `mirai-annotations` crate as a dependency to FRAME pallets without editing `Cargo.toml`](https://github.com/davidsemakula/pallet-verifier/blob/844a49f85f434442202f724c2b5a8aecd0cf9d84/src/driver.rs#L196-L254) (see also [this](https://github.com/davidsemakula/pallet-verifier/blob/844a49f85f434442202f724c2b5a8aecd0cf9d84/src/driver.rs#L201-L254) and [this](https://github.com/davidsemakula/pallet-verifier/blob/844a49f85f434442202f724c2b5a8aecd0cf9d84/src/main.rs#L259-L273)), [adding MIRAI annotations to MIR, and more specifically to support automatically adding annotations for verifying that integer `as` conversions don't overflow/underflow nor lose precision](https://github.com/davidsemakula/pallet-verifier/blob/master/src/providers/int_cast_overflow.rs).

Check out the [architecture document](https://github.com/davidsemakula/pallet-verifier/blob/master/ARCHITECTURE.md) for a detailed description of how the various components work and fit together. | **Additional Information** From 24b8cd4b7e36d3242c9ab2817df1444c658fd437 Mon Sep 17 00:00:00 2001 From: davidsemakula Date: Thu, 28 Nov 2024 13:07:10 +0300 Subject: [PATCH 5/5] update pallet-verifier: fix some code links --- deliveries/pallet-verifier.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deliveries/pallet-verifier.md b/deliveries/pallet-verifier.md index dbf8490da..13dd090f1 100644 --- a/deliveries/pallet-verifier.md +++ b/deliveries/pallet-verifier.md @@ -18,7 +18,7 @@ This is a combined delivery for both milestone 1 and 2. | **0c.** | Testing and Testing Guide | [Testing guide](https://github.com/davidsemakula/pallet-verifier/blob/master/TESTING.md). | [UI tests](https://rustc-dev-guide.rust-lang.org/tests/ui.html#introduction) are defined in the [tests/ui](https://github.com/davidsemakula/pallet-verifier/tree/master/tests/ui) directory using the [ui_test framework](https://crates.io/crates/ui_test) (also used by [clippy](https://github.com/rust-lang/rust-clippy) and [miri](https://github.com/rust-lang/miri))
Check out the ["Test Structure" section of the Testing Guide](https://github.com/davidsemakula/pallet-verifier/blob/master/TESTING.md#test-structure) for a detailed description of the purpose of the different test cases and test suites.

For milestone 1: All tests in the [tests/ui/driver](https://github.com/davidsemakula/pallet-verifier/tree/master/tests/ui/driver) and [tests/ui/cargo](https://github.com/davidsemakula/pallet-verifier/tree/master/tests/ui/cargo) subdirectories/ test suites except those related to "integer cast overflow" are relevant (i.e. tests with names that *DON'T* include "int-cast-overflow" suffix).

For milestone 2: Only "integer cast overflow" related tests in [tests/ui/driver](https://github.com/davidsemakula/pallet-verifier/tree/master/tests/ui/driver) and [tests/ui/cargo](https://github.com/davidsemakula/pallet-verifier/tree/master/tests/ui/cargo) are relevant (i.e. tests with names that include "int-cast-overflow" suffix).

Test cases in the [tests/ui/sdk](https://github.com/davidsemakula/pallet-verifier/tree/master/tests/ui/sdk) subdirectory/ test suite are production [FRAME](https://docs.substrate.io/learn/runtime-development/#frame) pallet tests, and include FRAME pallets copied directly from the [Polkadot SDK](https://github.com/paritytech/polkadot-sdk), and as such, apply to both milestones and serve to check the effectiveness of the tool on "real world" production FRAME pallets.

Lastly, the [custom benchmark suite](https://github.com/davidsemakula/pallet-verifier/blob/master/TESTING.md#the-custom-benchmark) is defined in the [benches directory](https://github.com/davidsemakula/pallet-verifier/tree/master/benches). Check out the ["custom benchmark" section of the Testing Guide](https://github.com/davidsemakula/pallet-verifier/blob/master/TESTING.md#the-custom-benchmark) for instructions for running the custom benchmark, and a description of how it works. | | **0d.** | Docker | N/A | | | **0e.** | Article | [Article](https://davidsemakula.com/blog/introducing-pallet-verifier) | | -| 1. | Rust binary crate | [GitHub repository](https://github.com/davidsemakula/pallet-verifier) | This includes deliveries for both milestone 1 and 2.

For milestone 1: [custom rustc driver](https://github.com/davidsemakula/pallet-verifier/blob/master/src/driver.rs), [custom cargo subcommand](https://github.com/davidsemakula/pallet-verifier/blob/master/src/main.rs), [MIRAI integration](https://github.com/davidsemakula/pallet-verifier/blob/master/src/callbacks/verifier.rs) ([see also](https://github.com/davidsemakula/pallet-verifier/blob/844a49f85f434442202f724c2b5a8aecd0cf9d84/src/driver.rs#L144-L168)) and [automatic tractable entry point generation](https://github.com/davidsemakula/pallet-verifier/blob/master/src/callbacks/entry_points.rs) ([see also](https://github.com/davidsemakula/pallet-verifier/blob/844a49f85f434442202f724c2b5a8aecd0cf9d84/src/driver.rs#L124-L142)).

For milestone 2: [adding the `mirai-annotations` crate as a dependency to FRAME pallets without editing `Cargo.toml`](https://github.com/davidsemakula/pallet-verifier/blob/844a49f85f434442202f724c2b5a8aecd0cf9d84/src/driver.rs#L196-L254) (see also [this](https://github.com/davidsemakula/pallet-verifier/blob/844a49f85f434442202f724c2b5a8aecd0cf9d84/src/driver.rs#L201-L254) and [this](https://github.com/davidsemakula/pallet-verifier/blob/844a49f85f434442202f724c2b5a8aecd0cf9d84/src/main.rs#L259-L273)), [adding MIRAI annotations to MIR, and more specifically to support automatically adding annotations for verifying that integer `as` conversions don't overflow/underflow nor lose precision](https://github.com/davidsemakula/pallet-verifier/blob/master/src/providers/int_cast_overflow.rs).

Check out the [architecture document](https://github.com/davidsemakula/pallet-verifier/blob/master/ARCHITECTURE.md) for a detailed description of how the various components work and fit together. | +| 1. | Rust binary crate | [GitHub repository](https://github.com/davidsemakula/pallet-verifier) | This includes deliveries for both milestone 1 and 2.

For milestone 1: [custom rustc driver](https://github.com/davidsemakula/pallet-verifier/blob/master/src/driver.rs), [custom cargo subcommand](https://github.com/davidsemakula/pallet-verifier/blob/master/src/main.rs), [MIRAI integration](https://github.com/davidsemakula/pallet-verifier/blob/master/src/callbacks/verifier.rs) ([see also](https://github.com/davidsemakula/pallet-verifier/blob/844a49f85f434442202f724c2b5a8aecd0cf9d84/src/driver.rs#L144-L168)) and [automatic tractable entry point generation](https://github.com/davidsemakula/pallet-verifier/blob/master/src/callbacks/entry_points.rs) ([see also](https://github.com/davidsemakula/pallet-verifier/blob/844a49f85f434442202f724c2b5a8aecd0cf9d84/src/driver.rs#L124-L142)).

For milestone 2: [adding the `mirai-annotations` crate as a dependency to FRAME pallets without editing `Cargo.toml`](https://github.com/davidsemakula/pallet-verifier/blob/844a49f85f434442202f724c2b5a8aecd0cf9d84/src/main.rs#L259-L273) (see also [this](https://github.com/davidsemakula/pallet-verifier/blob/844a49f85f434442202f724c2b5a8aecd0cf9d84/src/driver.rs#L196-L254), [this](https://github.com/davidsemakula/pallet-verifier/blob/844a49f85f434442202f724c2b5a8aecd0cf9d84/src/main.rs#L180-L223) and [this](https://github.com/davidsemakula/pallet-verifier/blob/844a49f85f434442202f724c2b5a8aecd0cf9d84/src/cli_utils.rs#L128-L138)), [adding MIRAI annotations to MIR, and more specifically to support automatically adding annotations for verifying that integer `as` conversions don't overflow/underflow nor lose precision](https://github.com/davidsemakula/pallet-verifier/blob/master/src/providers/int_cast_overflow.rs).

Check out the [architecture document](https://github.com/davidsemakula/pallet-verifier/blob/master/ARCHITECTURE.md) for a detailed description of how the various components work and fit together. | **Additional Information**