update docs

docs/specs.md

@@ -14,6 +14,7 @@ type InstructionData = List<u32>;
 
 /// Sequencer-supplied block height and timestamp.
 type BlockId = u64;
+/// Unix timestamp in milliseconds.
 type Timestamp = u64;
 
 /// Diversifies private accounts for a given NPK.
@@ -699,43 +700,52 @@ NSSA v0.3 supports the following built-in programs, loaded at genesis. They are
 
 ### Authorized transfer program
 
-Moves native tokens from a source account to a destination account, requiring the source account to be authorized. Has two modes selected by the instruction (`u128`):
+Moves native tokens from a source account to a destination account, requiring the source account to be authorized. Has two instruction variants:
 
-- `balance_to_move == 0` with a single pre-state: claims the pre-state account on behalf of the caller (a self-init).
-- `balance_to_move != 0` with two pre-states `[sender, recipient]`: standard transfer. The recipient is claimed only if its `program_owner` is currently the default — pre-existing accounts owned by other programs keep their owner.
+- `Initialize` with a single pre-state: claims the pre-state account (which must be `Account::default()`) on behalf of the caller. Authorization is enforced by the runtime when processing `Claim::Authorized`.
+- `Transfer { amount }` with two pre-states `[sender, recipient]`: standard transfer. Sender must be authorized. The recipient is claimed only if its `program_owner` is currently the default — pre-existing accounts owned by other programs keep their owner.
 
 ```rust
-/// Instruction data: u128 amount to transfer (0 means initialize-account).
+pub enum Instruction {
+    /// Initialize a new account under the ownership of this program.
+    /// Required accounts: `[account_to_initialize]`.
+    Initialize,
+
+    /// Transfer `amount` of native balance from sender to recipient.
+    /// Required accounts: `[sender, recipient]`.
+    Transfer { amount: u128 },
+}
+
 fn transfer_authorized(
     self_program_id: ProgramId,
     caller_program_id: Option<ProgramId>,
     pre_states: Vec<AccountWithMetadata>,
-    balance_to_move: u128,
+    instruction: Instruction,
 ) -> (Vec<AccountWithMetadata>, Vec<AccountPostState>, Vec<ChainedCall>) {
-    let post_states = match (pre_states.as_slice(), balance_to_move) {
-        ([account_to_claim], 0) => {
+    let post_states = match instruction {
+        Instruction::Initialize => {
+            let [account_to_claim] = <[_; 1]>::try_from(pre_states.clone()).unwrap();
             assert_eq!(account_to_claim.account, Account::default());
-            assert!(account_to_claim.is_authorized);
             vec![AccountPostState::new_claimed(
                 account_to_claim.account.clone(),
                 Claim::Authorized,
             )]
         }
-        ([sender, recipient], balance_to_move) => {
+        Instruction::Transfer { amount } => {
+            let [sender, recipient] = <[_; 2]>::try_from(pre_states.clone()).unwrap();
             assert!(sender.is_authorized, "Sender must be authorized");
 
             let mut sender_post = sender.account.clone();
-            sender_post.balance = sender_post.balance.checked_sub(balance_to_move).unwrap();
+            sender_post.balance = sender_post.balance.checked_sub(amount).unwrap();
 
             let mut recipient_post = recipient.account.clone();
-            recipient_post.balance = recipient_post.balance.checked_add(balance_to_move).unwrap();
+            recipient_post.balance = recipient_post.balance.checked_add(amount).unwrap();
 
             vec![
                 AccountPostState::new(sender_post),
                 AccountPostState::new_claimed_if_default(recipient_post, Claim::Authorized),
             ]
         }
-        _ => panic!("invalid params"),
     };
 
     (pre_states, post_states, vec![])
@@ -762,12 +772,9 @@ fn pinata(
 
     let challenge = Challenge::parse(&pinata.account.data);
     if !challenge.validate_solution(solution) {
-        // No valid solution: emit unchanged states and return.
-        let post_states = vec![
-            AccountPostState::new(pinata.account.clone()),
-            AccountPostState::new(winner.account.clone()),
-        ];
-        return (pre_states, post_states, vec![]);
+        // No valid solution: the program exits without writing any output,
+        // causing the sequencer to reject the transaction entirely.
+        return;
     }
 
     let mut pinata_post = pinata.account.clone();
@@ -931,6 +938,50 @@ The clock accounts are created at genesis and assigned `program_owner = clock_pr
 
 On execution, the program reads `block_id` from the `01` account, increments it, and updates each of the three clock accounts only when `new_block_id` is a multiple of the corresponding cadence.
 
