fix: harden SMT, JSON input, and TVM gas estimation

[yanghang8612]

Summary

• complete the SMTChecker model for TRON chain.*, msg.tokenid, and msg.tokenvalue magic members
• preserve conservative state invalidation for TRON state-changing builtins while constraining their uint return values
• keep nonpayable transaction-value assumptions off library functions, matching their DELEGATECALL runtime semantics
• reject malformed Standard JSON containers, scalar fields, debug-info components, and SMT response maps with structured JSONError results
• align GasMeter and optimizer cost models with TVM memory, MCOPY, NATIVEVOTE, CREATE2, and EXP rules
• refresh TRON-specific compiler and SMT test baselines for token guards and sun/trx denominations

Root cause and impact

The TRON transaction tuple used by SMTChecker did not include all magic members exposed by the type system. Legal contracts could therefore hit an assertion or an uncaught map lookup, and nonpayable functions did not constrain TRC-10 call fields. In addition, state-changing TRON builtins with uint returns were left as unbounded mathematical integers after symbolic state invalidation, which could produce false BMC/CHC counterexamples.

Nonpayable constraints were also applied to public library functions even though both code generators intentionally omit value and token guards for libraries. Since DELEGATECALL preserves the caller's transaction context, this allowed BMC and CHC to falsely prove assertions about msg.value, msg.tokenid, and msg.tokenvalue. Library entry points now remain unconstrained while ordinary nonpayable contracts retain the zero-value assumptions.

Standard JSON validation skipped type checks for some empty JSON values and performed unchecked string conversions for language and settings.debug.debugInfo. Malformed input could therefore be silently accepted or surface as an internal nlohmann exception. The parser now validates these shapes before conversion and consistently returns JSONError.

Gas estimation used wrapping u256 arithmetic for memory ranges and did not enforce TVM's 3 MiB memory limit. It also omitted the CREATE2 init-code hash charge and used fork-dependent Ethereum EXP byte pricing. The revised model uses checked bigint range calculations, handles MCOPY and NATIVEVOTE without wraparound, charges CREATE2 per init-code word, and uses TVM's fixed EXP cost across legacy and via-IR optimizer metrics. These changes affect estimates and optimization choices, not VM execution semantics.

Validation

• built solc and soltest
• full SMTChecker suite with Z3 4.13.3: 1439/1439 passed
• full StandardCompiler suite: 65/65 passed
• TRON SMTChecker directory: 7/7 passed
• EvmasmGasMeter: 13/13 passed
• Optimiser: 94/94 passed
• YulEVMMetrics: 1/1 passed
• Ethereum-denomination rejection tests passed for both the type layer and Standard JSON AST import
• direct BMC/CHC reproduction changed from a false safe result to the expected library assertion violation
• git diff --check passed

[github-actions]

Thank you for your contribution to the Solidity compiler! A team member will follow up shortly.

If you haven't read our contributing guidelines and our review checklist before, please do it now, this makes the reviewing process and accepting your contribution smoother.

If you have any questions or need our help, feel free to post them in the PR or talk to us directly on the #solidity-dev channel on Matrix.