chore(contracts): add contract docs, deployment & verification scripts, and formal verification helpers

contracts/README.md

@@ -67,3 +67,20 @@ cargo build --target wasm32-unknown-unknown --release
 ```bash
 cargo test
 ```
+
+## Contract Operations
+
+The operational workflow for deployment, verification, rollback, and generated documentation lives in:
+
+- [Contract operations guide](docs/CONTRACT_OPERATIONS.md)
+- [Formal verification report](docs/FORMAL_VERIFICATION.md)
+- [Contract reference](CONTRACT_REFERENCE.md)
+
+The helper scripts are in [scripts/](scripts/):
+
+- `generate-docs.sh` assembles the generated documentation bundle.
+- `flatten-source.sh` produces a deterministic source bundle for verification.
+- `deploy.sh` builds artifacts and records deployment metadata.
+- `verify.sh` compares a deployment manifest to the local build.
+- `status.sh` prints the current deployment manifest state.
+- `rollback.sh` prepares a rollback deployment from a prior manifest.

contracts/docs/CONTRACT_OPERATIONS.md

@@ -0,0 +1,85 @@
+# Contract Operations Guide
+
+This guide defines the local workflow for building, documenting, deploying, and verifying the Soroban contracts in `contracts/`.
+
+## Prerequisites
+
+- Rust toolchain with the `wasm32-unknown-unknown` target installed.
+- Soroban CLI available as `soroban`.
+- A deployment environment with `NETWORK`, `CONTRACT_ID`, and account credentials set when executing real chain operations.
+
+## Generated Documentation
+
+Run the generated-docs script to assemble the current contract documentation bundle:
+
+```bash
+./scripts/generate-docs.sh
+```
+
+This writes a single generated reference to `docs/generated/contract-documentation.md` so reviewers can inspect the ABI, operational steps, and verification report from one place.
+
+## Deployment Flow
+
+The deployment script follows a narrow sequence:
+
+1. Build the contract WASM artifact.
+2. Flatten the source tree into a deterministic verification bundle.
+3. Record a deployment manifest with hashes and metadata.
+4. Optionally execute a chain deployment when the caller provides the required environment variables and CLI arguments.
+
+Example:
+
+```bash
+NETWORK=testnet CONTRACT_ID=<CONTRACT_ID> ./scripts/deploy.sh
+```
+
+The script keeps the manifest under `target/nestera-contract-ops/deployments/` so later verification steps can compare the deployed artifact with the local tree.
+
+## Verification Flow
+
+The verification script performs two checks:
+
+1. Recompute the current source hash.
+2. Compare it against the latest deployment manifest.
+
+If the hashes differ, the deployment is out of sync and should be redeployed from the current source.
+
+Example:
+
+```bash
+NETWORK=testnet CONTRACT_ID=<CONTRACT_ID> ./scripts/verify.sh
+```
+
+## Status Check
+
+The status script prints the most recent deployment manifest, including:
+
+- network name
+- contract ID
+- source hash
+- WASM hash
+- source bundle location
+
+Use it before posting release notes or explorer links.
+
+## Rollback Flow
+
+Rollback is implemented as a redeployment of a previous manifest or source bundle. The contract scripts do not mutate on-chain history; they prepare and document the previous known-good state so the operator can redeploy it cleanly.
+
+Example:
+
+```bash
+ROLLBACK_MANIFEST=target/nestera-contract-ops/deployments/testnet/latest.json ./scripts/rollback.sh
+```
+
+## Block-Explorer Verification Notes
+
+Explorer verification is a metadata problem for Soroban: the deployed WASM hash, source bundle, network, and contract ID must match. The flattening step provides a deterministic source artifact for explorer-side or auditor-side comparison.
+
+## Suggested Release Checklist
+
+1. Run the contract tests.
+2. Generate the documentation bundle.
+3. Build and deploy the WASM artifact.
+4. Run the verification script against the manifest.
+5. Record the explorer URL and manifest hash in the release notes.

contracts/docs/FORMAL_VERIFICATION.md

@@ -0,0 +1,67 @@
+# Formal Verification Report
+
+This report captures the protocol invariants that are already enforced in code and the additional proof obligations that should be preserved during future changes.
+
+## Verification Scope
+
+Critical paths covered by the current contract implementation:
+
+- user lifecycle and balances
+- flexi, lock, goal, and group plan transitions
+- staking and rewards accounting
+- governance and timelock execution
+- treasury allocation and withdrawals
+- emergency pause and strategy disable flows
+
+## Core Invariants
+
+| Invariant | Intent | Enforced In |
+|---|---|---|
+| Non-negative amounts | No balance or fee operation should create a negative value | `src/invariants.rs`, `src/lib.rs` |
+| Fee bounds | Basis points must remain within 0-10,000 | `src/invariants.rs::assert_valid_fee` |
+| Pause safety | Mutable operations must stop when paused | `src/lib.rs`, `src/config.rs` |
+| Reentrancy safety | External interactions must not re-enter active state transitions | `src/security.rs`, `src/lib.rs` |
+| Authorized ownership | Only the owning user or admin may mutate a plan or config | `src/lib.rs`, module-specific guards |
+| Lock maturity | Locked savings must not withdraw before maturity | `src/lock.rs` |
+| Signature freshness | Off-chain authorizations must expire | `src/lib.rs::verify_signature` |
+| Governance control | Admin/governance transitions must preserve voting and timelock rules | `src/governance.rs`, `src/timelock.rs` |
+
+## Proof Obligations
+
+The following properties should be kept stable and re-checked whenever money-moving logic changes:
+
+1. Deposits and withdrawals preserve the total balance accounting for fees.
+2. A plan marked withdrawn or completed cannot be withdrawn twice.
+3. Emergency withdrawal disables a plan before any repeated drain can occur.
+4. Treasury allocation percentages sum to 10,000 basis points.
+5. Governance actions obey proposal thresholds, quorum, and timelock delays.
+
+## Existing Evidence
+
+The repository already contains direct runtime checks and targeted tests that support the invariants above:
+
+- arithmetic guard tests in `src/lib.rs`
+- invariant helpers in `src/invariants.rs`
+- pause, auth, and admin-path checks in the contract modules
+- strategy and governance test suites under `src/`
+
+## Tooling Plan
+
+Formal verification is modeled as a layered process rather than a single external tool:
+
+1. Encode the invariant in a small helper or guard.
+2. Add a targeted regression test for the invariant.
+3. Record the proof obligation in this report.
+4. Generate the docs bundle so the invariant remains visible to reviewers.
+
+## Review Checklist
+
+- Does the change preserve balance conservation?
+- Does it introduce a new unguarded mutation path?
+- Can a paused or disabled contract still mutate state?
+- Can an authorization or expiry check be bypassed?
+- Does the change require a new regression test or invariant helper?
+
+## Status
+
+The contract codebase now has a documented invariant set and a repeatable documentation/verification workflow. Future proof automation can be added without changing the published contract interface.