Overview

A verified check_mem optimization for CertrBPF

Structure

The repo structure follows the one of CertrBPF, with additional files:

• The Coq implementation of our optimization is in the file model/Semantics.v
• The simplified version is in the file model/SemanticsSimpl.v
• The simplification correctness is in equivalence/equivalence_simpl.v
• The optimization correctness based on the simplified model is in equivalence/equivalence_opt.v

To validate the two theorems, please run make.