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.
Use this skill for the two-stage Shentu proof submission flow.
python3 and shentud, reads shared openmath-env.json, queries/broadcasts to a Shentu RPC endpoint, and uses the local OS keyring for signing flows.prover_address (the user's OpenMath Wallet Address).--config <path> → 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_ID and SHENTU_NODE_URL or built-in defaults, not from .openmath-env.json--keyring-backend os for local key lookups and generated submission commands.generate_submission.py --mode direct.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.
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, and treat any config write or key creation/recovery as an explicit-user-approval step, then validate:
python3 scripts/check_authz_setup.py [--config <path>]
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.
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.openmath-env.json exists in ./.openmath-skills/ or ~/.openmath-skills/, and check_authz_setup.py reports Status: ready.generate_submission.py hash <theoremId> <proofPath> <proverKeyOrAddress> <proverAddr> only after the first-run gate passes; this generates the commitment hash and the corresponding shentud tx authz exec proofhash.json ... --fee-granter <prover-address> flow.query_submission_status.py tx <txhash> --wait-seconds 6. Confirm proof in PROOF_STATUS_HASH_LOCK_PERIOD and record proof_id.generate_submission.py detail <proofId> <proofPath> <proverKeyOrAddress> only after the first-run gate passes; this reveals the proof detail and emits the corresponding shentud tx authz exec proofdetail.json ... --fee-granter <prover-address> flow. Do not wait for hash lock expiry.query_submission_status.py theorem <theoremId> --wait-seconds 6. Confirm theorem reaches THEOREM_STATUS_PASSED.| Script | Command | Use when |
|---|---|---|
| Authz readiness | python3 scripts/check_authz_setup.py [--config <path>] | Before first submission and when changing env; validates CLI, keys, RPC, authz, feegrant. |
| Stage 1 commands | python3 scripts/generate_submission.py hash <theoremId> <proofPath> <proverKeyOrAddress> <proverAddr> | 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 <proofId> <proofPath> <proverKeyOrAddress> | 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 <txhash> [--wait-seconds 6] | After broadcast to confirm inclusion. |
| Query theorem | python3 scripts/query_submission_status.py theorem <theoremId> [--wait-seconds 6] | Final status check. |
| Proof hash (debug) | python3 scripts/calculate_proof_hash.py <theoremId> <proverAddress> <proofContentOrFile> | 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 flowreferences/init-setup.md: openmath-env.json, local key setup, and the normal website authorization flowreferences/authz_setup.md: manual authz + feegrant CLI fallback after setupshentud tx authz exec with --fee-granter <prover-address>. For direct signer use --mode direct on generate_submission.py.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.$HOME/bin/shentud. Verify with command -v shentud and shentud version before submission.references/init-setup.md and references/openmath-env.example.json instead of having the skill rewrite openmath-env.json.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.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.PATH affects local python3 / shentud discovery, and references may use $HOME/bin when showing non-persistent local install examples.Load when needed (one level from this file):
openmath-env.json.