CodeHawks Escrow Contract - Competition Details

Summary

0.8.19:

• SMTChecker: New trusted mode that assumes that any compile-time available code is the actual used code, even in external calls.

Bug Fixes:

• Assembler: Avoid duplicating subassembly bytecode where possible.

• Code Generator: Avoid including references to the deployed label of referenced functions if they are called right away.

• ContractLevelChecker: Properly distinguish the case of missing base constructor arguments from having an unimplemented base function.

• SMTChecker: Fix internal error caused by unhandled z3 expressions that come from the solver when bitwise operators are used.

• SMTChecker: Fix internal error when using the custom NatSpec annotation to abstract free functions.

• TypeChecker: Also allow external library functions in using for.

0.8.20:

• Assembler: Use push0 for placing 0 on the stack for EVM versions starting from “Shanghai”. This decreases the deployment and runtime costs.

• EVM: Set default EVM version to “Shanghai”.

• EVM: Support for the EVM Version “Shanghai”.

• Optimizer: Re-implement simplified version of UnusedAssignEliminator and UnusedStoreEliminator. It can correctly remove some unused assignments in deeply nested loops that were ignored by the old version.

• Parser: Unary plus is no longer recognized as a unary operator in the AST and triggers an error at the parsing stage (rather than later during the analysis).

• SMTChecker: Group all messages about unsupported language features in a single warning. The CLI option --model-checker-show-unsupported and the JSON option settings.modelChecker.showUnsupported can be enabled to show the full list.

• SMTChecker: Properties that are proved safe are now reported explicitly at the end of analysis. By default, only the number of safe properties is shown. The CLI option --model-checker-show-proved-safe and the JSON option settings.modelChecker.showProvedSafe can be enabled to show the full list of safe properties.

• Standard JSON Interface: Add experimental support for importing ASTs via Standard JSON.

• Yul EVM Code Transform: If available, use push0 instead of codesize to produce an arbitrary value on stack in order to create equal stack heights between branches.

0.8.21:

• Code Generator: Always generate code for the expression in <expression>.selector in the legacy code generation pipeline.

• Yul Optimizer: Fix FullInliner step (i) not preserving the evaluation order of arguments passed into inlined functions in code that is not in expression-split form.

• Allow qualified access to events from other contracts.

• Relax restrictions on initialization of immutable variables. Reads and writes may now happen at any point at construction time outside of functions and modifiers. Explicit initialization is no longer mandatory.

Tools Used

Manual Review