formal-land · clarus · Jun 24, 2025 · May 20, 2025 · May 21, 2025 · May 21, 2025
diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml
@@ -260,6 +260,15 @@ jobs:
             rsync -rcv ./crates/stark-backend/src/ ../../CoqOfRust/openvm_stack_backend/version_v1_1_0/crates/stark_backend --include='*/' --include='*.v' --include='*.rs' --exclude='*'
             cd ../..
           endGroup
+          startGroup "Translate Pinocchio"
+            cd third-party/anza-xyz-pinocchio/sdk/pinocchio
+            cp ../../../../rust-toolchain ./
+            cargo coq-of-rust
+            touch src/lib.rs
+            cargo coq-of-rust
+            rsync -rcv ./src/ ../../../../CoqOfRust/pinocchio --include='*/' --include='*.v' --include='*.rs' --exclude='*'
+            cd ../../../..
+          endGroup
           startGroup "Generate Rocq files from Python"
             cd CoqOfRust
             make generate

diff --git a/.gitmodules b/.gitmodules
@@ -28,3 +28,6 @@
 [submodule "third-party/stark-backend"]
 	path = third-party/stark-backend
 	url = https://github.com/openvm-org/stark-backend.git
+[submodule "third-party/anza-xyz-pinocchio"]
+	path = third-party/anza-xyz-pinocchio
+	url = https://github.com/anza-xyz/pinocchio.git
diff --git a/CoqOfRust/core/links/cmp.v b/CoqOfRust/core/links/cmp.v
@@ -5,6 +5,7 @@ Require Import core.intrinsics.links.mod.
 Require Import core.links.option.
 Require Import core.ops.links.function.
 Require Export core.links.cmpOrdering.
