There are two components to this artifact. First, a we provide a mechanization of the formalization in the paper, as well as mechanized proofs of the main results from the paper. Second, we provide a full implementation of Poseidon Lua, the language implemented in the paper. Instructions for all components of the artifact are included in the sections below.