--- name: openmath-submit-theorem description: Submits proofs to the OpenMath platform using a two-stage commit-reveal flow. Use when the user wants to commit a proof hash or reveal a Lean/Rocq proof on the Shentu network. version: v1.0.7 requirements: commands: - python3 - shentud side_effects: - Reads shared openmath-env.json from --config, OPENMATH_ENV_CONFIG, or the standard project/user config locations - Queries and broadcasts to a remote Shentu RPC endpoint; defaults to https://rpc.shentu.org:443 unless SHENTU_NODE_URL overrides it - Uses the local OS keyring through shentud --keyring-backend os for key lookups and authz-exec signing - Reads PATH and optional OPENMATH_SHENTUD_BIN to discover shentud; may suggest a temporary PATH export or a trusted explicit binary path, but does not install binaries or edit shell startup files - Default flow treats openmath-env.json creation or editing, shentud installation, and local key creation or recovery as manual setup steps documented in references --- # OpenMath Submit Theorem ## Instructions Use this skill for the two-stage Shentu proof submission flow. - Stage 1 submits a proof hash as a commitment so others can see you already know the answer without learning the proof details. - Stage 2 submits the proof detail to reveal and verify the same proof on-chain. - This is an operational skill, not an instruction-only note: it shells out to trusted local `python3` and `shentud`, reads shared `openmath-env.json`, queries/broadcasts to a Shentu RPC endpoint, and uses the local OS keyring for signing flows. - Default: authz + feegrant from `prover_address` (the user's OpenMath Wallet Address). - Shared config resolution order: `--config ` → `OPENMATH_ENV_CONFIG` → `./.openmath-skills/openmath-env.json` → `~/.openmath-skills/openmath-env.json`. If `OPENMATH_ENV_CONFIG` is set, treat it as the selected config path. If that file is missing or invalid, stop and fix it instead of silently falling back. - Shentu chain/RPC settings come from `SHENTU_CHAIN_ID` and `SHENTU_NODE_URL` or built-in defaults, not from `openmath-env.json`. - The skill always uses `--keyring-backend os` for local key lookups and generated submission commands. - Direct signer fallback: `generate_submission.py --mode direct`. - Required local dependencies are `python3` and `shentud`. Environment variables are optional overrides, not mandatory setup: `OPENMATH_ENV_CONFIG`, `OPENMATH_SHENTUD_BIN`, `OPENMATH_SUBMISSION_MODE`, `OPENMATH_INNER_TX_FEES`, `OPENMATH_INNER_TX_GAS`, `SHENTU_CHAIN_ID`, and `SHENTU_NODE_URL`. For least-privilege operation, treat `openmath-env.json` creation or editing, `shentud` installation, and local key creation or recovery as manual prerequisites documented in `references/`. The default skill flow may run read-only checks such as `command -v shentud`, `shentud version`, or `shentud keys show`, but it should not auto-install binaries, auto-edit config files, or run `shentud keys add` as part of normal execution. Before any action that writes `openmath-env.json` or creates or recovers a local key, get explicit user approval. `shentud` installation should stay a manual user step, guided by the reference docs rather than performed by the skill. Prefer the official Shentu releases page plus a user-local install at `$HOME/bin/shentud`, and use `OPENMATH_SHENTUD_BIN` only as an explicit fallback. Do not generate or manage mnemonics on the user's machine without that approval. ### First-run gate If the selected `openmath-env.json` is missing, or if it exists but is missing `prover_address`, `agent_address`, or `agent_key_name`, **do not proceed**. Follow [references/init-setup.md](references/init-setup.md), and treat any config write or key creation/recovery as an explicit-user-approval step, then validate: ```bash python3 scripts/check_authz_setup.py [--config ] ``` Require `Status: ready` before any submission. Repeat on each new machine or workspace. This gate is mandatory for authz-mode scripts that advance the submission flow. `generate_submission.py` must not produce authz `proof-hash` or `proof-detail` commands until `check_authz_setup.py` returns `Status: ready`. Read-only status polling via `query_submission_status.py` is exempt. ### Workflow checklist - [ ] **Manual prerequisites**: If `shentud` is missing, use `references/submission_guidelines.md` for manual binary install. If `openmath-env.json` is missing or incomplete, or the local `os` key does not exist yet, use `references/init-setup.md`. If authz or feegrant is still missing after setup, use `references/authz_setup.md`. The default skill flow should not auto-edit config files, auto-install `shentud`, or auto-create or recover keys. - [ ] **Env**: `openmath-env.json` exists in `./.openmath-skills/` or `~/.openmath-skills/`, and `check_authz_setup.py` reports `Status: ready`. - [ ] **Stage 1 (Commit)**: Run `generate_submission.py hash ` only after the first-run gate passes; this generates the commitment hash and the corresponding `shentud tx authz exec proofhash.json ... --fee-granter ` flow. - [ ] **Wait**: 5–10 s, then `query_submission_status.py tx --wait-seconds 6`. Confirm proof in `PROOF_STATUS_HASH_LOCK_PERIOD` and record `proof_id`. - [ ] **Stage 2 (Reveal)**: Run `generate_submission.py detail ` only after the first-run gate passes; this reveals the proof detail and emits the corresponding `shentud tx authz exec proofdetail.json ... --fee-granter ` flow. Do not wait for hash lock expiry. - [ ] **Verify**: Wait 5–10 s, then `query_submission_status.py theorem --wait-seconds 6`. Confirm theorem reaches `THEOREM_STATUS_PASSED`. ### Scripts | Script | Command | Use when | |--------|---------|----------| | Authz readiness | `python3 scripts/check_authz_setup.py [--config ]` | Before first submission and when changing env; validates CLI, keys, RPC, authz, feegrant. | | Stage 1 commands | `python3 scripts/generate_submission.py hash ` | Generating `proofhash.json` and the broadcast command for the commitment stage. In authz mode, refuses to continue until the first-run gate passes. | | Stage 2 commands | `python3 scripts/generate_submission.py detail ` | Generating `proofdetail.json` and the broadcast command for the reveal stage (use `proof_id` from Stage 1). In authz mode, refuses to continue until the first-run gate passes. | | Query tx | `python3 scripts/query_submission_status.py tx [--wait-seconds 6]` | After broadcast to confirm inclusion. | | Query theorem | `python3 scripts/query_submission_status.py theorem [--wait-seconds 6]` | Final status check. | | Proof hash (debug) | `python3 scripts/calculate_proof_hash.py ` | Standalone hash check; normally used by generate_submission. | `submission_config.py` loads and validates only the identity/authz fields in `openmath-env.json` using the shared config resolution order above. Chain/RPC settings come from `SHENTU_CHAIN_ID` and `SHENTU_NODE_URL`. Reference split: - `references/submission_guidelines.md`: manual binary install, pre-submission checks, and the two-stage submit flow - `references/init-setup.md`: `openmath-env.json`, local key setup, and the normal website authorization flow - `references/authz_setup.md`: manual authz + feegrant CLI fallback after setup ### Notes - **Authz**: Default flow uses `shentud tx authz exec` with `--fee-granter `. For direct signer use `--mode direct` on `generate_submission.py`. - **Commit-reveal**: Stage 1 publishes only the proof hash as a commitment, which reduces proof leakage and front-running risk while reserving your claim. Stage 2 reveals the full proof detail for verification. - **Key material**: Treat local key creation or recovery as a manual step. If `shentud keys add` is needed, show the user the documented commands in the references instead of running them from the skill, and warn that mnemonics or recovery material may be shown. - **Binary setup**: Manual binary setup is required. Prefer a trusted release binary installed at `$HOME/bin/shentud`. Verify with `command -v shentud` and `shentud version` before submission. - **Config editing**: Manual config setup is preferred. Point the user to `references/init-setup.md` and `references/openmath-env.example.json` instead of having the skill rewrite `openmath-env.json`. - **Binary resolution**: Check the plain `shentud` command first. If `shentud` already works from `PATH`, do not force a separate binary path. Set `OPENMATH_SHENTUD_BIN` only as a fallback when the default `shentud` lookup is missing or broken and you need a specific trusted binary. - **Advanced env vars**: `OPENMATH_SUBMISSION_MODE` changes the default `generate_submission.py --mode` (`authz` by default). `OPENMATH_INNER_TX_FEES` and `OPENMATH_INNER_TX_GAS` override the generated inner `--generate-only` tx fees/gas in authz mode. - **Local shell env**: `PATH` affects local `python3` / `shentud` discovery, and references may use `$HOME/bin` when showing non-persistent local install examples. - **Block wait**: After each broadcast wait ~5–10 s before querying. ## References Load when needed (one level from this file): - **[references/init-setup.md](references/init-setup.md)** — Config-first env setup, local key resolution, and the normal website authorization flow. - **[references/openmath-env.example.json](references/openmath-env.example.json)** — Template for `openmath-env.json`. - **[references/submission_guidelines.md](references/submission_guidelines.md)** — Manual binary install, pre-submission checks, commit-reveal execution, and status verification. - **[references/authz_setup.md](references/authz_setup.md)** — Manual authz grants and feegrant fallback after setup.

openmath-submit-theorem

Description

Latest Changes

Install openmath-submit-theorem with One Click