+Require Import core.links.array.
 
 (*
 pub trait PartialEq<Rhs: ?Sized = Self> {
@@ -350,4 +351,32 @@ Module Impl_PartialEq_for_Ordering.
   Instance run : PartialEq.Run Self Self.
   Admitted.
 End Impl_PartialEq_for_Ordering.
-Export Impl_PartialEq_for_Ordering.
+
+Module Impl_PartialEq_for_U8.
+  Definition Self : Set := U8.t.
+
+  Instance run : PartialEq.Run Self Self.
+  Admitted.
+End Impl_PartialEq_for_U8.
+
+Module Impl_PartialEq_for_Array.
+  Definition Self (T U : Set) (N : Usize.t) `{Link T} `{Link U} : Set :=
+    array.t T N.
+
+  Instance run
+    (T U : Set) (N : Usize.t) `{Link T} `{Link U} `{PartialEq.Run T U}
+    : PartialEq.Run (array.t T N) (array.t U N).
+  Admitted.
+End Impl_PartialEq_for_Array.
+
+Module Impl_PartialEq_for_Ref.
+  Definition Self (A B : Set) `{Link A} `{Link B} : Set :=  
+  Ref.t Pointer.Kind.Ref A.
+
+  Instance run 
+    (A B : Set) `{Link A} `{Link B} 
+    : PartialEq.Run (Ref.t Pointer.Kind.Ref A) (Ref.t Pointer.Kind.Ref B).
+  Admitted.
+End Impl_PartialEq_for_Ref.
+
+Export Impl_PartialEq_for_Ref.
diff --git a/CoqOfRust/core/links/ptr.v b/CoqOfRust/core/links/ptr.v
@@ -0,0 +1,12 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+
+Require Import core.ptr.mod.
+Import core.ptr.mod.ptr.
+
+Definition run_write_volatile (T: Set) `{Link T} (dst: Ref.t Pointer.Kind.MutRef T) (src: T) :
+    Run.Trait
+        write_volatile [] [] [φ dst] unit.
+Proof.
+Admitted.
+
diff --git a/CoqOfRust/p_token/src/entrypoint.rs → CoqOfRust/p_token/entrypoint.rs b/CoqOfRust/p_token/src/entrypoint.rs → CoqOfRust/p_token/entrypoint.rs
diff --git a/CoqOfRust/p_token/src/entrypoint.v → CoqOfRust/p_token/entrypoint.v b/CoqOfRust/p_token/src/entrypoint.v → CoqOfRust/p_token/entrypoint.v
diff --git a/CoqOfRust/p_token/src/lib.rs → CoqOfRust/p_token/lib.rs b/CoqOfRust/p_token/src/lib.rs → CoqOfRust/p_token/lib.rs
diff --git a/...oken/src/processor/amount_to_ui_amount.rs → .../p_token/processor/amount_to_ui_amount.rs b/...oken/src/processor/amount_to_ui_amount.rs → .../p_token/processor/amount_to_ui_amount.rs
diff --git a/...token/src/processor/amount_to_ui_amount.v → ...t/p_token/processor/amount_to_ui_amount.v b/...token/src/processor/amount_to_ui_amount.v → ...t/p_token/processor/amount_to_ui_amount.v
diff --git a/CoqOfRust/p_token/src/processor/approve.rs → CoqOfRust/p_token/processor/approve.rs b/CoqOfRust/p_token/src/processor/approve.rs → CoqOfRust/p_token/processor/approve.rs
diff --git a/CoqOfRust/p_token/src/processor/approve.v → CoqOfRust/p_token/processor/approve.v b/CoqOfRust/p_token/src/processor/approve.v → CoqOfRust/p_token/processor/approve.v
diff --git a/.../p_token/src/processor/approve_checked.rs → ...Rust/p_token/processor/approve_checked.rs b/.../p_token/src/processor/approve_checked.rs → ...Rust/p_token/processor/approve_checked.rs
diff --git a/...t/p_token/src/processor/approve_checked.v → ...fRust/p_token/processor/approve_checked.v b/...t/p_token/src/processor/approve_checked.v → ...fRust/p_token/processor/approve_checked.v
diff --git a/CoqOfRust/p_token/src/processor/batch.rs → CoqOfRust/p_token/processor/batch.rs b/CoqOfRust/p_token/src/processor/batch.rs → CoqOfRust/p_token/processor/batch.rs
diff --git a/CoqOfRust/p_token/src/processor/batch.v → CoqOfRust/p_token/processor/batch.v b/CoqOfRust/p_token/src/processor/batch.v → CoqOfRust/p_token/processor/batch.v
diff --git a/CoqOfRust/p_token/src/processor/burn.rs → CoqOfRust/p_token/processor/burn.rs b/CoqOfRust/p_token/src/processor/burn.rs → CoqOfRust/p_token/processor/burn.rs
diff --git a/CoqOfRust/p_token/src/processor/burn.v → CoqOfRust/p_token/processor/burn.v b/CoqOfRust/p_token/src/processor/burn.v → CoqOfRust/p_token/processor/burn.v
diff --git a/...ust/p_token/src/processor/burn_checked.rs → CoqOfRust/p_token/processor/burn_checked.rs b/...ust/p_token/src/processor/burn_checked.rs → CoqOfRust/p_token/processor/burn_checked.rs
diff --git a/...Rust/p_token/src/processor/burn_checked.v → CoqOfRust/p_token/processor/burn_checked.v b/...Rust/p_token/src/processor/burn_checked.v → CoqOfRust/p_token/processor/burn_checked.v
diff --git a/...st/p_token/src/processor/close_account.rs → CoqOfRust/p_token/processor/close_account.rs b/...st/p_token/src/processor/close_account.rs → CoqOfRust/p_token/processor/close_account.rs
diff --git a/...ust/p_token/src/processor/close_account.v → CoqOfRust/p_token/processor/close_account.v b/...ust/p_token/src/processor/close_account.v → CoqOfRust/p_token/processor/close_account.v
diff --git a/...t/p_token/src/processor/freeze_account.rs → ...fRust/p_token/processor/freeze_account.rs b/...t/p_token/src/processor/freeze_account.rs → ...fRust/p_token/processor/freeze_account.rs
diff --git a/...st/p_token/src/processor/freeze_account.v → CoqOfRust/p_token/processor/freeze_account.v b/...st/p_token/src/processor/freeze_account.v → CoqOfRust/p_token/processor/freeze_account.v
diff --git a/...en/src/processor/get_account_data_size.rs → ..._token/processor/get_account_data_size.rs b/...en/src/processor/get_account_data_size.rs → ..._token/processor/get_account_data_size.rs
diff --git a/...ken/src/processor/get_account_data_size.v → ...p_token/processor/get_account_data_size.v b/...ken/src/processor/get_account_data_size.v → ...p_token/processor/get_account_data_size.v
diff --git a/...token/src/processor/initialize_account.rs → ...t/p_token/processor/initialize_account.rs b/...token/src/processor/initialize_account.rs → ...t/p_token/processor/initialize_account.rs
diff --git a/..._token/src/processor/initialize_account.v → ...st/p_token/processor/initialize_account.v b/..._token/src/processor/initialize_account.v → ...st/p_token/processor/initialize_account.v
diff --git a/...oken/src/processor/initialize_account2.rs → .../p_token/processor/initialize_account2.rs b/...oken/src/processor/initialize_account2.rs → .../p_token/processor/initialize_account2.rs
diff --git a/...token/src/processor/initialize_account2.v → ...t/p_token/processor/initialize_account2.v b/...token/src/processor/initialize_account2.v → ...t/p_token/processor/initialize_account2.v
diff --git a/...oken/src/processor/initialize_account3.rs → .../p_token/processor/initialize_account3.rs b/...oken/src/processor/initialize_account3.rs → .../p_token/processor/initialize_account3.rs
diff --git a/...token/src/processor/initialize_account3.v → ...t/p_token/processor/initialize_account3.v b/...token/src/processor/initialize_account3.v → ...t/p_token/processor/initialize_account3.v
diff --git a/...c/processor/initialize_immutable_owner.rs → ...n/processor/initialize_immutable_owner.rs b/...c/processor/initialize_immutable_owner.rs → ...n/processor/initialize_immutable_owner.rs
diff --git a/...rc/processor/initialize_immutable_owner.v → ...en/processor/initialize_immutable_owner.v b/...rc/processor/initialize_immutable_owner.v → ...en/processor/initialize_immutable_owner.v
diff --git a/.../p_token/src/processor/initialize_mint.rs → ...Rust/p_token/processor/initialize_mint.rs b/.../p_token/src/processor/initialize_mint.rs → ...Rust/p_token/processor/initialize_mint.rs
diff --git a/...t/p_token/src/processor/initialize_mint.v → ...fRust/p_token/processor/initialize_mint.v b/...t/p_token/src/processor/initialize_mint.v → ...fRust/p_token/processor/initialize_mint.v
diff --git a/...p_token/src/processor/initialize_mint2.rs → ...ust/p_token/processor/initialize_mint2.rs b/...p_token/src/processor/initialize_mint2.rs → ...ust/p_token/processor/initialize_mint2.rs
diff --git a/.../p_token/src/processor/initialize_mint2.v → ...Rust/p_token/processor/initialize_mint2.v b/.../p_token/src/processor/initialize_mint2.v → ...Rust/p_token/processor/initialize_mint2.v
diff --git a/...oken/src/processor/initialize_multisig.rs → .../p_token/processor/initialize_multisig.rs b/...oken/src/processor/initialize_multisig.rs → .../p_token/processor/initialize_multisig.rs
diff --git a/...token/src/processor/initialize_multisig.v → ...t/p_token/processor/initialize_multisig.v b/...token/src/processor/initialize_multisig.v → ...t/p_token/processor/initialize_multisig.v
diff --git a/...ken/src/processor/initialize_multisig2.rs → ...p_token/processor/initialize_multisig2.rs b/...ken/src/processor/initialize_multisig2.rs → ...p_token/processor/initialize_multisig2.rs
diff --git a/...oken/src/processor/initialize_multisig2.v → .../p_token/processor/initialize_multisig2.v b/...oken/src/processor/initialize_multisig2.v → .../p_token/processor/initialize_multisig2.v
diff --git a/CoqOfRust/p_token/src/processor/mint_to.rs → CoqOfRust/p_token/processor/mint_to.rs b/CoqOfRust/p_token/src/processor/mint_to.rs → CoqOfRust/p_token/processor/mint_to.rs
diff --git a/CoqOfRust/p_token/src/processor/mint_to.v → CoqOfRust/p_token/processor/mint_to.v b/CoqOfRust/p_token/src/processor/mint_to.v → CoqOfRust/p_token/processor/mint_to.v
diff --git a/.../p_token/src/processor/mint_to_checked.rs → ...Rust/p_token/processor/mint_to_checked.rs b/.../p_token/src/processor/mint_to_checked.rs → ...Rust/p_token/processor/mint_to_checked.rs
diff --git a/...t/p_token/src/processor/mint_to_checked.v → ...fRust/p_token/processor/mint_to_checked.v b/...t/p_token/src/processor/mint_to_checked.v → ...fRust/p_token/processor/mint_to_checked.v
diff --git a/CoqOfRust/p_token/src/processor/mod.rs → CoqOfRust/p_token/processor/mod.rs b/CoqOfRust/p_token/src/processor/mod.rs → CoqOfRust/p_token/processor/mod.rs
diff --git a/CoqOfRust/p_token/src/processor/mod.v → CoqOfRust/p_token/processor/mod.v b/CoqOfRust/p_token/src/processor/mod.v → CoqOfRust/p_token/processor/mod.v
diff --git a/CoqOfRust/p_token/src/processor/revoke.rs → CoqOfRust/p_token/processor/revoke.rs b/CoqOfRust/p_token/src/processor/revoke.rs → CoqOfRust/p_token/processor/revoke.rs
diff --git a/CoqOfRust/p_token/src/processor/revoke.v → CoqOfRust/p_token/processor/revoke.v b/CoqOfRust/p_token/src/processor/revoke.v → CoqOfRust/p_token/processor/revoke.v
diff --git a/...st/p_token/src/processor/set_authority.rs → CoqOfRust/p_token/processor/set_authority.rs b/...st/p_token/src/processor/set_authority.rs → CoqOfRust/p_token/processor/set_authority.rs
diff --git a/...ust/p_token/src/processor/set_authority.v → CoqOfRust/p_token/processor/set_authority.v b/...ust/p_token/src/processor/set_authority.v → CoqOfRust/p_token/processor/set_authority.v
diff --git a/...t/p_token/src/processor/shared/approve.rs → ...fRust/p_token/processor/shared/approve.rs b/...t/p_token/src/processor/shared/approve.rs → ...fRust/p_token/processor/shared/approve.rs
diff --git a/...st/p_token/src/processor/shared/approve.v → CoqOfRust/p_token/processor/shared/approve.v b/...st/p_token/src/processor/shared/approve.v → CoqOfRust/p_token/processor/shared/approve.v
diff --git a/...Rust/p_token/src/processor/shared/burn.rs → CoqOfRust/p_token/processor/shared/burn.rs b/...Rust/p_token/src/processor/shared/burn.rs → CoqOfRust/p_token/processor/shared/burn.rs
diff --git a/...fRust/p_token/src/processor/shared/burn.v → CoqOfRust/p_token/processor/shared/burn.v b/...fRust/p_token/src/processor/shared/burn.v → CoqOfRust/p_token/processor/shared/burn.v
diff --git a/...rc/processor/shared/initialize_account.rs → ...en/processor/shared/initialize_account.rs b/...rc/processor/shared/initialize_account.rs → ...en/processor/shared/initialize_account.rs
diff --git a/...src/processor/shared/initialize_account.v → ...ken/processor/shared/initialize_account.v b/...src/processor/shared/initialize_account.v → ...ken/processor/shared/initialize_account.v
diff --git a/...n/src/processor/shared/initialize_mint.rs → ...token/processor/shared/initialize_mint.rs b/...n/src/processor/shared/initialize_mint.rs → ...token/processor/shared/initialize_mint.rs
diff --git a/...en/src/processor/shared/initialize_mint.v → ..._token/processor/shared/initialize_mint.v b/...en/src/processor/shared/initialize_mint.v → ..._token/processor/shared/initialize_mint.v
diff --git a/...c/processor/shared/initialize_multisig.rs → ...n/processor/shared/initialize_multisig.rs b/...c/processor/shared/initialize_multisig.rs → ...n/processor/shared/initialize_multisig.rs
diff --git a/...rc/processor/shared/initialize_multisig.v → ...en/processor/shared/initialize_multisig.v b/...rc/processor/shared/initialize_multisig.v → ...en/processor/shared/initialize_multisig.v
diff --git a/...t/p_token/src/processor/shared/mint_to.rs → ...fRust/p_token/processor/shared/mint_to.rs b/...t/p_token/src/processor/shared/mint_to.rs → ...fRust/p_token/processor/shared/mint_to.rs
diff --git a/...st/p_token/src/processor/shared/mint_to.v → CoqOfRust/p_token/processor/shared/mint_to.v b/...st/p_token/src/processor/shared/mint_to.v → CoqOfRust/p_token/processor/shared/mint_to.v
diff --git a/...fRust/p_token/src/processor/shared/mod.rs → CoqOfRust/p_token/processor/shared/mod.rs b/...fRust/p_token/src/processor/shared/mod.rs → CoqOfRust/p_token/processor/shared/mod.rs
diff --git a/.../processor/shared/toggle_account_state.rs → .../processor/shared/toggle_account_state.rs b/.../processor/shared/toggle_account_state.rs → .../processor/shared/toggle_account_state.rs
diff --git a/...c/processor/shared/toggle_account_state.v → ...n/processor/shared/toggle_account_state.v b/...c/processor/shared/toggle_account_state.v → ...n/processor/shared/toggle_account_state.v
diff --git a/.../p_token/src/processor/shared/transfer.rs → ...Rust/p_token/processor/shared/transfer.rs b/.../p_token/src/processor/shared/transfer.rs → ...Rust/p_token/processor/shared/transfer.rs
diff --git a/...t/p_token/src/processor/shared/transfer.v → ...fRust/p_token/processor/shared/transfer.v b/...t/p_token/src/processor/shared/transfer.v → ...fRust/p_token/processor/shared/transfer.v
diff --git a/...Rust/p_token/src/processor/sync_native.rs → CoqOfRust/p_token/processor/sync_native.rs b/...Rust/p_token/src/processor/sync_native.rs → CoqOfRust/p_token/processor/sync_native.rs
diff --git a/...fRust/p_token/src/processor/sync_native.v → CoqOfRust/p_token/processor/sync_native.v b/...fRust/p_token/src/processor/sync_native.v → CoqOfRust/p_token/processor/sync_native.v
diff --git a/...ust/p_token/src/processor/thaw_account.rs → CoqOfRust/p_token/processor/thaw_account.rs b/...ust/p_token/src/processor/thaw_account.rs → CoqOfRust/p_token/processor/thaw_account.rs
diff --git a/...Rust/p_token/src/processor/thaw_account.v → CoqOfRust/p_token/processor/thaw_account.v b/...Rust/p_token/src/processor/thaw_account.v → CoqOfRust/p_token/processor/thaw_account.v
diff --git a/CoqOfRust/p_token/src/processor/transfer.rs → CoqOfRust/p_token/processor/transfer.rs b/CoqOfRust/p_token/src/processor/transfer.rs → CoqOfRust/p_token/processor/transfer.rs
diff --git a/CoqOfRust/p_token/src/processor/transfer.v → CoqOfRust/p_token/processor/transfer.v b/CoqOfRust/p_token/src/processor/transfer.v → CoqOfRust/p_token/processor/transfer.v
diff --git a/...p_token/src/processor/transfer_checked.rs → ...ust/p_token/processor/transfer_checked.rs b/...p_token/src/processor/transfer_checked.rs → ...ust/p_token/processor/transfer_checked.rs
diff --git a/.../p_token/src/processor/transfer_checked.v → ...Rust/p_token/processor/transfer_checked.v b/.../p_token/src/processor/transfer_checked.v → ...Rust/p_token/processor/transfer_checked.v
diff --git a/...oken/src/processor/ui_amount_to_amount.rs → .../p_token/processor/ui_amount_to_amount.rs b/...oken/src/processor/ui_amount_to_amount.rs → .../p_token/processor/ui_amount_to_amount.rs
diff --git a/...token/src/processor/ui_amount_to_amount.v → ...t/p_token/processor/ui_amount_to_amount.v b/...token/src/processor/ui_amount_to_amount.v → ...t/p_token/processor/ui_amount_to_amount.v
diff --git a/...src/processor/withdraw_excess_lamports.rs → ...ken/processor/withdraw_excess_lamports.rs b/...src/processor/withdraw_excess_lamports.rs → ...ken/processor/withdraw_excess_lamports.rs
diff --git a/.../src/processor/withdraw_excess_lamports.v → ...oken/processor/withdraw_excess_lamports.v b/.../src/processor/withdraw_excess_lamports.v → ...oken/processor/withdraw_excess_lamports.v