Paweł Bylica chfast

JUMPDEST analysis kernel proofs

z3 proofs that one loop step of Erigon's SIMD JUMPDEST analysis kernels (execution/vm/analysis_amd64.s, SSE4, and execution/vm/analysis_arm64.s, NEON) matches the scalar analysis.

For every 32 code bytes and every entry offset 0..32, the step writes the same 4 bytes of JUMPDEST bits as the scalar reference and returns the same entry into the next step (NEON: in all 16 lanes of V30). Table bytes that the loop writes may hold anything from earlier steps; the others hold their initial value. The loop carries only the entry between steps, so this covers every whole 32-byte step. The Go wrappers and the tail of less than 32 bytes are covered by the equivalence tests in Erigon.

goasm.py: Go assembly front end. The C preprocessor (cc -E) expands the macros; instructions are read from the real .s files.
amd64.py, arm64.py: z3 bit-vector semantics of the instructions the kernels use (the arm64 WORD-encoded SMAX and CMHI are decoded from their encodings).
`mem.

	block	tx	src	gas	to	value	inOffset	inSize	retOffset	retSize	args
	24018221	d45e12afe787738c96ff3a0e3591dab657700f6491cd5f74f7678722ba7c2888	a5487594bd2303af225f8c15e80ced0da883a0e8	782987	bf9e94b89d6f4f8da8e56bc2f92c058d5e12e1ae	0	320	612	0	0	9e00ccbf000000000000000000000000000000000000000000000000000000000000002000000000000000000000000000000000000000000000000001f93225870f8000000000000000000000000000c02aaa39b223fe8d0a0e5c4f27ead9083c756cc200000000000000000000000000000000000000000000000000000000000000c00000000000000000000000000000000000000000000000000000000000000100000000000000000000000000000000000000000000000000000000000000014000000000000000000000000000000000000000000000000000000000000001800000000000000000000000000000000000000000000000000000000000000001000000000000000000000000a0b86991c6218b36c1d19d4a2e9eb0ce3606eb480000000000000000000000000000000000000000000000000000000000000001000000000000000000000000000000000000000000000000000000001a6fc5030000000000000000000000000000000000000000000000000000000000000001000000

Ethereum SD-SAMETX events, blocks 20M – 25M

A dataset of every SELFDESTRUCT executed on a same-tx-created contract on Ethereum mainnet, blocks 20,000,000 – 24,999,999 (post-Cancun, after EIP-6780 took effect at block 19,426,587).

The "SD-SAMETX" name refers to events where the contract being destroyed was created in the same transaction (newContract == true in EIP-6780 terminology). This is the only path post-Cancun where SELFDESTRUCT actually destroys the account; on existing contracts the opcode is a no-op.

PUSH16/min_stack:
60ff5b6f00000000000000000000000000000000506f00000000000000000000000000000000506f00000000000000000000000000000000506f00000000000000000000000000000000506f00000000000000000000000000000000506f00000000000000000000000000000000506f00000000000000000000000000000000506f00000000000000000000000000000000506f00000000000000000000000000000000506f00000000000000000000000000000000506f00000000000000000000000000000000506f00000000000000000000000000000000506f00000000000000000000000000000000506f00000000000000000000000000000000506f00000000000000000000000000000000506f00000000000000000000000000000000506f00000000000000000000000000000000506f00000000000000000000000000000000506f00000000000000000000000000000000506f00000000000000000000000000000000506f00000000000000000000000000000000506f00000000000000000000000000000000506f00000000000000000000000000000000506f00000000000000000000000000000000506f00000000000000000000000000000000506f00000000000000000000000000000000506f00000000000000000000000000000000506f0000000000000000000000

Instantiation

                         fizzy 0.5.0  fizzy 0.4.0   wabt 1.0.19  wasm3 0.4.7
                 abs. [µs]  rel. [%]     rel. [%]      rel. [%]     rel. [%]
geometric mean                   100          101           279           27
blake2b                 28       100           99           306           38
ecpairing             1399       100          101           305            3
keccak256               47       100          103           289           18
memset                  10       100          100           285           79

	/home/chfast/Projects/ethereum/eof/venv/bin/python /home/chfast/Projects/ethereum/eof/analysis/malicious_bytes_analysis.py
	1000
	0xc02aaa39b223fe8d0a0e5c4f27ead9083c756cc2, 3124, 98:
	37, 4, []
	49, 12, []
	50, 14, []
	87, 13, []
	0x00001bea43608c5ee487f82b773af8bd7cb20a6f, 11293, 353:
	302, 0, []
	303, 30, []


	#include <ethash/keccak.hpp>
	#include <evmc/hex.hpp>
	#include <openssl/ec.h>
	#include <openssl/evp.h>
	#include <iostream>

	#include <dlfcn.h>

	int main(int argc, const char* argv[])

	/*
	The Keccak sponge function, designed by Guido Bertoni, Joan Daemen,
	Michaël Peeters and Gilles Van Assche. For more information, feedback or
	questions, please refer to our website: http://keccak.noekeon.org/

	Implementation by Ronny Van Keer,
	hereby denoted as "the implementer".

	To the extent possible under law, the implementer has waived all copyright
	and related or neighboring rights to the source code in this file.

	> ./run_benchmark.sh

	Finished bench [optimized] target(s) in 0.04s
	Running target/release/deps/eth_pairings-69a4e69246dcf782

	running 9 tests
	test bench::eip_2537::bench_eip_2537_g1_add ... bench: 5,702 ns/iter (+/- 180)
	test bench::eip_2537::bench_eip_2537_g1_double ... bench: 5,815 ns/iter (+/- 398)
	test bench::eip_2537::bench_eip_2537_g1_mul_worst_case_double_and_add ... bench: 266,373 ns/iter (+/- 2,488)
	test bench::eip_2537::bench_eip_2537_g2_add ... bench: 9,356 ns/iter (+/- 1,776)