Psy ZK Circuit Journey: Tracing Proofs and Assumptions

This document provides a detailed walkthrough of the Zero-Knowledge proof lifecycle in Psy, starting from a user's local actions to the final, globally verifiable block proof. We meticulously track what each circuit proves and, critically, the assumptions it makes and how those assumptions are discharged by subsequent circuits.

Goal: Illustrate the flow of cryptographic guarantees and the progressive reduction of trust assumptions, culminating in a block proof dependent only on the previous block's established state.

Key:

• Circuit: The specific ZK circuit being executed.
• High-Level Purpose: Why this circuit exists in the overall architecture.
• Proves (Technical Detail): Specific cryptographic guarantees and state relations enforced by the circuit's constraints.
• How: Key gadgets, hashing, and constraint mechanisms employed.
• Assumes [A_]: Inputs or states treated as correct before this circuit's verification.
• Discharges [R_]: Assumptions remaining from previous steps that are verified by this circuit.
• Remaining [R_]: Assumptions still held true after this circuit's verification, passed to the next stage.

Phase 1: User Proving Session (UPS) - Local Execution

(User executes transactions and builds a local proof chain)

Step 1: Start Session

• Circuit: UPSStartSessionCircuit
• High-Level Purpose: To establish a cryptographically verified starting point for the user's transaction batch, ensuring it begins from a consistent and valid state relative to the last finalized global block. Prevents users from initiating proofs based on invalid or outdated personal states.
• Proves:
  • The provided UserProvingSessionHeader witness (ups_header) contains an internally consistent session_start_context and current_state.
  • session_start_context.checkpoint_tree_root matches the root of the verified checkpoint_tree_proof witness.
  • session_start_context.checkpoint_leaf_hash matches the value of the checkpoint_tree_proof.
  • session_start_context.checkpoint_id matches the index of the checkpoint_tree_proof.
  • The hash of the provided checkpoint_leaf witness matches session_start_context.checkpoint_leaf_hash.
  • The hash of the provided state_roots witness (global_chain_root) matches checkpoint_leaf.global_chain_root.
  • state_roots.user_tree_root matches the root of the verified user_tree_proof witness.
  • session_start_context.start_session_user_leaf.user_id matches the index of the user_tree_proof.
  • The hash of session_start_context.start_session_user_leaf matches the value of the user_tree_proof.
  • current_state.user_leaf matches session_start_context.start_session_user_leaf except last_checkpoint_id is updated to session_start_context.checkpoint_id.
  • current_state.deferred_tx_debt_tree_root == EMPTY_TREE_ROOT.
  • current_state.inline_tx_debt_tree_root == EMPTY_TREE_ROOT.
  • current_state.tx_count == 0.
  • current_state.tx_hash_stack == ZERO_HASH.
• How: UPSStartStepGadget uses MerkleProofGadgets to verify paths, Psy...Leaf/RootsGadgets to hash witnesses and check consistency, direct comparisons and constant checks. Public inputs calculated via compute_tree_aware_proof_public_inputs.
• Assumes:
  • [A1.1] The root hash used in witness Merkle proofs (checkpoint_tree_root in ups_header.session_start_context) accurately reflects the globally finalized state of the previous block.
  • [A1.4] The constant empty_ups_proof_tree_root used for the tree-aware public inputs is correct for this session's start.
  • [A1.5] The constant ups_step_circuit_whitelist_root embedded in the output header is the correct root for allowed UPS circuits.
  • (Initial correctness of witness data like proofs and leaves is assumed, then verified internally).
