[WIP] dependently typed implementation of peephole rewrite verification

[math-fehr]

Exploration of using dependent types in the interpreter to make proofs much simpler in the peephole rewrite verification

[github-actions]

VeIR Benchmarks

Details

Benchmark suite	Current: 862a0e8	Previous: bb6ce4c	Ratio
add-fold-worklist/create	1893000 ns	2235000 ns	0.85
add-fold-worklist/rewrite	3447000 ns	3738000 ns	0.92
add-fold-worklist-local/create	1848000 ns	2196000 ns	0.84
add-fold-worklist-local/rewrite	2857000 ns	3048000 ns	0.94
add-zero-worklist/create	1860000 ns	2247000 ns	0.83
add-zero-worklist/rewrite	2199000 ns	2418000 ns	0.91
add-zero-reuse-worklist/create	1546000 ns	1941000 ns	0.80
add-zero-reuse-worklist/rewrite	1761000 ns	2009000 ns	0.88
mul-two-worklist/create	1848000 ns	2293000 ns	0.81
mul-two-worklist/rewrite	4810000 ns	5320000 ns	0.90
add-fold-forwards/create	1830000 ns	2326000 ns	0.79
add-fold-forwards/rewrite	2750000 ns	3023000 ns	0.91
add-zero-forwards/create	1857000 ns	2258000 ns	0.82
add-zero-forwards/rewrite	1781000 ns	1919000 ns	0.93
add-zero-reuse-forwards/create	1537000 ns	1884000 ns	0.82
add-zero-reuse-forwards/rewrite	1387000 ns	1541000 ns	0.90
mul-two-forwards/create	1904000 ns	2192000 ns	0.87
mul-two-forwards/rewrite	3233000 ns	3681000 ns	0.88
add-zero-reuse-first/create	1562000 ns	1867000 ns	0.84
add-zero-reuse-first/rewrite	9000 ns	8000 ns	1.13
add-zero-lots-of-reuse-first/create	1572000 ns	1832000 ns	0.86
add-zero-lots-of-reuse-first/rewrite	759000 ns	767000 ns	0.99

This comment was automatically generated by workflow using github-action-benchmark.