Exact and Linear-Time Gas-Cost Analysis
summary
A static tool called GasBoX computes exact gas bounds and removes runtime gas accounting by inserting Gas.deposit and amortizing gas into data with gas amortization so branch and recursive costs become constant. It formulates linear constraints solved by an LP solver, infers constant bounds in linear time, and returns proofs whose verification costs are microseconds while inference runs in milliseconds. A soundness theorem equates the static cost to the dynamic cost.
AI-written summary · about
chapters (13)
- 0:00Intro
- 1:13Execution Model
- 4:18Challenges
- 4:41Bidding in an Auction
- 5:40Gas.deposit operation
- 6:27Advantages of Gas.deposit
- 6:51Handling Unbounded Computation
- 8:47Stored Gas pays for Recursion
- 9:29Advantages of Gas Amortization
- 11:14Inference of Gas Bounds
- 12:13Formal Analysis
- 13:17Soundness Theorem
- 16:35Conclusion
related talks
19mBuilding Dynamic System Call Sandbox with Partial Order Analysis
15mSymbolic Value-Flow Static Analysis: Deep, Precise, Complete Modeling of Ethereum Smart Contracts
38mStatic Code Analysis - A Behind-the-scenes Look
33mSymbolic value-flow static analysis:deep,precise,complete modeling of Ethereum smartcontracts
48mFormal Modelling of Information-flow Control Systems: Some Lessons Learned
19mPolicy-as-Code for LLM Inference: Cost & Security Guardrails
28mImproving Build Time SBoMs
19mDecompiling for Constant-Time Analysis