• Discharges: Internal consistency checks discharge assumptions about the relationships between the provided witness components (e.g., leaf data matches proof value).
• Remaining:
  • [R1.1] = [A1.1] (Correctness of previous block's CHKP root).
  • [R1.4] = [A1.4] (Correctness of session's empty_ups_proof_tree_root).
  • [R1.5] = [A1.5] (Correctness of ups_step_circuit_whitelist_root).

Step 1.5: Execute Contract Function Circuit (CFC)

• Circuit: DapenContractFunctionCircuit (Specific instance per function)
• High-Level Purpose: To execute the specific smart contract logic defined by the developer for a single transaction call, locally generating a proof that this execution instance faithfully followed the code, given its specific inputs and assumed context. This decouples logic execution from state transition verification.
• Proves:
  • The sequence of internal operations matches the compiled DPNFunctionCircuitDefinition (fn_def).
  • Given the assumed tx_ctx_header witness (containing start states like start_contract_state_tree_root, start_deferred_tx_debt_tree_root, call arguments hash/length) and circuit inputs:
    • The simulated state commands (reads/writes to CST, debt tree interactions via StateReaderGadget) produce the end_contract_state_tree_root and end_deferred_tx_debt_tree_root recorded in tx_ctx_header.transaction_end_ctx.
    • The computed outputs_hash and outputs_length match those recorded in tx_ctx_header.transaction_end_ctx.
    • All assertions within the fn_def hold true.
  • The public inputs hash (combining session_proof_tree_root and tx_ctx_header hash) is correctly computed.
• How: PsyContractFunctionBuilderGadget interprets fn_def, simulating execution using SimpleDPNBuilder and StateReaderGadget. Connects computed vs witnessed values in tx_ctx_header.
• Assumes:
  • [A1.5.1] The DapenContractFunctionCircuitInput witness (esp. tx_input_ctx) accurately reflects the state before this CFC execution (derived from the previous UPS step's output) and the correct function inputs/outputs.
  • [A1.5.3] The session_proof_tree_root witness correctly represents the root of the user's recursive proof tree at this point.
• Discharges: Internal consistency of the execution trace vs. the code definition (fn_def).
• Remaining:
  • [R1.5.1] Correctness of the assumed tx_input_ctx (start state, inputs/outputs).
  • [R1.5.3] Correctness of the assumed session_proof_tree_root.
• Output: A CFC Proof object.

Step 2: Verify CFC & Process UPS Delta

• Circuit: UPSCFCStandardTransactionCircuit
• High-Level Purpose: To integrate the result of a local CFC execution (Step 1.5) into the user's main proof chain. It verifies the CFC was executed correctly and that its claimed start/end states correctly link the previous UPS state to the next UPS state, while also proving the previous UPS step itself was valid.
• Proves:
  • Previous Step Validity: Proof N-1 was valid & used a whitelisted UPS circuit ([R(N-1).5] discharged). Public inputs match header hash.
  • CFC Validity: CFC proof (from Step 1.5) is valid & exists in the same UPS proof tree as Proof N-1 ([R1.5.3] discharged). CFC function is registered globally (GCON/CFT check linked via [R(N-1).1]).
  • Context Link: The inner public inputs hash from the verified CFC proof matches the hash of the UPSCFCStandardStateDeltaInput witness used to calculate state changes ([R1.5.1] discharged). This is the critical link ensuring the state delta matches the verified computation.
  • State Delta Correctness: The UPS header transition from step N-1 to N is valid:
    • UCON root updated correctly based on user_contract_tree_update_proof.
    • Debt tree roots updated correctly based on deferred/inline_tx_debt_pivot_proofs (starting from prev step's end state).
    • tx_count incremented; tx_hash_stack updated correctly.
• How: VerifyPreviousUPSStepProofInProofTreeGadget, UPSVerifyCFCStandardStepGadget connects cfc_inner_public_inputs_hash between UPSVerifyCFCProofExistsAndValidGadget and UPSCFCStandardStateDeltaGadget. Delta/pivot proofs verified.
• Assumes:
  • [A2.1] Witness data for this step (attestations, state delta proofs) is correct initially.
  • [R(N-1).1] (Prev Step) Last block's CHKP root correctness (used for CFC inclusion context).
  • [R(N-1).4] (Prev Step) Session's empty_ups_proof_tree_root correctness (defines proof tree base).
• Discharges: [R(N-1).5] (Prev UPS whitelist), [R1.5.1] (CFC Context), [R1.5.3] (CFC Proof Tree Root).
• Remaining:
  • [RN.1] = [R(N-1).1] (Last block's CHKP root).
  • [RN.4] = [R(N-1).4] (Session's empty_ups_proof_tree_root).
  • [RN.5] (New) Current header's ups_step_circuit_whitelist_root correctness.

(Repeat Step 1.5 & 2, or deferred variant, for all user transactions)

Step 3: End Session

• Circuit: UPSStandardEndCapCircuit
• High-Level Purpose: To securely conclude the user's local proving session, producing a single proof that attests to the validity of the entire sequence of transactions, authorized by the user's signature, and ready for network submission. It ensures the session ends in a clean state (no outstanding debts).
• Proves:
  • Last UPS step proof valid & used correct whitelisted circuit ([R_Last.5] discharged against constant known_ups_circuit_whitelist_root).
  • ZK Signature proof valid & in same proof tree ([R_Last.4] discharged).
  • Signature corresponds to user's key & authenticates PsyUserProvingSessionSignatureDataCompact derived from final UPS header state.
  • Nonce incremented correctly.
  • last_checkpoint_id updated correctly in final UserLeaf.
  • Final debt tree roots are empty.
  • (Optional) UPS proof tree aggregation used correct circuits (known_proof_tree_circuit_whitelist_root).
  • Public Outputs (end_cap_result_hash, guta_stats_hash) correctly computed.
• How: UPSEndCapFromProofTreeGadget orchestrates verification of last step & signature, UPSEndCapCoreGadget enforces final constraints. Optional VerifyAggProofGadget.
• Assumes:
  • [A3.1] Witness data correct initially.
  • [A3.2] Constant known_ups_circuit_whitelist_root.
  • [A3.3] Constant known_proof_tree_circuit_whitelist_root (if used).
  • [R_Last.1] (Last tx step) Correctness of CHKP root used as session basis.
• Discharges: [R_Last.5], [R_Last.4]. Potentially UPS tree agg assumptions.
• Remaining: [R3.1] = [R_Last.1] (Correctness of initial CHKP root).

Output of Phase 1: End Cap Proof + Public Inputs + State Deltas from user

Phase 2: Network Aggregation - Parallel Execution (Realms & Coordinators)

(The Proving Network receives End Cap proofs + state deltas from users and aggregate them to prove the change in the blockchain state root)

Step 4: Process End Cap Proof(s) (GUTA Entry - Realm)

• Circuit(s):
  • GUTAVerifySingleEndCapCircuit (Handles a single End Cap, e.g., an odd leaf in aggregation)
  • GUTAVerifyTwoEndCapCircuit (Handles pairs of End Cap proofs, typical base case)
• High-Level Purpose: To securely ingest user End Cap proofs into the GUTA process, verify their validity against the protocol and historical state, and translate them into the standard GlobalUserTreeAggregatorHeader format needed for recursive aggregation.
• Proves:
  • Input End Cap proof(s) (proof_target, child_a/b_proof) are valid ZK proofs.
  • The End Cap proof(s) were generated by the official End Cap circuit (fingerprint checked against known_end_cap_fingerprint).
  • The public inputs of the End Cap proof(s) correctly match the claimed result/stats (end_cap_result, guta_stats) provided as witness.
  • The checkpoint_tree_root claimed by the user(s) existed historically in the CHKP tree (verified via checkpoint_historical_merkle_proof).
  • (For TwoEndCap): The Nearest Common Ancestor (NCA) logic correctly combines the two individual user state transitions (start_leaf -> end_leaf at user indices) into a single state transition at their parent node in the GUSR tree. Statistics are correctly summed.
  • Outputs a GlobalUserTreeAggregatorHeader representing the state transition for the node processed (either a single user leaf or the NCA parent) and the combined stats.
• How:
  • VerifyEndCapProofGadget: Used internally (once or twice) to perform core End Cap proof verification, fingerprint check, public input matching, and historical checkpoint validation.
  • TwoNCAStateTransitionGadget (in GUTAVerifyTwoEndCapCircuit): Combines the two GUSR leaf transitions (derived from End Cap results) using an NCA proof witness.
  • GUTAStatsGadget.combine_with: Sums stats (in GUTAVerifyTwoEndCapCircuit).
  • Constructs the output GlobalUserTreeAggregatorHeader.
• Assumes:
  • [A4.1] Witness data (End Cap proof(s), results, stats, historical proofs, NCA proof if applicable) is correct initially.
  • [A4.2] Constant known_end_cap_fingerprint_hash is correct.
  • [A4.3] Public Input guta_circuit_whitelist_root_hash is correct.
  • [R3.1] (Implicit in End Cap) User session(s) based on valid past CHKP root.
• Discharges:
  • [R3.1] (via VerifyEndCapProofGadget's historical proof check).
  • Validity of the input End Cap proof(s).
• Remaining:
  • [R4.1] (New) Correctness of the current block's checkpoint_tree_root (established by checkpoint_historical_merkle_proof.current_root and passed consistently upwards).
  • [R4.3] = [A4.3] (Correctness of guta_circuit_whitelist root).

Step 5: Aggregate GUTA Proofs (Recursive - Realm/Coordinator)

• Circuit(s):
  • GUTAVerifyTwoGUTACircuit (Aggregates two GUTA sub-proofs)
  • GUTAVerifyLeftGUTARightEndCapCircuit (Aggregates GUTA sub-proof and a new End Cap proof)
  • GUTAVerifyLeftEndCapRightGUTACircuit (Aggregates an End Cap proof and a GUTA sub-proof)
• High-Level Purpose: To recursively combine verified state transitions within the GUTA hierarchy. These circuits take proofs representing changes in subtrees (either previous GUTA aggregations or newly processed End Caps) and merge them into a proof for the parent node, typically using NCA logic.
• Proves:
  • Both input proofs (Type A and Type B, where Type can be GUTA or EndCap) are valid ZK proofs.
  • Input Proof A (if GUTA) used a whitelisted GUTA circuit ([R(A).3] discharged via VerifyGUTAProofGadget).
  • Input Proof A (if EndCap) used the whitelisted EndCap circuit ([A5.EndCapFingerprint] check via VerifyEndCapProofGadget).
  • Input Proof B processed similarly ([R(B).3] or [A5.EndCapFingerprint] discharged).
  • Both input proofs' headers/results reference the same checkpoint_tree_root ([R(A).1] and [R(B).1] verified to be equal, discharging one, remaining [RN.1]).
  • Both input proofs' headers reference the same guta_circuit_whitelist root ([R(A).3] and [R(B).3] verified to be equal, discharging one, remaining [RN.3]).
  • Public inputs of each input proof match their respective headers/results.
  • The NCA logic (TwoNCAStateTransitionGadget) correctly combines the state transitions (SubTreeNodeStateTransition from input GUTA headers or derived from EndCap results) based on the NCA proof witness.
  • Statistics are correctly summed (GUTAStatsGadget.combine_with).
  • Outputs a GlobalUserTreeAggregatorHeader for the parent NCA node.
• How:
  • VerifyGUTAProofGadget (for GUTA inputs).
  • VerifyEndCapProofGadget (for EndCap inputs).
  • TwoNCAStateTransitionGadget: Core aggregation logic using NCA proof witness.
  • Connections ensuring consistency of checkpoint_tree_root and guta_circuit_whitelist between inputs.
• Assumes:
  • [A5.1] Witness data (input proofs, headers/results, whitelist proofs, NCA proof) correct initially.
  • [A5.EndCapFingerprint] Constant known_end_cap_fingerprint_hash (if applicable).
  • [R(A).1], [R(B).1] (from inputs) CHKP root correctness.
  • [R(A).3], [R(B).3] (from inputs) GUTA whitelist correctness.
• Discharges: Validity/consistency of input proofs, their whitelist usage ([R(A/B).3]), and consistency of their assumed CHKP roots ([R(A).1] confirmed equal to [R(B).1]).
• Remaining:
  • [RN.1] = [R(A).1] (Common CHKP root correctness).
  • [RN.3] = [R(A).3] (Common GUTA whitelist correctness).

Step 5.5: Propagate GUTA Proof Upwards (Line Proof)

• Circuit: GUTAVerifyGUTAToCapCircuit (May be used within Realm or by Coordinator)
• High-Level Purpose: To efficiently propagate a verified state transition from a lower node up a direct path in the tree (where no merging is needed) to a higher level (e.g., the Realm root or the global root).
• Proves:
  • The input GUTA proof is valid and used a whitelisted GUTA circuit ([R_In.3] discharged).
  • The input proof references the correct CHKP root ([R_In.1]).
  • The state transition is correctly recalculated from the input proof's node level up to the target level (e.g., level 0) using the provided top_line_siblings witness.
  • Outputs a GlobalUserTreeAggregatorHeader with the state transition reflecting the change at the target level.
• How: VerifyGUTAProofToLineGadget (uses VerifyGUTAProofGadget and GUTAHeaderLineProofGadget which uses SubTreeNodeTopLineGadget).
• Assumes:
  • [A5.5.1] Witness data (input proof, header, whitelist proof, top_line_siblings) correct initially.
  • [R_In.1], [R_In.3] (from input proof).
• Discharges: [R_In.3] (GUTA whitelist). Validity of input proof relative to [R_In.1].
• Remaining:
  • [R5.5.1] = [R_In.1] (Common CHKP root correctness).
  • [R5.5.3] = [R_In.3] (Common GUTA whitelist correctness).

(Steps 5/5.5 repeat recursively until Realm roots are reached)

Step 5.N: Handle No GUTA Changes

• Circuit: GUTANoChangeCircuit
• High-Level Purpose: To allow the aggregation process to incorporate the latest checkpoint root even if no user activity (relevant to GUTA) occurred in a particular block or subtree. Maintains checkpoint consistency across the aggregation structure.
• Proves:
  • A specific checkpoint_leaf exists in the checkpoint_tree at the previous checkpoint_id.
  • The GUSR root remained unchanged between the previous and current checkpoint (new_guta_header.state_transition shows old_node_value == new_node_value at level 0).
  • Statistics are zero.
  • Outputs a GlobalUserTreeAggregatorHeader referencing the current checkpoint_tree_root but indicating no GUSR change.
• How: GUTANoChangeGadget (uses MerkleProofGadget for checkpoint proof, constructs no-op transition).
• Assumes:
  • [A5.N.1] Witness data correct initially.
  • [A5.N.3] Public Input guta_circuit_whitelist root is correct.
• Discharges: Internal consistency of checkpoint proof/leaf.
• Remaining:
  • [R5.N.1] (New) Correctness of the current checkpoint_tree_root (from the witness proof).
  • [R5.N.3] = [A5.N.3] (GUTA whitelist correctness).

Output of Phase 2: Aggregated GUTA proof(s) from each active Realm (or a NoChange proof), valid relative to [R_Realm.1] and [R_Realm.3].

Phase 3: Coordinator Level Aggregation - Network Execution

(Coordinator combines proofs from Realms and global tree updates)

Step 6: Process User Registrations

• Circuit: BatchAppendUserRegistrationTreeCircuit
• Proves: Correct batch append to URT (output root valid given input root [A6.3]). Respects register_users_circuit_whitelist ([A6.2]).
• Assumes: [A6.x] (Witness, whitelist, input URT root).
• Discharges: Internal append proof consistency.
• Remaining: [R6.2] (Whitelist), [R6.3] (Input URT root correctness).

Step 7: Process Contract Deployments

• Circuit: BatchDeployContractsCircuit
• Proves: Correct batch append to GCON (output root valid given input root [A7.3]). Witness leaves match hashes. Respects deploy_contract_circuit_whitelist ([A7.2]).
• How: BatchDeployContractsGadget.
• Assumes: [A7.x] (Witness, whitelist, input GCON root).
• Discharges: Internal append/leaf consistency.
• Remaining: [R7.2] (Whitelist), [R7.3] (Input GCON root correctness).

Step 8: Aggregate Part 1 (Combine UserReg + Deploy + GUTA)

• Circuit: VerifyAggUserRegistartionDeployContractsGUTACircuit
• Proves: Input proofs (Agg UserReg, Agg Deploy, Agg GUTA) valid & used respective whitelisted circuits ([R6.2], [R7.2], [R_GUTA.3] discharged). All inputs based on same CHKP root ([R_GUTA.1] verified across inputs). Output header correctly combines state transitions.
• How: VerifyAggUserRegistartionDeployContractsGUTAGadget.
• Assumes:
  • [A8.1] Witness data correct initially.
  • [R_GUTA.1] (Implicit common CHKP root from inputs).
  • [R6.3] (Input URT root correctness).
  • [R7.3] (Input GCON root correctness).
• Discharges: Whitelists ([R6.2], [R7.2], [R_GUTA.3]). Input proof validity. Consistency of CHKP root [R_GUTA.1].
• Remaining:
  • [R8.1] = [R_GUTA.1] (CHKP root correctness).
  • [R8.3] = [R6.3] (Input URT root correctness).
  • [R8.4] = [R7.3] (Input GCON root correctness).

Output of Phase 3: Single "Part 1" proof, valid relative to [R8.1], [R8.3], [R8.4].

Phase 4: Final Block Proof - Network Execution

Step 9: Final Block Transition

• Circuit: PsyCheckpointStateTransitionCircuit
• High-Level Purpose: To generate the definitive proof for the block, verifying all aggregated work and cryptographically linking the block to its predecessor, thereby discharging all temporary assumptions made during parallel processing.
• Proves:
  • Part 1 Agg proof (Step 8) valid & used correct circuit.
  • New CHKP Leaf computed correctly from Part 1 outputs (new global roots for URT ([R8.3] discharged), GCON ([R8.4] discharged), GUSR), stats, time, randomness.
  • CHKP tree append operation correct, transitioning from previous_checkpoint_proof.root ([R8.1]) to new_checkpoint_tree_root.
  • Final Chain Link: previous_checkpoint_proof.root matches the Public Input previous_block_chkp_root.
• How: CheckpointStateTransitionChildProofsGadget, CheckpointStateTransitionCoreGadget.
• Assumes:
  • [A9.1] Witness data correct initially.
  • [A9.2] Public Input previous_block_chkp_root == previous block's finalized CHKP root.
• Discharges: [R8.1] (CHKP root correctness discharged against public input [A9.2]). [R8.3] (URT root correctness), [R8.4] (GCON root correctness) implicitly discharged by relying on the verified Part 1 proof output.
• Remaining Assumptions: None.

Output: Final Block Proof. Its verification confirms the entire block's state transition is valid, contingent only on the validity of the previous block's state hash ([A9.2]) and ZKP soundness.

Psy: Horizontally Scalable Blockchain via PARTH and ZK Proofs

Introduction: The Serial Bottleneck

Traditional blockchains suffer from a serial execution bottleneck. They process transactions sequentially within a single state machine, meaning adding more nodes doesn't increase overall throughput (TPS). Parallel execution attempts often lead to race conditions and inconsistencies. Psy overcomes this fundamental limitation with its novel PARTH architecture and end-to-end Zero-Knowledge Proof (ZKP) system.

The PARTH Architecture: Foundation for Parallelism

PARTH (Parallelizable Account-based Recursive Transaction History) redefines blockchain state organization:

1. Granular State: Instead of one global state tree, Psy maintains a hierarchy of Merkle trees, most notably:

   • Per-User, Per-Contract State (CSTATE): Each user has a separate Merkle tree (CSTATE) representing their specific state within each smart contract they interact with.
   • User Contract Tree (UCON): Aggregates all CSTATE roots for a single user, representing their overall state across all contracts.
   • Global User Tree (GUSR): Aggregates all UCON roots, representing the state of all users.
   • Global Contract Tree (GCON): Represents the global state related to contract code/definitions.
   • Checkpoint Tree (CHKP): The top-level tree whose root hash represents a verifiable snapshot of the entire blockchain state at a given block.

2. Controlled Interaction Rules (Key to Scalability):

   • Write Locally: A transaction initiated by a user can only modify (write to) the state within that specific user's own trees (primarily their CSTATE and UCON trees).
   • Read Globally (Previous State): A transaction can read the state from any other user's trees (or global trees like GCON), but critically, it only sees the state as it was finalized at the end of the previous block.

3. Enabling Parallelism: Because write operations are isolated to the sender's state trees, and read operations access the immutable, finalized state of the last block, transactions from different users within the same block operate independently. They cannot conflict or cause race conditions. This independence is the architectural breakthrough that allows for massive parallel processing.

The End-to-End ZK Proof Process: Securing Parallelism

Psy uses a sophisticated system of ZK circuits and recursive proofs to verify all state transitions securely, even when processed in parallel.

Step 1: Local Transaction Execution & Proving (User Level)

• Action: A user interacts with a dApp, triggering one or more smart contract function calls.
• Execution: The logic defined in the specific Contract Function Circuit (CFC) associated with the smart contract is executed locally (or by a delegated prover).
• State Update: This execution modifies the user's CSTATE tree for that contract. The Merkle root of the user's UCON tree is also updated to reflect this change.
• Proof Generation: The user generates ZK proofs using User Proving Session (UPS) circuits. These proofs attest that:
  • The contract logic (CFC) was executed correctly.
  • The user's CSTATE and UCON trees transitioned correctly from a known previous state root to a new state root.
  • Assumptions: These proofs rely on public inputs that declare assumptions about the state of the blockchain before the transaction (e.g., the user's previous UCON root, the relevant GCON root, and crucially, the CHKP root of the last finalized block which guarantees the validity of any global state read).
• Recursion: If the user performs multiple actions, recursive proofs compress them into a single proof representing the net state change for that user within the block.

Step 2: Parallel Proof Aggregation (Decentralized Proving Network + Realms)

• Submission: Users submit their final proofs and delta merkle proofs (representing their state transitions for the block) to their corresponding realm node on the Psy network. (see handle_recv_end_cap_from_user)
• Parallel Processing: Thanks to the PARTH architecture ensuring user-transaction independence, the Decentralized Proving Network can take proofs from thousands or millions of users and begin verifying and aggregating them in parallel. Realms are in charge of sending the proofs to the queue to be aggregated by the proof workers
• Once all the update proofs are aggregated in a realm into a single proof, the realm sends that proof off to the block coordinator to be aggregated into a single proof of all realm updates at the end of the block.
• Hierarchical Aggregation: Specialized Aggregation Circuits (e.g., for aggregating user contract trees, or global user trees) recursively verify batches of proofs from the layer below within the PARTH structure.
  • Each aggregation circuit checks the validity of the input proofs it receives.
  • It enforces the assumptions declared in the public inputs of the lower-level proofs. For example, a circuit aggregating user states ensures all input proofs correctly referenced the same previous global user state root.
  • It outputs a single, smaller proof representing the validity of the entire batch it processed.

Step 3: Final Block Proof Generation (Consensus / Block Leader)

• Final Aggregation: The parallel aggregation process continues up the hierarchy, culminating in the Checkpoint Tree "Block" Circuit. This final circuit aggregates proofs from the top-level trees (like GUSR, GCON).
• Inductive Verification: Assumptions made by lower circuits are checked and discharged by higher circuits during the recursive process. By the time execution reaches the final "Block" circuit, the only remaining external assumption is the root hash of the previous block's Checkpoint Tree (CHKP root).
• Trustless Link: This final circuit verifies this previous CHKP root against the public input provided (which is the known, finalized root from the preceding block). This check creates a cryptographic, trustless link between consecutive blocks.
• Proof Singularity: The output is a single, succinct ZK proof for the entire block, proving the validity of all transactions and the overall state transition from the previous CHKP root to the new CHKP root, without needing to reveal individual transaction details or re-execute anything.

Step 4: Verification and Finalization

• The final block proof is broadcast and verified by consensus nodes (or potentially bridge contracts on other L1s).
• Verification is extremely fast as it only involves checking the single ZK proof and the link to the previous block's state.
• Once verified, the new CHKP root becomes the finalized, canonical state snapshot for that block.

The Role of the Checkpoint Tree (CHKP) and Circuits

• Global State Snapshot (CHKP): The CHKP root acts as a universal anchor. It captures a full snapshot of the entire chain and allows anyone to efficiently verify any piece of state information (user balance, contract variable, etc.) from any block by providing a Merkle proof linking that data back to the validated CHKP root of that block.
• Circuit Enforcement: Each tree update within the PARTH structure is strictly controlled. Updates are only permitted if accompanied by a valid ZK proof generated by a pre-approved, whitelisted circuit designed for that specific tree transition. This constraint, enforced by the aggregation circuits above, ensures state changes adhere precisely to the defined rules (contract logic, protocol rules).

Conclusion: Achieving Horizontal Scalability

Psy achieves true horizontal scalability through the synergy of:

1. PARTH Architecture: Its granular state and specific read/write rules eliminate conflicts between transactions from different users within a block.
2. Parallel Proving: This independence allows the computationally intensive task of ZK proof generation and aggregation to be massively parallelized across the Decentralized Proving Network.
3. Recursive ZK Proofs: Efficiently compress and verify vast amounts of computation and state changes into a single, easily verifiable proof for each block, secured by the inductive verification up to the final Block Circuit linking to the previous state.

By processing user transactions independently and in parallel, secured by end-to-end ZK verification, Psy breaks the serial bottleneck and offers a path to blockchain performance potentially orders of magnitude higher than traditional architectures, truly scaling horizontally as more proving resources are added.

Key terms: DPN - Dapen, the code name for the Psy rust smart contract language UPS - User Proving Session, the process by which users prove transactions locally and generate the delta merkle proofs to be sent off to chain End Cap - The last recursive proof which checks the signature and state deltas for a user GUTA - Global User Tree Aggregation

The Psy User Proving Session (UPS) Proof Tree: Efficient Recursive Verification

1. Introduction: The Challenge of Recursive Verification Costs

The User Proving Session (UPS) relies on recursive ZK proofs, where each step cryptographically verifies the previous one. A naive approach might involve embedding the entire verification logic of the previous step's circuit inside the current step's circuit. However, this leads to several problems:

1. Variable Circuit Complexity: Different UPS steps might verify different underlying circuits (standard CFC, deferred CFC, start session), each with varying verification costs. This makes creating fixed-size, efficient recursive circuits difficult.
2. Computational Bloat: Repeatedly verifying complex proofs within recursion significantly increases the computational cost and proving time for each step.
3. Limited Parallelism: Tightly coupling verification logic hinders the potential to parallelize the proving work, even if the witness generation is serial.

The UPS Proof Tree architecture elegantly solves these issues by deferring the direct verification cost and replacing it with cheap cryptographic commitments and existence checks.

2. The UPS Proof Tree: Commit, Don't Verify (Yet)

2.1 Core Concept: A Merkle Tree of Proof Commitments

Instead of fully verifying the previous proof within the current step's circuit, the UPS system commits each generated proof to a Merkle tree specific to the session.

• Leaf Content: Each leaf i stores a hash committing to the proof's identity and context:

  • Standard Proofs (like ZK Signature): LeafValue_i = Hash(ProofFingerprint_i, PublicInputsHash_i)
  • Tree-Aware Proofs (UPS Steps): LeafValue_i = Hash(ProofFingerprint_i, TreeAwarePublicInputsHash_i)
    • Where TreeAwarePublicInputsHash_i = Hash(ProofTreeRoot_i-1, InnerPublicInputsHash_i)

• Append-Only Construction: As each proof (CFC execution proof, UPS step proof, signature proof) is generated locally, its corresponding LeafValue is computed and appended to the tree. The tree root updates with each addition.

2.2 Cheap In-Circuit Checks: Attesting Existence and Linkage

The core innovation lies in using specialized gadgets instead of full verifiers within the recursive steps:

• Gadget 1: AttestProofInTreeGadget (For non-tree-aware proofs like Signatures)

  • Function: Proves that a commitment Hash(Fingerprint, PublicInputsHash) exists as a leaf within a tree identified by AttestedProofTreeRoot.
  • Mechanism: Takes Fingerprint, PublicInputsHash, and a Merkle inclusion_proof witness. Computes the expected leaf hash and verifies the Merkle proof against it.
  • Cost: Primarily the cost of Merkle proof verification (logarithmic hashing) and a few hashes/comparisons – significantly cheaper than verifying the actual ZK proof.
  • Assumption: The ZK proof corresponding to the Fingerprint and PublicInputsHash is itself valid. This gadget only proves commitment existence.

• Gadget 2: AttestTreeAwareProofInTreeGadget (For tree-aware UPS step proofs)

  • Function: Proves that a commitment for a tree-aware proof exists in the tree, linking it to the correct historical state of the tree.
  • Mechanism: Takes Fingerprint, InnerPublicInputsHash, an inclusion_proof (in the current tree), and a historical_root_proof (pivot proof showing Root_N-2 -> Root_N-1). It computes the expected tree-aware leaf hash Hash(Fingerprint, Hash(Root_N-1, InnerPublicInputsHash)) and verifies the inclusion_proof against it and the current root. It also verifies the historical_root_proof.
  • Cost: Cost of two Merkle proof verifications (inclusion and historical pivot) plus hashing/comparisons – still much cheaper than full ZK proof verification.
  • Assumption: The ZK proof corresponding to the Fingerprint and InnerPublicInputsHash (relative to Root_N-1) is itself valid.

2.3 How Recursion Works with the Tree: Deferral in Action

Consider UPS Step N verifying Step N-1:

1. Step N-1 Runs: Generates its ZK proof (Proof_N-1) and computes its tree-aware public inputs hash TAPH_N-1 = Hash(Root_N-2, InnerPubHash_N-1). Its commitment LeafValue_N-1 = Hash(Fingerprint_N-1, TAPH_N-1) is added to the tree, updating the root to Root_N-1.
2. Step N Circuit Runs:
   • Does NOT Verify Proof_N-1 directly.
   • Instead, it uses AttestTreeAwareProofInTreeGadget.
   • Assumes: The Proof_N-1 (whose commitment is being checked) is valid.
   • Takes Witness: Fingerprint_N-1, InnerPubHash_N-1, inclusion_proof (for Leaf N-1 in tree N-1), historical_root_proof (Root N-2 -> Root N-1).
   • Verifies: That the commitment to Proof_N-1 exists correctly linked to Root_N-2 within the tree state Root_N-1. This cryptographically confirms the sequential link.
   • Computes: Its own output header hash InnerPubHash_N.
   • Generates: Its own ZK proof (Proof_N) whose public inputs commit to Hash(Root_N-1, InnerPubHash_N).

Crucially, the circuit for Step N has a fixed, relatively low complexity, dominated by the Merkle proof gadgets, regardless of the complexity of the circuit used for Step N-1. It only deals with commitments to proofs, not the proofs themselves.

3. Discharging the Assumptions: The End Cap and Beyond

Throughout the UPS, the core assumption accumulates: "All ZK proofs committed to the tree are valid."

• The End Cap's Role: The UPSStandardEndCapCircuit is where this primary assumption begins to be addressed for the UPS internal proofs.

  • It verifies the last UPS step proof's commitment using AttestTreeAwareProofInTreeGadget.
  • It verifies the ZK Signature proof's commitment using AttestProofInTreeGadget.
  • It ensures both verifications reference the same final proof tree root, linking the signature to the end state of the transaction sequence.
  • Optional (but recommended): It often includes a VerifyAggProofGadget (or VerifyAggRootGadget). This gadget takes a ZK proof (generated outside the UPS circuit) that recursively verifies all the actual proofs committed to the UPS Proof Tree. This aggregation proof essentially proves the core assumption: "All proofs committed to the tree with root FinalRoot are valid". By verifying this single aggregation proof, the End Cap circuit discharges the validity assumption for all internal UPS steps.

• Deferred Verification: The actual computationally expensive work of verifying all the individual UPS step proofs and the signature proof is bundled into generating the separate UPS Proof Tree aggregation proof. This aggregation can happen:

  • Locally: After witness generation but before End Cap proving.
  • Remotely/Parallel: In a future design, the witness data and tree commitments could be sent to parallel provers. They generate proofs for each step and the final aggregation proof. The End Cap circuit then only needs to verify the single aggregation proof.

4. Benefits Summary

1. Constant Recursive Step Cost: The cost of verifying the previous step inside the current step's circuit is fixed and low (Merkle checks), independent of the previous step's circuit complexity. This allows for efficient recursion with consistent circuit degrees.
2. Deferral of Computation: The heavy lifting of verifying the actual ZK proofs is pushed out of the main recursive path and consolidated into a single (optional but recommended) aggregation proof verified at the end.
3. Enables Parallel Proving: By using the tree commitments as interfaces, the proving of individual UPS steps (and the final tree aggregation) can be parallelized across multiple workers, even if witness generation is serial. Workers only need the relevant witnesses and the expected tree roots/proofs to verify their step's link, without needing to run the entire previous circuit's verification logic.
4. Architectural Flexibility: The system clearly separates committing to a proof's existence/context from verifying the proof's internal validity, allowing different strategies for when and how the full verification occurs.

In essence, the UPS Proof Tree acts as a highly efficient cryptographic ledger within the proving session, allowing circuits to cheaply attest to the existence and sequential linkage of prior computational steps, while deferring the bulk verification cost to a final, potentially parallelizable, aggregation step.

Psy Architecture: Horizontally Scalable Blockchain via PARTH and ZK Proofs

1. Introduction: Beyond Sequential Limits

The evolution of blockchain technology has been marked by a persistent challenge: scalability. Traditional designs, processing transactions sequentially within a monolithic state machine, hit a throughput ceiling that cannot be overcome simply by adding more network nodes. Psy represents a fundamental leap forward, tackling this bottleneck through a revolutionary state architecture known as PARTH and a meticulously designed, end-to-end Zero-Knowledge Proof (ZKP) system. This architecture unlocks true horizontal scalability, enabling unprecedented transaction processing capacity while maintaining rigorous cryptographic security.

2. The PARTH Architecture: A Foundation for Parallelism

PARTH (Parallelizable Account-based Recursive Transaction History) dismantles the concept of a single, conflict-prone global state. Instead, it establishes a granular, hierarchical structure where state modifications are naturally isolated, paving the way for massive parallel processing.

2.1 The Hierarchical State Forest

Psy's state is not a single tree, but a "forest" of interconnected Merkle trees, each with a specific domain:

graph TD
    subgraph "Global State Snapshot (Block N)"
        CHKP(CHKP Root);
    end

    subgraph "Global Trees (Referenced by CHKP)"
      GUSR(GUSR Root);
      GCON(GCON Root);
      URT(URT Root);
      GDT(GDT Root);
      GWT(GWT Root);
      STATS(Block Stats Hash);
    end

    subgraph "User-Specific Trees (Leaf in GUSR)"
      ULEAF{User Leaf};
      UCON(UCON Root);
    end

    subgraph "Contract Definition (Leaf in GCON)"
       CLEAF{Contract Leaf};
       CFT(CFT Root);
    end

    subgraph "User+Contract Specific State (Leaf in UCON)"
      CST(CSTATE Root);
    end

    CHKP --> GUSR;
    CHKP --> GCON;
    CHKP --> URT;
    CHKP --> GDT;
    CHKP --> GWT;
    CHKP --> STATS;

    GUSR -- User ID --> ULEAF;
    ULEAF -- Contains --> UCON;
    ULEAF -- Contains --> UserMetadata[PK Hash, Bal, Nonce, etc.];

    GCON -- Contract ID --> CLEAF;
    CLEAF -- Contains --> CFT;
    CLEAF -- Contains --> ContractMetadata[Deployer Hash, CST Height];

    UCON -- Contract ID --> CST;
    CFT -- Function ID --> FuncFingerprint{Function Fingerprint};

    style CHKP fill:#f9f,stroke:#333,stroke-width:2px,font-weight:bold
    style GUSR fill:#ccf,stroke:#333,stroke-width:1px
    style GCON fill:#cfc,stroke:#333,stroke-width:1px
    style URT fill:#fec,stroke:#333,stroke-width:1px
    style ULEAF fill:#fcc,stroke:#333,stroke-width:1px,font-style:italic
    style CLEAF fill:#fcc,stroke:#333,stroke-width:1px,font-style:italic
    style UCON fill:#cff,stroke:#333,stroke-width:1px
    style CST fill:#ffc,stroke:#333,stroke-width:1px
    style CFT fill:#eef,stroke:#333,stroke-width:1px

• CHKP (Checkpoint Tree): The ultimate source of truth for a given block. Its root immutably represents the entire state snapshot, committing to the roots of all major global trees and block statistics. Verifying the CHKP root transitively verifies the entire state.
• GUSR (Global User Tree): Aggregates all registered users. Each leaf (ULEAF) corresponds to a user ID and contains their public key commitment, balance, nonce, last synchronized checkpoint ID, and, crucially, the root of their personal UCON tree.
• UCON (User Contract Tree): A per-user tree mapping Contract IDs to the roots of the user's corresponding CSTATE trees. This tree represents the user's state footprint across all contracts they've interacted with.
• CSTATE (Contract State Tree): The most granular level. This tree is specific to a single user AND a single contract. It holds the actual state variables (storage slots) pertinent to that user within that contract. This is where smart contract logic primarily operates.
• GCON (Global Contract Tree): Stores global information about deployed contracts via CLEAF nodes (Contract Leaf).
• CLEAF (Contract Leaf): Contains the deployer's identifier hash, the root of the contract's Function Tree (CFT), and the required height (size) for its associated CSTATE trees.
• CFT (Contract Function Tree): Per-contract tree whitelisting executable functions. Maps Function IDs to the ZK circuit fingerprint of the corresponding DapenContractFunctionCircuit, ensuring only verified code can be invoked.
• URT (User Registration Tree): Commits to user public keys during the registration process, ensuring uniqueness and linking registrations to cryptographic identities.
• Other Trees: Dedicated global trees handle deposits (GDT), withdrawals (GWT), event data (EDATA - conceptually), etc.

2.2 PARTH Interaction Rules: Enabling Concurrency

The genius of PARTH lies in its strict state access rules:

1. Localized Writes: A transaction initiated by User A can only modify state within User A's own trees. This typically involves changes within one or more of User A's CSTATE trees, which then requires updating the corresponding leaves in User A's UCON tree, ultimately updating User A's ULEAF in the GUSR. Crucially, User A cannot directly alter User B's CSTATE, UCON, or ULEAF.
2. Historical Global Reads: A transaction can read any state from the blockchain (e.g., User B's balance stored in their ULEAF, a variable in User B's CSTATE via User B's UCON root, or global contract data from GCON). However, these reads always access the state as it was finalized in the previous block's CHKP root. The current block's ongoing, parallel state changes are invisible to concurrent transactions.

2.3 The Scalability Breakthrough: Conflict-Free Parallelism

These rules eliminate the core bottleneck of traditional blockchains:

• No Write Conflicts: Since users only write to their isolated state partitions, transactions from different users within the same block cannot conflict.
• No Read-Write Conflicts: Reading only the previous, immutable block state prevents race conditions where one transaction's read is invalidated by another's concurrent write.
• Massively Parallel Execution & Proving: The PARTH architecture guarantees that the execution of transactions (CFCs) and the generation of their initial proofs (UPS) for different users are independent processes that can run entirely in parallel without requiring locks or complex synchronization.

3. End-to-End ZK Proof System: Securing Parallelism

Psy employs a multi-layered, recursive ZK proof system to cryptographically guarantee the integrity of every state transition, even those occurring concurrently.

3.1 Contract Function Circuits (CFCs) & Dapen (DPN)

• Role: Encapsulate the verifiable logic of smart contracts. They define the allowed state transitions within a user's CSTATE for that contract.
• Technology: Developed using high-level languages (TypeScript/JavaScript) and compiled into ZK circuits (DapenContractFunctionCircuit) via the Dapen (DPN) toolchain.
• Execution: run locally during a User Proving Session (UPS). A ZK proof is generated for each CFC execution, attesting that the logic was followed correctly given the inputs and starting state provided in its context.

3.2 User Proving Session (UPS)

• Role: Enables users (or their delegates) to locally process a sequence of their transactions for a block, generating a single, compact "End Cap" proof that summarizes and validates their entire session activity.
• Process:
  1. Initialization (UPSStartSessionCircuit): Securely anchors the session's starting state to the last globally finalized CHKP root and the user's corresponding ULEAF.
  2. Transaction Steps (UPSCFCStandardTransactionCircuit, etc.): For each transaction:
     • Verifies the ZK proof of the locally executed CFC (from step 3.1).
     • Verifies the ZK proof of the previous UPS step (ensuring recursive integrity).
     • Proves that the UPS state delta (changes to UCON root, debt trees, tx count/stack) correctly reflects the verified CFC's outcomes.
  3. Finalization (UPSStandardEndCapCircuit): Verifies the last UPS step, verifies the user's ZK signature authorizing the session, checks final conditions (e.g., all debts cleared), and outputs the net state change (start_user_leaf_hash -> end_user_leaf_hash) and aggregated statistics (GUTAStats).
• Scalability Impact: Drastically reduces the on-chain verification burden. Instead of verifying every transaction individually, the network only needs to verify one aggregate End Cap proof per active user per block.

3.3 Network Aggregation (Realms, Coordinators, GUTA)

The network takes potentially millions of End Cap proofs and efficiently aggregates them in parallel using a hierarchy of specialized ZK circuits.

• Realms:

  • Role: Distributed ingestion and initial aggregation points for user state changes (GUSR), sharded by user ID ranges.
  • Function:
    1. Receive End Cap proofs from users within their range.
    2. Verify these proofs using circuits like GUTAVerifySingleEndCapCircuit (for individual proofs) or GUTAVerifyTwoEndCapCircuit (for pairs). These circuits use the VerifyEndCapProofGadget internally to check the End Cap proof validity, fingerprint, and historical checkpoint link, outputting a standardized GlobalUserTreeAggregatorHeader.
    3. Recursively aggregate the resulting GUTA headers using circuits like GUTAVerifyTwoGUTACircuit, GUTAVerifyLeftGUTARightEndCapCircuit, or GUTAVerifyLeftEndCapRightGUTACircuit. These employ VerifyGUTAProofGadget to check sub-proofs and TwoNCAStateTransitionGadget (or line proof logic) to combine state transitions.
    4. If necessary, use GUTAVerifyGUTAToCapCircuit (which uses VerifyGUTAProofToLineGadget) to bring a proof up to the Realm's root level.
    5. Handle periods of inactivity using GUTANoChangeCircuit.
    6. Submit the final aggregated GUTA proof for their user segment (representing the net change at the Realm's root node in GUSR) to the Coordinator layer.
  • Scalability Impact: Distributes the initial proof verification and GUSR aggregation load.

• Coordinators:

  • Role: Higher-level aggregators combining proofs across Realms and across different global state trees.
  • Function:
    1. Verify aggregated GUTA proofs from multiple Realms (using GUTAVerifyTwoGUTACircuit or similar, employing VerifyGUTAProofGadget).
    2. Verify proofs for global operations:
       • User Registrations (BatchAppendUserRegistrationTreeCircuit).
       • Contract Deployments (BatchDeployContractsCircuit).
    3. Combine these different types of state transitions using aggregation circuits like VerifyAggUserRegistartionDeployContractsGUTACircuit, ensuring consistency relative to the same checkpoint.
    4. Prepare the final inputs for the block proof circuit (PsyCheckpointStateTransitionCircuit).
  • Scalability Impact: Manages the convergence of parallel proof streams from different state components and realms.

• Proving Workers:

  • Role: The distributed computational workforce of the network. They execute the intensive ZK proof generation tasks requested by Realms and Coordinators.
  • Function: Stateless workers that fetch proving jobs (circuit type, input witness ID, dependency proof IDs) from a queue, retrieve necessary data from the Node State Store, generate the required ZK proof, and write the result back to the store.
  • Scalability Impact: The core engine of computational scalability. The network's proving capacity can be scaled horizontally simply by adding more (potentially permissionless) Proving Workers.

3.4 Final Block Proof Generation

• Role: Creates the single, authoritative ZK proof for the entire block.
• Circuit: PsyCheckpointStateTransitionCircuit.
• Function: Takes the final aggregated state transition proofs from the Coordinator layer (representing net changes to GUSR, GCON, URT, etc.). Verifies these proofs. Computes the new global state roots and combines them with aggregated block statistics (PsyCheckpointLeafStats) to form the new PsyCheckpointLeaf. Proves the correct update of the CHKP tree by appending this new leaf hash. Critically, it verifies that the entire process correctly transitioned from the state defined by the previous block's finalized CHKP root (provided as a public input).
• Output: A highly succinct ZK proof whose public inputs are the previous CHKP root and the new CHKP root.

4. Node State Architecture: Redis & KVQ Backend

Supporting this massive parallelism requires a high-performance, shared backend infrastructure.

• Core Technology: Psy leverages Redis, a distributed in-memory key-value store known for its speed and scalability, as the primary backend. Redis Clusters allow horizontal scaling of storage and throughput.
• Abstraction Layer (KVQ): A custom Rust library providing traits and adapters (KVQSerializable, KVQStandardAdapter, model types like KVQFixedConfigMerkleTreeModel) for structured, type-safe interaction with Redis. It simplifies key generation, serialization, and potentially caching.
• Logical Components:
  • Proof Store (ProofStoreFred, implements QProofStore... traits): Stores ZK proofs and input witnesses, keyed by QProvingJobDataID. Uses Redis Hashes (HSET, HGET) and potentially atomic counters (HINCRBY) for managing job dependencies.
  • State Store (Models implementing PsyCoordinatorStore..., PsyRealmStore... traits): Stores the canonical blockchain state, primarily Merkle tree nodes (KVQMerkleNodeKey) and leaf data (UserLeaf, ContractLeaf, etc.). Uses standard Redis keys managed via KVQ models.
  • Queues (CheckpointDrainQueue, CheckpointHistoryQueue, WorkerEventQueue traits): Implement messaging between components. Uses Redis Lists (LPUSH, LPOP/BLPOP, LRANGE) for job queues and potentially Pub/Sub or simple keys/sorted sets for history tracking and notifications. ProofStoreFred often implements these queue interaction traits.
  • Local Caching (PsyCmdStoreWithCache, used within PsyLocalProvingSessionStore): Provides an in-memory cache layer for frequently accessed state data (e.g., contract definitions, user leaves from the previous block) during local UPS execution or within Realm/Coordinator nodes, reducing load on the central Redis cluster.
• Scalability:
  • Redis Performance: Provides low-latency access required for coordinating many workers.
  • Horizontal Scaling: Redis clusters can scale to handle increased load.
  • Concurrency: Redis handles concurrent connections from numerous DPN nodes.
  • Decoupling: Proving computation (Workers) is separated from state storage and coordination (Redis + Control Nodes), allowing independent scaling.

graph TB
    %% External Network
    Internet[🌐 Internet] --> IGW[Internet Gateway]
    
    %% VPC Container
    subgraph VPC["🏢 VPC (10.0.0.0/16)"]
        IGW --> ALB[🔀 Application Load Balancer<br/>Ports: 8545, 8546, 8547]
        
        %% Availability Zone A
        subgraph AZ1["🏛️ Availability Zone A"]
            subgraph PubSub1["🌍 Public Subnet 1<br/>(10.0.0.0/24)"]
                ALB
            end
            
            subgraph PrivSub1["🔒 Private Subnet 1<br/>(10.0.2.0/24)"]
                ECS_Coord[🐳 ECS Task<br/>Coordinator]
                ECS_R0[🐳 ECS Task<br/>Realm 0]
                ECS_R1[🐳 ECS Task<br/>Realm 1]
                
                Redis_Coord[🔴 Redis<br/>Coordinator]
                Redis_R0[🔴 Redis<br/>Realm 0]
                Redis_R1[🔴 Redis<br/>Realm 1]
                
                EFS_Mount1[📁 EFS Mount Target 1]
            end
        end
        
        %% Availability Zone B
        subgraph AZ2["🏛️ Availability Zone B"]
            subgraph PubSub2["🌍 Public Subnet 2<br/>(10.0.1.0/24)"]
                ALB_HA[🔀 ALB HA Deployment]
            end
            
            subgraph PrivSub2["🔒 Private Subnet 2<br/>(10.0.3.0/24)"]
                EFS_Mount2[📁 EFS Mount Target 2]
            end
        end
        
        ALB -.-> ALB_HA
    end
    
    %% External AWS Services
    subgraph AWS_Services["☁️ AWS Services"]
        ECR[📦 ECR Repository<br/>psy-protocol]
        S3[🪣 S3 Bucket<br/>Artifacts Storage]
        CloudWatch[📊 CloudWatch Logs<br/>/ecs/psy-protocol]
        EFS[💾 EFS FileSystem<br/>LMDBX Storage]
        ServiceDiscovery[🔍 Service Discovery<br/>psy.local]
    end
    
    %% ECS Cluster
    subgraph ECS_Cluster["🚢 ECS Cluster psy-cluster"]
        ECS_Coord
        ECS_R0
        ECS_R1
    end
    
    %% Connection Relationships - ALB to ECS
    ALB -->|Port 8545| ECS_Coord
    ALB -->|Port 8546| ECS_R0
    ALB -->|Port 8547| ECS_R1
    
    %% ECS to Redis Connections
    ECS_Coord <--> Redis_Coord
    ECS_R0 <--> Redis_R0
    ECS_R1 <--> Redis_R1
    
    %% EFS Connections
    EFS --> EFS_Mount1
    EFS --> EFS_Mount2
    ECS_Coord <--> EFS_Mount1
    ECS_R0 <--> EFS_Mount1
    ECS_R1 <--> EFS_Mount1
    
    %% ECS to External Services
    ECS_Coord <--> S3
    ECS_R0 <--> S3
    ECS_R1 <--> S3
    
    ECR --> ECS_Coord
    ECR --> ECS_R0
    ECR --> ECS_R1
    
    ECS_Coord --> CloudWatch
    ECS_R0 --> CloudWatch
    ECS_R1 --> CloudWatch
    
    ServiceDiscovery <--> ECS_Coord
    ServiceDiscovery <--> ECS_R0
    ServiceDiscovery <--> ECS_R1
    
    %% Style Definitions
    classDef vpc fill:#e1f5fe,stroke:#01579b,stroke-width:3px
    classDef publicSubnet fill:#e8f5e8,stroke:#2e7d32,stroke-width:2px
    classDef privateSubnet fill:#ffebee,stroke:#c62828,stroke-width:2px
    classDef ecs fill:#e3f2fd,stroke:#1565c0,stroke-width:2px
    classDef redis fill:#ffcdd2,stroke:#d32f2f,stroke-width:2px
    classDef storage fill:#f3e5f5,stroke:#7b1fa2,stroke-width:2px
    classDef loadbalancer fill:#fff3e0,stroke:#ef6c00,stroke-width:2px
    classDef external fill:#f5f5f5,stroke:#424242,stroke-width:2px
    
    class VPC vpc
    class PubSub1,PubSub2 publicSubnet
    class PrivSub1,PrivSub2 privateSubnet
    class ECS_Coord,ECS_R0,ECS_R1 ecs
    class Redis_Coord,Redis_R0,Redis_R1 redis
    class EFS,EFS_Mount1,EFS_Mount2,S3 storage
    class ALB,ALB_HA loadbalancer
    class ECR,CloudWatch,ServiceDiscovery external

5. Security Guarantees

Psy's security rests on multiple pillars:

1. ZK Proof Soundness: Mathematical guarantee that invalid computations or state transitions cannot produce valid proofs.
2. Circuit Whitelisting: State trees (GUSR, GCON, CFT, etc.) can only be modified by proofs generated from circuits whose fingerprints are present in designated whitelist Merkle trees. This prevents unauthorized code execution. Aggregation circuits enforce these checks recursively.
3. Recursive Verification: Each layer of aggregation cryptographically verifies the proofs from the layer below.
4. Checkpoint Anchoring: The final block circuit explicitly links the new state to the previous block's verified CHKP root, creating an unbroken chain of state validity.

6. Conclusion: A New Era of Blockchain Scalability

Psy's architecture is a fundamental departure from sequential blockchain designs. By leveraging the PARTH state model for conflict-free parallel execution and securing it with an end-to-end recursive ZKP system, Psy achieves true horizontal scalability. The intricate dance between local user proving (UPS/CFC), distributed network aggregation (Realms/Coordinators/GUTA), and a scalable backend (Redis/KVQ) allows the network's throughput to grow with the addition of computational resources (Proving Workers), paving the way for decentralized applications demanding high performance and robust security.

Realm & GUTA Gadgets

These gadgets are used within the circuits run by the network's Realm and Coordinator nodes for aggregating proofs.

GUTAStatsGadget

• File: guta_stats_rs.txt
• Purpose: Represents and aggregates key statistics during GUTA processing (fees, operations counts, slots modified).
• Technical Function: Data structure holding targets for stats. Provides combine_with method for additive aggregation and to_hash for commitment.
• Inputs/Witness: Targets for fees_collected, user_ops_processed, total_transactions, slots_modified.
• Outputs/Computed: Combined stats (via combine_with), hash of stats (to_hash).
• Constraints: combine_with uses addition constraints. to_hash uses packing/hashing.
• Assumptions: Assumes input target values are correct.
• Role: Tracks operational metrics through the aggregation tree.

GlobalUserTreeAggregatorHeaderGadget

• File: guta_header_rs.txt
• Purpose: Defines the standard public input structure for all GUTA-related aggregation circuits. Encapsulates the result of an aggregation step.
• Technical Function: Data structure holding guta_circuit_whitelist root, checkpoint_tree_root, the state_transition (SubTreeNodeStateTransitionGadget) for the GUSR tree segment covered, and aggregated stats (GUTAStatsGadget). Provides to_hash method.
• Inputs/Witness: Component targets/gadgets.
• Outputs/Computed: Hash of the header (to_hash).
• Constraints: to_hash combines hashes of components.
• Assumptions: Assumes input components are correctly formed/verified.
• Role: Standardizes the interface between recursive GUTA circuits, ensuring consistent information propagation and verification.

VerifyEndCapProofGadget

• File: verify_end_cap_rs.txt
• Purpose: Verifies a user's submitted End Cap proof (output of UPS Phase 1) at the entry point of the GUTA aggregation (typically within a Realm node circuit).
• Technical Function: Verifies the End Cap ZK proof, checks its fingerprint against the known constant, matches public inputs against witness data (result/stats), verifies the user's claimed checkpoint root against a historical checkpoint proof, and translates the result into a GlobalUserTreeAggregatorHeaderGadget.
• Inputs/Witness:
  • end_cap_result_gadget, guta_stats: Witness for claimed outputs.
  • checkpoint_historical_merkle_proof: Witness proving user's checkpoint_tree_root_hash was valid historically.
  • verifier_data, proof_target: The End Cap proof itself and its verifier data.
  • known_end_cap_fingerprint_hash: Constant parameter.
• Outputs/Computed: Implements ToGUTAHeader to output a GlobalUserTreeAggregatorHeaderGadget.
• Constraints:
  • Verifies proof_target using verifier_data.
  • Computes fingerprint from verifier_data, connects to known_end_cap_fingerprint_hash.
  • Computes expected public inputs hash from end_cap_result_gadget and guta_stats, connects to proof_target.public_inputs.
  • Verifies checkpoint_historical_merkle_proof using HistoricalRootMerkleProofGadget.
  • Connects historical_proof.historical_root to end_cap_result.checkpoint_tree_root_hash.
  • Constructs output GUTA header using historical_proof.current_root as the checkpoint_tree_root, deriving the state transition from end_cap_result (leaf hashes and user ID), and using the verified guta_stats.
• Assumptions: Assumes witness data is valid initially. Assumes known_end_cap_fingerprint_hash and input default_guta_circuit_whitelist are correct.
• Role: Securely ingests a user's proven session result into the GUTA aggregation, validating it against global rules and historical state before converting it to the standard GUTA format.

VerifyGUTAProofGadget

• File: verify_guta_proof_rs.txt
• Purpose: Verifies a GUTA proof generated by a lower level in the aggregation hierarchy (e.g., verifying a Realm's proof at the Coordinator level, or verifying sub-realm proofs within a Realm).
• Technical Function: Verifies the input GUTA ZK proof, checks its fingerprint against the GUTA circuit whitelist, and ensures its public inputs match the claimed GUTA header witness.
• Inputs/Witness:
  • guta_proof_header_gadget: Witness for the claimed header of the proof being verified.
  • guta_whitelist_merkle_proof: Witness proving the sub-proof's circuit fingerprint is in the GUTA whitelist.
  • verifier_data, proof_target: The GUTA proof and its verifier data.
• Outputs/Computed: The verified guta_proof_header_gadget.
• Constraints:
  • Verifies proof_target using verifier_data.
  • Computes fingerprint from verifier_data.
  • Verifies guta_whitelist_merkle_proof.
  • Connects guta_proof_header.guta_circuit_whitelist to whitelist_proof.root.
  • Computes expected public inputs hash from guta_proof_header, connects to proof_target.public_inputs.
  • Connects whitelist_proof.value to computed fingerprint.
• Assumptions: Assumes witness data is valid initially.
• Role: The core recursive verification step for GUTA aggregation circuits. Ensures that only valid proofs generated by allowed GUTA circuits are incorporated into higher levels of aggregation.

TwoNCAStateTransitionGadget

• File: two_nca_state_transition_rs.txt
• Purpose: Combines the GUSR state transitions from two independent GUTA proofs (A and B) that modify different branches of the tree, computing the resulting state transition at their Nearest Common Ancestor (NCA).
• Technical Function: Uses UpdateNearestCommonAncestorProofOptGadget to verify the NCA proof witness against the state transitions provided by the input GUTA headers (a_header, b_header). Combines statistics and outputs a new GUTA header for the NCA node.
• Inputs/Witness:
  • a_header, b_header: Verified GUTA headers from the two child proofs.
  • UpdateNearestCommonAncestorProof: Witness containing NCA proof data (partial or full).
• Outputs/Computed: new_guta_header representing the transition at the NCA.
• Constraints:
  • Connects a_header.checkpoint_tree_root == b_header.checkpoint_tree_root.
  • Connects a_header.guta_circuit_whitelist == b_header.guta_circuit_whitelist.
  • Connects a_header.state_transition fields (old/new value, index, level) to update_nca_proof_gadget.child_a fields.
  • Connects b_header.state_transition fields to update_nca_proof_gadget.child_b fields.
  • Computes new_stats = a_header.stats.combine_with(b_header.stats).
  • Constructs new_guta_header using whitelist/checkpoint from children, the NCA state transition details from update_nca_proof_gadget, and new_stats.
• Assumptions: Assumes input headers a_header and b_header have already been verified. Assumes the NCA proof witness is valid initially.
• Role: Enables efficient parallel aggregation by merging results from independent subtrees using cryptographic proofs of their combined effect at the parent node.

GUTAHeaderLineProofGadget

• File: guta_line_rs.txt
• Purpose: Propagates a GUTA state transition upwards along a direct path in the GUSR tree (when there's only one child updating that path segment).
• Technical Function: Uses SubTreeNodeTopLineGadget to recompute the Merkle root hash from the child's transition level up to a specified higher level (e.g., Realm root or global root), using sibling hashes provided as witness.
• Inputs/Witness:
  • child_proof_header: The verified GUTA header from the lower level.
  • siblings: Witness array of Merkle sibling hashes for the path.
  • Height parameters.
• Outputs/Computed: new_guta_header with the state transition updated to reflect the higher level.
• Constraints: Relies on SubTreeNodeTopLineGadget's internal Merkle hashing constraints.
• Assumptions: Assumes child_proof_header is verified. Assumes siblings witness is correct.
• Role: Efficiently moves a verified state transition up the tree hierarchy when merging (NCA) is not required.

VerifyGUTAProofToLineGadget

• File: verify_guta_proof_to_line_rs.txt
• Purpose: Combines verifying a lower-level GUTA proof with immediately propagating its state transition upwards using a line proof.
• Technical Function: Orchestrates VerifyGUTAProofGadget followed by GUTAHeaderLineProofGadget.
• Inputs/Witness: Combines witnesses for both sub-gadgets (proof, header, whitelist proof, siblings).
• Outputs/Computed: new_guta_header at the top of the line.
• Constraints: Instantiates and connects the two sub-gadgets.
• Assumptions: Relies on sub-gadget assumptions.
• Role: A common pattern gadget simplifying the verification and upward propagation of a single GUTA proof branch.

(Coordinator/GUTA Gadgets related to User Registration: GUTARegisterUserCoreGadget, GUTARegisterUserFullGadget, GUTARegisterUsersGadget, GUTAOnlyRegisterUsersGadget, GUTARegisterUsersBatchGadget - Descriptions remain largely the same as the previous detailed version, focusing on GUSR tree updates and User Registration Tree checks.)

GUTANoChangeGadget

• File: guta_no_change_gadget_rs.txt
• Purpose: Creates a GUTA header signifying that the GUSR tree state did not change for this block/subtree, while still potentially updating the referenced checkpoint_tree_root.
• Technical Function: Verifies a checkpoint proof to get the current checkpoint_tree_root and the corresponding user_tree_root from the checkpoint leaf. Constructs a GUTA header with a "no-op" state transition (old=new=user_tree_root at level 0) and zero stats.
• Inputs/Witness:
  • guta_circuit_whitelist: Input constant/parameter.
  • checkpoint_tree_proof: Witness proving checkpoint_leaf existence.
  • checkpoint_leaf_gadget: Witness for the PsyCheckpointLeafCompactWithStateRoots.
• Outputs/Computed: new_guta_header (indicating no GUSR change).
• Constraints: Verifies checkpoint proof (MerkleProofGadget). Verifies consistency between proof value and leaf hash. Constructs header with no-op transition and zero stats.
• Assumptions: Assumes witness proof/leaf data is valid initially. Assumes input guta_circuit_whitelist is correct.
• Role: Allows the GUTA aggregation structure to remain consistent and synchronized with the main Checkpoint Tree advancement even during periods where no user state relevant to GUTA was modified.

Psy Protocol Wiki: Achieving Scalability with PARTH and ZK Proofs

1. Introduction: The Scalability Challenge and Psy's Solution

Traditional blockchains often face a serial execution bottleneck. Transactions are typically processed one after another within a single state machine context. Adding more validator nodes doesn't necessarily increase the overall transaction processing capacity (TPS), as they all work on the same sequential task list. Attempts at parallel execution often introduce complexity, race conditions, and potential state inconsistencies.

Psy (Quantum Entangled Data) tackles this fundamental limitation through two core innovations:

1. PARTH (Parallelizable Account-based Recursive Transaction History) Architecture: A novel way of organizing blockchain state that inherently allows for parallel processing of transactions from different users within the same block.
2. End-to-End Zero-Knowledge Proofs (ZKPs): A sophisticated system of ZK circuits that rigorously verify every state transition, ensuring the security and consistency of the parallel execution enabled by PARTH.

This wiki page details the journey of a transaction from user initiation to final block inclusion, focusing on the ZK circuits involved, the assumptions they make, what they prove, and how these assumptions are systematically verified and discharged throughout the process.

2. The PARTH Architecture: Foundation for Parallelism

PARTH reorganizes blockchain state into a hierarchy of Merkle trees, enabling fine-grained state access and modification control:

• Per-User, Per-Contract State (CSTATE): Each user maintains a separate Merkle tree (CSTATE) for their specific state within each smart contract they interact with.
• User Contract Tree (UCON): Aggregates all CSTATE roots for a single user, representing their state across all contracts.
• Global User Tree (GUSR): Aggregates all UCON roots, representing the state of all users.
• Global Contract Tree (GCON): Represents the global state related to contract code definitions and metadata.
• User Registration Tree: Tracks registered users and their public keys (relevant for GUTARegisterUserCircuit).
• Checkpoint Tree (CHKP): The top-level tree. Its root hash serves as a cryptographic snapshot (checkpoint) of the entire verifiable blockchain state at a specific block height.

Key PARTH Rules Enabling Scalability:

1. Write Locally: A transaction initiated by User A can only modify (write to) the state within User A's own trees (their various CSTATEs and subsequently their UCON root).
2. Read Globally (Previous State): A transaction can read state from any tree (User A's, User B's, GCON, etc.), but it reads the state as it was finalized at the end of the previous block (anchored by the previous block's CHKP root).

Because write operations are isolated and reads access immutable past state, transactions from different users within the same block operate independently and cannot conflict. This architectural design is the cornerstone of Psy's horizontal scalability.

3. The Big Picture: End-to-End ZK Proof Flow

The process of validating transactions and building a block involves three main phases, each relying on specific ZK circuits:

1. Phase 1: User Proving Session (UPS) - Local Execution & Proving: The user (or a delegated prover) executes their transactions locally and generates a chain of recursive ZK proofs culminating in a single "End Cap" proof for their activity within the block.
2. Phase 2: Global User Tree Aggregation (GUTA) - Parallel Network Execution: The Psy network's Decentralized Proving Network (DPN) takes End Cap proofs (and other GUTA-related proofs like registrations) from many users and aggregates them in parallel using specialized GUTA circuits.
3. Phase 3: Final Block Proof Generation: A final aggregation step combines the top-level GUTA proof (representing all user state changes) with proofs for other global state changes (like contract deployments) into a single block proof anchored to the previous block's state.

4. Phase 1: User Proving Session (UPS) Circuits

This phase occurs locally, building a user-specific proof chain.

4.1. UPSStartSessionCircuit

• Purpose: Initializes the proving session for a user, establishing a secure starting point based on the last globally finalized block state.
• Core Gadget: UPSStartStepGadget
• Input Data: UPSStartStepInput (contains the target starting UserProvingSessionHeader, the corresponding PsyCheckpointLeaf and PsyCheckpointGlobalStateRoots from the last block, and Merkle proofs (checkpoint_tree_proof, user_tree_proof) linking them together).
• What it Proves:
  • Consistency of Initial State: The provided UserProvingSessionHeader.session_start_context is consistent with the provided PsyCheckpointLeaf, PsyCheckpointGlobalStateRoots, and the user's leaf (start_session_user_leaf) within the user_tree_root (part of PsyCheckpointGlobalStateRoots). It verifies that the user leaf, global roots, and checkpoint leaf all correctly correspond to the provided checkpoint_tree_root via the Merkle proofs.
  • Correct Initialization: The UserProvingSessionHeader.current_state is correctly initialized based on the session_start_context (e.g., user_leaf.last_checkpoint_id is updated, deferred_tx_debt_tree_root and inline_tx_debt_tree_root are empty hashes, tx_count is zero, tx_hash_stack is an empty hash).
  • Header Integrity: The hash of the entire ups_header is correctly computed.
  • Proof Tree Anchor: The final public output hash combines the ups_header hash with the empty_ups_proof_tree_root (a known constant representing the start of this session's proof tree), using compute_tree_aware_proof_public_inputs.
• Assumptions Made:
  1. The witness data (UPSStartStepInput) provided by the user (fetched from querying the last finalized block state) is accurate at the start of verification.
  2. The globally known constant empty_ups_proof_tree_root (hash of an empty Merkle tree of height UPS_SESSION_PROOF_TREE_HEIGHT) is correct.
  3. The previous block's checkpoint_tree_root (implicitly contained within the input witness) is valid (this is the key assumption passed into the entire UPS).
• How Assumptions are Discharged:
  • Assumption 1 is checked by the circuit's constraints, ensuring internal consistency between the header, leaf data, global roots, and Merkle proofs. If the witness data is inconsistent, proof generation fails.
  • Assumption 2 is a system parameter.
  • Assumption 3 is not discharged here; it's carried forward implicitly by using the state derived from that root as the starting point.
• Contribution to Horizontal Scalability: Provides a secure, independent starting point for each user's session based on the common, finalized global state, allowing many users to start their sessions in parallel.
• High-Level Functionality: Securely begins a user's batch of transactions for the current block context.

4.2. UPSCFCStandardTransactionCircuit

• Purpose: Processes a standard Contract Function Call (CFC) transaction, extending the user's recursive proof chain. Executed potentially multiple times per session.
• Core Gadgets: VerifyPreviousUPSStepProofInProofTreeGadget, UPSVerifyCFCStandardStepGadget
• Input Data: UPSCFCStandardTransactionCircuitInput (contains info about the previous UPS step's proof and header (verify_previous_ups_step), and details for the current CFC step (standard_cfc_step)).
• What it Proves:
  • Previous Step Validity: The ZK proof (previous_step_proof) provided for the previous UPS step (either the UPSStartSessionCircuit or another UPSCFC...Circuit) is valid.
  • Previous Step Whitelist: The previous step's proof was generated by a circuit whose fingerprint is present in the ups_circuit_whitelist_root specified in the previous_step_header.
  • Previous Step Linkage: The public inputs hash of the previous_step_proof correctly corresponds to the provided previous_step_header and the previous_proof_tree_root.
  • CFC Proof Validity & Inclusion: The ZK proof for the current CFC execution (verify_cfc_proof_input) is valid and is correctly included in the current current_proof_tree_root.
  • Contract Function Validity: The CFC proof corresponds to a function whose details (cfc_inclusion_proof) are correctly included in the Global Contract Tree (GCON) root referenced within the session's checkpoint context (checkpoint_state).
  • State Transition Correctness: Executing the CFC logically transitions the state represented by previous_step_header.current_state to the state represented by new_header_gadget.current_state. This includes updates to the user's user_leaf (specifically the user_contract_tree_root), potentially the deferred_tx_debt_tree_root or inline_tx_debt_tree_root, the tx_hash_stack, and incrementing the tx_count. The session_start_context and ups_step_circuit_whitelist_root remain unchanged.
  • Proof Tree Update: The output public inputs correctly combine the hash of the new_header_gadget with the current_proof_tree_root.
• Assumptions Made:
  1. The witness data (UPSCFCStandardTransactionCircuitInput) for this specific step (including the previous step's proof/header, the CFC proof/details, state delta witnesses) is accurate initially.
  2. The current_proof_tree_root provided as input correctly represents the root of the session's proof tree after including the current CFC proof.
  3. The assumption about the original starting checkpoint_tree_root (from UPSStartSessionCircuit) is still carried forward implicitly.
• How Assumptions are Discharged:
  • Assumption 1 is checked by verifying the previous step's proof, the CFC proof, the contract inclusion proof, and the state delta transition logic based on the witness.
  • Assumption 2 is not discharged here; it's passed implicitly to the next UPS step or the End Cap circuit, forming part of the recursive structure.
  • Assumption 3 remains implicitly carried forward.
• Contribution to Horizontal Scalability: Allows users to process their transactions sequentially locally, independent of other users' activities within the same block. The proof chain maintains self-consistency.
• High-Level Functionality: Securely executes and proves a single smart contract interaction within the user's session.

4.3. UPSCFCDeferredTransactionCircuit

• Purpose: Processes a transaction that first settles a deferred debt item and then executes the main CFC logic.
• Core Gadgets: VerifyPreviousUPSStepProofInProofTreeGadget, UPSVerifyPopDeferredTxStepGadget
• Input Data: UPSCFCDeferredTransactionCircuitInput
• What it Proves: Everything proven by UPSCFCStandardTransactionCircuit, plus:
  • Debt Removal: A specific deferred transaction was correctly removed from the deferred_tx_debt_tree (verified via ups_pop_deferred_tx_proof, a DeltaMerkleProofCore). The state transition reflects this removal before the main CFC logic is applied.
  • Debt-CFC Link: The data associated with the removed debt item matches the parameters required by the subsequent CFC execution.
• Assumptions Made: Same as UPSCFCStandardTransactionCircuit, plus assumes the witness for the DeltaMerkleProofCore (debt removal) is accurate initially.
• How Assumptions are Discharged: Same as standard, plus verifies the debt removal proof and its consistency with the CFC witness data. The starting state assumption and proof tree root assumption are carried forward.
• Contribution to Horizontal Scalability: Local serial execution, same as standard.
• High-Level Functionality: Enables settlement of asynchronous/deferred transaction calls within the user's proving flow.

4.4. UPSStandardEndCapCircuit

• Purpose: Finalizes the user's entire proving session for the block, verifying the signature and packaging the net result.
• Core Gadgets: UPSEndCapFromProofTreeGadget (which uses VerifyPreviousUPSStepProofInProofTreeGadget, AttestProofInTreeGadget, UPSEndCapCoreGadget, PsyUserProvingSessionSignatureDataCompactGadget)
• Input Data: UPSEndCapFromProofTreeGadgetInput (contains info about the last UPS step, the ZK signature proof (verify_zk_signature_proof_input), signature parameters (user_public_key_param, nonce), and slots_modified).
• What it Proves:
  • Last Step Validity: The proof for the last UPS transaction step is valid and used an allowed circuit (verify_previous_ups_step_gadget).
  • Signature Proof Validity & Inclusion: The ZK proof for the user's signature (verify_zk_signature_proof_gadget) is valid and is correctly included in the final UPS proof tree root (current_proof_tree_root).
  • Signature Authentication: The public key (user_public_key_param) used to verify the signature matches the public key stored in the previous_step_header.current_state.user_leaf.
  • Signature Payload Integrity: The ZK signature proof attests to a specific payload hash. This circuit proves that this payload hash correctly corresponds to a PsyUserProvingSessionSignatureDataCompact structure containing:
    • start_user_leaf_hash: Matches the start_session_user_leaf_hash from the previous_step_header.session_start_context.
    • end_user_leaf_hash: Matches the hash of the previous_step_header.current_state.user_leaf.
    • checkpoint_leaf_hash: Matches the checkpoint_leaf_hash from the previous_step_header.session_start_context.
    • tx_stack_hash: Matches the tx_hash_stack from the previous_step_header.current_state.
    • tx_count: Matches the tx_count from the previous_step_header.current_state.
  • Nonce Validity: The nonce used in the signature matches the nonce in the previous_step_header.current_state.user_leaf. (The state delta within the End Cap implicitly increments the nonce in the output UPSEndCapResultCompact).
  • Session Completion: The deferred_tx_debt_tree_root and inline_tx_debt_tree_root in the previous_step_header.current_state are both empty hashes (verified by end_cap_core_gadget.enforce_signature_constraints).
  • Checkpoint Consistency: The last_checkpoint_id in the previous_step_header.current_state.user_leaf matches the checkpoint_id from the session_start_context.
  • Final Output Structure: The public inputs of the End Cap proof hash a UPSEndCapResultCompact structure containing the start_user_leaf_hash, end_user_leaf_hash, checkpoint_tree_root_hash (all from the final previous_step_header), and the user_id.
• Assumptions Made:
  1. The witness data (UPSEndCapFromProofTreeGadgetInput) provided is accurate initially.
  2. System constants like network_magic, DEFERRED_TRANSACTION_TREE_HEIGHT, INLINE_TRANSACTION_TREE_HEIGHT (for deriving empty roots) are correct.
  3. The assumption about the validity of the starting checkpoint_tree_root (from UPSStartSessionCircuit) is still carried forward implicitly into the UPSEndCapResultCompact output.
• How Assumptions are Discharged:
  • Assumption 1 is checked by verifying the last step proof, the signature proof, and ensuring consistency between the signature payload data and the final UPS header state.
  • Assumption 2 relies on correct system setup.
  • Assumption 3 is not discharged. The End Cap proof essentially certifies: "Assuming the starting checkpoint X was valid, User Y correctly transitioned their state to Z and authorized it". All internal UPS assumptions (like correct proof tree construction, valid intermediate steps, correct CFC execution) have been verified and compressed into this final proof.
• Contribution to Horizontal Scalability: Packages the user's entire block activity into a single, efficiently verifiable proof. This proof can be submitted to the network and processed by the GUTA layer in parallel with End Cap proofs from countless other users.
• High-Level Functionality: Securely concludes and authorizes a user's transaction batch, preparing it for network-level aggregation.

5. Phase 2: Global User Tree Aggregation (GUTA) Circuits

The DPN receives End Cap proofs and potentially other state change proofs (like user registrations) and aggregates them in parallel using GUTA circuits. These circuits operate on GlobalUserTreeAggregatorHeader structures, which track state transitions within the Global User Tree (GUSR).

(Note: The exact circuit implementations are inferred from the gadgets. These circuits follow standard recursive aggregation patterns.)

5.1. GUTAProcessEndCapCircuit (Hypothetical)

• Purpose: Integrates a validated user End Cap proof into the GUTA hierarchy.
• Core Gadget: VerifyEndCapProofGadget
• Input: An UPSStandardEndCapCircuit proof and its associated UPSEndCapResultCompact data. Also needs witness for checkpoint_historical_merkle_proof and guta_stats.
• What it Proves:
  • End Cap Proof Validity: The provided End Cap proof is valid and was generated by the correct circuit (known_end_cap_fingerprint_hash).
  • End Cap Result Consistency: The public inputs hash of the End Cap proof matches the hash of the provided UPSEndCapResultCompact data.
  • Historical Checkpoint Validity: The checkpoint_tree_root_hash claimed in the UPSEndCapResultCompact existed as a historical root within the checkpoint_historical_merkle_proof.current_root (which represents the CHKP root being targeted by this GUTA aggregation step).
  • GUTA Header Output: Correctly constructs a GlobalUserTreeAggregatorHeader where:
    • guta_circuit_whitelist is set (likely from input/config).
    • checkpoint_tree_root matches checkpoint_historical_merkle_proof.current_root.
    • state_transition reflects the change from start_user_leaf_hash to end_user_leaf_hash at the correct user_id index (level GLOBAL_USER_TREE_HEIGHT).
    • stats are populated based on input witness.
• Assumptions Made:
  1. Witness data (End Cap proof, result, stats, historical proof) is accurate initially.
  2. The known_end_cap_fingerprint_hash constant is correct.
  3. The guta_circuit_whitelist root provided (implicitly or explicitly) is correct for this GUTA context.
  4. The checkpoint_historical_merkle_proof.current_root provided accurately represents the target CHKP root for this aggregation level. (This implicitly carries forward the assumption about the original starting checkpoint root's validity).
• How Assumptions are Discharged:
  • Assumption 1 is checked by verifying the End Cap proof and the historical checkpoint proof.
  • Assumption 2 is a system parameter.
  • Assumptions 3 and 4 are not discharged; they are bundled into the output GlobalUserTreeAggregatorHeader and passed upwards to the next GUTA aggregation level.
• Contribution to Horizontal Scalability: Allows individual user session results (already proven locally) to be independently verified against historical state and prepared as standardized GUTA inputs for parallel aggregation.
• High-Level Functionality: Validates and incorporates user end-of-session proofs into the global state aggregation process.

5.2. GUTARegisterUserCircuit (Hypothetical)

• Purpose: Processes the registration of new users, updating the GUSR tree.
• Core Gadgets: GUTAOnlyRegisterUsersGadget, GUTARegisterUsersGadget, GUTARegisterUserFullGadget, GUTARegisterUserCoreGadget
• Input: Data for users being registered, including proofs linking their public keys to a user_registration_tree_root, and delta proofs for GUSR updates. Also needs the target guta_circuit_whitelist and checkpoint_tree_root.
• What it Proves:
  • Valid Registration: Each user's provided public_key is present in the user_registration_tree_root.
  • Correct GUSR Insertion: For each user, the GUSR tree correctly transitioned at the user_id index from an empty hash to the new PsyUserLeaf hash (initialized with the verified public_key and default_user_state_tree_root). This is verified using delta proofs.
  • GUTA Header Output: Correctly constructs a GlobalUserTreeAggregatorHeader representing the combined state transition for all registered users. stats are typically zero for pure registrations. The header uses the input guta_circuit_whitelist and checkpoint_tree_root.
• Assumptions Made:
  1. Witness data (registration proofs, user data, delta proofs) is accurate initially.
  2. The input guta_circuit_whitelist and checkpoint_tree_root are correct for this context.
  3. The default_user_state_tree_root constant is correct.
  4. The underlying assumption about the validity of the input checkpoint_tree_root is carried forward.
• How Assumptions are Discharged:
  • Assumption 1 is checked by verifying registration proofs and GUSR delta proofs.
  • Assumption 2 & 4 are passed upwards via the output header.
  • Assumption 3 is a system parameter.
• Contribution to Horizontal Scalability: Allows batches of user registrations to be processed, potentially in parallel branches of the GUTA aggregation tree.
• High-Level Functionality: Securely adds new users to the global system state.

5.3. GUTAAggregationCircuit (Hypothetical - Multiple Variants Possible)

• Purpose: The workhorse of parallel aggregation. Combines the results (headers) from two lower-level GUTA proofs (which could originate from End Caps, registrations, or previous aggregations).
• Core Gadgets: VerifyGUTAProofGadget, TwoNCAStateTransitionGadget (for combining different branches), GUTAHeaderLineProofGadget (for propagating up a single branch), GUTAStatsGadget
• Input: Two input GUTA proofs (ProofWithPublicInputs) and their corresponding GlobalUserTreeAggregatorHeader data. Witness for NCA proofs if needed.
• What it Proves:
  • Input Proof Validity: Both input GUTA proofs are valid.
  • Input Proof Whitelist: Both input proofs were generated by circuits listed in the same guta_circuit_whitelist (taken from their headers).
  • Input Proof Checkpoint Consistency: Both input proofs reference the same checkpoint_tree_root (taken from their headers).
  • Input Header Consistency: The public inputs hash of each input proof matches the hash of its corresponding provided GlobalUserTreeAggregatorHeader.
  • State Transition Combination Logic: The state_transition in the output GUTA header correctly combines the state_transitions from the two input headers. This involves:
    • Verifying NCA proofs if combining transitions on different branches (TwoNCAStateTransitionGadget).
    • Ensuring direct linkage (old_root matches new_root) if combining transitions on the same path.
    • Correctly propagating the transition upwards if only one input represents a change (GUTAHeaderLineProofGadget).
  • Stats Combination: The stats in the output header are the correct sum of the stats from the input headers (GUTAStatsGadget.combine_with).
  • GUTA Header Output: Correctly constructs the output GlobalUserTreeAggregatorHeader using the combined state transition, combined stats, and the common guta_circuit_whitelist and checkpoint_tree_root from the inputs.
• Assumptions Made:
  1. Witness data (input proofs, headers, NCA/sibling proofs) is accurate initially.
  2. The assumptions about the validity of the common guta_circuit_whitelist and checkpoint_tree_root carried by the input proofs are implicitly carried forward.
• How Assumptions are Discharged:
  • Assumption 1 is checked by verifying the input proofs, their linkage to the input headers, and the logic for combining state transitions and stats.
  • Assumption 2 is not discharged; these common contextual assumptions are passed upwards in the output header.
• Contribution to Horizontal Scalability: This is the core mechanism enabling parallel processing. Thousands of these circuits can run concurrently on the DPN, merging branches of the GUTA proof tree structure, dramatically speeding up aggregation compared to sequential processing.
• High-Level Functionality: Securely and recursively combines verified state changes from multiple independent sources into larger, aggregated proofs.

5.4. GUTANoChangeCircuit

• Purpose: Handles intervals where no relevant user state changed (GUSR root remains the same) but the network needs to acknowledge the advancement of the checkpoint_tree_root.
• Core Gadget: GUTANoChangeGadget
• Input: Proof (checkpoint_tree_proof) that a specific checkpoint_leaf exists in the target checkpoint_tree_root. The target guta_circuit_whitelist root.
• What it Proves:
  • Checkpoint Validity: The provided checkpoint_leaf hash matches the value proven to be in the checkpoint_tree_proof.
  • GUSR Consistency: The global_state_roots.user_tree_root within the checkpoint_leaf is used as both the old_node_value and new_node_value in the output header's state_transition.
  • GUTA Header Output: Correctly constructs a GlobalUserTreeAggregatorHeader with the input guta_circuit_whitelist, the input checkpoint_tree_root, a state transition showing no change in the GUSR root (at index 0, level 0), and zeroed stats.
• Assumptions Made:
  1. Witness data (checkpoint proof, leaf) is accurate initially.
  2. The input guta_circuit_whitelist root is correct for this context.
  3. The assumption about the validity of the input checkpoint_tree_root is carried forward.
• How Assumptions are Discharged:
  • Assumption 1 is checked by verifying the checkpoint proof.
  • Assumptions 2 and 3 are passed upwards via the output header.
• Contribution to Horizontal Scalability: Ensures the GUTA aggregation process can produce valid proofs even for periods of inactivity in user state changes, keeping the aggregation synchronized with the progressing checkpoint tree.
• High-Level Functionality: Allows the GUTA layer to represent a "no-op" state transition correctly anchored to an updated checkpoint.

6. Phase 3: Final Block Proof Generation

6.1. Checkpoint Tree "Block" Circuit (Top-Level Aggregation)

• Purpose: The final circuit in the chain. It aggregates the ultimate proofs from the top-level state trees (the final GUTA proof for GUSR, proofs for GCON updates, etc.) and verifies the transition against the previous block's finalized state.
• Core Logic: Likely uses variants of VerifyStateTransitionProofGadget or similar aggregation gadgets tailored for combining the top-level tree proofs. It takes the previous block's CHKP root as a crucial public input.
• Input: The final aggregated proof from the GUTA layer (representing all GUSR changes), potentially proofs for GCON changes (e.g., new contract deployments via VerifyAggUserRegistrationDeployGuta logic), and the previous block's finalized CHKP root hash.
• What it Proves:
  • Top-Level Proof Validity: The input proofs (e.g., final GUTA proof) are valid and adhere to their respective whitelists and checkpoint contexts.
  • State Root Consistency: The final roots of GUSR, GCON, etc., derived from the input proofs are correctly assembled into the PsyCheckpointGlobalStateRoots for the new block.
  • New Checkpoint Leaf Construction: The new PsyCheckpointLeaf is correctly constructed using the new global state roots and other block metadata (e.g., block number, timestamp).
  • New Checkpoint Root Computation: The new CHKP root hash is correctly computed based on the new leaf and its position in the Checkpoint Tree.
  • Final State Link: The critical verification: it proves that the state transitions represented by the input proofs (originating from potentially millions of user transactions) correctly and validly transform the state anchored by the input previous_block_chkp_root into the state represented by the computed new_chkp_root.
• Assumptions Made:
  1. The only remaining significant external assumption is that the public input previous_block_chkp_root hash is indeed the valid, finalized root hash of the immediately preceding block.
• How Assumptions are Discharged:
  • All assumptions related to internal consistency, circuit whitelists, correct state transitions, user signatures, etc., have been recursively verified and discharged by the preceding UPS and GUTA circuit layers.
  • Assumption 1 is discharged by the consensus mechanism or the verifier. They know the hash of the last finalized block and check if the proof's public input matches it. If it matches, the proof demonstrates a valid state transition between the two blocks.
• Contribution to Horizontal Scalability: This final step takes the output of the massively parallel GUTA aggregation and produces a single, constant-size ZK proof for the entire block's validity. Verifying this proof is extremely fast, regardless of how many transactions were processed in parallel.
• High-Level Functionality: Creates the final, succinct, and efficiently verifiable proof for the entire block, cryptographically linking it to the previous block and enabling trustless verification of the entire chain's state transition.

7. Assumption Reduction Summary: The Journey to Trustlessness

The Psy circuit flow demonstrates a progressive reduction and discharge of assumptions:

1. Start UPS: Assumes initial state fetched from the last block is correct locally and that the last block's CHKP root was valid. Verifies local consistency.
2. UPS Transactions: Assumes previous step was valid, assumes current step's witness is correct. Verifies previous proof, verifies current CFC/debt logic, verifies state delta. Passes on proof tree root assumption and the original starting CHKP root assumption.
3. UPS End Cap: Assumes last step was valid, assumes signature proof/witness correct. Verifies last step, verifies signature proof, verifies consistency between final UPS state and signature payload. Discharges all internal UPS assumptions (proof tree validity, intermediate step validity). Outputs a proof carrying only the assumption about the original starting CHKP root.
4. GUTA (Process End Cap/Register User): Assumes End Cap/Registration proof is valid, assumes historical checkpoint/whitelist context. Verifies input proof against context. Outputs a GUTA header carrying the context assumptions upwards.
5. GUTA (Aggregation): Assumes input GUTA proofs are valid and share context. Verifies input proofs, verifies combination logic. Outputs an aggregated GUTA header carrying the common context assumptions upwards.
6. Final Block Circuit: Assumes top-level proofs (like final GUTA) are valid. Takes the previous block's CHKP root as the only major external assumption. Verifies input proofs, verifies construction of the new CHKP root based on inputs. Discharges all remaining contextual assumptions (whitelists, checkpoints derived from the input proofs). The final proof stands as: "IF the previous CHKP root was X, THEN the new CHKP root is validly Y".

This journey transforms broad initial assumptions about state correctness into a single, verifiable dependency on the previously accepted state, underpinned by the mathematical certainty of ZK proofs.

8. Conclusion: Scalability Through Parallelism and Proofs

Psy achieves true horizontal scalability by combining:

1. PARTH Architecture: Isolates user state modifications, enabling conflict-free parallel transaction execution within a block.
2. User Proving Sessions (UPS): Allows users to locally prove their own transaction sequences, offloading initial proving work.
3. Parallel ZK Aggregation (GUTA & DPN): Enables the network to verify and combine proofs from millions of users concurrently, overcoming the limitations of sequential processing.
4. Recursive Proofs: Compresses vast amounts of computation into succinct, fixed-size proofs, making final block verification extremely efficient.

This document describes the end-to-end flow of circuits involved in processing user transactions and aggregating them into a final block proof within the Psy system. It highlights the assumptions made at each stage and how they are progressively verified, ultimately enabling horizontal scalability.

Phase 1: User Proving Session (UPS) - Local Execution

This phase happens locally on the user's device (or via a delegated prover). The user builds a recursive chain of proofs for their transactions within a single block context.

1. UPSStartSessionCircuit

• Purpose: Initializes the proving session for a user based on the last finalized blockchain state.
• What it Proves:
  • The starting UserProvingSessionHeader is valid.
  • This header is correctly anchored to a specific checkpoint_leaf_hash which exists at checkpoint_id within the checkpoint_tree_root from the last finalized block.
  • The session_start_context within the header accurately reflects the user's state (start_session_user_leaf_hash, user_id, etc.) as found in the user_tree_root associated with the starting checkpoint.
  • The current_state within the starting header is correctly initialized (user leaf last_checkpoint_id updated, debt trees empty, tx count/stack zero).
• Assumptions:
  • The witness data (UPSStartStepInput) provided by the user (fetching state from the last block) is correct initially. Constraints verify its consistency.
  • The constant empty_ups_proof_tree_root (representing the start of the recursive proof tree for this session) is correct.
• How Assumptions are Discharged: Internal consistency checks verify the relationships between the provided header, checkpoint leaf, state roots, user leaf, and the Merkle proofs linking them. The assumption about the previous block's checkpoint_tree_root being correct is implicitly carried forward, as this circuit uses it as the basis for initialization.
• Contribution to Horizontal Scalability: Establishes a user-specific, isolated starting point based on globally finalized state, allowing this session to proceed independently of other users' sessions within the same new block.
• High-Level Functionality: Securely starts a user's transaction batch processing.

2. UPSCFCStandardTransactionCircuit (Executed potentially multiple times)

• Purpose: Processes a single standard transaction (contract call) within the user's ongoing session, extending the recursive proof chain.
• What it Proves:
  • The ZK proof for the previous UPS step is valid.
  • The previous step's proof was generated by a circuit listed in the ups_circuit_whitelist_root specified in the previous step's header.
  • The public inputs (header hash) of the previous step's proof match the provided previous_step_header.
  • The ZK proof for the current Contract Function Call (CFC) exists within the current current_proof_tree_root.
  • This CFC proof corresponds to a function registered in the GCON tree (via checkpoint context).
  • Executing this CFC correctly transitions the state from the previous_step_header to the new_header_gadget state (updating CSTATE->UCON root, debt trees, tx count/stack).
• Assumptions:
  • The witness data (UPSCFCStandardTransactionCircuitInput) for this specific step (CFC proof, state delta witnesses, previous step proof info) is correct initially.
  • The current_proof_tree_root provided matches the actual root of the recursive proof tree being built.
• How Assumptions are Discharged:
  • Verifies the previous step's proof using VerifyPreviousUPSStepProofInProofTreeGadget. This discharges the assumption about the previous step's validity and its public inputs.
  • Verifies the CFC proof and its link to the contract state using UPSVerifyCFCStandardStepGadget.
  • Verifies the state delta logic, ensuring the transition is correct based on witness data.
  • The assumption about the current_proof_tree_root is passed implicitly to the next step or the End Cap circuit.
• Contribution to Horizontal Scalability: User processes transactions locally and serially for themselves, maintaining self-consistency without interacting with other users' current block activity.
• High-Level Functionality: Securely executes and proves individual smart contract interactions locally.

3. UPSCFCDeferredTransactionCircuit (Executed if applicable)

• Purpose: Processes a transaction that settles a deferred debt, then executes the main CFC logic.
• What it Proves: Similar to the standard circuit, but additionally proves:
  • A specific deferred transaction item was removed from the deferred_tx_debt_tree.
  • The item removed corresponds exactly to the call data of the CFC being executed.
  • The subsequent CFC state transition starts from the state after the debt was removed.
• Assumptions: Same as the standard circuit, plus assumes the witness for the deferred transaction removal proof (DeltaMerkleProofGadget) is correct initially.
• How Assumptions are Discharged: Verifies previous step proof. Verifies the debt removal proof and its consistency with the CFC call data. Verifies the subsequent state delta.
• Contribution to Horizontal Scalability: Same as standard transaction circuit (local serial execution).
• High-Level Functionality: Enables settlement of asynchronous transaction debts within the local proving flow.

4. UPSStandardEndCapCircuit

• Purpose: Finalizes the user's entire proving session for the block.
• What it Proves:
  • The proof for the last UPS transaction step is valid and used an allowed circuit.
  • The ZK proof for the user's signature (authorizing the session) is valid and exists in the same UPS proof tree.
  • The signature corresponds to the user's registered public key (derived from signature proof parameters).
  • The signature payload (PsyUserProvingSessionSignatureDataCompact) correctly reflects the session's start/end user leaves, checkpoint, final tx stack, and tx count.
  • The nonce used in the signature is valid (incremented).
  • The final UPS state shows both deferred_tx_debt_tree_root and inline_tx_debt_tree_root are empty (all debts settled).
  • The last_checkpoint_id in the final user leaf matches the session's checkpoint_id and has progressed correctly.
  • (If aggregation proof verification included): The UPS proof tree itself was constructed using circuits from a known proof_tree_circuit_whitelist_root.
• Assumptions:
  • Witness data (UPSEndCapFromProofTreeGadgetInput, potentially agg proof witness) is correct initially.
  • Known constants (network_magic, empty debt roots, known_ups_circuit_whitelist_root, known_proof_tree_circuit_whitelist_root) are correct.
• How Assumptions are Discharged:
  • Verifies the last UPS step proof.
  • Verifies the ZK signature proof.
  • Connects signature data to the final UPS header state.
  • Checks nonce, checkpoint ID, empty debt trees.
  • Verifies proofs against whitelists using provided roots.
  • The output of this circuit (the End Cap proof) now implicitly carries the assumption that the starting checkpoint_tree_root (used in the UPSStartSessionCircuit) was correct. All internal UPS assumptions have been discharged.
• Contribution to Horizontal Scalability: Creates a single, verifiable proof representing all of a user's activity for the block. This proof can now be processed in parallel with proofs from other users by the GUTA layer.
• High-Level Functionality: Securely concludes a user's transaction batch, authorizes it, and packages it for network aggregation.

Phase 2: Global User Tree Aggregation (GUTA) - Parallel Network Execution

The Decentralized Proving Network (DPN) takes End Cap proofs (and potentially other GUTA proofs like user registrations) from many users and aggregates them in parallel. This involves specialized GUTA circuits.

(Note: The provided files focus heavily on UPS and GUTA gadgets. The exact structure of the GUTA circuits using these gadgets is inferred but follows standard recursive proof aggregation patterns.)

Example GUTA Circuits (Inferred):

5. GUTAProcessEndCapCircuit (Hypothetical)

• Purpose: To take a user's validated UPSStandardEndCapCircuit proof and integrate its state change into the GUTA proof hierarchy.
• Core Logic: Uses VerifyEndCapProofGadget.
• What it Proves:
  • The End Cap proof is valid and used the correct circuit (known_end_cap_fingerprint_hash).
  • The checkpoint_tree_root claimed by the user in the End Cap result existed historically.
  • Outputs a standard GlobalUserTreeAggregatorHeader representing the user's GUSR tree state transition (start leaf hash -> end leaf hash at the user's ID index) and stats.
• Assumptions:
  • Witness (End Cap proof, result, stats, historical proof) is correct initially.
  • The known_end_cap_fingerprint_hash constant is correct.
  • A default_guta_circuit_whitelist root is provided or known.
• How Assumptions are Discharged: Verifies the End Cap proof and historical checkpoint proof. Packages the result into a standard GUTA header. The assumption about the default_guta_circuit_whitelist is passed upwards. The assumption about the current checkpoint_tree_root (from the historical proof) is passed upwards.
• Contribution to Horizontal Scalability: Allows individual user session results to be verified independently and prepared for parallel aggregation.
• High-Level Functionality: Validates and incorporates user end-of-session proofs into the global aggregation process.

6. GUTARegisterUserCircuit (Hypothetical)

• Purpose: To process the registration of one or more new users.
• Core Logic: Uses GUTAOnlyRegisterUsersGadget (which uses GUTARegisterUsersGadget, GUTARegisterUserFullGadget, GUTARegisterUserCoreGadget).
• What it Proves:
  • For each registered user, their public_key was correctly inserted at their user_id index in the GUSR tree (transitioning from zero hash to the new user leaf hash).
  • The public_key used matches an entry in the user_registration_tree_root.
  • Outputs a GlobalUserTreeAggregatorHeader representing the aggregate GUSR state transition for all registered users, with zero stats.
• Assumptions:
  • Witness (registration proofs, user count) is correct initially.
  • guta_circuit_whitelist and checkpoint_tree_root inputs are correct for this context.
  • default_user_state_tree_root constant is correct.
• How Assumptions are Discharged: Verifies delta proofs for GUSR insertion and Merkle proofs against the registration tree. Outputs a standard GUTA header, passing assumptions about whitelist/checkpoint upwards.
• Contribution to Horizontal Scalability: User registration can be batched and potentially processed in parallel branches of the GUTA tree.
• High-Level Functionality: Securely adds new users to the system state.

7. GUTAAggregationCircuit (Hypothetical - Multiple Variants)

• Purpose: To combine the results (headers) from two or more lower-level GUTA proofs (which could be End Cap results, registrations, or previous aggregations).
• Core Logic:
  • Verifies each input GUTA proof using VerifyGUTAProofGadget.
  • Ensures all input proofs used circuits from the same guta_circuit_whitelist and reference the same checkpoint_tree_root.
  • Combines the state_transitions from the input proofs:
    • If transitions are on different branches, uses TwoNCAStateTransitionGadget with an NCA proof.
    • If transitions are on the same branch (e.g., one input is a line proof output), connects them directly (old_root of current matches new_root of previous).
    • If only one input, uses GUTAHeaderLineProofGadget to propagate upwards.
  • Combines the stats from input proofs using GUTAStatsGadget.combine_with.
  • Outputs a single GlobalUserTreeAggregatorHeader representing the combined state transition and stats.
• What it Proves: That given valid input GUTA proofs operating under the same whitelist and checkpoint context, the combined state transition and stats represented by the output header are correct.
• Assumptions:
  • Witness (input proofs, headers, NCA/sibling proofs) is correct initially.
• How Assumptions are Discharged: Verifies input proofs and their headers. Verifies the logic of combining state transitions (NCA/Line/Direct). Passes the common whitelist/checkpoint root assumptions upwards.
• Contribution to Horizontal Scalability: This is the core of parallel aggregation. Multiple instances of this circuit run concurrently across the DPN, merging proof branches in a tree structure (like MapReduce).
• High-Level Functionality: Securely and recursively combines verified state changes from multiple sources into larger, aggregated proofs.

8. GUTANoChangeCircuit (Hypothetical)

• Purpose: To handle cases where no user state changed but the checkpoint advanced.
• Core Logic: Uses GUTANoChangeGadget.
• What it Proves: That given a new checkpoint_leaf verified to be in the checkpoint_tree_proof, the GUSR tree root remains unchanged, and stats are zero. Outputs a GUTA header reflecting this.
• Assumptions: Witness (checkpoint proof, leaf) is correct initially. Input guta_circuit_whitelist is correct.
• How Assumptions are Discharged: Verifies checkpoint proof. Outputs a standard GUTA header passing assumptions upward.
• Contribution to Horizontal Scalability: Allows the aggregation process to stay synchronized with the checkpoint tree even during periods of inactivity for certain state trees.
• High-Level Functionality: Advances the aggregated checkpoint state reference.

Phase 3: Final Block Proof

9. Checkpoint Tree "Block" Circuit (Top-Level Aggregation)

• Purpose: The final aggregation circuit that combines proofs from the roots of all major state trees (like GUSR via the top-level GUTA proof, GCON, etc.) for the block.
• Core Logic:
  • Verifies the top-level GUTA proof (and proofs for other top-level trees if applicable).
  • Takes the previous block's finalized CHKP root as a public input.
  • Constructs the new CHKP leaf based on the newly computed roots of GUSR, GCON, etc., and other block metadata.
  • Computes the new CHKP root.
  • The only external assumption verified here is that the input previous_block_chkp_root matches the actual finalized root of the last block.
• What it Proves: That the entire state transition for the block, represented by the change from the previous_block_chkp_root to the new_chkp_root, is valid, having recursively verified all constituent user transactions and aggregations according to protocol rules and circuit whitelists.
• Assumptions: The only remaining input assumption is the hash of the previous block's CHKP root.
• How Assumptions are Discharged: All assumptions from lower levels (circuit whitelists, internal state consistencies) have been verified recursively. The final link to the previous block state is checked against the public input.
• Contribution to Horizontal Scalability: Represents the culmination of the massively parallel aggregation process, producing a single, succinct proof for the entire block's validity.
• High-Level Functionality: Creates the final, verifiable proof of state transition for the entire block, linking it cryptographically to the previous block. This proof can be efficiently verified by any node or light client.

Coordinator Gadgets

These gadgets are components used within circuits run by the Coordinator nodes.

BatchAppendUserRegistrationTreeGadget

• File: append_user_registration_tree.rs (Gadget definition)
• Purpose: Aggregates multiple "Spiderman" append proofs sequentially for the User Registration Tree (URT). Handles padding for a fixed maximum number of sub-tree appends.
• Key Inputs/Witness:
  • user_registration_tree_height, batch_sub_tree_height, max_sub_trees: Parameters.
  • SpidermanUpdateProof[]: Array witness containing the append proofs for each sub-tree batch being added.
• Key Outputs/Computed Values:
  • old_root: The root of the URT before all appends in this gadget instance.
  • new_root: The root of the URT after all appends in this gadget instance.
• Core Logic/Constraints:
  • Instantiates max_sub_trees instances of SpidermanAppendProofGadget.
  • Connects the new_root of one gadget to the old_root of the next in sequence.
  • Handles witness padding by setting dummy proofs for unused slots.
• Assumptions: Assumes witness SpidermanUpdateProof array is valid initially (constraints verify internal consistency). Assumes old_root of the first gadget matches the tree state before this operation.
• Role: Allows efficient batching of user registration appends into a single ZK proof step for the Coordinator.

BatchDeployContractsGadget

• File: deploy_contract.rs (Gadget definition)
• Purpose: Handles the proof logic for appending a batch of new contracts to the Global Contract Tree (GCON). Verifies one Spiderman append proof and ensures the provided contract leaf data matches the appended hashes.
• Key Inputs/Witness:
  • contract_tree_height, batch_sub_tree_height: Parameters.
  • SpidermanUpdateProof: Witness for the batch append operation on GCON.
  • PsyContractLeaf[]: Array witness containing the data for each deployed contract leaf in the batch.
• Key Outputs/Computed Values:
  • old_root, new_root: Start and end roots of the GCON tree for this batch append (from spiderman_gadget).
• Core Logic/Constraints:
  • Instantiates SpidermanAppendProofGadget.
  • Instantiates PsyContractLeafGadget for each potential leaf slot in the batch.
  • For each leaf slot marked as added (is_added from Spiderman proof):
    • Computes the hash of the corresponding PsyContractLeafGadget witness.
    • Asserts this computed hash matches the new_leaves[i] value from the Spiderman proof.
  • Handles witness padding for unused leaf slots.
• Assumptions: Assumes witness SpidermanUpdateProof and PsyContractLeaf array are valid initially. Assumes old_root of the Spiderman gadget matches the GCON state before this operation.
• Role: Securely proves the batch addition of new contracts to the global contract tree, verifying consistency between the state update and the provided contract metadata.

VerifyAggUserRegistartionDeployContractsGUTAHeaderGadget

• File: verify_agg_user_registration_deploy_guta.rs
• Purpose: Represents the combined state transitions resulting from aggregating User Registrations, Contract Deployments, and GUTA proofs. Acts as the core data structure within the Part 1 Aggregation circuit.
• Key Inputs/Witness: (Typically derived from verified sub-proofs)
  • user_registration_tree_delta: AggStateTransitionGadget for URT.
  • global_contract_tree_delta: AggStateTransitionGadget for GCON.
  • global_user_tree_delta: GlobalUserTreeAggregatorHeaderGadget for GUSR.
• Key Outputs/Computed Values:
  • combined_hash: A single hash representing the start/end states of all three trees and the GUTA header.
• Core Logic/Constraints: Primarily a data structure. get_combined_hash defines the specific hashing scheme to commit to all input state transitions.
• Assumptions: Assumes the input transition/header gadgets are correctly derived from verified proofs.
• Role: Standardizes the output structure of the Part 1 aggregation step, providing a single hash commitment for verification by the final block circuit.

VerifyAggUserRegistartionDeployContractsGUTAGadget

• File: verify_agg_user_registration_deploy_guta.rs
• Purpose: The core gadget within the Part 1 Aggregation circuit. Verifies the aggregated proofs for User Registrations, Contract Deployments, and GUTA, ensuring they are valid, used whitelisted circuits, and reference the same checkpoint state.
• Key Inputs/Witness:
  • Parameters and configuration for verifying each of the three input proofs (common data, whitelist/fingerprint configs, GUTA params).
  • Proof objects and verifier data for each of the three input proofs.
  • Witnesses for state transitions/headers corresponding to each proof.
  • GUTA whitelist Merkle proof.
• Key Outputs/Computed Values:
  • header: A VerifyAggUserRegistartionDeployContractsGUTAHeaderGadget containing the verified state transitions.
• Core Logic/Constraints:
  • Instantiates VerifyStateTransitionProofGadget for User Registrations, verifying the proof against its config/fingerprint.
  • Instantiates VerifyStateTransitionProofGadget for Contract Deployments similarly.
  • Instantiates VerifyGUTAProofGadget for the GUTA proof, verifying it against its config/fingerprint and the GUTA whitelist root.
  • Connects the checkpoint_tree_root from the GUTA header to ensure consistency (implicitly assumes UserReg/Deploy proofs are for the same checkpoint, which should be enforced by job planning). Correction: This gadget doesn't directly connect checkpoint roots; that consistency is usually handled by the job system ensuring proofs for the same checkpoint are aggregated.
  • Constructs the output header from the verified transition gadgets.
• Assumptions: Assumes witness proofs, headers, and verifier data are valid initially. Assumes input configuration (common data, fingerprint configs, whitelist root) is correct.
• Role: Securely combines the results of the three major parallel state update processes (User Reg, Deploy Contract, GUTA) into a single verifiable unit, discharging assumptions about their individual validity and circuit usage.

PsyPart1StateDeltaResultGadget

• File: checkpoint_state_transition_proofs.rs
• Purpose: Takes the verified combined header from the Part 1 aggregation (VerifyAggUserRegistartionDeployContractsGUTAHeaderGadget) and combines it with previous block stats and new block info (time, randomness) to calculate the new Checkpoint Leaf state.
• Key Inputs/Witness:
  • part_1_header: Output from the Part 1 aggregation gadget.
  • old_stats: PsyCheckpointLeafStatsGadget witness for the previous block's stats.
  • block_time: Target witness for the current block's timestamp.
  • final_random_seed_contribution: Hash witness for randomness.
• Key Outputs/Computed Values:
  • old_state_roots, new_state_roots: Derived directly from part_1_header.
  • new_stats: Computed by combining GUTA stats with time, randomness, etc.
  • old_checkpoint_leaf: Constructed from old_state_roots and old_stats.
  • new_checkpoint_leaf: Constructed from new_state_roots and new_stats.
• Core Logic/Constraints:
  • Constructs old_state_roots and new_state_roots gadgets.
  • Computes new_stats based on inputs (copying GUTA stats, hashing random seed, setting time, zeroing PM/DA stats for now).
  • Constructs old_checkpoint_leaf and new_checkpoint_leaf gadgets.
  • Asserts block_time > old_stats.block_time.
• Assumptions: Assumes part_1_header is correctly verified. Assumes old_stats, block_time, final_random_seed_contribution witnesses are correct.
• Role: Calculates the state transition specifically for the Checkpoint Leaf data based on the aggregated results from the rest of the block's activities.

CheckpointStateTransitionChildProofsGadget

• File: checkpoint_state_transition_proofs.rs
• Purpose: Verifies the "Part 1" aggregation proof within the final block circuit and instantiates the gadget (PsyPart1StateDeltaResultGadget) that calculates the Checkpoint Leaf transition.
• Key Inputs/Witness:
  • Parameters for verifying the Part 1 proof (common data, cap height, known fingerprint).
  • Part 1 proof object and verifier data.
  • Witnesses needed by PsyPart1StateDeltaResultGadget (old_stats, block_time, random_seed).
• Key Outputs/Computed Values:
  • state_delta_gadget: The instantiated PsyPart1StateDeltaResultGadget.
• Core Logic/Constraints:
  • Verifies the part_1_proof_target against part_1_verifier_data.
  • Checks the fingerprint of part_1_verifier_data against known_part_1_fingerprint.
  • Instantiates PsyPart1StateDeltaResultGadget.
  • Computes the expected public inputs hash for the Part 1 proof using the state_delta_gadget.part_1_header.
  • Asserts this computed hash matches the actual public inputs from part_1_proof_target.
• Assumptions: Assumes witness proofs, verifier data, and state delta inputs are correct initially. Assumes known_part_1_fingerprint constant is correct.
• Role: Securely incorporates the aggregated result of UserReg/Deploy/GUTA processing (the Part 1 proof) into the final block transition calculation.

CheckpointStateTransitionCoreGadget

• File: checkpoint_state_transition.rs
• Purpose: Handles the core Merkle proof logic for updating the Checkpoint Tree (CHKP) itself. Verifies the append operation for the new checkpoint leaf and its consistency with the previous checkpoint leaf.
• Key Inputs/Witness:
  • checkpoint_tree_height: Parameter.
  • append_checkpoint_tree_proof: DeltaMerkleProofCore witness for appending the new leaf.
  • previous_checkpoint_proof: MerkleProofCore witness proving the existence of the previous checkpoint leaf.
• Key Outputs/Computed Values:
  • old_checkpoint_tree_root, new_checkpoint_tree_root: Roots before/after append.
  • old_checkpoint_leaf_hash, new_checkpoint_leaf_hash: Leaf hashes involved.
• Core Logic/Constraints:
  • Instantiates DeltaMerkleProofGadget for the append proof and MerkleProofGadget for the previous proof.
  • Asserts append_checkpoint_tree_proof.old_value is zero hash (ensures append).
  • Asserts append_checkpoint_tree_proof.old_root matches previous_checkpoint_proof.root (ensures continuity).
  • Asserts append_checkpoint_tree_proof.index == previous_checkpoint_proof.index + 1.
• Assumptions: Assumes witness Merkle proofs are valid initially.
• Role: Enforces the append-only nature and sequential integrity of the main Checkpoint Tree, linking the current block's update directly to the previous block's verified state.

User Proving Session (UPS) Gadgets

These gadgets are primarily used within the circuits executed locally by users (or their delegates) to prove their transaction sequences.

CorrectUPSHeaderHashesGadget

• File: correct_header_hashes_rs.txt
• Purpose: A data structure gadget to hold potentially modified starting debt tree roots for a UPS step. Used when a transaction (like debt repayment) needs to alter the context before the main state delta logic of that same step runs.
• Technical Function: Stores previous_step_deferred_tx_debt_tree_root and previous_step_inline_tx_debt_tree_root. These values can override the corresponding roots from the actual previous step's header when passed into gadgets like UPSCFCStandardStateDeltaGadget.
• Inputs/Witness: Takes a reference to the previous step's UserProvingSessionHeaderGadget.
• Outputs/Computed: The overridden hash targets.
• Constraints: None internally; constraints are applied where its output values are consumed.
• Assumptions: Assumes the input previous_step header is correctly formed (though its values might be overridden).
• Role: Enables flexible ordering of operations within a single UPS step, specifically allowing debt tree modifications (like popping an item) to be accounted for before the main transaction logic uses those trees.

UPSVerifyCFCProofExistsAndValidGadget

• File: ups_cfc_verify_inclusion_rs.txt
• Purpose: Verifies two critical aspects of a Contract Function Call (CFC) within a UPS: (1) That the ZK proof for the CFC execution exists and is valid within the user's current UPS proof tree, and (2) That the specific function being called is officially registered within the contract's definition on the blockchain (via checkpoint context).
• Technical Function: Combines proof attestation within the UPS tree with function inclusion verification against global contract state.
• Inputs/Witness:
  • checkpoint_state_gadget: Witness for PsyCheckpointLeafCompactWithStateRoots providing context (global roots).
  • verify_cfc_proof_gadget: Witness (AttestTreeAwareProofInTreeInput) for the CFC proof itself, including its Merkle proof within the session_proof_tree.
  • cfc_inclusion_proof_gadget: Witness (PsyContractFunctionInclusionProof) proving the function's fingerprint exists in the contract's function tree (CFT).
  • ups_session_proof_tree_height: Parameter.
• Outputs/Computed:
  • attested_proof_tree_root: Root of the UPS session proof tree containing the CFC proof.
  • checkpoint_leaf_hash: Hash of the contextual checkpoint leaf.
  • cfc_fingerprint: The verified fingerprint (verifier data hash) of the CFC circuit.
  • cfc_inner_public_inputs_hash: Hash of the CFC proof's original public inputs (before tree awareness wrapping).
  • cfc_contract_id, cfc_method_id, cfc_num_inputs, cfc_num_outputs: Metadata extracted from the function inclusion proof.
• Constraints:
  • Verifies CFC proof validity and inclusion in the session tree via AttestTreeAwareProofInTreeGadget.
  • Verifies function inclusion in the contract's CFT via PsyContractFunctionInclusionProofGadget.
  • Connects cfc_inclusion_proof.contract_inclusion_proof.contract_tree_merkle_proof.root to checkpoint_state_gadget.global_state_roots.contract_tree_root (ensuring CFC inclusion is checked against the correct global contract state).
  • Connects cfc_inclusion_proof.function_verifier_fingerprint to verify_cfc_proof_gadget.fingerprint (ensuring the proven function matches the verified CFC circuit).
• Assumptions: Assumes witness data (proofs, state, inclusion proofs) is valid initially. Assumes ups_session_proof_tree_height is correct.
• Role: Acts as a crucial security gate within UPS, ensuring that the user is proving the execution of a legitimate, registered smart contract function and that this execution proof is part of their current, consistent session proof sequence.

UPSCFCStandardStateDeltaGadget

• File: ups_standard_cfc_state_delta_rs.txt
• Purpose: Calculates the precise changes to the user's state (UserProvingSessionHeader) resulting from a single, standard CFC transaction. It enforces the consistency between the transaction's claimed effects (witnessed context) and the cryptographic updates to the relevant Merkle trees.
• Technical Function: Verifies delta/pivot proofs for state updates and computes the next header state.
• Inputs/Witness:
  • previous_step_header_gadget: Header state before this transaction.
  • corrections: Optional CorrectUPSHeaderHashesGadget to override starting debt tree roots.
  • contract_state_tree_height: Target specifying the height of the specific CSTATE tree being modified.
  • UPSCFCStandardStateDeltaInput: Witness containing:
    • cfc_transaction_input_context: Start (transaction_call_start_ctx) and end (transaction_end_ctx) contexts claimed by the CFC execution.
    • user_contract_tree_update_proof: DeltaMerkleProofCore showing the change to the user's UCON tree (updating the root hash for the specific contract_id).
    • deferred_tx_debt_pivot_proof, inline_tx_debt_pivot_proof: MerkleProofCore showing the start and end roots of the debt trees remain consistent (pivot proofs).
• Outputs/Computed:
  • (Self, UserProvingSessionHeaderGadget): Returns the gadget instance and the new header state after applying the delta.
  • cfc_inner_public_inputs_hash: Hash of the cfc_transaction_input_context (used for linking to verification).
  • cfc_contract_id, cfc_method_id, etc.: Metadata passed through.
• Constraints:
  • CFC Context Hash: Computes cfc_inner_public_inputs_hash from witness.
  • UCON Update: Verifies user_contract_tree_update_proof:
    • old_root matches previous_step_header.current_state.user_leaf.user_state_tree_root.
    • index matches cfc_transaction_input_context...contract_id.
    • old_value consistency check: If zero, ensures start_ctx.start_contract_state_tree_root matches the default zero hash for the given contract_state_tree_height. If non-zero, ensures it matches start_ctx.start_contract_state_tree_root.
    • new_value matches end_ctx.end_contract_state_tree_root.
  • Debt Tree Pivots: Verifies deferred/inline_tx_debt_pivot_proof:
    • historical_root matches the corrected previous step debt root (from previous_step_header or corrections).
    • current_root matches the end_ctx.end_deferred/inline_tx_debt_tree_root.
  • Start State Consistency: Connects start_ctx fields (balance, event index, debt roots) to the corresponding fields in the (potentially corrected) previous_step_header.
  • Counters & Stack: Increments tx_count. Pushes hash of TransactionLogStackItemGadget onto tx_hash_stack using SimpleHashStackGadget.
  • Construct New Header: Creates the output UserProvingSessionHeaderGadget with updated roots, counts, stack, and user leaf values (balance/event index updated based on end_ctx). Note: Currently balance/event updates are disabled via constraints.
• Assumptions: Assumes witness proofs and contexts are valid initially. Assumes previous_step_header and corrections are correctly provided.
• Role: The core state transition engine for UPS. It cryptographically enforces that the claimed effects of a CFC execution (start/end states) are correctly reflected in the updates to the user's persistent state trees (UCON, debt trees) and session metadata (tx count/stack).

UPSVerifyCFCStandardStepGadget

• File: ups_cfc_standard_rs.txt
• Purpose: Encapsulates a complete, standard transaction processing step within UPS. It combines the verification of the CFC proof's existence and validity with the calculation and verification of the resulting state delta.
• Technical Function: Orchestrates UPSVerifyCFCProofExistsAndValidGadget and UPSCFCStandardStateDeltaGadget, connecting their inputs and outputs to ensure consistency.
• Inputs/Witness:
  • previous_step_header_gadget: Header state before this step.
  • current_proof_tree_root: Root of the UPS proof tree this step belongs to.
  • ups_session_proof_tree_height: Parameter.
  • UPSVerifyCFCStandardStepInput: Witness containing inputs for both sub-gadgets.
• Outputs/Computed:
  • new_header_gadget: The header state after this transaction step.
• Constraints:
  • Instantiates the verification and state delta sub-gadgets.
  • verify_cfc_exists_and_valid_gadget.attested_proof_tree_root == current_proof_tree_root.
  • verify_cfc_exists_and_valid_gadget.checkpoint_leaf_hash == previous_step_header_gadget.session_start_context.checkpoint_leaf_hash.
  • Connects all key metadata (contract_id, method_id, num_inputs/outputs, inner_public_inputs_hash) between the verification and state delta gadgets, ensuring they operate on the exact same verified transaction.
• Assumptions: Relies on sub-gadget assumptions. Assumes current_proof_tree_root is correct.
• Role: Defines a standard, verifiable "block" within the user's local recursive proof chain, corresponding to processing one smart contract call.

UPSVerifyPopDeferredTxStepGadget

• File: ups_cfc_standard_pop_deferred_tx_rs.txt
• Purpose: Handles transactions specifically designed to settle a previously incurred deferred transaction debt. It verifies the debt removal and then processes the corresponding CFC execution.
• Technical Function: Verifies a delta proof for removing an item from the deferred debt tree, checks its consistency with the CFC being executed, and then uses UPSVerifyCFCStandardStepGadget with a corrected starting context.
• Inputs/Witness:
  • previous_step_header_gadget, current_proof_tree_root, ups_session_proof_tree_height: Same as standard step.
  • UPSVerifyPopDeferredTxStepInput: Witness containing standard step inputs plus ups_pop_deferred_tx_proof (a DeltaMerkleProofCore for the deferred debt tree).
• Outputs/Computed: Exposes outputs from the internal standard_cfc_verify_gadget, notably the new_header_gadget.
• Constraints:
  • Verifies ups_pop_deferred_tx_proof using DeltaMerkleProofGadget.
  • ups_pop_deferred_tx_proof.old_root == previous_step_header.current_state.deferred_tx_debt_tree_root.
  • ups_pop_deferred_tx_proof.new_value == ZERO_HASH (proves removal).
  • Computes expected hash of the deferred item (DeferredTransactionStackItemGadget) based on the CFC's call_data.
  • ups_pop_deferred_tx_proof.old_value == computed deferred item hash (ensures correct debt removed).
  • Instantiates CorrectUPSHeaderHashesGadget, setting previous_step_deferred_tx_debt_tree_root = ups_pop_deferred_tx_proof.new_root.
  • Instantiates UPSVerifyCFCStandardStepGadget using the corrections.
• Assumptions: Relies on sub-gadget assumptions. Assumes witness delta proof is valid initially.
• Role: Enables verifiable settlement of asynchronous obligations (deferred calls) generated by previous transactions within the UPS flow.

PsyUserProvingSessionSignatureDataCompactGadget

• File: ups_signature_data_rs.txt
• Purpose: Defines the precise data structure that is cryptographically signed by the user to authorize the submission of their completed User Proving Session.
• Technical Function: Aggregates key state identifiers from the start and end of the UPS into a single, hashable structure, then combines it with context (network, user, nonce) for signing.
• Inputs/Witness: start_user_leaf_hash, end_user_leaf_hash, checkpoint_leaf_hash, tx_stack_hash, tx_count.
• Outputs/Computed: ups_end_cap_sighash (via get_sig_action_with_user_info).
• Constraints: Internal hashing logic (to_hash method) combines inputs. get_sig_action_with_user_info uses compute_sig_action_hash_circuit to combine the data hash with network_magic, user_id, nonce, and the PSY_SIG_ACTION_SIGN_UPS_END_CAP constant.
• Assumptions: Assumes input hash/target values correctly represent the final UPS state.
• Role: Standardizes the payload for UPS authorization, ensuring all critical state transition elements are committed to before the user signs off.

UPSEndCapResultCompactGadget

• File: ups_end_cap_result_rs.txt
• Purpose: Defines the minimal, verifiable summary of a completed UPS, intended for submission to the GUTA layer.
• Technical Function: A data structure containing the essential start/end state identifiers needed for aggregation.
• Inputs/Witness: start_user_leaf_hash, end_user_leaf_hash, checkpoint_tree_root_hash, user_id.
• Outputs/Computed: end_cap_result_hash (to_hash method).
• Constraints: Hashing logic combines inputs with the GLOBAL_USER_TREE_HEIGHT constant.
• Assumptions: Assumes input hash/target values correctly represent the final UPS state and context.
• Role: Creates the standardized output data that represents the user's net state change for the block in a format suitable for GUTA circuits.

UPSEndCapCoreGadget

• File: ups_end_cap_rs.txt
• Purpose: Enforces the final set of critical constraints required to validly conclude a User Proving Session, linking the final state to the user's signature authorization.
• Technical Function: Verifies nonce progression, public key consistency, signature data correctness, checkpoint progression, empty debt trees, and computes final outputs (Result and Stats).
• Inputs/Witness:
  • last_header_gadget: Final header state of the UPS.
  • sig_proof_public_inputs_hash: Public inputs hash from the user's signature proof.
  • sig_proof_fingerprint, sig_proof_param_hash: Signature circuit identifier hashes.
  • nonce, slots_modified: Witness targets.
  • network_magic, empty debt root constants: Parameters.
• Outputs/Computed: sig_data_compact_gadget, end_cap_result_gadget, guta_stats.
• Constraints:
  • Nonce Check: nonce > start_user_leaf.nonce. Updates final leaf nonce.
  • PK Check: Derives expected PK from sig proof params, ensures start/end user leaves have this same PK.
  • User ID Check: Start/End user IDs match.
  • Sig Data Check: Instantiates PsyUserProvingSessionSignatureDataCompactGadget, computes expected sig_proof_public_inputs_hash, connects it to the input hash from the sig proof.
  • Checkpoint Check: Ensures end_user_leaf.last_checkpoint_id == session checkpoint_id > start_user_leaf.last_checkpoint_id.
  • Debt Check: Connects last_header.current_state debt roots to empty root constants.
  • Output Generation: Instantiates UPSEndCapResultCompactGadget and GUTAStatsGadget.
• Assumptions: Assumes input last_header_gadget is correct (verified by previous step). Assumes signature proof is valid (verified elsewhere). Assumes witness nonce/slots/params are correct.
• Role: The final gatekeeper for UPS validity, ensuring all protocol rules for session finalization are met and linking the state transition to cryptographic authorization before generating the outputs for network submission.

VerifyPreviousUPSStepProofInProofTreeGadget

• File: verify_previous_ups_step_rs.txt
• Purpose: Essential gadget for recursion within UPS. It verifies the ZK proof generated by the immediately preceding UPS step, ensuring the chain of proofs is unbroken and follows protocol rules.
• Technical Function: Verifies a proof (AttestTreeAwareProofInTreeGadget), checks its circuit fingerprint against a whitelist (MerkleProofGadget), and confirms its public inputs match the expected previous header state hash.
• Inputs/Witness:
  • VerifyPreviousUPSStepProofInProofTreeInput: Contains attestation witness, previous_step_header witness, and whitelist Merkle proof witness.
  • Tree height parameters.
• Outputs/Computed: previous_step_header_gadget (representing verified public inputs), current_proof_tree_root, ups_step_circuit_whitelist_root.
• Constraints:
  • Verifies proof attestation.
  • Verifies whitelist proof.
  • Connects attestation fingerprint to whitelist proof value.
  • Connects previous_step_header.ups_step_circuit_whitelist_root to whitelist proof root.
  • Computes hash of previous_step_header witness.
  • Connects computed hash to proof_attestation_gadget.inner_public_inputs_hash.
• Assumptions: Assumes witness data (proofs, header, whitelist proof) is valid initially.
• Role: Enforces the integrity of the recursive proof chain generated locally by the user, step by step. Ensures only allowed UPS circuits are used.

VerifyPreviousUPSStepProofInProofTreePartialFromCurrentGadget

• File: verify_previous_ups_step_partial_from_current_rs.txt
• Purpose: An optimized version of the previous gadget, used when the session_start_context is constant within the verifying circuit (like the End Cap circuit). Reduces witness size.
• Technical Function: Similar to the full gadget, but reconstructs the previous_step_header_gadget internally using the known session_start_context (from current_header input) and only requiring the previous_step_state portion as witness.
• Inputs/Witness:
  • current_header: Input gadget (not witness).
  • VerifyPreviousUPSStepProofInProofTreePartialInput: Contains attestation witness, previous_step_state witness, whitelist proof witness.
• Outputs/Computed: Same as the full gadget.
• Constraints: Similar to full gadget, plus connects current_header.ups_step_circuit_whitelist_root to the whitelist proof root. Reconstructs previous header internally before hashing and connecting to attestation inner public inputs.
• Assumptions: Assumes input current_header is correct. Assumes witness data is valid initially.
• Role: Witness optimization for recursive proof verification in specific circuit contexts.

UPSEndCapFromProofTreeGadget

• File: ups_end_cap_tree_rs.txt
• Purpose: Top-level gadget within the UPSStandardEndCapCircuit. Orchestrates the verification of the final UPS step, verification of the ZK signature, and enforcement of final session constraints.
• Technical Function: Instantiates and connects VerifyPreviousUPSStepProofInProofTreeGadget (often partial), AttestProofInTreeGadget (for signature), and UPSEndCapCoreGadget.
• Inputs/Witness:
  • UPSEndCapFromProofTreeGadgetInput: Contains witnesses for previous step verification, signature verification, user_public_key_param, nonce, slots_modified.
  • Tree height and network parameters.
• Outputs/Computed: end_cap_core_gadget, current_proof_tree_root.
• Constraints:
  • Instantiates sub-gadgets.
  • Connects verify_zk_signature_proof_gadget.attested_proof_tree_root to verify_previous_ups_step_gadget.current_proof_tree_root (ensures signature and last step are in the same proof tree).
  • Passes verified data (previous header, signature hashes) and witnesses (nonce, slots, params) into UPSEndCapCoreGadget for final checks.
• Assumptions: Relies on sub-gadget assumptions. Assumes witness data is valid initially.
• Role: Coordinates the final verification checks within the End Cap circuit, ensuring the entire session is valid, linked, and authorized.

UPSStartStepGadget

• File: ups_start_rs.txt
• Purpose: Core logic for the UPSStartSessionCircuit. Verifies the user's provided initial state against the last finalized block's checkpoint data and initializes the session header.
• Technical Function: Verifies Merkle proofs linking the checkpoint leaf to the checkpoint root and the user leaf to the user tree root within that checkpoint. Ensures header consistency and correct initialization of session state (debt trees, counters).
• Inputs/Witness: UPSStartStepInput (header witness, checkpoint leaf/roots witness, checkpoint proof, user proof).
• Outputs/Computed: header_gadget (the validated starting header).
• Constraints:
  • Verifies consistency between checkpoint_tree_proof and header_gadget.session_start_context (root, leaf hash, ID).
  • Verifies consistency between checkpoint_leaf_gadget, state_roots_gadget, and header data.
  • Verifies user_tree_proof.root matches state_roots_gadget.user_tree_root.
  • Verifies user_tree_proof.value matches header_gadget.session_start_context.start_session_user_leaf_hash.
  • Verifies user_tree_proof.index matches user_id.
  • Verifies current_state initialization (updated last_checkpoint_id, empty debts, zero counts/stack).
• Assumptions: Assumes witness data is valid initially. Assumes empty tree root constants are correct.
• Role: Securely bootstraps the UPS, ensuring it starts from a globally valid and consistent state anchor.

This document details the various gadgets used within the Psy ZK circuits, primarily focusing on the User Proving Session (UPS) and Global User Tree Aggregation (GUTA) systems. Gadgets are reusable circuit components that enforce specific constraints and logic.

UPS Gadgets (User Proving Session)

These gadgets are components used within the circuits that users run locally to prove their sequence of transactions.

CorrectUPSHeaderHashesGadget

• File: correct_header_hashes.rs
• Purpose: To hold potentially modified hash roots from a previous UPS step header. This is specifically used when a transaction needs to alter the starting state assumptions for debt trees (e.g., paying back a deferred transaction before processing the current transaction's main logic).
• Key Inputs/Witness: Takes a UserProvingSessionHeaderGadget representing the actual previous step.
• Key Outputs/Computed Values:
  • previous_step_deferred_tx_debt_tree_root: The deferred debt root to assume as the starting point for the next step's logic.
  • previous_step_inline_tx_debt_tree_root: The inline debt root to assume as the starting point for the next step's logic.
• Core Logic/Constraints: Primarily a data structure. Its values are used by other gadgets (like UPSCFCStandardStateDeltaGadget) to override the default assumption that the starting debt roots are identical to the previous step's ending debt roots.
• Assumptions: Assumes the input previous_step header gadget is correctly formed (though its values might be overridden).
• Role: Enables flexible handling of transaction debt repayment within the UPS flow, allowing debts to be settled before the main state delta logic runs, without breaking the constraint flow.

UPSVerifyCFCProofExistsAndValidGadget

• File: ups_cfc_verify_inclusion.rs
• Purpose: To verify that a specific Contract Function Call (CFC) proof exists within the user's current UPS proof tree and that the function being called is validly registered within the global contract structure.
• Key Inputs/Witness:
  • AttestTreeAwareProofInTreeInput: Witness for the CFC proof's existence and validity within the UPS proof tree.
  • PsyCheckpointLeafCompactWithStateRoots: Witness for the relevant checkpoint state.
  • PsyContractFunctionInclusionProof: Witness proving the function's fingerprint exists in the contract's function tree.
  • ups_session_proof_tree_height: Parameter.
• Key Outputs/Computed Values:
  • attested_proof_tree_root: The root of the UPS proof tree the CFC proof is part of.
  • checkpoint_leaf_hash: Hash of the checkpoint leaf used for context.
  • cfc_fingerprint: The fingerprint (verifier data hash) of the CFC proof being verified.
  • cfc_inner_public_inputs_hash: The hash of the CFC proof's internal public inputs (before wrapping with tree awareness).
  • cfc_contract_id, cfc_method_id, cfc_num_inputs, cfc_num_outputs: Metadata about the contract function extracted from the inclusion proof.
• Core Logic/Constraints:
  • Verifies the CFC proof using AttestTreeAwareProofInTreeGadget.
  • Verifies the function's inclusion in the contract tree using PsyContractFunctionInclusionProofGadget.
  • Connects the contract tree root from the inclusion proof to the one in the checkpoint state.
  • Connects the CFC fingerprint from the proof attestation to the one in the inclusion proof.
• Assumptions: Assumes the witness data provided (proofs, checkpoint state) is valid for the constraints to pass.
• Role: Ensures that the CFC proof being processed corresponds to a valid, registered function and exists within the user's current session proof tree. Links the specific CFC execution to the global contract state via the checkpoint.

UPSCFCStandardStateDeltaGadget

• File: ups_standard_cfc_state_delta.rs
• Purpose: Calculates the state changes to a user's UPS header based on executing a standard CFC transaction. It updates the user's contract state tree root, transaction debt trees, transaction count, and transaction hash stack.
• Key Inputs/Witness:
  • previous_step_header_gadget: The header state before this transaction.
  • corrections: Optional CorrectUPSHeaderHashesGadget to override starting debt tree roots.
  • contract_state_tree_height: The height of the specific CSTATE tree being modified.
  • UPSCFCStandardStateDeltaInput: Witness containing the transaction input context (start/end states) and proofs for tree updates (user contract tree delta, debt tree pivots).
• Key Outputs/Computed Values:
  • new_header_gadget: The UserProvingSessionHeaderGadget representing the state after this transaction.
  • cfc_inner_public_inputs_hash: Hash of the CFC transaction input context (used for connecting to verification gadgets).
  • cfc_contract_id, cfc_method_id, cfc_num_inputs, cfc_num_outputs: Metadata passed through.
• Core Logic/Constraints:
  • Computes the expected cfc_inner_public_inputs_hash from the transaction context witness.
  • Verifies the user_contract_tree_update_proof (DeltaMerkleProofGadget):
    • Checks old_root matches the user_state_tree_root in the previous_step_header_gadget.
    • Checks index matches the tx_in_contract_id.
    • Checks old_value consistency (handles initialization from zero hash to default root based on height).
    • Checks new_value matches the tx_in_end_contract_state_tree_root.
  • Verifies deferred_tx_debt_pivot_proof (HistoricalRootMerkleProofGadget):
    • Checks historical_root matches the corrected previous_step_deferred_tx_debt_tree_root.
    • Checks current_root matches tx_in_end_deferred_tx_debt_tree_root.
  • Verifies inline_tx_debt_pivot_proof similarly.
  • Checks consistency between previous header state (balance, event index) and transaction start context.
  • Updates transaction count (new_tx_count = old_tx_count + 1).
  • Pushes the transaction log item onto the tx_hash_stack.
  • Constructs the new_header_gadget with updated values.
• Assumptions: Assumes witness proofs and context are valid. Assumes the previous_step_header_gadget and corrections are correctly provided.
• Role: The core engine for calculating user state updates resulting from a standard contract call within the UPS.

UPSVerifyCFCStandardStepGadget

• File: ups_cfc_standard.rs
• Purpose: Combines the verification of a CFC proof's existence/validity (UPSVerifyCFCProofExistsAndValidGadget) with the calculation of its resulting state changes (UPSCFCStandardStateDeltaGadget). It acts as the main gadget for processing a standard transaction step within a UPS circuit.
• Key Inputs/Witness:
  • previous_step_header_gadget: Header state before this step.
  • current_proof_tree_root: The root of the UPS proof tree this step belongs to.
  • ups_session_proof_tree_height: Parameter.
  • UPSVerifyCFCStandardStepInput: Witness containing inputs for both sub-gadgets.
• Key Outputs/Computed Values:
  • new_header_gadget: The UserProvingSessionHeaderGadget representing the state after this transaction step.
  • (Internal gadgets expose their outputs too).
• Core Logic/Constraints:
  • Instantiates UPSVerifyCFCProofExistsAndValidGadget and UPSCFCStandardStateDeltaGadget.
  • Connects current_proof_tree_root to the attested_proof_tree_root of the verification gadget.
  • Connects the checkpoint_leaf_hash between the verification gadget and the previous_step_header_gadget.
  • Connects key metadata (cfc_contract_id, cfc_method_id, cfc_num_inputs, cfc_num_outputs, cfc_inner_public_inputs_hash) between the verification gadget and the state delta gadget to ensure they operate on the same transaction.
• Assumptions: Relies on the assumptions of its constituent gadgets. Assumes current_proof_tree_root is correctly provided.
• Role: Represents a complete, verifiable step for processing one standard CFC transaction within the user's local proving session.

UPSVerifyPopDeferredTxStepGadget

• File: ups_cfc_standard_pop_deferred_tx.rs
• Purpose: Processes a transaction that pays back a previously incurred deferred transaction debt. It verifies the removal of the debt item from the deferred debt tree and then processes the CFC transaction itself (using the standard step gadget but with a corrected starting deferred debt state).
• Key Inputs/Witness:
  • previous_step_header_gadget: Header state before this step.
  • current_proof_tree_root: The root of the UPS proof tree this step belongs to.
  • ups_session_proof_tree_height: Parameter.
  • UPSVerifyPopDeferredTxStepInput: Witness containing inputs for the standard CFC step and the DeltaMerkleProof for removing the deferred transaction.
• Key Outputs/Computed Values:
  • (Exposes outputs from UPSVerifyCFCStandardStepGadget, notably the new_header_gadget).
• Core Logic/Constraints:
  • Instantiates DeltaMerkleProofGadget (ups_pop_deferred_tx_proof) for the deferred debt tree.
  • Connects ups_pop_deferred_tx_proof.old_root to the deferred_tx_debt_tree_root in previous_step_header_gadget.
  • Asserts ups_pop_deferred_tx_proof.new_value is the zero hash (proving removal).
  • Computes the hash of the expected deferred transaction item based on the call data from the CFC being processed.
  • Asserts ups_pop_deferred_tx_proof.old_value (the item removed) matches the computed hash.
  • Creates a CorrectUPSHeaderHashesGadget, setting previous_step_deferred_tx_debt_tree_root to ups_pop_deferred_tx_proof.new_root.
  • Instantiates UPSVerifyCFCStandardStepGadget using the corrected header hashes.
• Assumptions: Relies on assumptions of sub-gadgets. Assumes witness data (proofs, context) is valid.
• Role: Enables verifiable settlement of deferred transaction debts within the UPS, ensuring the debt removed matches the transaction being executed.

PsyUserProvingSessionSignatureDataCompactGadget

• File: ups_signature_data.rs
• Purpose: Defines the data structure that gets signed by the user's private key (or equivalent signature scheme) to authorize the end of a User Proving Session.
• Key Inputs/Witness:
  • start_user_leaf_hash: Hash of the user leaf at the start of the session.
  • end_user_leaf_hash: Hash of the user leaf at the end of the session.
  • checkpoint_leaf_hash: Hash of the checkpoint leaf the session was based on.
  • tx_stack_hash: Final hash of the transaction log stack.
  • tx_count: Total number of transactions processed.
• Key Outputs/Computed Values:
  • ups_end_cap_sighash: The final hash (part of the signature pre-image) computed from the input data combined with network magic, user ID, and nonce.
• Core Logic/Constraints:
  • Computes an intermediate hash combining start/end user leaves.
  • Computes an intermediate hash combining tx stack and count.
  • Computes an intermediate hash combining checkpoint leaf and user leaf combo.
  • Computes the final data hash by combining the state context and tx combo hashes.
  • Uses compute_sig_action_hash_circuit to combine this data hash with network magic, user ID, nonce, and the specific signature action code (PSY_SIG_ACTION_SIGN_UPS_END_CAP) to produce the final ups_end_cap_sighash.
• Assumptions: Assumes input hashes and targets are correctly provided.
• Role: Standardizes the data payload for UPS end cap signatures, ensuring all necessary state transition information is committed to before signing.

UPSEndCapResultCompactGadget

• File: ups_end_cap_result.rs
• Purpose: Defines the compact data structure representing the result of a completed UPS, which is submitted to the GUTA layer for aggregation.
• Key Inputs/Witness:
  • start_user_leaf_hash: Hash of the user leaf at the start of the session.
  • end_user_leaf_hash: Hash of the user leaf at the end of the session.
  • checkpoint_tree_root_hash: Root of the checkpoint tree the session was based on.
  • user_id: The ID of the user.
• Key Outputs/Computed Values:
  • end_cap_result_hash: The hash representing this result structure.
• Core Logic/Constraints:
  • Computes an intermediate hash combining user ID, start/end user leaves, and the global user tree height constant.
  • Computes the final end_cap_result_hash by hashing the intermediate hash with the checkpoint_tree_root_hash.
• Assumptions: Assumes input hashes and targets are correctly provided.
• Role: Creates the standardized, hashable output data for a completed UPS, suitable for inclusion as a public input in the end cap proof and for verification by GUTA circuits.

UPSEndCapCoreGadget

• File: ups_end_cap.rs
• Purpose: Enforces the core constraints for finalizing a User Proving Session (End Cap). It connects the final UPS state to the signature proof and prepares the final output data (result and stats).
• Key Inputs/Witness:
  • last_header_gadget: The header state at the end of the UPS (after the last transaction).
  • sig_proof_public_inputs_hash: Public inputs hash from the user's signature proof.
  • sig_proof_fingerprint, sig_proof_param_hash: Hashes related to the signature circuit's verifier data and parameters (used to derive the expected public key).
  • nonce: The nonce used in the signature, provided as witness.
  • slots_modified: Total storage slots modified, provided as witness.
  • network_magic, empty_deferred_tx_debt_tree_root, empty_inline_tx_debt_tree_root: Constants/parameters.
• Key Outputs/Computed Values:
  • sig_data_compact_gadget: The computed signature data payload.
  • end_cap_result_gadget: The computed end cap result structure.
  • guta_stats: The computed GUTA statistics for this session.
• Core Logic/Constraints:
  • Checks nonce progression: Ensures the final nonce is greater than the starting nonce and updates the user leaf nonce.
  • Verifies public key consistency:
    • Derives the expected_public_key from the signature proof fingerprint/params.
    • Asserts the start and end user leaves have the same public key.
    • Asserts this public key matches the expected_public_key.
  • Verifies user ID consistency.
  • Instantiates PsyUserProvingSessionSignatureDataCompactGadget using data from the last_header_gadget.
  • Computes the expected ups_end_cap_sighash using the signature data gadget, network magic, user ID, and nonce.
  • Computes the expected sig_proof_public_inputs_hash by hashing the ups_end_cap_sighash with the sig_proof_param_hash.
  • Asserts the computed sig_proof_public_inputs_hash matches the one provided as input.
  • Instantiates UPSEndCapResultCompactGadget with final state data.
  • Checks checkpoint ID progression: Ensures the final user leaf's last_checkpoint_id matches the session's checkpoint ID and is greater than the starting leaf's last_checkpoint_id.
  • Asserts final debt trees are empty by comparing their roots in last_header_gadget to the provided empty tree root constants.
  • Instantiates GUTAStatsGadget using the final transaction count and provided slots_modified.
• Assumptions: Assumes input hashes, targets, and the last_header_gadget are correct. Assumes the signature proof itself is valid (verification happens elsewhere or is implied).
• Role: The central gadget for validating the conditions required to end a UPS, linking the final state to the signature authorization and generating the outputs needed for GUTA.

VerifyPreviousUPSStepProofInProofTreeGadget

• File: verify_previous_ups_step.rs
• Purpose: Verifies a ZK proof corresponding to the previous step in the User Proving Session's recursive chain. It ensures the proof is valid, exists in the expected UPS proof tree, used an allowed UPS circuit, and matches the expected previous header state.
• Key Inputs/Witness:
  • ups_session_proof_tree_height, ups_circuit_whitelist_tree_height: Parameters.
  • VerifyPreviousUPSStepProofInProofTreeInput: Witness containing:
    • AttestTreeAwareProofInTreeInput: Witness for the previous step's proof attestation.
    • UserProvingSessionHeader: Witness for the header state that should be the public input of the previous proof.
    • MerkleProof: Witness proving the previous proof's circuit fingerprint is in the UPS circuit whitelist.
• Key Outputs/Computed Values:
  • proof_attestation_gadget: The underlying attestation gadget.
  • previous_step_header_gadget: The header gadget representing the public inputs of the verified proof.
  • ups_circuit_whitelist_merkle_proof: The whitelist proof gadget.
  • current_proof_tree_root: The root of the UPS proof tree identified by the attestation proof.
  • ups_step_circuit_whitelist_root: The root of the UPS circuit whitelist tree.
• Core Logic/Constraints:
  • Instantiates AttestTreeAwareProofInTreeGadget to verify the previous proof's existence in the tree.
  • Instantiates UserProvingSessionHeaderGadget for the previous step's public inputs (header).
  • Instantiates MerkleProofGadget for the circuit whitelist check.
  • Connects the fingerprint from the proof attestation to the value in the whitelist proof.
  • Connects the ups_step_circuit_whitelist_root from the previous header gadget to the root of the whitelist proof gadget.
  • Computes the expected hash of the previous_step_header_gadget.
  • Connects this expected hash to the inner_public_inputs_hash from the proof attestation gadget.
• Assumptions: Assumes witness data (proofs, headers) is valid for constraints to pass.
• Role: Crucial for the recursive nature of UPS. Each step verifies the previous step's proof, ensuring the integrity of the entire transaction chain generated locally by the user. Links the execution to the allowed set of UPS circuits.

VerifyPreviousUPSStepProofInProofTreePartialFromCurrentGadget

• File: verify_previous_ups_step_partial_from_current.rs
• Purpose: Similar to the full verification gadget, but optimized for cases where the current header's session_start_context is already known and fixed within the circuit. It only needs the previous step's state (UserProvingSessionCurrentStateGadget) as witness, reconstructing the full previous header internally.
• Key Inputs/Witness:
  • current_header: The current step's header gadget (provided as input, not witness).
  • ups_session_proof_tree_height, ups_circuit_whitelist_tree_height: Parameters.
  • VerifyPreviousUPSStepProofInProofTreePartialInput: Witness containing:
    • AttestTreeAwareProofInTreeInput: Witness for the previous proof attestation.
    • UserProvingSessionCurrentState: Witness for the state portion of the previous header.
    • MerkleProof: Witness for the UPS circuit whitelist proof.
• Key Outputs/Computed Values: Same as VerifyPreviousUPSStepProofInProofTreeGadget.
• Core Logic/Constraints:
  • Similar logic to the full version, but it constructs the previous_step_header_gadget by combining the known session_start_context from the current_header with the previous_step_state provided as witness.
  • Enforces the same connections for fingerprint, whitelist root, and inner public inputs hash.
  • Adds a constraint connecting the ups_step_circuit_whitelist_root from the current header to the whitelist proof root.
• Assumptions: Assumes the provided current_header gadget is correct. Assumes witness data is valid.
• Role: An optimization for verifying previous steps within circuits where the session start context is constant (like the End Cap circuit). Reduces witness size.

UPSEndCapFromProofTreeGadget

• File: ups_end_cap_tree.rs
• Purpose: Orchestrates the entire End Cap process within a ZK circuit. It verifies the last UPS step proof, verifies the user's ZK signature proof, and enforces the final End Cap constraints.
• Key Inputs/Witness:
  • ups_session_proof_tree_height, ups_circuit_whitelist_tree_height: Parameters.
  • network_magic: Parameter.
  • UPSEndCapFromProofTreeGadgetInput: Witness containing:
    • VerifyPreviousUPSStepProofInProofTreeInput: Witness for verifying the last UPS step.
    • AttestProofInTreeInput: Witness for verifying the ZK signature proof.
    • user_public_key_param: Hash representing signature parameters.
    • nonce: The nonce used for signing.
    • slots_modified: Total storage slots modified.
• Key Outputs/Computed Values:
  • end_cap_core_gadget: The core gadget performing final checks.
  • current_proof_tree_root: The root of the UPS proof tree.
• Core Logic/Constraints:
  • Instantiates VerifyPreviousUPSStepProofInProofTreeGadget to verify the last UPS step.
  • Instantiates AttestProofInTreeGadget to verify the ZK signature proof.
  • Connects the attested_proof_tree_root from the signature proof verification to the current_proof_tree_root from the previous step verification (ensuring both proofs are in the same tree).
  • Defines empty debt tree root constants.
  • Instantiates UPSEndCapCoreGadget, passing outputs from the verification gadgets (previous_step_header_gadget, signature proof hashes) and witness values (nonce, slots_modified, user_public_key_param) along with constants.
• Assumptions: Relies on assumptions of sub-gadgets. Assumes witness data is valid.
• Role: The top-level gadget within the End Cap circuit, ensuring the final UPS state is valid, linked to the previous step, and properly authorized by a valid ZK signature, all within the same consistent UPS proof tree.

UPSStartStepGadget

• File: ups_start.rs
• Purpose: Initializes a User Proving Session. It takes the user's initial state (from the last finalized block's checkpoint) and sets up the starting header for the UPS circuit chain.
• Key Inputs/Witness:
  • UPSStartStepInput: Witness containing:
    • UserProvingSessionHeader: The expected starting header.
    • PsyCheckpointLeaf: Witness for the checkpoint leaf data.
    • PsyCheckpointGlobalStateRoots: Witness for the global state roots within the checkpoint.
    • MerkleProof: Proof linking the checkpoint leaf to the checkpoint tree root.
    • MerkleProof: Proof linking the user's starting leaf hash to the global user tree root.
• Key Outputs/Computed Values:
  • header_gadget: The validated starting header gadget.
• Core Logic/Constraints:
  • Constraint Set 1 (Start Session Context):
    • Verifies checkpoint_tree_proof consistency with header_gadget.session_start_context (root, leaf hash, ID).
    • Verifies consistency between checkpoint_leaf_gadget, state_roots_gadget, and the header_gadget (checkpoint leaf hash, global chain root).
    • Verifies user_tree_proof root matches the user_tree_root in state_roots_gadget.
    • Verifies user_tree_proof value matches header_gadget.session_start_context.start_session_user_leaf_hash.
    • Verifies user_tree_proof index matches the user_id in the header's start leaf.
  • Constraint Set 2 (Current State Initialization):
    • Computes the hash of the expected current user leaf (start leaf with last_checkpoint_id updated to the session's checkpoint ID).
    • Asserts this computed hash matches the hash of the header_gadget.current_state.user_leaf.
    • Asserts the deferred_tx_debt_tree_root and inline_tx_debt_tree_root in header_gadget.current_state match the known empty tree root constants.
    • Asserts tx_hash_stack is zero hash and tx_count is zero.
• Assumptions: Assumes the witness data (header, proofs, leaves, roots) is valid for constraints to pass. Assumes the empty tree root constants are correct.
• Role: Securely bootstraps the User Proving Session, anchoring the initial state to a verified checkpoint and user leaf from the last finalized block and ensuring the session starts with clean debt trees and transaction counts.

GUTA Gadgets (Global User Tree Aggregation)

These gadgets are components used within the circuits run by the decentralized proving network to aggregate proofs from multiple users into a single block proof.

GUTAStatsGadget

• File: guta_stats.rs
• Purpose: Represents and processes statistics aggregated during the GUTA process.
• Key Inputs/Witness: fees_collected, user_ops_processed, total_transactions, slots_modified.
• Key Outputs/Computed Values: Can compute a hash of the stats.
• Core Logic/Constraints: Primarily a data structure. Includes a combine_with method to add stats from two gadgets together (used during aggregation). to_hash packs the stats into a HashOutTarget.
• Assumptions: Assumes input target values are correct.
• Role: Tracks key metrics about the aggregated user operations within a GUTA proof branch.

GlobalUserTreeAggregatorHeaderGadget

• File: guta_header.rs
• Purpose: Represents the public inputs (header) of a GUTA proof. It encapsulates the essential information about the aggregation step.
• Key Inputs/Witness:
  • guta_circuit_whitelist: Root hash of the allowed GUTA circuits.
  • checkpoint_tree_root: Root hash of the checkpoint tree relevant to this aggregation step.
  • state_transition: A SubTreeNodeStateTransitionGadget representing the change in the Global User Tree (GUSR) this proof covers.
  • stats: A GUTAStatsGadget containing aggregated statistics.
• Key Outputs/Computed Values: Computes the hash of the entire header.
• Core Logic/Constraints: Data structure. to_hash computes the final header hash by combining hashes of state_transition, stats, checkpoint_tree_root, and guta_circuit_whitelist.
• Assumptions: Assumes input targets/gadgets are correctly formed.
• Role: Defines the standard public interface for all GUTA circuits, ensuring consistent information is passed and verified during recursive aggregation.

VerifyEndCapProofGadget

• File: verify_end_cap.rs
• Purpose: Verifies a user's End Cap proof within the GUTA aggregation process. It checks the proof's validity, ensures it used the correct End Cap circuit, verifies the user's claimed checkpoint root is historical, and extracts the state transition and stats.
• Key Inputs/Witness:
  • proof_common_data, verifier_data_cap_height: Parameters for proof verification.
  • known_end_cap_fingerprint_hash: Constant representing the hash of the official End Cap circuit's verifier data.
  • UPSEndCapResultCompact: Witness for the result claimed by the End Cap proof.
  • GUTAStats: Witness for the stats claimed by the End Cap proof.
  • MerkleProofCore: Witness for the historical checkpoint root proof.
  • ProofWithPublicInputs: The End Cap proof itself.
  • VerifierOnlyCircuitData: Verifier data matching the proof.
• Key Outputs/Computed Values:
  • (Implements ToGUTAHeader) Outputs a GlobalUserTreeAggregatorHeaderGadget representing the state transition performed by this user.
• Core Logic/Constraints:
  • Verifies the proof_target using the provided verifier_data.
  • Computes the proof_fingerprint from the verifier_data.
  • Asserts proof_fingerprint matches known_end_cap_fingerprint_hash.
  • Instantiates UPSEndCapResultCompactGadget and GUTAStatsGadget from witness.
  • Computes the expected public inputs hash by hashing the result and stats gadgets.
  • Asserts the computed hash matches the hash derived from proof_target.public_inputs.
  • Verifies the checkpoint_historical_merkle_proof, connecting its historical_root to the checkpoint_tree_root_hash from the end cap result gadget.
  • Constructs the output GlobalUserTreeAggregatorHeaderGadget:
    • Uses a default/input guta_circuit_whitelist.
    • Uses the current_root from the historical proof as the checkpoint_tree_root.
    • Creates a SubTreeNodeStateTransitionGadget using start/end user leaf hashes and user ID from the result gadget, marking the level as GLOBAL_USER_TREE_HEIGHT.
    • Includes the verified guta_stats.
• Assumptions: Assumes witness data (proofs, results, stats) is valid. Assumes known_end_cap_fingerprint_hash is correct.
• Role: The entry point for incorporating a user's completed UPS into the GUTA aggregation tree. Verifies the user's session proof and translates its result into the standard GUTA header format for further aggregation.

VerifyGUTAProofGadget

• File: verify_guta_proof.rs
• Purpose: Verifies a GUTA proof generated by a lower level in the aggregation hierarchy. Checks the proof validity, ensures it used an allowed GUTA circuit, and extracts its header.
• Key Inputs/Witness:
  • proof_common_data, verifier_data_cap_height: Parameters.
  • GlobalUserTreeAggregatorHeader: Witness for the header claimed by the proof being verified.
  • MerkleProof: Witness proving the sub-proof's circuit fingerprint is in the GUTA circuit whitelist.
  • ProofWithPublicInputs: The GUTA proof itself.
  • VerifierOnlyCircuitData: Verifier data for the proof.
• Key Outputs/Computed Values:
  • guta_proof_header_gadget: The verified header gadget of the sub-proof.
• Core Logic/Constraints:
  • Verifies the proof_target using the provided verifier_data.
  • Computes the proof_fingerprint from the verifier_data.
  • Verifies the guta_whitelist_merkle_proof.
  • Connects the guta_proof_header_gadget.guta_circuit_whitelist to the guta_whitelist_merkle_proof.root.
  • Computes the expected public inputs hash from the guta_proof_header_gadget.
  • Asserts this matches the hash derived from proof_target.public_inputs.
  • Asserts the guta_whitelist_merkle_proof.value matches the computed proof_fingerprint.
• Assumptions: Assumes witness data is valid.
• Role: The core recursive verification step within GUTA. Allows aggregation circuits to securely incorporate results from lower-level GUTA proofs.

TwoNCAStateTransitionGadget

• File: two_nca_state_transition.rs
• Purpose: Combines the state transitions from two child GUTA proofs (a_header, b_header) that modify different parts of the Global User Tree. It uses a Nearest Common Ancestor (NCA) proof to compute the resulting state transition at their common parent node in the tree.
• Key Inputs/Witness:
  • a_header, b_header: The headers of the two child GUTA proofs.
  • UpdateNearestCommonAncestorProof: Witness containing the NCA proof data.
• Key Outputs/Computed Values:
  • new_guta_header: The combined GUTA header representing the transition at the NCA.
• Core Logic/Constraints:
  • Instantiates UpdateNearestCommonAncestorProofOptGadget.
  • Connects a_header.checkpoint_tree_root to b_header.checkpoint_tree_root.
  • Connects a_header.guta_circuit_whitelist to b_header.guta_circuit_whitelist.
  • Connects a_header.state_transition fields (old/new value, index, level) to the child_a fields in the NCA proof gadget.
  • Connects b_header.state_transition fields similarly to child_b.
  • Combines stats: new_stats = a_header.stats.combine_with(b_header.stats).
  • Constructs new_guta_header:
    • Uses whitelist/checkpoint root from children (they must match).
    • Creates state_transition using the old/new_nearest_common_ancestor_value, index, and level from the NCA proof gadget.
    • Includes the new_stats.
• Assumptions: Assumes input headers are valid (verified previously). Assumes the NCA proof witness is valid. Assumes children operate on the same checkpoint and whitelist.
• Role: A fundamental building block for parallel aggregation. Allows merging results from independent branches of the GUTA proof tree efficiently using NCA proofs.

GUTAHeaderLineProofGadget

• File: guta_line.rs
• Purpose: Aggregates a GUTA proof state transition upwards along a direct line towards the root of the Global User Tree realm. Used when a node only has one child contributing to the update in that part of the tree.
• Key Inputs/Witness:
  • global_user_tree_realm_height, global_user_tree_height: Parameters.
  • child_proof_header: The header of the single child GUTA proof.
  • siblings: Witness containing the Merkle sibling hashes needed to recompute the root along the path.
• Key Outputs/Computed Values:
  • new_guta_header: The GUTA header representing the state transition at the top of the line (realm root).
• Core Logic/Constraints:
  • Instantiates SubTreeNodeTopLineGadget, providing the child's state transition. This gadget internally performs the Merkle path hashing using the provided siblings.
  • Constructs new_guta_header:
    • Copies whitelist/checkpoint root/stats from the child.
    • Uses the new_state_transition computed by the SubTreeNodeTopLineGadget.
• Assumptions: Assumes child_proof_header is valid. Assumes sibling hashes in the witness are correct.
• Role: Efficiently propagates a state change up the GUTA tree when no merging (NCA) is required. Used to bring proofs to a common level before NCA or to reach the final realm root.

VerifyGUTAProofToLineGadget

• File: verify_guta_proof_to_line.rs
• Purpose: Combines verifying a lower-level GUTA proof with aggregating its state transition upwards using a line proof.
• Key Inputs/Witness:
  • proof_common_data, verifier_data_cap_height: Parameters.
  • global_user_tree_realm_height, global_user_tree_height: Parameters.
  • MerkleProofCore: GUTA whitelist proof witness.
  • GlobalUserTreeAggregatorHeader: Child proof header witness.
  • ProofWithPublicInputs, VerifierOnlyCircuitData: Child GUTA proof and verifier data witness.
  • top_line_siblings: Sibling hashes for the line proof witness.
• Key Outputs/Computed Values:
  • new_guta_header: The final GUTA header at the top of the line.
• Core Logic/Constraints:
  • Instantiates VerifyGUTAProofGadget to verify the child proof.
  • Instantiates GUTAHeaderLineProofGadget, using the verified header from the first gadget as input.
• Assumptions: Relies on assumptions of sub-gadgets. Assumes witness data is valid.
• Role: A common pattern in GUTA aggregation: verify a child proof and immediately propagate its result upwards via a line proof.

GUTARegisterUserCoreGadget

• File: guta_register_user_core.rs
• Purpose: Handles the core logic for registering a single new user in the Global User Tree (GUSR). It verifies the update proof that inserts the new user leaf.
• Key Inputs/Witness:
  • global_user_tree_realm_height, global_user_tree_height: Parameters.
  • default_user_state_tree_root: Constant.
  • input_height_target: Optional target for variable height proof.
  • public_key: The public key hash for the new user (can be witness or input).
  • DeltaMerkleProofCore: Witness for the GUSR tree update.
• Key Outputs/Computed Values:
  • user_id: The ID (index) of the newly registered user.
  • user_leaf_hash: The hash of the newly created user leaf.
  • state_transition: Represents the GUTA state transition for this single registration.
• Core Logic/Constraints:
  • Instantiates VariableHeightDeltaMerkleProofOptGadget for the GUSR update.
  • Asserts the old_value in the proof is the zero hash (ensuring it's an insertion into an empty slot).
  • Creates the default PsyUserLeafGadget using the proof's index (user ID), the public_key, and default_user_state_tree_root.
  • Computes the user_leaf_hash.
  • Asserts the new_value in the proof matches the computed user_leaf_hash.
  • Calculates the state_transition based on the delta proof's old/new roots, height, and computed parent index.
• Assumptions: Assumes witness proof and public key (if witness) are valid. Assumes default_user_state_tree_root is correct.
• Role: The lowest-level gadget for handling user registration state changes in GUTA.

GUTARegisterUserFullGadget

• File: guta_register_user_full.rs
• Purpose: Extends the core registration by adding verification against a user registration tree. This tree (presumably managed off-chain or via a separate mechanism) maps user IDs to public keys. This gadget ensures the public key used for registration matches the one committed to in the registration tree.
• Key Inputs/Witness:
  • (Inherits inputs from Core gadget).
  • MerkleProofCore: Witness proving the public_key exists at the correct index (user ID) in the user_registration_tree.
• Key Outputs/Computed Values:
  • (Inherits outputs from Core gadget).
  • user_registration_tree_root: The root of the user registration tree.
• Core Logic/Constraints:
  • Instantiates MerkleProofGadget for the user registration tree.
  • Maps the proof's index bits to an expected user ID.
  • Asserts the value (public key) from the registration tree proof is non-zero.
  • Instantiates GUTARegisterUserCoreGadget, passing the value from the registration proof as the public_key.
  • Asserts the user_id from the Core gadget matches the expected_user_id derived from the registration proof index.
• Assumptions: Relies on Core gadget assumptions. Assumes the user registration tree proof witness is valid.
• Role: Adds a layer of validation, ensuring user registrations correspond to pre-committed public keys in a dedicated registration structure.

GUTARegisterUsersGadget

• File: guta_register_users.rs
• Purpose: Aggregates multiple user registration operations (using GUTARegisterUserFullGadget) sequentially within a single circuit. Handles padding/disabling for a fixed maximum number of users.
• Key Inputs/Witness:
  • (Inherits inputs from Full gadget).
  • max_users: Parameter.
  • GUTARegisterUserFullInput[]: Array witness for each potential user registration (proofs).
  • register_user_count: Witness target indicating the actual number of users being registered (<= max_users).
• Key Outputs/Computed Values:
  • state_transition: The aggregate state transition covering all registered users.
  • user_registration_tree_root: Root of the registration tree (taken from the first user, checked for consistency).
• Core Logic/Constraints:
  • Instantiates max_users instances of GUTARegisterUserFullGadget.
  • Asserts register_user_count is non-zero.
  • Iterates from the second user onwards:
    • Compares loop index i with register_user_count to determine if the current user slot is_disabled.
    • If not disabled:
      • Connects the current user's old_global_user_tree_root to the previous user's new_global_user_tree_root.
      • Connects the current user's user_registration_tree_root to the root from the first user (ensuring consistency).
      • Connects proof heights.
      • Updates the aggregate state_transition.new_node_value to the current user's new_global_user_tree_root.
    • Selects the final new_node_value based on the last enabled user's output.
• Assumptions: Relies on Full gadget assumptions. Assumes witness array and count are valid. Assumes dummy inputs are used correctly for padding.
• Role: Allows batching multiple user registrations into a single GUTA proof step, improving aggregation efficiency.

GUTAOnlyRegisterUsersGadget

• File: guta_only_register_users_gadget.rs
• Purpose: A specialized GUTA gadget that only performs user registration (using GUTARegisterUsersGadget) and assumes no other state changes (zero stats).
• Key Inputs/Witness:
  • guta_circuit_whitelist, checkpoint_tree_root: Inputs (likely from a previous step or constant).
  • (Inherits inputs for GUTARegisterUsersGadget).
• Key Outputs/Computed Values:
  • new_guta_header: The GUTA header representing only the registration state change.
• Core Logic/Constraints:
  • Instantiates GUTARegisterUsersGadget.
  • Constructs new_guta_header:
    • Uses input guta_circuit_whitelist and checkpoint_tree_root.
    • Uses the state_transition from the GUTARegisterUsersGadget.
    • Creates a zeroed GUTAStatsGadget.
• Assumptions: Relies on GUTARegisterUsersGadget assumptions. Assumes the provided whitelist/checkpoint roots are correct for this context.
• Role: Provides a dedicated gadget for GUTA steps that solely involve registering new users.

GUTARegisterUsersBatchGadget

• File: guta_register_users_batch.rs
• Purpose: Combines verification of a previous GUTA proof (brought up to a certain tree level via a line proof) with a subsequent batch registration of new users.
• Key Inputs/Witness:
  • (Inherits inputs for VerifyGUTAProofToLineGadget).
  • (Inherits inputs for GUTARegisterUsersGadget).
• Key Outputs/Computed Values:
  • new_guta_header: The combined GUTA header.
• Core Logic/Constraints:
  • Instantiates VerifyGUTAProofToLineGadget (verify_to_line_gadget).
  • Instantiates GUTARegisterUsersGadget (register_users_gadget).
  • Connects the state transitions:
    • line_state_transition.node_index == register_users_state_transiton.node_index.
    • line_state_transition.node_level == register_users_state_transiton.node_level.
    • line_state_transition.new_node_value == register_users_state_transiton.old_node_value (ensures the registration starts from the state reached by the verified line proof).
  • Constructs new_guta_header:
    • Uses whitelist/checkpoint root/stats from the line proof header.
    • Creates combined state_transition: old_node_value from line, new_node_value from registration, index/level from line (must match registration).
• Assumptions: Relies on assumptions of sub-gadgets. Assumes witness data is valid.
• Role: Handles a common GUTA pattern: verifying a previous aggregation step and then applying a batch of user registrations originating from the state achieved by that previous step.

GUTANoChangeGadget

• File: guta_no_change_gadget.rs
• Purpose: Represents a GUTA step where the Global User Tree (GUSR) does not change. It primarily serves to advance the checkpoint_tree_root based on a new checkpoint.
• Key Inputs/Witness:
  • guta_circuit_whitelist: Input constant/parameter.
  • checkpoint_tree_height: Parameter.
  • MerkleProofCore: Witness proving a checkpoint_leaf exists in the checkpoint_tree.
  • PsyCheckpointLeafCompactWithStateRoots: Witness for the checkpoint leaf data.
• Key Outputs/Computed Values:
  • new_guta_header: GUTA header indicating no user tree change but potentially a new checkpoint root.
• Core Logic/Constraints:
  • Verifies the checkpoint_tree_proof (append-only).
  • Verifies the hash of checkpoint_leaf_gadget matches the value in the proof.
  • Constructs new_guta_header:
    • Uses input guta_circuit_whitelist.
    • Uses the checkpoint_tree_proof.root as the checkpoint_tree_root.
    • Creates a "no-op" state_transition: old_node_value and new_node_value are both set to the user_tree_root from the checkpoint_leaf_gadget, with index/level zero.
    • Creates a zeroed GUTAStatsGadget.
• Assumptions: Assumes witness proof and leaf data are valid. Assumes guta_circuit_whitelist is correct.
• Role: Allows the GUTA aggregation to incorporate new checkpoints even if no user state changed during that period, keeping the aggregated checkpoint root up-to-date.

Circuit Definition Files (Higher Level)

These files define complete ZK circuits, orchestrating various gadgets to perform end-to-end tasks like starting a session, processing transactions, or finalizing a session.

UPSStartSessionCircuit

• File: ups_start.rs (Circuit definition wrapping UPSStartStepGadget)
• Purpose: The circuit executed to begin a User Proving Session.
• Core Logic: Primarily uses the UPSStartStepGadget to verify the initial state against a checkpoint and set up the starting header. Computes the final public inputs hash by wrapping the inner header hash (start_step_gadget.header_gadget.to_hash()) with tree awareness information (using compute_tree_aware_proof_public_inputs), assuming the proof tree starts empty (empty_ups_proof_tree_root_target).
• What it Proves: That a valid starting UserProvingSessionHeader has been constructed, correctly anchored to a specific, verified checkpoint and user leaf state from the last finalized block, and that the session starts with empty debt trees and zero transaction count.
• Assumptions: Assumes the witness (UPSStartStepInput) containing the starting header, proofs, and state roots is valid before constraints are applied. Assumes the provided empty_ups_proof_tree_root constant is correct.
• Role: Securely initializes the recursive proof chain for a user's local transactions.

UPSCFCStandardTransactionCircuit

• File: ups_cfc_standard.rs (Circuit definition wrapping VerifyPreviousUPSStepProofInProofTreeGadget and UPSVerifyCFCStandardStepGadget)
• Purpose: Processes a single, standard Contract Function Call (CFC) transaction within an ongoing User Proving Session.
• Core Logic:
  • Uses VerifyPreviousUPSStepProofInProofTreeGadget to verify the proof of the previous UPS step.
  • Uses UPSVerifyCFCStandardStepGadget (which internally uses verification and state delta gadgets) to:
    • Verify the CFC proof exists in the current proof tree.
    • Verify the CFC function is valid.
    • Calculate the state changes based on the CFC execution.
  • Connects the current_proof_tree_root from the previous step verification to the standard step gadget.
  • Computes the final public inputs hash by wrapping the new header hash (standard_cfc_step_gadget.new_header_gadget.to_hash()) with tree awareness information (current_proof_tree_root).
• What it Proves: That given a valid previous UPS step proof and header, executing the specified CFC transaction (verified to exist and be valid) correctly transitions the UPS state to the new header state.
• Assumptions: Assumes the witness (UPSCFCStandardTransactionCircuitInput) containing the previous step proof details, the current transaction details (proofs, context), and circuit whitelist proofs is valid. Relies on the validity of the previous UPS step proof (which is verified internally).
• Role: The workhorse circuit for processing most user transactions locally within the recursive UPS chain.

UPSCFCDeferredTransactionCircuit

• File: ups_cfc_deferred_tx.rs (Circuit definition wrapping VerifyPreviousUPSStepProofInProofTreeGadget and UPSVerifyPopDeferredTxStepGadget)
• Purpose: Processes a transaction that pays back a deferred transaction debt within an ongoing User Proving Session.
• Core Logic:
  • Uses VerifyPreviousUPSStepProofInProofTreeGadget to verify the previous UPS step proof.
  • Uses UPSVerifyPopDeferredTxStepGadget to:
    • Verify the removal of the correct deferred transaction item from the debt tree.
    • Process the CFC itself using corrected starting state assumptions.
  • Connects the current_proof_tree_root appropriately.
  • Computes the final public inputs hash by wrapping the new header hash (deferred_tx_cfc_step_gadget...new_header_gadget.to_hash()) with tree awareness information.
• What it Proves: That given a valid previous UPS step, the specified deferred transaction debt was correctly removed, and executing the corresponding CFC transaction correctly transitions the UPS state to the new header state.
• Assumptions: Assumes the witness (UPSCFCDeferredTransactionCircuitInput) is valid. Relies on the validity of the previous UPS step proof.
• Role: Enables the settlement of deferred transaction debts within the user's local proof chain.

UPSStandardEndCapCircuit

• File: end_cap.rs (Circuit definition wrapping UPSEndCapFromProofTreeGadget and proof verification gadgets)
• Purpose: The final circuit in a User Proving Session. It verifies the last UPS step, verifies the user's ZK signature proof, enforces final state conditions (e.g., empty debt trees), and generates the final public outputs (End Cap Result hash and GUTA Stats hash).
• Core Logic:
  • Uses UPSEndCapFromProofTreeGadget which orchestrates:
    • Verification of the last UPS step proof (VerifyPreviousUPSStepProofInProofTreeGadget).
    • Verification of the ZK signature proof (AttestProofInTreeGadget).
    • Enforcement of final conditions via UPSEndCapCoreGadget.
  • (Original end_cap.rs also includes VerifyAggProofGadget): Verifies a proof about the UPS proof tree itself (e.g., ensuring the tree was built using allowed aggregation circuits). This connects the user's session to the global proof aggregation infrastructure rules.
  • Connects the proof tree root from the UPS gadget to the state transition end of the verified aggregation proof.
  • Connects the UPS circuit whitelist root from the UPS gadget to a known constant or input, ensuring the UPS steps used allowed circuits.
  • Connects the proof tree aggregation circuit whitelist root to a known constant (ensuring the tree proof used allowed circuits).
  • Computes the final public inputs hash by hashing the end_cap_result_gadget hash and the guta_stats hash.
• What it Proves: That the entire User Proving Session was valid (by verifying the last step), the final state is consistent (empty debts, correct nonce/checkpoint progression), the session is authorized by a valid ZK signature corresponding to the user's key, the session used allowed UPS circuits, and the session's proof tree was built correctly using allowed aggregation circuits. It outputs the final state transition hash and stats hash.
• Assumptions: Assumes the witness (UPSEndCapFromProofTreeGadgetInput, aggregation proof witnesses) is valid. Assumes the known whitelist root constants are correct.
• Role: Securely concludes the user's local proving session, producing a verifiable proof and result ready for submission to the GUTA layer. Links the user's activity to global rules via whitelist checks.

Circuits.md

This document describes the end-to-end flow of circuits involved in processing user transactions and aggregating them into a final block proof within the Psy system. It highlights the assumptions made at each stage and how they are progressively verified, ultimately enabling horizontal scalability.

Phase 1: User Proving Session (UPS) - Local Execution

This phase happens locally on the user's device (or via a delegated prover). The user builds a recursive chain of proofs for their transactions within a single block context.

1. UPSStartSessionCircuit

• Purpose: Initializes the proving session for a user based on the last finalized blockchain state.
• What it Proves:
  • The starting UserProvingSessionHeader is valid.
  • This header is correctly anchored to a specific checkpoint_leaf_hash which exists at checkpoint_id within the checkpoint_tree_root from the last finalized block.
  • The session_start_context within the header accurately reflects the user's state (start_session_user_leaf_hash, user_id, etc.) as found in the user_tree_root associated with the starting checkpoint.
  • The current_state within the starting header is correctly initialized (user leaf last_checkpoint_id updated, debt trees empty, tx count/stack zero).
• Assumptions:
  • The witness data (UPSStartStepInput) provided by the user (fetching state from the last block) is correct initially. Constraints verify its consistency.
  • The constant empty_ups_proof_tree_root (representing the start of the recursive proof tree for this session) is correct.
• How Assumptions are Discharged: Internal consistency checks verify the relationships between the provided header, checkpoint leaf, state roots, user leaf, and the Merkle proofs linking them. The assumption about the previous block's checkpoint_tree_root being correct is implicitly carried forward, as this circuit uses it as the basis for initialization.
• Contribution to Horizontal Scalability: Establishes a user-specific, isolated starting point based on globally finalized state, allowing this session to proceed independently of other users' sessions within the same new block.
• High-Level Functionality: Securely starts a user's transaction batch processing.

2. UPSCFCStandardTransactionCircuit (Executed potentially multiple times)

• Purpose: Processes a single standard transaction (contract call) within the user's ongoing session, extending the recursive proof chain.
• What it Proves:
  • The ZK proof for the previous UPS step is valid.
  • The previous step's proof was generated by a circuit listed in the ups_circuit_whitelist_root specified in the previous step's header.
  • The public inputs (header hash) of the previous step's proof match the provided previous_step_header.
  • The ZK proof for the current Contract Function Call (CFC) exists within the current current_proof_tree_root.
  • This CFC proof corresponds to a function registered in the GCON tree (via checkpoint context).
  • Executing this CFC correctly transitions the state from the previous_step_header to the new_header_gadget state (updating CSTATE->UCON root, debt trees, tx count/stack).
• Assumptions:
  • The witness data (UPSCFCStandardTransactionCircuitInput) for this specific step (CFC proof, state delta witnesses, previous step proof info) is correct initially.
  • The current_proof_tree_root provided matches the actual root of the recursive proof tree being built.
• How Assumptions are Discharged:
  • Verifies the previous step's proof using VerifyPreviousUPSStepProofInProofTreeGadget. This discharges the assumption about the previous step's validity and its public inputs.
  • Verifies the CFC proof and its link to the contract state using UPSVerifyCFCStandardStepGadget.
  • Verifies the state delta logic, ensuring the transition is correct based on witness data.
  • The assumption about the current_proof_tree_root is passed implicitly to the next step or the End Cap circuit.
• Contribution to Horizontal Scalability: User processes transactions locally and serially for themselves, maintaining self-consistency without interacting with other users' current block activity.
• High-Level Functionality: Securely executes and proves individual smart contract interactions locally.

3. UPSCFCDeferredTransactionCircuit (Executed if applicable)

• Purpose: Processes a transaction that settles a deferred debt, then executes the main CFC logic.
• What it Proves: Similar to the standard circuit, but additionally proves:
  • A specific deferred transaction item was removed from the deferred_tx_debt_tree.
  • The item removed corresponds exactly to the call data of the CFC being executed.
  • The subsequent CFC state transition starts from the state after the debt was removed.
• Assumptions: Same as the standard circuit, plus assumes the witness for the deferred transaction removal proof (DeltaMerkleProofGadget) is correct initially.
• How Assumptions are Discharged: Verifies previous step proof. Verifies the debt removal proof and its consistency with the CFC call data. Verifies the subsequent state delta.
• Contribution to Horizontal Scalability: Same as standard transaction circuit (local serial execution).
• High-Level Functionality: Enables settlement of asynchronous transaction debts within the local proving flow.

4. UPSStandardEndCapCircuit

• Purpose: Finalizes the user's entire proving session for the block.
• What it Proves:
  • The proof for the last UPS transaction step is valid and used an allowed circuit.
  • The ZK proof for the user's signature (authorizing the session) is valid and exists in the same UPS proof tree.
  • The signature corresponds to the user's registered public key (derived from signature proof parameters).
  • The signature payload (PsyUserProvingSessionSignatureDataCompact) correctly reflects the session's start/end user leaves, checkpoint, final tx stack, and tx count.
  • The nonce used in the signature is valid (incremented).
  • The final UPS state shows both deferred_tx_debt_tree_root and inline_tx_debt_tree_root are empty (all debts settled).
  • The last_checkpoint_id in the final user leaf matches the session's checkpoint_id and has progressed correctly.
  • (If aggregation proof verification included): The UPS proof tree itself was constructed using circuits from a known proof_tree_circuit_whitelist_root.
• Assumptions:
  • Witness data (UPSEndCapFromProofTreeGadgetInput, potentially agg proof witness) is correct initially.
  • Known constants (network_magic, empty debt roots, known_ups_circuit_whitelist_root, known_proof_tree_circuit_whitelist_root) are correct.
• How Assumptions are Discharged:
  • Verifies the last UPS step proof.
  • Verifies the ZK signature proof.
  • Connects signature data to the final UPS header state.
  • Checks nonce, checkpoint ID, empty debt trees.
  • Verifies proofs against whitelists using provided roots.
  • The output of this circuit (the End Cap proof) now implicitly carries the assumption that the starting checkpoint_tree_root (used in the UPSStartSessionCircuit) was correct. All internal UPS assumptions have been discharged.
• Contribution to Horizontal Scalability: Creates a single, verifiable proof representing all of a user's activity for the block. This proof can now be processed in parallel with proofs from other users by the GUTA layer.
• High-Level Functionality: Securely concludes a user's transaction batch, authorizes it, and packages it for network aggregation.

Phase 2: Global User Tree Aggregation (GUTA) - Parallel Network Execution

The Decentralized Proving Network (DPN) takes End Cap proofs (and potentially other GUTA proofs like user registrations) from many users and aggregates them in parallel. This involves specialized GUTA circuits.

(Note: The provided files focus heavily on UPS and GUTA gadgets. The exact structure of the GUTA circuits using these gadgets is inferred but follows standard recursive proof aggregation patterns.)

Example GUTA Circuits (Inferred):

5. GUTAProcessEndCapCircuit (Hypothetical)

• Purpose: To take a user's validated UPSStandardEndCapCircuit proof and integrate its state change into the GUTA proof hierarchy.
• Core Logic: Uses VerifyEndCapProofGadget.
• What it Proves:
  • The End Cap proof is valid and used the correct circuit (known_end_cap_fingerprint_hash).
  • The checkpoint_tree_root claimed by the user in the End Cap result existed historically.
  • Outputs a standard GlobalUserTreeAggregatorHeader representing the user's GUSR tree state transition (start leaf hash -> end leaf hash at the user's ID index) and stats.
• Assumptions:
  • Witness (End Cap proof, result, stats, historical proof) is correct initially.
  • The known_end_cap_fingerprint_hash constant is correct.
  • A default_guta_circuit_whitelist root is provided or known.
• How Assumptions are Discharged: Verifies the End Cap proof and historical checkpoint proof. Packages the result into a standard GUTA header. The assumption about the default_guta_circuit_whitelist is passed upwards. The assumption about the current checkpoint_tree_root (from the historical proof) is passed upwards.
• Contribution to Horizontal Scalability: Allows individual user session results to be verified independently and prepared for parallel aggregation.
• High-Level Functionality: Validates and incorporates user end-of-session proofs into the global aggregation process.

6. GUTARegisterUserCircuit (Hypothetical)

• Purpose: To process the registration of one or more new users.
• Core Logic: Uses GUTAOnlyRegisterUsersGadget (which uses GUTARegisterUsersGadget, GUTARegisterUserFullGadget, GUTARegisterUserCoreGadget).
• What it Proves:
  • For each registered user, their public_key was correctly inserted at their user_id index in the GUSR tree (transitioning from zero hash to the new user leaf hash).
  • The public_key used matches an entry in the user_registration_tree_root.
  • Outputs a GlobalUserTreeAggregatorHeader representing the aggregate GUSR state transition for all registered users, with zero stats.
• Assumptions:
  • Witness (registration proofs, user count) is correct initially.
  • guta_circuit_whitelist and checkpoint_tree_root inputs are correct for this context.
  • default_user_state_tree_root constant is correct.
• How Assumptions are Discharged: Verifies delta proofs for GUSR insertion and Merkle proofs against the registration tree. Outputs a standard GUTA header, passing assumptions about whitelist/checkpoint upwards.
• Contribution to Horizontal Scalability: User registration can be batched and potentially processed in parallel branches of the GUTA tree.
• High-Level Functionality: Securely adds new users to the system state.

7. GUTAAggregationCircuit (Hypothetical - Multiple Variants)

• Purpose: To combine the results (headers) from two or more lower-level GUTA proofs (which could be End Cap results, registrations, or previous aggregations).
• Core Logic:
  • Verifies each input GUTA proof using VerifyGUTAProofGadget.
  • Ensures all input proofs used circuits from the same guta_circuit_whitelist and reference the same checkpoint_tree_root.
  • Combines the state_transitions from the input proofs:
    • If transitions are on different branches, uses TwoNCAStateTransitionGadget with an NCA proof.
    • If transitions are on the same branch (e.g., one input is a line proof output), connects them directly (old_root of current matches new_root of previous).
    • If only one input, uses GUTAHeaderLineProofGadget to propagate upwards.
  • Combines the stats from input proofs using GUTAStatsGadget.combine_with.
  • Outputs a single GlobalUserTreeAggregatorHeader representing the combined state transition and stats.
• What it Proves: That given valid input GUTA proofs operating under the same whitelist and checkpoint context, the combined state transition and stats represented by the output header are correct.
• Assumptions:
  • Witness (input proofs, headers, NCA/sibling proofs) is correct initially.
• How Assumptions are Discharged: Verifies input proofs and their headers. Verifies the logic of combining state transitions (NCA/Line/Direct). Passes the common whitelist/checkpoint root assumptions upwards.
• Contribution to Horizontal Scalability: This is the core of parallel aggregation. Multiple instances of this circuit run concurrently across the DPN, merging proof branches in a tree structure (like MapReduce).
• High-Level Functionality: Securely and recursively combines verified state changes from multiple sources into larger, aggregated proofs.

8. GUTANoChangeCircuit (Hypothetical)

• Purpose: To handle cases where no user state changed but the checkpoint advanced.
• Core Logic: Uses GUTANoChangeGadget.
• What it Proves: That given a new checkpoint_leaf verified to be in the checkpoint_tree_proof, the GUSR tree root remains unchanged, and stats are zero. Outputs a GUTA header reflecting this.
• Assumptions: Witness (checkpoint proof, leaf) is correct initially. Input guta_circuit_whitelist is correct.
• How Assumptions are Discharged: Verifies checkpoint proof. Outputs a standard GUTA header passing assumptions upward.
• Contribution to Horizontal Scalability: Allows the aggregation process to stay synchronized with the checkpoint tree even during periods of inactivity for certain state trees.
• High-Level Functionality: Advances the aggregated checkpoint state reference.

Phase 3: Final Block Proof

9. Checkpoint Tree "Block" Circuit (Top-Level Aggregation)

• Purpose: The final aggregation circuit that combines proofs from the roots of all major state trees (like GUSR via the top-level GUTA proof, GCON, etc.) for the block.
• Core Logic:
  • Verifies the top-level GUTA proof (and proofs for other top-level trees if applicable).
  • Takes the previous block's finalized CHKP root as a public input.
  • Constructs the new CHKP leaf based on the newly computed roots of GUSR, GCON, etc., and other block metadata.
  • Computes the new CHKP root.
  • The only external assumption verified here is that the input previous_block_chkp_root matches the actual finalized root of the last block.
• What it Proves: That the entire state transition for the block, represented by the change from the previous_block_chkp_root to the new_chkp_root, is valid, having recursively verified all constituent user transactions and aggregations according to protocol rules and circuit whitelists.
• Assumptions: The only remaining input assumption is the hash of the previous block's CHKP root.
• How Assumptions are Discharged: All assumptions from lower levels (circuit whitelists, internal state consistencies) have been verified recursively. The final link to the previous block state is checked against the public input.
• Contribution to Horizontal Scalability: Represents the culmination of the massively parallel aggregation process, producing a single, succinct proof for the entire block's validity.
• High-Level Functionality: Creates the final, verifiable proof of state transition for the entire block, linking it cryptographically to the previous block. This proof can be efficiently verified by any node or light client.

Proving Jobs Architecture

Overview

This document describes the proving jobs architecture for both Realm and Coordinator processors, including the tree structure of different proof types and their public inputs layout.

Public Inputs Layout Standard

IMPORTANT: Different circuit types have different public inputs layouts!

Coordinator Main Circuits (19 inputs)

• [0..4]: commitment
• [4..8]: worker_public_key
• [8..11]: pm_jobs_completed_stats (deploy_contracts_completed, register_users_completed, gutas_completed)
• [11..15]: circuit_whitelist_root
• [15..19]: state_transition_hash

GUTA Circuits (15 inputs)

• [0..4]: commitment
• [4..8]: worker_public_key
• [8..11]: pm_jobs_completed_stats
• [11..15]: guta_header_hash

Special: AggUserRegistrationDeployContractsGUTA (19 inputs)

• [0..4]: state_transition_hash (NOT commitment!)
• [4..8]: hash(user_registration_commitment, user_registration_worker_pk)
• [8..12]: hash(deploy_contracts_commitment, deploy_contracts_worker_pk)
• [12..16]: hash(guta_commitment, guta_worker_pk)
• [16..19]: additional data

Realm Proving Jobs

User Operations Tree

graph TB
    subgraph "User Operations Leaves"
        UO1[UserOp 1<br/>Circuit: ProcessUserOp]
        UO2[UserOp 2<br/>Circuit: ProcessUserOp]
        UO3[UserOp 3<br/>Circuit: ProcessUserOp]
        UON[UserOp N<br/>Circuit: ProcessUserOp]
    end

    subgraph "Aggregation Layer"
        AGG1[Aggregate UserOps<br/>Circuit: AggregateUserOps]
        AGG2[Aggregate UserOps<br/>Circuit: AggregateUserOps]
    end

    subgraph "Root"
        ROOT[Realm State Transition<br/>Circuit: RealmStateTransition]
    end

    UO1 --> AGG1
    UO2 --> AGG1
    UO3 --> AGG2
    UON --> AGG2
    AGG1 --> ROOT
    AGG2 --> ROOT

Realm Circuit Details

Coordinator Proving Jobs

Three Main Trees + Final Aggregation

graph TB
    subgraph "GUTA Tree"
        subgraph "GUTA Leaves"
            GUTA1[Realm GUTA 1]
            GUTA2[Realm GUTA 2]
            GUTAN[Realm GUTA N]
        end

        subgraph "GUTA Aggregation"
            GUTA_AGG1[GUTATwoGUTA]
            GUTA_AGG2[GUTATwoGUTA]
            GUTA_CAP[GUTAVerifyToCap<br/>Optional]
        end

        GUTA1 --> GUTA_AGG1
        GUTA2 --> GUTA_AGG1
        GUTAN --> GUTA_AGG2
        GUTA_AGG1 --> GUTA_CAP
        GUTA_AGG2 --> GUTA_CAP
    end

    subgraph "Register Users Tree"
        subgraph "Register Users Leaves"
            RU1[Batch 1<br/>Circuit: BatchAppendUserRegistrationTree]
            RU2[Batch 2<br/>Circuit: BatchAppendUserRegistrationTree]
            RUN[Batch N<br/>Circuit: BatchAppendUserRegistrationTree]
        end

        subgraph "Register Users Aggregation"
            RU_AGG1[Circuit: AggStateTransition]
            RU_AGG2[Circuit: AggStateTransition]
            RU_ROOT[Root Aggregation<br/>Circuit: AggStateTransition]
        end

        RU1 --> RU_AGG1
        RU2 --> RU_AGG1
        RUN --> RU_AGG2
        RU_AGG1 --> RU_ROOT
        RU_AGG2 --> RU_ROOT
    end

    subgraph "Deploy Contracts Tree"
        subgraph "Deploy Contracts Leaves"
            DC1[Batch 1<br/>Circuit: BatchDeployContracts]
            DC2[Batch 2<br/>Circuit: BatchDeployContracts]
            DCN[Batch N<br/>Circuit: BatchDeployContracts]
        end

        subgraph "Deploy Contracts Aggregation"
            DC_AGG1[Circuit: AggStateTransition]
            DC_AGG2[Circuit: AggStateTransition]
            DC_ROOT[Root Aggregation<br/>Circuit: AggStateTransition]
        end

        DC1 --> DC_AGG1
        DC2 --> DC_AGG1
        DCN --> DC_AGG2
        DC_AGG1 --> DC_ROOT
        DC_AGG2 --> DC_ROOT
    end

    subgraph "Final Aggregation"
        STATE_PART_1[State Part 1<br/>Circuit: AggUserRegistrationDeployContractsGUTA]
        CHECKPOINT[Checkpoint State Transition<br/>Circuit: CheckpointStateTransition]
    end

    GUTA_CAP --> STATE_PART_1
    RU_ROOT --> STATE_PART_1
    DC_ROOT --> STATE_PART_1
    STATE_PART_1 --> CHECKPOINT

GUTA Circuit Variants

The GUTA (Global User Tree Aggregator) has multiple circuit variants to handle different scenarios:

GUTA Circuit Types and Usage

graph LR
    subgraph "Leaf Circuits (No Child Proofs)"
        GNC[GUTANoChange<br/>No state changes]
        GSE[GUTASingleEndCap<br/>Single realm update]
        GOR[GUTAOnlyRegisterUsers<br/>Only user registrations]
        GRU[GUTARegisterUsers<br/>With user ops]
    end

    subgraph "Two Children Aggregation"
        GTG[GUTATwoGUTA<br/>Two GUTA proofs]
        GTE[GUTATwoEndCap<br/>Two EndCap proofs]
        GLR[GUTALeftGUTARightEndCap<br/>GUTA + EndCap]
        GLE[GUTALeftEndCapRightGUTA<br/>EndCap + GUTA]
    end

    subgraph "Special Purpose"
        GVC[GUTAVerifyToCap<br/>Verify to tree cap]
    end

GUTA Circuit Details

Additional GUTA Circuits

Other GUTA circuits (also 15 inputs, same layout):

• GUTANoChange: No state changes
• GUTATwoEndCap: Aggregate two EndCap proofs
• GUTAVerifyToCap: Verify GUTA to tree cap
• GUTATwoGUTAWithCheckpointUpgrade: Two GUTA with checkpoint upgrade
• GUTAVerifyToCapWithCheckpointUpgrade: Verify to cap with checkpoint upgrade

All follow the same commitment calculation rules based on their dependency count.

State Part 1 (AggUserRegistrationDeployContractsGUTA)

This circuit aggregates the three main trees:

Inputs

• Register Users proof (from aggregation root)
• Deploy Contracts proof (from aggregation root)
• GUTA proof (from aggregation root or GUTAVerifyToCap)

Public Inputs Layout (19 total) - SPECIAL LAYOUT!

WARNING: This circuit has a unique layout different from other circuits!

• [0..4]: state_transition_hash (NOT commitment!)
• [4..8]: hash(register_users_commitment, register_users_worker_pk)
• [8..12]: hash(deploy_contracts_commitment, deploy_contracts_worker_pk)
• [12..16]: hash(guta_commitment, guta_worker_pk)
• [16..19]: additional data

How Child Proofs Are Processed

#![allow(unused)]
fn main() {
// Extract from each child proof:
let user_registration_commitment = child_proof.public_inputs[0..4];
let user_registration_worker_pk = child_proof.public_inputs[4..8];
let user_registration_final = hash(commitment, worker_pk);

// This final hash goes into parent's public_inputs[4..8]
}

PM Rewards Commitment

The PM (Prover/Miner) Rewards Commitment is calculated from these three roots:

#![allow(unused)]
fn main() {
PMRewardCommitment {
    register_users_root,
    deploy_contracts_root,
    gutas_root,
}
}

Checkpoint State Transition

The final circuit that creates the checkpoint proof:

Inputs

• State Part 1 proof
• Previous checkpoint proof
• Checkpoint tree merkle proof
• Various metadata (block time, random seed, etc.)

Public Inputs Layout (19 inputs total)

• [0..4]: commitment
• [4..8]: worker_public_key
• [8..11]: pm_jobs_completed_stats (from State Part 1 proof)
• [11..15]: old_checkpoint_tree_root
• [15..19]: new_checkpoint_tree_root

Job Dependencies and Task Graph

graph LR
    subgraph "Parallel Execution"
        RU[Register Users Jobs<br/>PM Stats: (0, N, 0)]
        DC[Deploy Contracts Jobs<br/>PM Stats: (M, 0, 0)]
        GUTA[GUTA Jobs<br/>PM Stats: (0, 0, K)]
    end

    subgraph "Sequential Dependencies"
        SP1[State Part 1<br/>PM Stats: (M, N, K)]
        CST[Checkpoint State Transition<br/>PM Stats: (M, N, K)]
        NOTIFY[Notify Block Complete]
    end

    RU --> SP1
    DC --> SP1
    GUTA --> SP1
    SP1 --> CST
    CST --> NOTIFY

The dependency graph shows how PM stats flow through the system:

1. Parallel Trees: Each tree type accumulates its specific job counts
2. State Part 1: Combines PM stats from all three trees
3. Checkpoint: Preserves the combined PM stats for final reward calculation
4. Block Completion: Uses PM stats to calculate and distribute rewards

Commitment Calculation Rules

The commitment calculation follows a consistent pattern across all circuits:

1. Leaf Circuits (No Dependencies)

#![allow(unused)]
fn main() {
commitment = worker_public_key
}

Examples: GUTANoChange, GUTAOnlyRegisterUsers, BatchDeployContracts, AppendUserRegistrationTree

2. Single Dependency Circuits (One Child Proof)

#![allow(unused)]
fn main() {
commitment = hash(child.commitment, worker_public_key)
}

Examples: GUTASingleEndCap, GUTARegisterUsers, GUTAVerifyToCap, GUTAVerifyToCapWithCheckpointUpgrade

3. Two Dependencies Circuits (Two Child Proofs)

#![allow(unused)]
fn main() {
commitment = hash(hash(left.commitment, right.commitment), worker_public_key)
}

Examples: GUTATwoGUTA, GUTATwoGUTAWithCheckpointUpgrade, GUTATwoEndCap, GUTALeftGUTARightEndCap, AggStateTransition

Core Design Principles

1. Commitment Chain: Forms a tree structure but NOT for reward distribution as originally thought

   • ALL leaf circuits: commitment = hash(0, 0) (constant value!)
   • Aggregation circuits: commitment = hash(hash(child1.commit, child1.worker), hash(child2.commit, child2.worker))

2. Job Categories: Three parallel proving trees

   • User Registration: batch_append → state_transition → final aggregation
   • Contract Deployment: batch_deploy → state_transition → final aggregation
   • GUTA Tree: Various GUTA circuits → final aggregation

3. Special Cases:

   • Dummy circuits: Used when no real work is available
   • AggUserRegistration: Unique layout combining all three trees
   • Checkpoint: Final proof creating the rollup state transition

Core Proving Circuits

Coordinator Main Circuits (19 inputs)

Public Inputs Layout (19 total):

• [0..4]: commitment
• [4..8]: worker_public_key
• [8..11]: pm_jobs_completed_stats
• [11..15]: circuit_whitelist
• [15..19]: state_transition_hash

GUTA Core Circuits (15 inputs)

Public Inputs Layout (15 total):

• [0..4]: commitment
• [4..8]: worker_public_key
• [8..11]: pm_jobs_completed_stats
• [11..15]: guta_header_hash

Final Aggregation Circuits

PM Jobs Completed Stats Tracking

The PM (Proof Miner) jobs completed stats track the number of different types of jobs completed throughout the circuit hierarchy. These stats flow upward through the trees and are combined at aggregation points.

PM Stats Components

• deploy_contracts_completed: Number of deploy contract jobs completed in this subtree
• register_users_completed: Number of user registration jobs completed in this subtree
• gutas_completed: Number of GUTA jobs completed in this subtree

How Stats Flow Through the Hierarchy

Leaf Circuits

Leaf circuits initialize their PM stats based on the work they perform:

• Deploy Contract leaves (BatchDeployContracts): pm_stats = (batch_size, 0, 0)
• Register Users leaves (AppendUserRegistrationTree): pm_stats = (0, batch_size, 0)
• GUTA leaves (GUTANoChange, GUTASingleEndCap, etc.): pm_stats = (0, 0, 0) initially
• Dummy circuits (AggStateTransitionDummy): pm_stats = (0, 0, 0) (all zeros)

Aggregation Circuits

Aggregation circuits combine PM stats from their children:

#![allow(unused)]
fn main() {
// Two children aggregation (AggStateTransition, GUTATwoGUTA)
final_pm_stats = PMJobsCompletedStats {
    deploy_contracts_completed: left.pm_stats[0] + right.pm_stats[0],
    register_users_completed: left.pm_stats[1] + right.pm_stats[1],
    gutas_completed: left.pm_stats[2] + right.pm_stats[2],
}
}

GUTA Circuits Special Handling

GUTA circuits add 1 to their gutas_completed count:

#![allow(unused)]
fn main() {
// Single child GUTA aggregation (GUTAVerifyToCap)
final_pm_stats = PMJobsCompletedStats {
    deploy_contracts_completed: child.pm_stats[0],
    register_users_completed: child.pm_stats[1],
    gutas_completed: child.pm_stats[2] + 1, // Add 1 GUTA completion
}
}

Final Aggregation

At the State Part 1 level (AggUserRegistrationDeployContractsGUTA), the PM stats from all three trees are combined:

#![allow(unused)]
fn main() {
final_pm_stats = register_users_proof.pm_stats +
                 deploy_contracts_proof.pm_stats +
                 guta_proof.pm_stats
}

This provides a complete count of all work performed in the current checkpoint.

Key Design Principles

1. Consistent Public Inputs: All circuits follow the same [commitment, worker_public_key, pm_jobs_completed_stats, data_hash] layout
2. Tree Aggregation: Each category (GUTA, Register Users, Deploy Contracts) forms its own tree
3. Parallel Processing: The three trees can be processed in parallel
4. Commitment Chain: Commitments flow up from leaves to root, enabling reward distribution
5. Flexibility: GUTA circuits handle various scenarios (no changes, single realm, multiple realms)
6. Worker Tracking: Every circuit includes the worker's public key who computed that proof
7. PM Stats Tracking: Job completion counts flow upward through the tree hierarchy for reward calculation

Introduction

This is the documentation for [Psy Smart Contract Language], a new programming language designed for ["safe and efficient smart contract development"]. This book serves as a comprehensive guide for developers interested in learning the language and building applications with it.

[Psy Smart Contract Language] is in active development and a work in progress. If you have feedback or suggestions, feel free to contribute via the GitHub repository.

This book covers the core features of [Psy Smart Contract Language], including its syntax, module system, structs, traits, and storage capabilities.

Design Philosophy

Psy Smart Contract Language embodies a unique design philosophy specifically crafted for zero-knowledge proof systems. While drawing inspiration from modern languages like Jakt, Noir, Sway, and Cairo, Psy takes a fundamentally different approach optimized for circuit generation.

Core Design Principles

ZK-Native Architecture

Unlike traditional virtual machines that operate on stacks and registers, Psy compiles to DPN opcodes optimized for zkVM execution. Our primary goal is to generate efficient opcodes that produce minimal circuits during proof generation, which directly translates to:

• Faster proof generation
• Lower computational overhead
• Reduced memory requirements
• Improved scalability

Symbolic Execution Model

At the heart of Psy's design lies symbolic execution rather than traditional runtime execution:

#![allow(unused)]
fn main() {
// Traditional VM approach - Simple addition
// Requires multiple stack/register operations
fn add_numbers(a: Felt, b: Felt) -> Felt {
    a + b
}
// VM execution steps:
// 1. PUSH a               (push 'a' onto stack)
// 2. PUSH b               (push 'b' onto stack)  
// 3. POP R2               (pop 'b' into register R2)
// 4. POP R1               (pop 'a' into register R1)
// 5. ADD R3, R1, R2       (add R1 + R2, store in R3)
// 6. PUSH R3              (push result back to stack)
// 7. POP result           (pop final result)
// Total: 7 VM operations + stack/register management overhead

// Psy's symbolic execution approach  
// Converts directly to a single ZK constraint
fn add_numbers(a: Felt, b: Felt) -> Felt {
    a + b  // Single arithmetic gate: result = a + b
}
// Circuit: 1 addition constraint, no VM overhead
}

Function-to-Symbol Transformation

Every function in a Psy smart contract is transformed into a mathematical symbol or constraint system:

1. Variables become circuit wires
2. Operations become arithmetic gates
3. Control flow is flattened into conditional execution using boolean arithmetic
4. State changes become constraint updates on state variables

Control Flow Flattening Example

#![allow(unused)]
fn main() {
// Psy source code with branching
fn min(a: Felt, b: Felt) -> Felt {
    if a < b {
        a
    } else {
        b
    }
}

// Compiler flattens to conditional arithmetic (no dynamic jumps)
// Both paths computed, result selected using boolean arithmetic:
fn min_flattened(a: Felt, b: Felt) -> Felt {
    let condition = (a < b) as Felt;  // 1 if true, 0 if false
    let true_path = a;
    let false_path = b;
    // Arithmetic selection instead of branching:
    condition * true_path + (1 - condition) * false_path
}
}

This transforms if (a > 1) { execute_branch() } into:

condition = (a > 1) as Felt;  // 0 or 1
execution_weight = condition;
no_execution_weight = 1 - condition;
// Both branches computed, weighted by condition

Architectural Differences from Traditional Languages

Control Flow Flattening

Traditional programming languages use dynamic control flow with jumps and branches. Psy flattens all control structures at compile time:

If-Else Flattening

#![allow(unused)]
fn main() {
// Source code
fn conditional_logic(condition: bool, a: Felt, b: Felt) -> Felt {
    if condition {
        a + b
    } else {
        a * b
    }
}

// Flattened to circuit constraints
fn conditional_logic(condition: bool, a: Felt, b: Felt) -> Felt {
    let condition_felt = condition as Felt;
    let sum = a + b;
    let product = a * b;
    // Select result based on condition using arithmetic
    sum * condition_felt + product * (1 - condition_felt)
}
}

Loop Unrolling

#![allow(unused)]
fn main() {
// Source code with bounded loop (simplified fibonacci)
fn fibonacci_partial() -> Felt {
    let mut a: Felt = 2;
    let mut b: Felt = 3;
    let mut i: Felt = 2;
    while i <= 5 {  // Fixed bound of 3 iterations
        let next = a + b;
        a = b;
        b = next;
        i += 1;
    }
    b
}

// Completely unrolled at compile time (3 iterations)
fn fibonacci_partial_unrolled() -> Felt {
    // Initial state
    let mut a_0: Felt = 2;
    let mut b_0: Felt = 3;
    let mut i_0: Felt = 2;
    
    // Iteration 1: i = 2, condition (2 <= 5) = true
    let next_1 = a_0 + b_0;  // 5
    let a_1 = b_0;           // 3
    let b_1 = next_1;        // 5
    let i_1 = i_0 + 1;       // 3
    
    // Iteration 2: i = 3, condition (3 <= 5) = true  
    let next_2 = a_1 + b_1;  // 8
    let a_2 = b_1;           // 5
    let b_2 = next_2;        // 8
    let i_2 = i_1 + 1;       // 4
    
    // Iteration 3: i = 4, condition (4 <= 5) = true
    let next_3 = a_2 + b_2;  // 13
    let a_3 = b_2;           // 8  
    let b_3 = next_3;        // 13
    let i_3 = i_2 + 1;       // 5
    
    // Iteration 4: i = 5, condition (5 <= 5) = true
    let next_4 = a_3 + b_3;  // 21
    let a_4 = b_3;           // 13
    let b_4 = next_4;        // 21
    let i_4 = i_3 + 1;       // 6
    
    // Iteration 5: i = 6, condition (6 <= 5) = false - exit
    b_4  // Return 21
}
}

No Runtime Stack or Registers

Traditional VMs maintain:

• Call stack for function invocation
• Registers for temporary values
• Memory management with allocation/deallocation

Psy optimizes this by:

• Static analysis of all possible execution paths
• Compile-time memory layout determination
• Compilation to DPN opcodes which are executed by zkVM to generate contract call proofs

Inline Function Calls by Default

Unlike traditional VMs that use call stacks, Psy inlines all function calls by default. Each function is compiled to its own set of DPN opcodes:

// Source code with nested function calls (from actual test)
fn add(a: Felt, b: Felt) -> Felt {
    let mut c: Felt = a + b;
    return c;
}

fn mul(a: Felt, b: Felt) -> Felt {
    let mut c: Felt = a * b;
    return c;
}

fn main() {
    // Complex nested function calls
    let mut f: Felt = add(add(1, 2), 2);        // add() called twice, nested
    let mut g: Felt = add(1 + 3, mul(2, 3));    // add() and mul() calls
}

// Each function generates its own DPN opcode sequence:
// add() -> [Constant(a), Constant(b), Add, InputTarget] opcodes
// mul() -> [Constant(x), Constant(y), Mul, InputTarget] opcodes  

// At compilation, all calls are inlined:
fn main_inlined() {
    // add(add(1, 2), 2) becomes completely flattened:
    // Inner add(1, 2):
    // - Constant(1), Constant(2), Add -> temp1 = 3
    // Outer add(temp1, 2): 
    // - Constant(3), Constant(2), Add -> f = 5
    
    // add(1 + 3, mul(2, 3)) becomes:
    // mul(2, 3):
    // - Constant(2), Constant(3), Mul -> temp2 = 6
    // add(4, temp2):
    // - Constant(4), Constant(6), Add -> g = 10
}

Benefits of Default Inlining:

• No call overhead - eliminates stack push/pop operations
• Better optimization - enables cross-function optimizations
• Predictable circuit size - function calls don't add dynamic overhead
• Simplified analysis - all execution paths are statically visible

Circuit-First Design Benefits

Predictable Circuit Size

Since all control flow is flattened at compile time, developers can predict exact circuit sizes:

#![allow(unused)]
fn main() {
// Circuit size is deterministic
fn deterministic_function(x: Felt, y: Felt) -> Felt {
    // Always exactly 3 arithmetic gates
    let intermediate = x + y;      // 1 gate
    let result = intermediate * 2;  // 1 gate  
    result + 1                     // 1 gate
}
}

Optimized Constraint Systems

The compiler can perform aggressive optimizations specific to arithmetic circuits:

• Gate merging - Combine multiple operations
• Constant propagation - Eliminate unnecessary constraints
• Dead code elimination - Remove unused circuit paths
• Algebraic simplification - Reduce constraint complexity

Zero-Knowledge Friendly Primitives

Psy provides built-in primitives that map directly to efficient ZK operations:

#![allow(unused)]
fn main() {
// Poseidon hash - ZK-friendly cryptographic hash
fn hash_example() -> Hash {
    let data: Hash = [1, 2, 3, 4];
    hash(data)  // Built-in Poseidon hash function
}

// ECDSA signature verification using secp256k1
fn signature_verification() -> bool {
    let pub_key = [4203227662u32, 540940946u32, 962567723u32, 1830567167u32, 
                   3450763808u32, 3950740017u32, 3026903052u32, 3029228469u32, 
                   1837759160u32, 825683440u32, 3630293783u32, 436568768u32, 
                   3543321651u32, 1044682747u32, 168350425u32, 936127172u32];
    
    let sig = [201339544u32, 2533129003u32, 3911198242u32, 2163032835u32, 
               2488559593u32, 2971164201u32, 3572923983u32, 3650316646u32, 
               3964687905u32, 1624041662u32, 2373224611u32, 3243422930u32, 
               1353934640u32, 2321957132u32, 2691932396u32, 1560388502u32];
    
    let msg = [6716978020874491267, 18326158388222717469, 
               7113070761591959818, 9714795267687279217];
    
    let signature_is_valid = __secp256k1_verify(pub_key, msg, sig);
    assert(signature_is_valid, "signature is not valid");
    signature_is_valid
}

// Example: Combining both primitives for authenticated operations
fn authenticated_hash(input_data: Hash, pub_key: [u32; 16], msg: [u64; 4], sig: [u32; 16]) -> Hash {
    // Verify signature first
    let signature_is_valid = __secp256k1_verify(pub_key, msg, sig);
    assert(signature_is_valid, "Invalid signature");
    
    // Then hash the authenticated data
    hash(input_data)
}
}

Language Design Trade-offs

What We Gain

• Minimal circuit overhead
• Predictable performance
• Formal verification friendly
• Optimal proof generation

What We Accept

• Static loop bounds (no dynamic iteration)
• Compile-time complexity for circuit optimization
• Limited recursion (must be bounded and unrollable)
• Circuit-aware programming model

Language Syntax Design

Psy adopts a Rust-like syntax that provides familiarity for developers while being optimized for ZK circuit compilation:

#![allow(unused)]
fn main() {
// Familiar Rust-style struct definitions
pub struct Person {
    pub age: Felt,
    male: bool,
}

// Rust-style implementations
impl Person {
    pub fn get_age(self: Person) -> Felt {
        return self.age;
    }
}

// Rust-style function definitions with type annotations
fn add_numbers(a: Felt, b: Felt) -> Felt {
    a + b
}

// Rust-style control flow
fn conditional_min(a: Felt, b: Felt) -> Felt {
    if a < b {
        a
    } else {
        b
    }
}
}

This familiar syntax reduces the learning curve while the compiler performs ZK-specific optimizations behind the scenes.

The Psy Innovation

Psy's unique contribution is ZK-optimized compilation through symbolic execution. By treating smart contract functions as mathematical transformations and compiling to DPN opcodes, we achieve:

1. Optimized DPN opcode generation for zkVM execution
2. Efficient proof generation for contract calls
3. Predictable circuit characteristics
4. Streamlined ZK proving pipeline

This design philosophy makes Psy particularly suitable for applications where proof generation speed and circuit size are critical, such as high-frequency DeFi operations, privacy-preserving computations, and scalable rollup systems.

Looking Forward

As the ZK ecosystem evolves, Psy's circuit-first design positions it to take advantage of new developments in:

• Advanced circuit optimizations
• Hardware acceleration
• Recursive proof systems
• Cross-chain interoperability

The symbolic execution model ensures that improvements in the underlying proof systems automatically benefit all Psy programs without requiring language-level changes.

Language Features

Psy Smart Contract Language provides a comprehensive set of features designed for zero-knowledge circuit development. This page outlines all major language features with examples and explanations.

Basic Types

Psy supports a range of primitive and composite types optimized for ZK circuit generation.

Primitive Types

Felt

The fundamental numeric type representing a field element in the Goldilocks field.

#![allow(unused)]
fn main() {
let value: Felt = 42;
let negative: Felt = -10;
let arithmetic: Felt = value + negative * 2;
}

Boolean

Boolean values for logical operations.

#![allow(unused)]
fn main() {
let flag: bool = true;
let condition: bool = false;
let result: bool = flag && !condition;
}

u32

32-bit unsigned integer type for efficient arithmetic operations.

#![allow(unused)]
fn main() {
let count: u32 = 100u32;
let mask: u32 = 0xFFFFu32;
let shifted: u32 = count << 2;
}

Composite Types

Arrays

Fixed-size arrays with compile-time known lengths.

#![allow(unused)]
fn main() {
let numbers: [Felt; 4] = [1, 2, 3, 4];
let matrix: [[Felt; 2]; 2] = [[1, 2], [3, 4]];
let element: Felt = numbers[0];
}

Tuples

Heterogeneous collections of values with full support for nesting, mutation, and complex access patterns.

#![allow(unused)]
fn main() {
// Basic tuple creation and access
let pair: (Felt, bool) = (42, true);
let triple: (Felt, Felt, bool) = (1, 2, false);
let first: Felt = pair.0;
let flag: bool = pair.1;

// Mutable tuples
let mut coordinates: (Felt, Felt) = (10, 20);
coordinates.0 = 15;  // Modify x coordinate
coordinates.1 = 25;  // Modify y coordinate
coordinates = (30, 40);  // Replace entire tuple

// Nested tuples
let nested: ((Felt, Felt), (Felt, Felt)) = ((1, 2), (3, 4));
let deeply_nested: (((Felt, Felt), Felt), Felt) = (((5, 6), 7), 8);

// Complex nested tuple manipulation
let mut complex_tuple: ((Felt, Felt), (Felt, Felt)) = ((9, 10), (11, 12));
complex_tuple.0.1 = 42;     // Modify first tuple's second element
complex_tuple.1 = (20, 21); // Replace entire second tuple

// Tuples in structs
struct TupleHolder {
    pub pair: (Felt, Felt),
    pub nested: ((Felt, Felt), Felt),
}

let mut holder: TupleHolder = new TupleHolder {
    pair: (22, 23),
    nested: ((24, 25), 26),
};
holder.pair.1 = 99;          // Modify tuple field in struct
holder.nested.0.0 = 88;      // Modify nested tuple in struct

// Functions returning tuples
fn create_tuple(x: Felt, y: Felt) -> (Felt, Felt) {
    (x + 1, y + 1)
}

// Functions taking tuples as parameters
fn sum_tuple(input: (Felt, Felt)) -> Felt {
    input.0 + input.1
}

let result_tuple: (Felt, Felt) = create_tuple(30, 31);
let sum_result: Felt = sum_tuple((40, 50));

// Tuples with different types
let mixed: (Felt, bool, u32) = (100, true, 42u32);
let complex_mixed: ((Felt, bool), (u32, Felt)) = ((1, false), (10u32, 2));
}

Tuple Features:

• Type Safety: Each tuple element has a specific type
• Indexed Access: Use .0, .1, .2, etc. to access elements
• Mutation Support: Both individual elements and entire tuples can be modified
• Arbitrary Nesting: Tuples can contain other tuples to any depth
• Function Integration: Can be passed to and returned from functions
• Struct Fields: Tuples can be used as struct field types

Note: Tuple destructuring (pattern matching like let (x, y) = tuple) is not currently supported, but individual element access provides full functionality.

Structs

User-defined composite types with named fields.

#![allow(unused)]
fn main() {
pub struct Person {
    pub age: Felt,
    male: bool,
}

let person: Person = new Person {
    age: 25,
    male: true,
};
}

Hash Type

Special 4-element array type for cryptographic operations.

#![allow(unused)]
fn main() {
let data: Hash = [1, 2, 3, 4];
let result: Hash = hash(data);
}

Functions

Functions are first-class citizens with support for parameters, return types, and inlining.

Basic Functions

#![allow(unused)]
fn main() {
fn add(a: Felt, b: Felt) -> Felt {
    a + b
}

fn greet() {
    // No return value
}
}

Function Calls and Inlining

All function calls are inlined by default for optimal circuit generation.

#![allow(unused)]
fn main() {
fn multiply(x: Felt, y: Felt) -> Felt {
    x * y
}

fn complex_calculation(a: Felt, b: Felt, c: Felt) -> Felt {
    // These calls get inlined at compile time
    let product = multiply(a, b);
    add(product, c)
}
}

Closures

Anonymous functions that can capture variables from their environment.

fn main() -> Felt {
    let multiplier: Felt = 3;
    
    let triple = |x: Felt| -> Felt {
        x * multiplier  // Captures 'multiplier' from environment
    };
    
    triple(5)  // Returns 15
}

Constants

Compile-time constant values for improved optimization.

#![allow(unused)]
fn main() {
const MAX_USERS: Felt = 1000;
const PI_APPROXIMATION: Felt = 3141;
const DEFAULT_AMOUNT: Felt = 100;

fn validate_user_count(count: Felt) -> bool {
    count <= MAX_USERS
}

fn calculate_with_constant() -> Felt {
    DEFAULT_AMOUNT + PI_APPROXIMATION
}
}

Comptime

Compile-time evaluation for constant folding and optimization.

#![allow(unused)]
fn main() {
// Complex constant expressions are evaluated at compile time
const COMPLEX_CALC: Felt = ((100 + 200) * 3 - 50) / 2 + (10 * 10);

fn use_constants() -> Felt {
    // All constant arithmetic is folded during compilation
    COMPLEX_CALC + 42
}
}

Control Flow

If Expressions

Conditional expressions that are flattened into arithmetic selection during compilation.

#![allow(unused)]
fn main() {
fn min(a: Felt, b: Felt) -> Felt {
    if a < b {
        a
    } else {
        b
    }
}

// Supports complex nested conditions
fn classify_number(x: Felt) -> Felt {
    if x > 100 {
        if x > 1000 {
            3  // Very large
        } else {
            2  // Large
        }
    } else {
        1  // Small
    }
}
}

Block Expressions

Scoped code blocks that return values.

#![allow(unused)]
fn main() {
fn calculate() -> Felt {
    let result = {
        let temp1 = 10;
        let temp2 = 20;
        temp1 + temp2  // Block returns this value
    };
    result * 2
}
}

Match Expressions

Pattern matching for control flow.

#![allow(unused)]
fn main() {
fn process_status(status: Felt) -> Felt {
    match status {
        0 => 10,        // Pending
        1 => 20,        // Processing  
        2 => 30,        // Complete
        _ => 0,         // Unknown
    }
}
}

Loops

Bounded loops that are completely unrolled at compile time.

#![allow(unused)]
fn main() {
fn sum_range() -> Felt {
    let mut total: Felt = 0;
    let mut i: Felt = 1;
    
    while i <= 5 {  // Fixed bound - unrolled at compile time
        total += i;
        i += 1;
    }
    
    total  // Returns 15
}
}

Modules

Code organization and namespace management.

Module Definition

#![allow(unused)]
fn main() {
mod math {
    pub fn add(a: Felt, b: Felt) -> Felt {
        a + b
    }
    
    fn private_helper() -> Felt {
        42
    }
}
}

Module Usage

use math::*;

fn main() -> Felt {
    add(10, 20)  // Using imported function
}

Nested Modules

#![allow(unused)]
fn main() {
mod crypto {
    pub mod hash {
        pub fn poseidon(input: Hash) -> Hash {
            hash(input)
        }
    }
    
    pub mod signature {
        pub fn verify(msg: [u64; 4], sig: [u32; 16], pubkey: [u32; 16]) -> bool {
            __secp256k1_verify(pubkey, msg, sig)
        }
    }
}
}

Traits

Interface definitions for shared behavior across types.

Basic Traits

#![allow(unused)]
fn main() {
pub trait Arithmetic {
    fn add(self, other: Self) -> Self;
    fn multiply(self, other: Self) -> Self;
}

pub trait Display {
    fn show(self) -> Felt;
}
}

Trait Implementation

#![allow(unused)]
fn main() {
struct Point {
    x: Felt,
    y: Felt,
}

impl Arithmetic for Point {
    fn add(self, other: Point) -> Point {
        new Point {
            x: self.x + other.x,
            y: self.y + other.y,
        }
    }
    
    fn multiply(self, other: Point) -> Point {
        new Point {
            x: self.x * other.x,
            y: self.y * other.y,
        }
    }
}
}

Generics

Type parameters for code reuse and type safety.

Generic Functions

#![allow(unused)]
fn main() {
fn identity<T>(value: T) -> T {
    value
}

fn pair<T, U>(first: T, second: U) -> (T, U) {
    (first, second)
}
}

Generic Structs

#![allow(unused)]
fn main() {
struct Container<T> {
    value: T,
}

impl<T> Container<T> {
    pub fn new(value: T) -> Container<T> {
        new Container { value }
    }
    
    pub fn get(self) -> T {
        self.value
    }
}
}

Generic Traits

#![allow(unused)]
fn main() {
trait Convert<T> {
    fn convert(self) -> T;
}

impl Convert<Felt> for u32 {
    fn convert(self) -> Felt {
        self as Felt
    }
}
}

Type System Features

Type Checking

Static type checking ensures type safety at compile time.

#![allow(unused)]
fn main() {
fn type_safe_function(x: Felt, y: bool) -> (Felt, bool) {
    // Compiler verifies all types match
    let result_x: Felt = x + 1;      // ✓ Felt arithmetic
    let result_y: bool = y && true;  // ✓ Boolean logic
    (result_x, result_y)
}
}

Type Hints

Explicit type annotations for clarity and optimization.

#![allow(unused)]
fn main() {
fn with_type_hints() {
    let inferred = 42;              // Type inferred as Felt
    let explicit: Felt = 42;        // Explicit type annotation
    let tuple: (Felt, bool) = (1, true);  // Tuple type hint
}
}

Trait Constraints

Generic type constraints using trait bounds.

#![allow(unused)]
fn main() {
fn generic_add<T: Arithmetic>(a: T, b: T) -> T {
    a.add(b)  // T must implement Arithmetic trait
}

fn display_value<T: Display + Clone>(value: T) -> Felt {
    value.show()  // T must implement both Display and Clone
}
}

Storage and Smart Contracts

Persistent state management for blockchain applications.

Storage Structs

#![allow(unused)]
fn main() {
#[storage]
struct TokenContract {
    // Contract state fields
}

impl TokenContract {
    pub fn mint(amount: Felt) -> Felt {
        let user_id = get_user_id();
        let current_state = get_state_hash_at(user_id);
        let current_balance = current_state[0];
        
        let new_balance = current_balance + amount;
        cset_state_hash_at(user_id, [new_balance, current_state[1], current_state[2], current_state[3]]);
        
        new_balance
    }
}
}

Built-in Functions

ZK-optimized cryptographic and system functions.

Cryptographic Functions

#![allow(unused)]
fn main() {
// Poseidon hash
let data: Hash = [1, 2, 3, 4];
let hash_result: Hash = hash(data);

// ECDSA signature verification
let pubkey = [/* 16 u32 values */];
let message = [/* 4 u64 values */];  
let signature = [/* 16 u32 values */];
let is_valid: bool = __secp256k1_verify(pubkey, message, signature);
}

System Functions

#![allow(unused)]
fn main() {
// State access functions
let user_id: Felt = get_user_id();
let contract_id: Felt = get_contract_id();
let checkpoint: Felt = get_checkpoint_id();
let user_state: Hash = get_state_hash_at(user_id);
}

Development Tools

Dargo Package Manager

Complete project lifecycle management.

# Initialize new project
dargo init

# Create new project
dargo new my_project

# Compile contract
dargo compile --contract-name MyContract --method-names deploy transfer

# Execute with parameters  
dargo execute --contract-name MyContract --method-names mint --parameters 100

# Run tests
dargo test

# Format code
dargo fmt src/main.psy

Language Server Protocol (LSP)

IDE integration for enhanced development experience.

Supported Features:

• Hover - Type information and documentation
• Go to Definition - Navigate to symbol definitions
• Find References - Locate all symbol usages
• Code Formatting - Automatic code formatting
• Error Diagnostics - Real-time error reporting

IDE Support:

• Visual Studio Code
• Neovim
• RustRover/IntelliJ

Error Reporting

Precise error diagnostics with line and column information.

#![allow(unused)]
fn main() {
// Error example
fn invalid_function() {
    let x: Felt = true;  // Type mismatch error
    //    ^^^^     ^^^^ 
    //    |        |
    //    |        Expected Felt, found bool
    //    |
    //    Variable declared as Felt
}
}

Error Message:

error[E0308]: mismatched types
 --> src/main.psy:2:19
  |
2 |     let x: Felt = true;
  |            ----   ^^^^ expected `Felt`, found `bool`
  |            |
  |            expected due to this type annotation

Testing Framework

Built-in testing support with the #[test] attribute.

#![allow(unused)]
fn main() {
#[test]
fn test_arithmetic() {
    let result = add(2, 3);
    assert_eq(result, 5, "2 + 3 should equal 5");
}

#[test]
fn test_contract_mint() {
    // Test contract functionality
    let initial_balance = 100;
    let mint_amount = 50;
    let expected = initial_balance + mint_amount;
    
    let result = mint(mint_amount);
    assert(result > initial_balance, "Balance should increase after minting");
}
}

Package System (Crates)

Modular code organization and dependency management.

Dargo.toml Configuration

[package]
name = "my_contract"
version = "0.1.0"
edition = "2024"

[dependencies]
std = "0.1.0"
crypto = "0.2.0"

[lib]
name = "my_contract"
path = "src/lib.psy"

Library Structure

my_project/
├── Dargo.toml
├── src/
│   ├── main.psy
│   ├── lib.psy
│   └── utils/
│       ├── mod.psy
│       ├── math.psy
│       └── crypto.psy
└── tests/
    └── integration_test.psy

Zero-Knowledge Optimizations

All language features are designed with ZK circuit efficiency in mind:

• Control flow flattening - Branches become arithmetic selections
• Loop unrolling - Bounded loops are completely expanded
• Function inlining - Eliminates call overhead
• Constant folding - Compile-time evaluation
• Dead code elimination - Unused code paths removed
• Arithmetic optimization - Efficient field operations

This comprehensive feature set makes Psy a powerful language for developing efficient zero-knowledge smart contracts while maintaining familiar programming patterns and strong type safety.

Before We Begin

[Psy Smart Contract Language] requires a development environment to write and run programs. This chapter covers the prerequisites: setting up your IDE, installing the compiler, and understanding the basic tools.

If you already have the compiler installed (via git or another method), you can skip to the next chapter.

Installing the Compiler

The Psy compiler (dargo) is available from the official repository at [https://github.com/PsyProtocol/psy-compiler].

Installation via Cargo

Currently, the only supported installation method is via Cargo (Rust package manager):

Install the Psy compiler:

cargo install --git https://github.com/PsyProtocol/psy-compiler dargo

Install the Language Server (for IDE support):

cargo install --git https://github.com/PsyProtocol/psy-compiler psy-lsp-server

Prerequisites:

• Rust toolchain installed (visit rustup.rs to install)
• Git for cloning the repository

Note: Package managers like Homebrew (macOS) and Chocolatey (Windows) are not currently supported, but may be available in future releases.

Verifying Installation

After installation, verify that both tools are available in your PATH:

# Verify the compiler
dargo --version

# Verify the language server
psy-lsp-server --version

You should see version information for both the Psy compiler and language server.

Environment Setup

Set the DARGO_STD_PATH environment variable to point to the standard library:

# For bash/zsh
export DARGO_STD_PATH="$HOME/Projects/psy-compiler/psy-std/std.psy"

# For fish shell
set -gx DARGO_STD_PATH "$HOME/Projects/psy-compiler/psy-std/std.psy"

Add this to your shell configuration file (.bashrc, .zshrc, or ~/.config/fish/config.fish) to make it persistent.

Setting Up Your IDE

Psy provides Language Server Protocol (LSP) support for enhanced development experience. Currently supported IDEs:

• Visual Studio Code - Full LSP support with extension
• Neovim - LSP configuration guide

See the Set up your IDE section for detailed configuration instructions.

LSP Features:

• Hover for type information
• Go to definition
• Find references
• Code formatting
• Real-time error diagnostics

Getting Started

Once you have dargo installed and your IDE configured, you're ready to start writing Psy smart contracts! Continue to the Hello, World! chapter to create your first program.

Psy LSP Developer Tutorial

Psy is a custom language with a dedicated Language Server Protocol (LSP) service, providing basic features such as hover, goto definition, find references, and formatting.

This document introduces how to use the Psy language server psy-lsp-server for a better development experience in VSCode, Neovim, and RustRover.

🛠️ Preparation

1. Clone repository:

  git clone https://github.com/PsyProtocol/psy-compiler.git
  cd psy-compiler

2. Compile psy-lsp-server：

  cd psy-lsp-server
  cargo build --release

⚠️ Note: Regardless of which IDE you are using, the psy-lsp-server binary is required for the language features to work properly.
Please make sure you have built it and remember its path.

💻 VSCode Usage Tutorial

Developer debugging mode (recommended for developers)

1. Start VSCode:

  cd psy-lsp-server/psy-lsp-vscode
  code .

2. Press F5 to enter plugin debugging mode. VSCode will start a new VSCode window and load the local plugin.
3. In the new window, open a Psy project containing Dargo.toml to enable plugin features, such as:
   • Mouse hover → Show type information
   • Right click → Goto Definition / Find References / Format

💡 Note: In the file psy-lsp-vscode/src/extension.ts, the path to the psy-lsp-server binary is currently hardcoded:

const serverExecutable = path.join(
    // Warning: this path is hardcoded and may not be portable across systems.
    context.extensionPath, '..', '..', 'target', 'release', 'psy-lsp-server'
);

This assumes you've built the LSP server in the psy-compiler directory. If you need to change the path (for example, to use a different build directory or binary location), please modify this line accordingly and then rebuild the extension by running:

  npm run build

🧑‍💻 Neovim Configuration for Psy

This guide shows how to configure Neovim for Psy development using the Language Server Protocol.

⚠️ Prerequisites: Ensure psy-lsp-server is installed and available in your PATH.

1️⃣ File Type Detection

Add this to your Neovim configuration to recognize .psy and .qed files:

-- File type detection for Psy files
vim.api.nvim_create_augroup("FiletypeConfig", { clear = true })

vim.api.nvim_create_autocmd({ "BufNewFile", "BufReadPost" }, {
    pattern = "*.psy",
    group = "FiletypeConfig",
    callback = function()
        vim.bo.filetype = "psy"
    end,
})

vim.api.nvim_create_autocmd({ "BufNewFile", "BufReadPost" }, {
    pattern = "*.qed",
    group = "FiletypeConfig",
    callback = function()
        vim.bo.filetype = "qed"
    end,
})

2️⃣ LSP Configuration

Configure the Psy language server:

-- Configure Psy LSP
vim.lsp.config('psy_lsp', {
    cmd = { "psy-lsp-server" },
    filetypes = { "psy", "qed" },
    root_markers = { "Dargo.toml" },
    settings = {},
})

-- Enable Psy LSP
vim.lsp.enable('psy_lsp')

3️⃣ Syntax Highlighting

Configure Tree-sitter to use Rust highlighting for Psy files:

-- Reuse Rust syntax highlighting for Psy files
vim.treesitter.language.register("rust", "psy")
vim.treesitter.language.register("rust", "qed")

4️⃣ LSP Key Mappings

Set up key bindings for LSP functionality:

-- LSP key mappings
vim.api.nvim_create_autocmd("LspAttach", {
    desc = "LSP actions",
    callback = function(event)
        local bufmap = function(mode, lhs, rhs)
            local opts = { buffer = true }
            vim.keymap.set(mode, lhs, rhs, opts)
        end

        -- Core LSP navigation
        bufmap("n", "gd", "<cmd>lua vim.lsp.buf.definition()<cr>")
        bufmap("n", "gr", "<cmd>lua vim.lsp.buf.references()<cr>")
        bufmap("n", "gi", "<cmd>lua vim.lsp.buf.implementation()<cr>")
        bufmap("n", "gy", "<cmd>lua vim.lsp.buf.type_definition()<cr>")

        -- Code actions and formatting
        bufmap("n", "<leader>f", "<cmd>lua vim.lsp.buf.format()<cr>")
        bufmap("n", "<leader>rn", "<cmd>lua vim.lsp.buf.rename()<cr>")
        bufmap("n", "<leader>ca", "<cmd>lua vim.lsp.buf.code_action()<cr>")
    end,
})

5️⃣ Comment Support

Configure comment strings for Psy files:

-- Comment configuration for Psy
vim.api.nvim_create_autocmd("FileType", {
    pattern = { "psy", "qed" },
    callback = function()
        vim.bo.commentstring = "//%s"
    end,
})

6️⃣ Complete Configuration Example

Here's a complete minimal configuration for Psy development:

-- File type detection
vim.api.nvim_create_augroup("FiletypeConfig", { clear = true })

local filetypes = {
    psy = "*.psy",
    qed = "*.qed",
}

for filetype, pattern in pairs(filetypes) do
    vim.api.nvim_create_autocmd({ "BufNewFile", "BufReadPost" }, {
        pattern = pattern,
        group = "FiletypeConfig",
        callback = function()
            vim.bo.filetype = filetype
        end,
    })
end

-- LSP configuration
vim.lsp.config('psy_lsp', {
    cmd = { "psy-lsp-server" },
    filetypes = { "psy", "qed" },
    root_markers = { "Dargo.toml" },
    settings = {},
})

vim.lsp.enable('psy_lsp')

-- Syntax highlighting
vim.treesitter.language.register("rust", "psy")
vim.treesitter.language.register("rust", "qed")

-- Comment support
vim.api.nvim_create_autocmd("FileType", {
    pattern = { "psy", "qed" },
    callback = function()
        vim.bo.commentstring = "//%s"
    end,
})

-- LSP key mappings
vim.api.nvim_create_autocmd("LspAttach", {
    desc = "LSP actions",
    callback = function(event)
        local bufmap = function(mode, lhs, rhs)
            local opts = { buffer = true }
            vim.keymap.set(mode, lhs, rhs, opts)
        end

        bufmap("n", "gd", "<cmd>lua vim.lsp.buf.definition()<cr>")
        bufmap("n", "gr", "<cmd>lua vim.lsp.buf.references()<cr>")
        bufmap("n", "<leader>f", "<cmd>lua vim.lsp.buf.format()<cr>")
        bufmap("n", "<leader>rn", "<cmd>lua vim.lsp.buf.rename()<cr>")
        bufmap("n", "<leader>ca", "<cmd>lua vim.lsp.buf.code_action()<cr>")
    end,
})

📚 Key Bindings Summary

🔧 Additional IDE Support

While VSCode and Neovim have official configuration guides, other IDEs may be supported through generic LSP clients. If you're using a different IDE that supports LSP, you can configure it to use psy-lsp-server as the language server for .psy files.

General LSP Configuration:

• Server Command: psy-lsp-server
• File Extensions: *.psy
• Language ID: psy
• Root Pattern: Dargo.toml

For specific IDE setup instructions, please refer to your IDE's LSP configuration documentation.

Setting up Shell Completions

Shell completions allow you to use the Tab key to autocomplete commands, options, and arguments when working with the Psy CLI tools. This makes development faster and more convenient.

This guide will help you set up shell completions for the Dargo CLI.

Zsh Completions

You can add the completions script to your Zsh completions directory:

# Create the completions directory if it doesn't exist
mkdir -p ~/.zsh/completions

# Generate and save the completion script
dargo complete zsh > ~/.zsh/completions/_dargo

# Add the directory to your fpath in ~/.zshrc if you haven't already
echo 'fpath=(~/.zsh/completions $fpath)' >> ~/.zshrc
echo 'autoload -U compinit && compinit' >> ~/.zshrc

# Reload your shell
source ~/.zshrc

Bash Completions

You can add the completions script to your Bash environment in a few ways:

If you have bash-completion installed:

# Generate and save the completion script to the bash-completion directory
dargo complete bash > /usr/local/etc/bash_completion.d/dargo

Without bash-completion, you can add it to your profile:

# Create a completions directory if you don't have one
mkdir -p ~/.bash_completions

# Generate and save the completion script
dargo complete bash > ~/.bash_completions/dargo.bash

# Add the following line to your ~/.bash_profile or ~/.bashrc
echo 'source ~/.bash_completions/dargo.bash' >> ~/.bashrc

# Reload your shell
source ~/.bashrc

Fish Completions

For Fish shell users, you can easily set up completions:

# Generate and save the completion script to the Fish completions directory
dargo complete fish > ~/.config/fish/completions/dargo.fish

No additional steps are needed as Fish automatically loads completions from this directory.

Verifying Completions

To verify that completions are working correctly, type dargo followed by a space and press Tab. You should see a list of available commands.

Try:

dargo <TAB>

You should see a list of commands like new, build, compile, etc.

Troubleshooting

If completions aren't working:

1. Make sure you've restarted your terminal or sourced your .zshrc file
2. Check that the dargo complete zsh command works and produces output
3. Verify that the path to the completion script is correct
4. Ensure that Zsh completions are enabled in your shell configuration

Hello, World!

This chapter walks you through creating your first [Psy Smart Contract Language] program.

Creating a New Program

Create a new project:

dargo new hello_world

This creates a new directory with a basic project structure. Navigate to the project and edit the src/main.psy file:

// input: 2,3
// output: 5
fn main(a: Felt, b: Felt) -> Felt {
    assert(a < b, "a should be less than b");
    assert_eq(b - a, 1, "b - a should equal 1");
    return a + b;
}

This simple program:

• Takes two Felt parameters (a and b)
• Asserts that a is less than b
• Asserts that the difference is exactly 1
• Returns the sum of a and b

Compiling

Compile the program using the compiler:

dargo compile

You will see a target directory created with the compiled output. The Psy compiler generates DPN opcodes and circuit data for each function.

[
    {
        "name": "main",
        "method_id": 680917438,
        "circuit_inputs": [
            0,
            1
        ],
        "circuit_outputs": [],
        "state_commands": [],
        "state_command_resolution_indices": [],
        "assertions": [
            {
                "left": 4294967296,
                "right": 4294967297,
                "message": "x != y"
            }
        ],
        "definitions": [
            {
                "data_type": 0,
                "index": 0,
                "op_type": 0,
                "inputs": [
                    0
                ]
            },
            {
                "data_type": 0,
                "index": 1,
                "op_type": 0,
                "inputs": [
                    1
                ]
            },
            {
                "data_type": 1,
                "index": 0,
                "op_type": 13,
                "inputs": [
                    0,
                    1
                ]
            },
            {
                "data_type": 1,
                "index": 1,
                "op_type": 2,
                "inputs": [
                    1
                ]
            }
        ]
    }
]

Running

Execute the program with test inputs:

dargo execute --program-dir . --entry-path src/main.psy --parameters 2,3

This runs the main function with the parameters 2 and 3. You should see the output result_vm: [5] as the result.

Basic Syntax

[Psy Smart Contract Language] uses a syntax inspired by [Rust]. Here are the basics:

Variables

Variables are declared with let and can be mutable with mut:

Basic Type Assignment

#![allow(unused)]
fn main() {
// Felt type assignment
let a: Felt = 1;
let b = 42; // Type inference
let mut c: Felt = 0;
c = 100;

// Boolean assignment
let flag: bool = true;
let mut status = false;
status = true;

// u32 assignment  
let count: u32 = 42u32;
let mut index = 0u32;
index = 5u32;
}

Array Assignment

#![allow(unused)]
fn main() {
// Fixed-size array assignment
let numbers: [Felt; 3] = [1, 2, 3];
let mut values: [u32; 5] = [0u32, 1u32, 2u32, 3u32, 4u32];

// Individual element assignment
values[0] = 10u32;
values[1] = 20u32;

// Nested array assignment
let mut matrix: [[Felt; 2]; 3] = [[1, 2], [3, 4], [5, 6]];
matrix[0][1] = 99;
}

Tuple Assignment

#![allow(unused)]
fn main() {
// Tuple assignment
let point: (Felt, Felt) = (10, 20);
let mixed: (Felt, bool, u32) = (42, true, 100u32);

// Individual element assignment
let mut coordinates: (Felt, Felt) = (0, 0);
coordinates.0 = 5;
coordinates.1 = 15;

// Nested tuple assignment
let mut complex: ((Felt, Felt), (Felt, Felt)) = ((1, 2), (3, 4));
complex.0.1 = 42; // Assign to nested element
}

Struct Assignment

#![allow(unused)]
fn main() {
struct Point {
    pub x: Felt,
    pub y: Felt,
}

// Struct creation assignment
let origin: Point = new Point { x: 0, y: 0 };

// Field assignment
let mut position: Point = new Point { x: 10, y: 20 };
position.x = 15;
position.y = 25;

// Struct with complex types
struct Container {
    pub data: [Felt; 3],
    pub coords: (Felt, Felt),
}

let mut container: Container = new Container {
    data: [1, 2, 3],
    coords: (10, 20),
};
container.data[0] = 99;
container.coords.1 = 30;
}

Comments

Psy supports both single-line and multi-line comments:

#![allow(unused)]
fn main() {
// Single-line comment
let a: Felt = 1;

/*
 * Multi-line comment
 * across multiple lines
 */
let b: Felt = 2;

/* Single-line block comment */
let c: Felt = 3;
}

Placement

Comments can be placed in these locations:

#![allow(unused)]
fn main() {
// Comment before struct
struct Point {
    pub x: Felt,
    // Comment between fields
    pub y: Felt,
}

// Comment before function
fn calculate(a: Felt, b: Felt) -> Felt {
    // Comment inside function
    let result = a + b;
    return result;
}

#[test]
fn test_function() {
    // Comment in test
    assert_eq(calculate(1, 2), 3, "should be 3");
}
}

Limitations

Comments cannot be placed in these locations:

#![allow(unused)]
fn main() {
// ❌ Invalid: After attributes
#[test] // This causes an error
fn test_func() { }

// ❌ Invalid: Inside parameter lists
fn invalid_func(
    // This causes an error
    a: Felt,
    b: Felt
) -> Felt { a + b }

// ❌ Invalid: In middle of declarations  
struct InvalidStruct {
    pub /* error here */ x: Felt,
}
}

Operators

This chapter covers all operators available in Psy, including arithmetic, logical, comparison, bitwise, and special operators.

Arithmetic Operators

Basic Arithmetic

Psy supports standard arithmetic operations for both Felt and u32 types:

fn main() {
    let a = 10;
    let b = 3;
    
    // Addition
    let sum = a + b;        // 13
    
    // Subtraction
    let diff = a - b;       // 7
    
    // Multiplication
    let product = a * b;    // 30
    
    // Division
    let quotient = a / b;   // 3 (integer division)
    
    // Modulo
    let remainder = a % b;  // 1
}

Exponentiation

Psy provides the exponentiation operator **:

fn main() {
    let base = 2;
    let exponent = 8;
    let result = base ** exponent;  // 256
    
    // u32 exponentiation
    let u32_base = 2u32;
    let u32_exp = 5u32;
    let u32_result = u32_base ** u32_exp;  // 32u32
    
    // Large numbers
    let large = 2 ** 64;  // 4294967295
}

Unary Operators

fn main() {
    let positive = 5;
    let negative = -positive;  // -5
    
    // Negation of zero
    let zero = 0;
    let neg_zero = -zero;  // Still 0
}

Comparison Operators

All comparison operators return bool values:

fn main() {
    let a = 10;
    let b = 5;
    let c = 10;
    
    // Equality
    let equal = a == c;        // true
    let not_equal = a != b;    // true
    
    // Ordering
    let less = b < a;          // true
    let less_equal = b <= a;   // true
    let greater = a > b;       // true
    let greater_equal = a >= c; // true
}

Type-specific Comparisons

fn main() {
    // u32 comparisons
    let u32_a = 100u32;
    let u32_b = 50u32;
    let u32_less = u32_b < u32_a;  // true
    
    // bool comparisons
    let bool_a = true;
    let bool_b = false;
    let bool_equal = bool_a == bool_b;  // false
}

Logical Operators

Boolean Logic

Logical operators work with bool types:

fn main() {
    let true_val = true;
    let false_val = false;
    
    // Logical AND
    let and_result = true_val && false_val;   // false
    
    // Logical OR
    let or_result = true_val || false_val;    // true
    
    // Logical XOR
    let xor_result = true_val ^ false_val;    // true
    
    // Logical NOT
    let not_result = !false_val;              // true
}

Felt Logic

For Felt values, logical NOT treats 0 as false and 1 as true:

fn main() {
    let zero = 0;
    let one = 1;
    
    let not_zero = !zero;  // 1 (true)
    let not_one = !one;    // 0 (false)
}

Bitwise Operators (u32 only)

Bitwise operations are only available for u32 type:

fn main() {
    let a = 0b11110000u32;  // 240
    let b = 0b00111100u32;  // 60
    
    // Bitwise AND
    let and_bits = a & b;   // 0b00110000 = 48
    
    // Bitwise OR
    let or_bits = a | b;    // 0b11111100 = 252
    
    // Bitwise XOR
    let xor_bits = a ^ b;   // 0b11001100 = 204
}

Bit Shifting

fn main() {
    let value = 0b11111111u32;  // 255
    
    // Left shift
    let left_shift = value << 1u32;   // 0b11111110 = 254
    let left_shift_8 = value << 8u32; // 65280
    
    // Right shift
    let right_shift = value >> 1u32;  // 0b01111111 = 127
    let right_shift_4 = value >> 4u32; // 15
    
    // Shift by 32 or more results in zero
    let zero_result = value << 32u32;  // 0
}

Advanced Bitwise Examples

fn main() {
    let max_u32 = 4294967295u32;  // 0xFFFFFFFF
    let high_bit = 2147483648u32;  // 0x80000000
    
    // Extract specific bits
    let masked = max_u32 & high_bit;  // 2147483648u32
    
    // Set all bits except high bit
    let almost_max = max_u32 ^ high_bit;  // 2147483647u32
    
    // Combine values
    let combined = high_bit | 42u32;  // 2147483690u32
}

Special Operators

Bit Manipulation Functions

Psy provides special functions for bit manipulation:

fn main() {
    let value = 12345;
    
    // Split a Felt into individual bits
    let bits = __split_bits(value, 32);  // Returns [Felt; 32]
    
    // Reconstruct from bits
    let reconstructed = __sum_bits(bits);
    // reconstructed equals original value
    
    // Working with specific bit positions
    let bit_0 = bits[0];   // Least significant bit
    let bit_15 = bits[15]; // 16th bit from right
}

Advanced Bit Operations

fn main() {
    let large_number = 2 ** 32;  // 4294967296
    
    // Split into 64 bits
    let bits_64 = __split_bits(large_number, 33);  // Needs 33 bits for 2^32
    
    // Verify specific bits
    let bit_31 = bits_64[31];  // 0
    let bit_32 = bits_64[32];  // 1 (the 2^32 bit)
    
    // Reconstruct
    let sum = __sum_bits(bits_64);  // Equals large_number
}

Type Casting

Casting Between Types

fn main() {
    // bool to other types
    let bool_val = true;
    let bool_as_u32 = bool_val as u32;   // 1u32
    let bool_as_felt = bool_val as Felt;  // 1
    
    // u32 to other types
    let u32_val = 42u32;
    let u32_as_felt = u32_val as Felt;   // 42
    let u32_as_bool = 1u32 as bool;      // true (only 0 and 1 are valid)
    
    // Felt to other types
    let felt_val = 123;
    let felt_as_u32 = felt_val as u32;   // 123u32 (if in valid range)
    let felt_as_bool = 0 as bool;        // false
}

Casting Constraints

fn main() {
    // Valid bool casts
    let zero_bool = 0 as bool;      // false
    let one_bool = 1 as bool;       // true
    
    // Invalid bool cast (would panic)
    // let invalid_bool = 2 as bool;  // Error: Invalid bool value
    
    // Valid u32 range
    let max_u32_felt = 4294967295;
    let valid_u32 = max_u32_felt as u32;  // 4294967295u32
    
    // Invalid u32 cast (would panic)
    // let invalid_u32 = 4294967296 as u32;  // Error: Invalid u32 value
}

Field Arithmetic (Felt)

Psy operates over the Goldilocks field with prime p = 18446744069414584321:

fn main() {
    let zero = 0;
    let one = 1;
    let two = 2;
    
    // Field arithmetic wraps around at the prime
    let p_minus_one = zero - one;  // 18446744069414584320 (p-1)
    
    // Division in field arithmetic is multiplicative inverse
    // NOT integer division - computes x such that (divisor * x) ≡ dividend (mod p)
    let half = p_minus_one / two;  // (p-1)/2 = multiplicative inverse
    let inv_two = one / two;       // 1/2 in field arithmetic
    
    // Verify: division result times divisor equals dividend
    let verify = inv_two * two;    // Should equal 1
    
    // Multiplication
    let result = p_minus_one * p_minus_one;  // 1 (since (-1)² = 1)
}

Large Number Examples

fn main() {
    // Working with large field elements
    let large = 2 ** 63;  // 9223372036854775808
    let modulo_result = large % (3 ** 35);  // 17567738638829720
    
    // Field inverse behavior
    let p = 18446744069414584321;  // Field prime
    let one = 1;
    let two = 2;
    let inv_two = one / two;  // Multiplicative inverse of 2
}

Operator Precedence

Operators follow standard mathematical precedence:

1. Unary operators: -, !
2. Exponentiation: ** (right-associative)
3. Multiplicative: *, /, %
4. Additive: +, -
5. Shift: <<, >>
6. Bitwise AND: &
7. Bitwise XOR: ^
8. Bitwise OR: |
9. Comparison: <, <=, >, >=, ==, !=
10. Logical AND: &&
11. Logical OR: ||

fn main() {
    let result = 2 + 3 * 4 ** 2;  // 2 + (3 * (4 ** 2)) = 2 + 48 = 50
    let complex = 8 / 2 + 3 * 2;  // (8 / 2) + (3 * 2) = 4 + 6 = 10
    
    // Use parentheses for clarity
    let explicit = (2 + 3) * (4 ** 2);  // 5 * 16 = 80
}

Type Compatibility

Compatible Operations

fn main() {
    // Same-type operations
    let felt_result = 10 + 20;          // Felt + Felt
    let u32_result = 10u32 + 20u32;     // u32 + u32
    let bool_result = true && false;    // bool && bool
    
    // Mixed with literals
    let mixed1 = 10u32 + 5u32;          // u32 + u32 literal
    let mixed2 = 10 + 5;                // Felt + Felt literal
}

Type Errors

fn main() {
    // These would cause compilation errors:
    // let invalid1 = 10 + 10u32;       // Error: Felt + u32
    // let invalid2 = true + false;     // Error: bool + bool
    // let invalid3 = 10u32 && 20u32;   // Error: u32 && u32
    
    // Use explicit casting instead:
    let valid1 = 10 + (10u32 as Felt);  // Cast u32 to Felt
    let valid2 = (10 as u32) + 10u32;   // Cast Felt to u32
}

Performance Considerations

ZK-Circuit Friendly Operations

Some operations are more efficient in zero-knowledge circuits:

fn main() {
    // Efficient: Basic arithmetic
    let efficient = a + b * c;
    
    // Less efficient: Division (requires field inversion)
    let less_efficient = a / b;
    
    // Moderately efficient: Comparisons
    let comparison = a < b;
    
    // Bit operations are expanded to constraints
    let bitwise = a_u32 & b_u32;  // Generates multiple constraints
}

Key Points

1. Arithmetic: Standard +, -, *, /, %, ** operators
2. Comparison: All comparison operators return bool
3. Logical: &&, ||, ^, ! for boolean logic
4. Bitwise: &, |, ^, <<, >> for u32 only
5. Casting: Explicit type conversion with as keyword
6. Field Arithmetic: Operations over Goldilocks field for Felt
7. Type Safety: Operations must be between compatible types
8. Bit Functions: __split_bits and __sum_bits for bit manipulation
9. Precedence: Standard mathematical operator precedence
10. ZK Optimization: Some operations are more circuit-friendly than others

Structs and Implementations

Structs define custom data types that group related data together, and impl blocks add methods to operate on that data. This chapter covers struct definition, implementation patterns, and method types.

Defining Structs

Basic Struct Definition

#![allow(unused)]
fn main() {
// Public struct with mixed field visibility
pub struct Person {
    pub age: Felt,        // Public field - accessible from anywhere
    pub name_hash: Felt,  // Public field
    is_active: bool,      // Private field - only accessible within this module
}

// Private struct - only accessible within this module
struct InternalData {
    value: Felt,          // Private field in private struct
}

pub struct Point {
    pub x: Felt,          // Public field
    pub y: Felt,          // Public field
}

pub struct Rectangle {
    pub top_left: Point,  // Public field
    pub width: Felt,      // Public field
    pub height: Felt,     // Public field
}
}

Visibility Rules

Struct Visibility:

• struct Name - Private struct, only accessible within the same module
• pub struct Name - Public struct, accessible from other modules

Field Visibility:

• field: Type - Private field, only accessible within the struct's own methods
• pub field: Type - Public field, accessible wherever the struct is accessible

#![allow(unused)]
fn main() {
// Examples of visibility combinations
pub struct PublicStruct {
    pub public_field: Felt,    // ✅ Accessible wherever struct is accessible
    private_field: Felt,       // ❌ Only accessible within struct's own methods
}

struct PrivateStruct {
    pub public_field: Felt,    // ❌ Still not accessible outside module (struct is private)
    private_field: Felt,       // ❌ Only accessible within struct's own methods
}

// Demonstrating private field access
pub struct BankAccount {
    pub account_number: Felt,
    balance: Felt,  // Private - can only be accessed via methods
}

impl BankAccount {
    pub fn new(account_number: Felt, initial_balance: Felt) -> BankAccount {
        return new BankAccount {
            account_number: account_number,
            balance: initial_balance,  // ✅ Can access private field in constructor
        };
    }
    
    pub fn get_balance(self) -> Felt {
        return self.balance;  // ✅ Can access private field in method
    }
    
    pub fn deposit(mut self, amount: Felt) -> BankAccount {
        self.balance = self.balance + amount;  // ✅ Can modify private field in method
        return self;
    }
}
}

Structs with Arrays and Tuples

#![allow(unused)]
fn main() {
struct Vector3D {
    pub components: [Felt; 3],
    pub magnitude: Felt,
}

struct BoundingBox {
    pub corners: (Point, Point), // (min_corner, max_corner)
    pub is_valid: bool,
}

struct Matrix2x2 {
    pub data: [[Felt; 2]; 2],
    pub determinant: Felt,
}
}

Implementation Blocks

Instance Methods

Instance methods operate on a specific instance of the struct. In Psy, the self parameter follows the same passing rules as function parameters:

self Parameter Passing:

• Structs with only value types (Felt, u32, bool) - Passed by copy
• Structs with reference types (arrays, other structs) - Passed by move/reference
• Mixed structs - Follow the most restrictive member (move/reference if any member requires it)

Important: Psy only supports self and mut self syntax, never &self or &mut self.

Method Visibility:

• fn method_name - Private method, only callable within the same module
• pub fn method_name - Public method, callable wherever the struct is accessible

#![allow(unused)]
fn main() {
impl Point {
    // Public instance method - accessible from anywhere
    pub fn distance_from_origin(self) -> Felt {
        // Simplified distance calculation
        return self.x + self.y;
    }
    
    // Public instance method that modifies the point
    pub fn translate(mut self, dx: Felt, dy: Felt) -> Point {
        self.x = self.x + dx;
        self.y = self.y + dy;
        return self;
    }
    
    // Public instance method that uses other structs
    pub fn distance_to(self, other: Point) -> Felt {
        return self.calculate_manhattan_distance(other);
    }
    
    // Private helper method - only usable within this module
    fn calculate_manhattan_distance(self, other: Point) -> Felt {
        let dx = if self.x > other.x { self.x - other.x } else { other.x - self.x };
        let dy = if self.y > other.y { self.y - other.y } else { other.y - self.y };
        return dx + dy;
    }
}
}

Static Methods (Associated Functions)

Static methods don't take self and are called on the type itself, not an instance.

#![allow(unused)]
fn main() {
impl Point {
    // Static method - constructor
    pub fn new(x: Felt, y: Felt) -> Point {
        return new Point { x: x, y: y };
    }
    
    // Static method - create special points
    pub fn origin() -> Point {
        return new Point { x: 0, y: 0 };
    }
    
    // Static method - utility functions
    pub fn midpoint(p1: Point, p2: Point) -> Point {
        let mid_x = (p1.x + p2.x) / 2;
        let mid_y = (p1.y + p2.y) / 2;
        return new Point { x: mid_x, y: mid_y };
    }
}
}

The self Parameter

Important: Psy only supports self syntax, not &self or &mut self:

#![allow(unused)]
fn main() {
impl Rectangle {
    // ✅ Valid: self moves the struct into the method
    pub fn area(self) -> Felt {
        return self.width * self.height;
    }
    
    // ✅ Valid: mut self allows modification
    pub fn scale(mut self, factor: Felt) -> Rectangle {
        self.width = self.width * factor;
        self.height = self.height * factor;
        return self;
    }
    
    // ✅ Valid: self is alias for self: Self
    pub fn perimeter(self) -> Felt {
        return 2 * (self.width + self.height);
    }
    
    // ❌ Invalid: Psy doesn't support reference syntax
    // pub fn invalid_method(&self) -> Felt { ... }
    // pub fn invalid_mut(&mut self) { ... }
}
}

Complex Examples

Vector3D Implementation

#![allow(unused)]
fn main() {
impl Vector3D {
    pub fn new(x: Felt, y: Felt, z: Felt) -> Vector3D {
        let components = [x, y, z];
        let magnitude = x * x + y * y + z * z; // Simplified magnitude
        return new Vector3D {
            components: components,
            magnitude: magnitude,
        };
    }
    
    pub fn dot_product(self, other: Vector3D) -> Felt {
        return self.components[0] * other.components[0] +
               self.components[1] * other.components[1] +
               self.components[2] * other.components[2];
    }
    
    pub fn scale(mut self, factor: Felt) -> Vector3D {
        self.components[0] = self.components[0] * factor;
        self.components[1] = self.components[1] * factor;
        self.components[2] = self.components[2] * factor;
        self.magnitude = self.magnitude * (factor * factor);
        return self;
    }
    
    pub fn get_x(self) -> Felt {
        return self.components[0];
    }
    
    pub fn get_y(self) -> Felt {
        return self.components[1];
    }
    
    pub fn get_z(self) -> Felt {
        return self.components[2];
    }
}
}

Matrix2x2 Implementation

#![allow(unused)]
fn main() {
impl Matrix2x2 {
    pub fn new(a: Felt, b: Felt, c: Felt, d: Felt) -> Matrix2x2 {
        let data = [[a, b], [c, d]];
        let determinant = a * d - b * c;
        return new Matrix2x2 {
            data: data,
            determinant: determinant,
        };
    }
    
    pub fn identity() -> Matrix2x2 {
        return Matrix2x2::new(1, 0, 0, 1);
    }
    
    pub fn multiply(self, other: Matrix2x2) -> Matrix2x2 {
        let a = self.data[0][0] * other.data[0][0] + self.data[0][1] * other.data[1][0];
        let b = self.data[0][0] * other.data[0][1] + self.data[0][1] * other.data[1][1];
        let c = self.data[1][0] * other.data[0][0] + self.data[1][1] * other.data[1][0];
        let d = self.data[1][0] * other.data[0][1] + self.data[1][1] * other.data[1][1];
        
        return Matrix2x2::new(a, b, c, d);
    }
    
    pub fn apply_to_point(self, point: Point) -> Point {
        let new_x = self.data[0][0] * point.x + self.data[0][1] * point.y;
        let new_y = self.data[1][0] * point.x + self.data[1][1] * point.y;
        return new Point { x: new_x, y: new_y };
    }
}
}

Usage Examples

#![allow(unused)]
fn main() {
#[test]
fn test_point_operations() {
    // Using static methods
    let origin = Point::origin();
    let p1 = Point::new(3, 4);
    let p2 = Point::new(6, 8);
    
    // Using instance methods
    let distance = p1.distance_from_origin();
    let moved = p1.translate(2, 1);
    let mid = Point::midpoint(p1, p2);
    
    assert_eq(distance, 7, "distance should be 3 + 4 = 7");
    assert_eq(moved.x, 5, "moved x should be 3 + 2 = 5");
    assert_eq(mid.x, 4, "midpoint x should be (3 + 6) / 2 = 4");
}

#[test]
fn test_vector_operations() {
    let v1 = Vector3D::new(1, 2, 3);
    let v2 = Vector3D::new(4, 5, 6);
    
    let dot = v1.dot_product(v2);
    let scaled = v1.scale(2);
    
    assert_eq(dot, 32, "dot product should be 1*4 + 2*5 + 3*6 = 32");
    assert_eq(scaled.get_x(), 2, "scaled x should be 1 * 2 = 2");
}

#[test]
fn test_matrix_operations() {
    let m1 = Matrix2x2::new(1, 2, 3, 4);
    let identity = Matrix2x2::identity();
    let point = Point::new(5, 7);
    
    let result = m1.multiply(identity);
    let transformed = m1.apply_to_point(point);
    
    assert_eq(result.data[0][0], 1, "identity multiplication preserves values");
    assert_eq(transformed.x, 19, "transformed x should be 1*5 + 2*7 = 19");
}
}

Method Call Syntax

#![allow(unused)]
fn main() {
// Both syntaxes are equivalent
let p = Point::new(3, 4);

// Method syntax (recommended)
let distance1 = p.distance_from_origin();

// Function syntax (also valid)
let distance2 = Point::distance_from_origin(p);

// Static methods can only be called with :: syntax
let origin = Point::origin();
let mid = Point::midpoint(p1, p2);
}

Arrays and Tuples

This chapter covers arrays and tuples in Psy, two important data structures for grouping values together.

Arrays

Arrays in Psy are fixed-size sequences of elements of the same type. They are defined with the syntax [T; N] where T is the element type and N is the compile-time known size.

Basic Array Usage

fn main() {
    // Array of 5 Felt values
    let numbers = [1, 2, 3, 4, 5];
    
    // Array with explicit type annotation
    let coordinates: [Felt; 3] = [10, 20, 30];
    
    // Array initialized with same value
    let zeros = [0; 4]; // [0, 0, 0, 0]
    
    // Accessing elements
    let first = numbers[0];
    let third = coordinates[2];
}

Arrays in Structs

struct HW {
    pub height: Felt,
    pub weight: Felt,
}

struct Person {
    pub age: Felt,
    pub hw: [HW; 2],
}

fn main() {
    let hw1 = new HW { height: 180, weight: 140 };
    let hw2 = new HW { height: 175, weight: 110 };
    
    let person = new Person {
        age: 25,
        hw: [hw1, hw2],
    };
    
    // Access nested array elements
    let first_height = person.hw[0].height;
    let second_weight = person.hw[1].weight;
}

Nested Arrays

fn main() {
    // 2D array (matrix)
    let matrix: [[Felt; 3]; 2] = [
        [1, 2, 3],
        [4, 5, 6]
    ];
    
    // Accessing nested elements
    let element = matrix[1][2]; // Gets 6
    
    // 3D array
    let cube: [[[Felt; 2]; 2]; 2] = [
        [[1, 2], [3, 4]],
        [[5, 6], [7, 8]]
    ];
    
    let deep_value = cube[1][0][1]; // Gets 6
}

Mutable Array Operations

fn main() {
    let hw1 = new HW { height: 180, weight: 140 };
    let hw2 = new HW { height: 175, weight: 110 };
    
    let person1 = new Person { age: 8, hw: [hw1, hw1] };
    let person2 = new Person { age: 18, hw: [hw2, hw2] };
    
    let mut people: [Person; 2] = [person1, person2];
    
    // Modify array elements
    people[0].hw[1] = new HW { height: 160, weight: 110 };
    
    // Access modified values
    let total_height = people[0].hw[0].height + people[0].hw[1].height;
}

Array Methods with Generics

Arrays support methods through generic implementations. However, specialized implementations for specific array types are not currently supported:

impl<T, N: u32> [T; N] {
    pub const fn len() -> u32 {
        return N;
    }
}

fn main() {
    // Call len() method on array type
    let length = <[Felt; 5]>::len(); // Returns 5
}

Working with Arrays Using Functions

Since custom array methods are not currently supported, use regular functions to operate on arrays:

fn array_sum(arr: [Felt; 3]) -> Felt {
    return arr[0] + arr[1] + arr[2];
}

fn array_dot_product(a: [Felt; 3], b: [Felt; 3]) -> Felt {
    return a[0] * b[0] + a[1] * b[1] + a[2] * b[2];
}

fn array_max(arr: [Felt; 4]) -> Felt {
    let mut max_val = arr[0];
    if arr[1] > max_val { max_val = arr[1]; };
    if arr[2] > max_val { max_val = arr[2]; };
    if arr[3] > max_val { max_val = arr[3]; };
    return max_val;
}

fn main() {
    let v1 = [1, 2, 3];
    let v2 = [4, 5, 6];
    
    let sum = array_sum(v1); // Returns 6
    let dot = array_dot_product(v1, v2); // Returns 32
    
    let grades = [85, 92, 78, 95];
    let highest = array_max(grades); // Returns 95
}

Tuples

Tuples are fixed-size sequences that can contain elements of different types. They are defined with parentheses and comma-separated values.

Basic Tuple Usage

fn main() {
    // Basic tuple assignment
    let a: Felt = 10;
    let b: Felt = 11;
    let c: (Felt, Felt) = (12, 13);
    let d: (Felt, Felt) = (a, b);
    
    // Mutable tuple
    let mut e: (Felt, Felt) = (14, 15);
    
    // Change tuple elements
    e.0 = 16;
    e.1 = 17;
    e = (18, 19);
    
    // Accessing tuple elements
    let first = c.0;  // Gets 12
    let second = c.1; // Gets 13
}

Nested Tuples

fn main() {
    // Nested tuple
    let nested_tuple: ((Felt, Felt), (Felt, Felt)) = ((1, 2), (3, 4));
    
    // Deeply nested tuple
    let deeply_nested: (((Felt, Felt), Felt), Felt) = (((5, 6), 7), 8);
    
    // Modify nested tuples
    let mut complex_tuple: ((Felt, Felt), (Felt, Felt)) = ((9, 10), (11, 12));
    complex_tuple.0.1 = 42;  // Change nested element
    complex_tuple.1 = (20, 21); // Replace entire sub-tuple
    
    // Access nested elements
    let value = nested_tuple.0.1;  // Gets 2
    let deep_value = deeply_nested.0.0.1; // Gets 6
}

Tuples in Structs

struct TupleHolder {
    pub pair: (Felt, Felt),
    pub nested: ((Felt, Felt), Felt),
}

fn main() {
    let mut struct_with_tuple = new TupleHolder {
        pair: (22, 23),
        nested: ((24, 25), 26),
    };
    
    // Modify tuple fields in struct
    struct_with_tuple.pair.1 = 99;
    struct_with_tuple.nested.0.0 = 88;
    
    // Access tuple elements in struct
    let pair_first = struct_with_tuple.pair.0;
    let nested_value = struct_with_tuple.nested.1;
}

Functions with Tuples

fn create_tuple(x: Felt, y: Felt) -> (Felt, Felt) {
    return (x + 1, y + 1);
}

fn sum_tuple(input: (Felt, Felt)) -> Felt {
    return input.0 + input.1;
}

fn swap_tuple(input: (Felt, Felt)) -> (Felt, Felt) {
    return (input.1, input.0);
}

fn process_nested(input: ((Felt, Felt), Felt)) -> Felt {
    return input.0.0 + input.0.1 + input.1;
}

fn main() {
    // Function returning tuple
    let returned_tuple = create_tuple(30, 31);
    // returned_tuple is (31, 32)
    
    // Function taking tuple as parameter
    let result = sum_tuple((40, 50));
    // result is 90
    
    // More complex operations
    let swapped = swap_tuple((10, 20));
    // swapped is (20, 10)
    
    let nested_result = process_nested(((1, 2), 3));
    // nested_result is 6
}

Tuple Parameter Passing

Tuples follow mixed semantics based on their member types:

fn main() {
    // Tuple with only value types - passed by copy
    let simple_tuple = (1, 2, true);
    process_simple(simple_tuple);
    
    // Tuple with reference types - passed by move/reference
    let array_tuple = ([1, 2, 3], 42);
    process_complex(array_tuple);
}

fn process_simple(t: (Felt, Felt, bool)) {
    let sum = t.0 + t.1;
    let flag = t.2;
}

fn process_complex(t: ([Felt; 3], Felt)) {
    let array_sum = t.0[0] + t.0[1] + t.0[2];
    let extra = t.1;
}

Current Limitations

Tuple Destructuring

Note: Tuple destructuring is not currently supported:

fn main() {
    // ❌ Not supported yet
    // let (x, y) = (50, 60);
    // let ((a, b), c) = ((1, 2), 3);
    
    // ✅ Use explicit access instead
    let pair = (50, 60);
    let x = pair.0;
    let y = pair.1;
}

Arrays vs Tuples

Complex Examples

Game Inventory System

struct Item {
    pub id: Felt,
    pub quantity: Felt,
}

struct Player {
    pub health: Felt,
    pub position: (Felt, Felt),
    pub inventory: [Item; 5],
    pub stats: (Felt, Felt, Felt), // (strength, defense, speed)
}

fn main() {
    let sword = new Item { id: 1, quantity: 1 };
    let potion = new Item { id: 2, quantity: 3 };
    let empty_slot = new Item { id: 0, quantity: 0 };
    
    let mut player = new Player {
        health: 100,
        position: (10, 20),
        inventory: [sword, potion, empty_slot, empty_slot, empty_slot],
        stats: (15, 10, 12)
    };
    
    // Move player
    player.position.0 = player.position.0 + 5;
    player.position.1 = player.position.1 - 2;
    
    // Add item to inventory
    player.inventory[2] = new Item { id: 3, quantity: 2 };
    
    // Increase stats
    player.stats.0 = player.stats.0 + 1; // strength + 1
    
    let total_strength = player.stats.0;
    let current_x = player.position.0;
}

Matrix Operations

fn matrix_multiply(a: [[Felt; 2]; 2], b: [[Felt; 2]; 2]) -> [[Felt; 2]; 2] {
    let row1_col1 = a[0][0] * b[0][0] + a[0][1] * b[1][0];
    let row1_col2 = a[0][0] * b[0][1] + a[0][1] * b[1][1];
    let row2_col1 = a[1][0] * b[0][0] + a[1][1] * b[1][0];
    let row2_col2 = a[1][0] * b[0][1] + a[1][1] * b[1][1];
    
    return [[row1_col1, row1_col2], [row2_col1, row2_col2]];
}

fn main() {
    let matrix_a: [[Felt; 2]; 2] = [[1, 2], [3, 4]];
    let matrix_b: [[Felt; 2]; 2] = [[5, 6], [7, 8]];
    
    let result = matrix_multiply(matrix_a, matrix_b);
    
    // result is [[19, 22], [43, 50]]
    let top_left = result[0][0]; // 19
    let bottom_right = result[1][1]; // 50
}

Database Record Simulation

type UserRecord = (Felt, (Felt, Felt, Felt), [Felt; 3], bool);

fn create_user_record(
    user_id: Felt, 
    birth_year: Felt, 
    birth_month: Felt, 
    birth_day: Felt,
    scores: [Felt; 3], 
    is_active: bool
) -> UserRecord {
    return (user_id, (birth_year, birth_month, birth_day), scores, is_active);
}

fn get_user_age(record: UserRecord, current_year: Felt) -> Felt {
    let birth_date = record.1;
    return current_year - birth_date.0;
}

fn calculate_average_score(record: UserRecord) -> Felt {
    let scores = record.2;
    return (scores[0] + scores[1] + scores[2]) / 3;
}

fn main() {
    let user = create_user_record(12345, 1990, 5, 15, [85, 92, 78], true);
    
    let age = get_user_age(user, 2023); // 33
    let avg_score = calculate_average_score(user); // 85
    
    let is_active = user.3;
    let birth_month = user.1.1;
}

Key Points

1. Arrays: Fixed-size, same type, indexable with [], support custom methods through generics
2. Tuples: Fixed-size, mixed types, accessible with .N, elements can be modified
3. Parameter Passing:
   • Arrays are always passed by reference
   • Tuples follow mixed semantics based on member types
4. Generic Methods: Arrays support generic methods but not specialized implementations
5. Access Patterns: Arrays use index notation, tuples use field notation
6. Type Safety: Both are statically typed with compile-time size checking
7. Mutability: Both arrays and tuples support mutable operations on their elements
8. Nested Structures: Both support arbitrary nesting levels
9. Current Limitations: Tuple destructuring is not yet implemented

Conditional Statements

This chapter covers conditional control flow in Psy: if, else if, else, and match expressions.

If Statements

Basic If-Else

The most basic form of conditional control flow is the if expression:

fn min(a: Felt, b: Felt) -> Felt {
    if a < b {
        a
    } else {
        b
    }
}

fn main() {
    let x = 5;
    let y = 10;
    let result = min(x, y);
    // result is 5
}

If as Expression

In Psy, if is an expression that returns a value:

fn main() {
    let a = 10;
    let b = 11;
    let c = 12;
    let d = 13;
    
    // If expression assigned to variable
    let basic = if a > b {
        c
    } else {
        d
    };
    
    // basic will be 13 since 10 > 11 is false
}

If-Else If-Else Chains

You can chain multiple conditions using else if:

fn main() {
    let a = 10;
    let b = 11;
    let c = 12;
    let d = 13;
    let e = 14;
    
    let result = if a > b {
        c
    } else if b > a {
        d
    } else {
        e
    };
    
    // result will be 13 since b > a (11 > 10) is true
}

Nested If Statements

If statements can be nested within other if statements:

fn middle(a: Felt, b: Felt, c: Felt) -> Felt {
    if a > b {
        if b > c {
            b
        } else if a > c {
            c
        } else {
            a
        }
    } else {
        if a > c {
            a
        } else if b > c {
            c
        } else {
            b
        }
    }
}

fn main() {
    let result = middle(5, 3, 7); // Returns 5
    let result2 = middle(1, 8, 4); // Returns 4
}

Complex Nested Examples

fn main() {
    let a = 10;
    let b = 11;
    let c = 12;
    let d = 13;
    let e = 14;
    
    // Nested if with multiple else if branches
    let embedded = if a > b {
        if a > b {
            c
        } else if b > a {
            d
        } else {
            e
        }
    } else if c > d {
        if a > b {
            c
        } else if b > a {
            d
        } else {
            e
        }
    } else {
        if a > b {
            c
        } else if b > a {
            d
        } else {
            e
        }
    };
}

If with Local Variables

You can declare variables inside if blocks:

fn main() {
    let a = 1;
    let b = 2;
    let c = 3;
    let d = 4;
    
    let result = if a > b {
        let tmp0 = 1;
        let tmp1 = 2;
        if tmp0 > tmp1 {
            tmp0
        } else {
            tmp1
        }
    } else if c > d {
        let tmp2 = 3;
        let tmp3 = 4;
        if tmp2 > tmp3 {
            tmp2
        } else {
            tmp3
        }
    } else {
        let tmp4 = 5;
        let tmp5 = 6;
        if tmp4 > tmp5 {
            tmp4
        } else {
            tmp5
        }
    };
}

If in Function Calls

If expressions can be used as arguments to function calls:

fn process(x: Felt, y: Felt) {
    // Function body
}

fn main() {
    let n1 = 1;
    let n2 = 2;
    
    process(if n1 > n2 {
        n1
    } else {
        n2
    }, n2);
}

Match Expressions

Match expressions provide a powerful way to handle multiple possible values:

Basic Match

fn match_test_case(input: Felt) -> Felt {
    match input {
        0 => 10,
        1 => 20,
        2 => 30,
        _ => 40,  // Default case
    }
}

fn main() {
    let result1 = match_test_case(0); // Returns 10
    let result2 = match_test_case(1); // Returns 20
    let result3 = match_test_case(5); // Returns 40 (default case)
}

Match with Blocks

Match arms can contain blocks for more complex logic:

#![allow(unused)]
fn main() {
fn match_with_blocks(input: Felt) -> Felt {
    let mut result = 0;
    match input {
        0 => {
            result += 10;
        },
        1 => {
            result += 20;
        },
        2 => {
            result += 30;
        },
        3 => {
            result += 40;
        },
        4 => {
            result += 40;
        },
        _ => {
            result += 50;
        },
    };
    result
}
}

Match as Expression

Match can be used as an expression to assign values:

fn main() {
    let input = 2;
    
    let base_value = match input {
        0 => 100,
        1 => 200,
        2 => 300,
        _ => 400,
    };
    
    // base_value will be 300
}

Match with Different Types

Match works with various types:

// Match with bool
fn match_bool_test(input: bool) -> Felt {
    match input {
        true => 100,
        false => 200,
    }
}

// Match with u32
fn match_u32_test(input: u32) -> Felt {
    let mut result = 0;
    match input {
        0u32 => {
            result += 5;
        },
        1u32 => {
            result += 15;
        },
        2u32 => {
            result += 25;
        },
        3u32 => {
            result += 35;
        },
        4u32 => {
            result += 45;
        },
        _ => {
            result += 55;
        },
    };
    
    let extra = match input {
        0u32 => 50,
        1u32 => 150,
        2u32 => 250,
        3u32 => 350,
        _ => 450,
    };
    
    result + extra
}

fn main() {
    let bool_result = match_bool_test(true);  // Returns 100
    let u32_result = match_u32_test(2u32);   // Returns 275 (25 + 250)
}

Complex Match Example

#![allow(unused)]
fn main() {
fn complex_match_example(input: Felt) -> Felt {
    let base = match input {
        0 => {
            let temp = 10;
            temp * 2
        },
        1 => {
            let temp = 20;
            temp + 5
        },
        2 => {
            let temp = 30;
            temp - 5
        },
        _ => {
            let temp = 40;
            temp + 10
        },
    };
    
    let multiplier = match input {
        0 => 2,
        1 => 2,
        2 => 3,
        _ => 1,
    };
    
    base * multiplier
}
}

Current Limitations

Multiple Patterns: Multiple patterns in match expressions (e.g., 0 | 1 => value) are not currently supported. Use separate match arms for each pattern:

#![allow(unused)]
fn main() {
// ❌ Not supported
match value {
    0 | 1 => result1,
    2 | 3 => result2,
    _ => default,
}

// ✅ Use this instead
match value {
    0 => result1,
    1 => result1,
    2 => result2,
    3 => result2,
    _ => default,
}
}

Important Notes

No Early Returns in Conditionals

Important: Psy does not support early returns within if statements:

#![allow(unused)]
fn main() {
fn example(x: Felt) -> Felt {
    // ❌ This will cause a compilation error
    // if x > 10 {
    //     return x * 2;
    // }
    
    // ✅ Use expression-based returns instead
    if x > 10 {
        x * 2
    } else {
        x
    }
}
}

Expression-Based Design

Both if and match are expressions in Psy, meaning they return values that can be assigned to variables or used in other expressions:

fn main() {
    let x = 5;
    
    // If as expression
    let result1 = if x > 0 { x } else { -x };
    
    // Match as expression  
    let result2 = match x {
        0 => 0,
        n => n * 2,
    };
    
    // Can be used in function calls
    process_value(if x > 0 { x } else { 0 });
}

fn process_value(value: Felt) {
    // Function implementation
}

Key Points

1. If statements are expressions that return values
2. Else if allows chaining multiple conditions
3. Nested if statements are fully supported
4. Match expressions provide pattern matching capabilities
5. No early returns are allowed in conditional blocks
6. All branches of an if expression must return the same type
7. Default case in match expressions uses _ wildcard
8. Both if and match can be used anywhere expressions are expected

Loops

This chapter covers loop constructs in Psy: while loops and for loops.

While Loops

While loops execute a block of code repeatedly as long as a condition remains true.

Basic While Loop

fn main() -> Felt {
    let mut res = 0;
    let mut i = 0;
    while i < 10 {
        res += i;
        i += 1;
    }
    res  // Returns 45 (0+1+2+...+9)
}

Fibonacci Sequence with While

fn fibonacci(a: Felt, b: Felt) -> Felt {
    let mut res = 0;
    let mut a = a;
    let mut b = b;
    let mut i = 2;
    let mut c = 0;
    
    while i <= 10 {
        let d = a + b;
        c = d;
        a = b;
        b = c;
        i += 1;
    }
    
    res = b;
    return res;
}

fn main() {
    let result = fibonacci(2, 3); // Returns 233
}

While with Complex State

fn main() {
    let mut sum = 0;
    let mut count = 0;
    let mut current = 1;
    
    while current <= 100 {
        if current % 2 == 0 {  // Even numbers only
            sum += current;
            count += 1;
        } else {
            // Do nothing for odd numbers  
        };
        current += 1;
    }
    
    // sum contains sum of all even numbers from 1 to 100
    // count contains how many even numbers were found
}

While with Arrays

#![allow(unused)]
fn main() {
struct Data {
    pub values: [Felt; 5],
    pub count: Felt,
}

fn process_data() -> Data {
    let mut data = new Data {
        values: [0; 5],
        count: 0,
    };
    
    let mut i = 0;
    while i < 5 {
        data.values[i] = i * i;  // Square of index
        data.count += 1;
        i += 1;
    }
    
    return data;
}
}

For Loops

For loops provide a way to iterate over ranges with automatic index management.

Basic For Loop

fn main() -> Felt {
    let mut sum = 0;
    for n in 0u32..100u32 {
        sum += (n as Felt);
    }
    sum  // Returns 4950 (sum of 0 to 99)
}

For Loop with Arrays

struct TestSibling {
    pub value: [Felt; 4],
}

fn main() {
    let mut test_array: [TestSibling; 3] = [
        new TestSibling { value: [1, 2, 3, 4] },
        new TestSibling { value: [5, 6, 7, 8] },
        new TestSibling { value: [9, 10, 11, 12] }
    ];

    for i in 0u32..3u32 {
        let level_index = i as Felt;
        let sibling = test_array[level_index];
        let value = sibling.value;

        // Process each element
        let sum = value[0] + value[1] + value[2] + value[3];
        
        // Modify array element
        test_array[level_index] = new TestSibling {
            value: [sum, sum, sum, sum]
        };
    }
}

For Loop with Conditionals

fn main() {
    let mut test_array: [TestSibling; 3] = [
        new TestSibling { value: [1, 2, 3, 4] },
        new TestSibling { value: [0, 0, 0, 0] },
        new TestSibling { value: [0, 0, 0, 0] }
    ];

    for i in 0u32..3u32 {
        let level_index = i as Felt;
        let sibling = test_array[level_index];
        let value = sibling.value;

        if level_index < 1 {
            // First element has specific values
            // value[0] == 1, value[1] == 2, etc.
        } else {
            // Other elements are zeros
            // value[0] == 0, value[1] == 0, etc.
        }
    }
}

For Loop with Complex Processing

#![allow(unused)]
fn main() {
fn matrix_multiplication() {
    let matrix_a: [[Felt; 3]; 3] = [
        [1, 2, 3],
        [4, 5, 6],
        [7, 8, 9]
    ];
    
    let matrix_b: [[Felt; 3]; 3] = [
        [9, 8, 7],
        [6, 5, 4],
        [3, 2, 1]
    ];
    
    let mut result: [[Felt; 3]; 3] = [[0; 3]; 3];
    
    for i in 0u32..3u32 {
        for j in 0u32..3u32 {
            let mut sum = 0;
            for k in 0u32..3u32 {
                let ii = i as Felt;
                let jj = j as Felt;
                let kk = k as Felt;
                sum += matrix_a[ii][kk] * matrix_b[kk][jj];
            }
            result[i as Felt][j as Felt] = sum;
        }
    }
}
}

For Loop with Accumulation

#![allow(unused)]
fn main() {
fn calculate_factorials() -> [Felt; 10] {
    let mut factorials = [0; 10];
    
    for i in 0u32..10u32 {
        let mut factorial = 1;
        let num = (i + 1u32) as Felt; // Calculate factorial of (i+1)
        
        for j in 1u32..(i + 2u32) {
            factorial *= j as Felt;
        }
        
        factorials[i as Felt] = factorial;
    }
    
    return factorials;
}
}

Loop Patterns

Counting Patterns

#![allow(unused)]
fn main() {
// Count up
fn count_up() {
    for i in 1u32..11u32 {  // 1 to 10
        let value = i as Felt;
        // Process value
    }
}

// Count with step
fn count_with_step() {
    for i in 0u32..10u32 {
        let value = (i * 2) as Felt;  // 0, 2, 4, 6, 8, ...
        // Process even numbers
    }
}

// Count down (using while)
fn count_down() {
    let mut i = 10;
    while i > 0 {
        // Process i
        i -= 1;
    }
}
}

Array Processing Patterns

#![allow(unused)]
fn main() {
// Initialize array
fn initialize_array() -> [Felt; 5] {
    let mut arr = [0; 5];
    for i in 0u32..5u32 {
        arr[i as Felt] = (i + 1) as Felt;
    }
    return arr; // [1, 2, 3, 4, 5]
}

// Sum array elements
fn sum_array(arr: [Felt; 5]) -> Felt {
    let mut sum = 0;
    for i in 0u32..5u32 {
        sum += arr[i as Felt];
    }
    return sum;
}

// Find maximum
fn find_max(arr: [Felt; 5]) -> Felt {
    let mut max = arr[0];
    for i in 1u32..5u32 {
        let current = arr[i as Felt];
        if current > max {
            max = current;
        }
    }
    return max;
}
}

Nested Loop Patterns

#![allow(unused)]
fn main() {
// Create multiplication table
fn multiplication_table() -> [[Felt; 10]; 10] {
    let mut table = [[0; 10]; 10];
    
    for i in 0u32..10u32 {
        for j in 0u32..10u32 {
            let ii = i as Felt;
            let jj = j as Felt;
            table[ii][jj] = (ii + 1) * (jj + 1);
        }
    }
    
    return table;
}

// Process 2D grid
fn process_grid() {
    let mut grid: [[Felt; 5]; 5] = [[0; 5]; 5];
    
    for row in 0u32..5u32 {
        for col in 0u32..5u32 {
            let r = row as Felt;
            let c = col as Felt;
            
            // Set diagonal elements to 1
            if r == c {
                grid[r][c] = 1;
            } else {
                grid[r][c] = r + c;
            }
        }
    }
}
}

Search Patterns

#![allow(unused)]
fn main() {
// Linear search
fn linear_search(arr: [Felt; 10], target: Felt) -> Felt {
    for i in 0u32..10u32 {
        if arr[i as Felt] == target {
            return i as Felt;  // Return index
        }
    }
    return 10;  // Not found (return invalid index)
}

// Search with condition
fn find_first_even(arr: [Felt; 10]) -> Felt {
    for i in 0u32..10u32 {
        let value = arr[i as Felt];
        if value % 2 == 0 {
            return value;
        }
    }
    return 0;  // No even number found
}
}

Loop Control Notes

Range Syntax

For loops in Psy use range syntax:

#![allow(unused)]
fn main() {
// Inclusive ranges
for i in 0u32..5u32 {  // i goes from 0 to 4 (5 is excluded)
    // Loop body
}

// Must specify u32 type for ranges
for i in 1u32..10u32 {  // i goes from 1 to 9
    let value = i as Felt;  // Convert to Felt if needed
    // Process value
}
}

Type Conversions in Loops

fn main() {
    for i in 0u32..10u32 {
        let index = i as Felt;        // Convert u32 to Felt for array indexing
        let squared = index * index;   // Felt arithmetic
        
        // Use index for array operations
        let mut arr = [0; 10];
        arr[index] = squared;
    }
}

Loop Variable Scope

fn main() {
    // Loop variable 'i' is only available inside the loop
    for i in 0u32..5u32 {
        let doubled = (i * 2) as Felt;
        // 'i' and 'doubled' are available here
    }
    // 'i' is not available here
    
    let mut counter = 0;
    while counter < 5 {
        let temp = counter * 2;
        // 'counter' and 'temp' are available here
        counter += 1;
    }
    // 'counter' is still available here (declared outside loop)
    // 'temp' is not available here
}

Important Considerations

Psy vs Rust Syntax Differences

Psy has some important syntax differences from Rust:

#![allow(unused)]
fn main() {
// ❌ Psy requires explicit u32 type in arithmetic
for i in 0u32..10u32 {
    let value = (i + 1) as Felt;     // Error: type mismatch
}

// ✅ Correct: use explicit u32 literals
for i in 0u32..10u32 {
    let value = (i + 1u32) as Felt;  // Correct
}

// ❌ If statements as statements need semicolons
if condition {
    // do something
} else {
    // do something else
}
next_statement();  // Error: missing semicolon

// ✅ Correct: add semicolon after if-else statement
if condition {
    // do something  
} else {
    // do something else
};  // Required semicolon
next_statement();
}

No Break or Continue

Psy loops do not support break or continue statements. Loop control must be managed through conditions:

#![allow(unused)]
fn main() {
// ❌ Not supported
// for i in 0u32..10u32 {
//     if condition {
//         break;
//     }
// }

// ✅ Use conditional logic instead
fn controlled_loop() {
    let mut should_continue = true;
    let mut i = 0;
    
    while i < 10 && should_continue {
        // Process logic
        if some_condition {
            should_continue = false;  // Equivalent to break
        } else {
            // Process normally
        }
        i += 1;
    }
}
}

Loop Unrolling for ZK

Since Psy compiles to zero-knowledge circuits, loops are unrolled at compile time. This means:

1. Fixed iterations: Loop bounds must be known at compile time
2. No dynamic bounds: Cannot loop based on runtime values
3. Resource usage: Each loop iteration becomes part of the circuit

#![allow(unused)]
fn main() {
// ✅ Valid: Fixed bounds known at compile time
for i in 0u32..100u32 {
    // Loop body
}

// ❌ Invalid: Runtime-dependent bounds
fn invalid_loop(n: Felt) {
    // This would not work as n is not known at compile time
    // for i in 0u32..n {  
    //     // Loop body
    // }
}
}

Key Points

1. While loops execute while a condition is true
2. For loops iterate over fixed ranges with u32 indices
3. No break/continue - use conditional logic instead
4. Fixed bounds - loop iterations must be compile-time constant
5. Type conversion - convert u32 loop indices to Felt for array access
6. Nested loops are fully supported
7. Loop unrolling - all loops are unrolled in the final circuit
8. Scope rules - loop variables have block scope
9. Syntax differences from Rust:
   • u32 arithmetic requires explicit u32 literals (e.g., i + 1u32)
   • If-else statements used as statements need trailing semicolons
   • Empty else blocks should contain at least one statement