+### Vault program
+
+Provides a native-token escrow via per-user vault PDAs. Each user's vault is a PDA of the Vault program keyed by the user's account ID. Two instructions:
+
+- `Transfer { recipient_id, amount }` — accounts: `[sender, recipient, recipient_vault_pda]`. Sender must be authorized. Transfers `amount` native tokens from `sender` to the vault PDA of `recipient_id`. The vault PDA is claimed on first use.
+- `Claim { amount }` — accounts: `[owner, owner_vault_pda]`. Owner must be authorized. Withdraws `amount` native tokens from the owner's vault PDA back to the owner's account.
+
+Vault PDA seed derivation:
+
+```rust
+const VAULT_SEED_DOMAIN_SEPARATOR: &[u8; 32] = b"/LEZ/v0.3/VaultSeed/00000000000/";
+
+pub fn compute_vault_seed(owner_id: AccountId) -> PdaSeed {
+    let mut bytes = [0_u8; 64];
+    bytes[..32].copy_from_slice(VAULT_SEED_DOMAIN_SEPARATOR);
+    bytes[32..64].copy_from_slice(&owner_id.to_bytes());
+    PdaSeed::new(sha256(bytes))
+}
+
+pub fn compute_vault_account_id(vault_program_id: ProgramId, owner_id: AccountId) -> AccountId {
+    AccountId::for_public_pda(&vault_program_id, &compute_vault_seed(owner_id))
+}
+```
+
+### Faucet program
+
+Manages the system faucet, a pre-funded account used to distribute native tokens. The faucet account is a public PDA of the Faucet program, created at genesis. One instruction:
+
+- `Transfer { vault_program_id, recipient_id, amount }` — accounts: `[faucet_pda, recipient_vault_pda]`. Transfers `amount` native tokens from the system faucet to the vault PDA of `recipient_id`. User-submitted transactions cannot invoke the Faucet program directly; only sequencer-originated transactions may do so.
+
+Faucet PDA seed and account derivation:
+
+```rust
+const FAUCET_SEED_DOMAIN_SEPARATOR: [u8; 32] = *b"/LEZ/v0.3/FaucetSeed/0000000000/";
+
+pub fn compute_faucet_seed() -> PdaSeed {
+    PdaSeed::new(FAUCET_SEED_DOMAIN_SEPARATOR)
+}
+
+pub fn compute_faucet_account_id(faucet_program_id: ProgramId) -> AccountId {
+    AccountId::for_public_pda(&faucet_program_id, &compute_faucet_seed())
+}
+```
+
 ### Built-in program registry
 
 The genesis state ships with the following built-in programs registered:
@@ -940,8 +991,9 @@ The genesis state ships with the following built-in programs registered:
 - AMM (`AMM_ID`)
 - Associated Token Account (`ASSOCIATED_TOKEN_ACCOUNT_ID`)
 - Clock (`CLOCK_ID`)
+- Vault (`VAULT_ID`)
+- Faucet (`FAUCET_ID`)
 - Piñata (`PINATA_ID`) — testnet only
-- Piñata Token (`PINATA_TOKEN_ID`) — testnet only
 
 All built-in programs are part of the trusted computing base, registered at genesis, and immutable. Additional user-defined programs may also be deployed via `ProgramDeploymentTransaction` (see "State transition from program deployment transactions").
 
@@ -1036,7 +1088,17 @@ The hash is `SHA256(PREFIX || borsh_serialize(message))`.
 
 The circuit is a RISC-V program proven with the risc0 zkVM. It is executed entirely off-chain by the transaction sender; the sequencer only verifies the proof. It is not a built-in program in the NSSA sense — it wraps the execution of built-in programs inside a ZK proof.
 
-The circuit supports a single chain of tail-calls (each program invocation may chain to at most one subsequent program).
+**Workflow:**
+The circuit takes as private inputs a `PrivacyPreservingCircuitInput`: the sequence of `ProgramOutput`s for each call in the execution chain, one `InputAccountIdentity` per pre-state (carrying nullifier secret keys, shared secret keys, membership proofs, and identifiers as required by each account variant), and the top-level program ID.
+
+1. Verify that each `ProgramOutput` in the chain has a valid proof of execution for the corresponding program.
+2. Verify that `validate_execution` passes for each program call.
+3. Check that chained-call instruction data and accounts are consistent across caller/callee boundaries.
+4. For each account:
+   - Public: collect pre/post state; increment nonce if authorized.
+   - Private init: verify pre-state is default; derive account_id; compute init nullifier; set nonce via `nonce_init`; encrypt post-state.
+   - Private update: verify membership proof; compute update nullifier; increment nonce via `nonce_increment`; encrypt post-state.
+5. Emit `PrivacyPreservingCircuitOutput`.
 
 ### Circuit input
 
@@ -1128,22 +1190,12 @@ For each `InputAccountIdentity` the circuit performs the following:
 | `PrivateAuthorizedUpdate` | `from_private(npk(nsk), ident)` | `nonce_increment(nsk)` | update nullifier | nsk + membership proof | **not enforced** (skipped) |
 | `PrivateUnauthorized` | `from_private(npk, ident)` | `nonce_init(account_id)` | init nullifier | none | **not enforced** (skipped) |
 | `PrivatePdaInit` | `for_private_pda(prog, seed, npk, ident)` | `nonce_init(account_id)` | init nullifier | pda_seeds/Claim::Pda | `is_authorized` must be `true` |
-| `PrivatePdaUpdate` | `for_private_pda(prog, seed, npk(nsk), ident)` | `nonce_increment(nsk)` | update nullifier | nsk + membership proof | `is_authorized` must be `true` |
+| `PrivatePdaUpdate` | `for_private_pda(prog, seed, npk(nsk), ident)` | `nonce_increment(nsk)` | update nullifier | pda_seeds + nsk + membership proof | `is_authorized` must be `true` |
 
 For each private account the post-state commitment is `Commitment::new(account_id, post_account)` (with the new nonce applied). The ciphertext is `EncryptionScheme::encrypt(post_account, kind, ssk, commitment, output_index)`.
 
-The chain-of-calls logic and `validate_execution` rules are identical to the public execution path. The claiming rules diverge for **standalone private accounts only**: `Claim::Authorized` on a `Regular` private kind is allowed unconditionally (no `is_authorized` check), because operating these accounts already requires possession of the corresponding `nsk`. For public accounts and private PDAs, `Claim::Authorized` enforcement matches the public path.
+The chain-of-calls logic and `validate_execution` rules are identical to the public execution path. The claiming rules diverge for **standalone private accounts only**: `Claim::Authorized` on a `Regular` private kind is allowed unconditionally (no `is_authorized` check). For public accounts and private PDAs, `Claim::Authorized` enforcement matches the public path.
 
-**Workflow:**
-
-1. Verify that each `ProgramOutput` in the chain is a valid proof of execution for the corresponding program.
-2. Verify that `validate_execution` passes for each program call.
-3. Check that chained-call instruction data and accounts are consistent across caller/callee boundaries.
-4. For each account:
-   - Public: collect pre/post state; increment nonce if authorized.
-   - Private init: verify pre-state is default; derive account_id; compute init nullifier; set nonce via `nonce_init`; encrypt post-state.
-   - Private update: verify membership proof; compute update nullifier; increment nonce via `nonce_increment`; encrypt post-state.
-5. Emit `PrivacyPreservingCircuitOutput`.
 
 ## Encrypted private account discovery and tagging