Prove the paper's counts, levelization, depth bounds, recipe lengths and Section 6 in Rocq, and revise the paper
8397e00 | From Stdlib Require Import Extraction ExtrOcamlBasic ExtrOcamlNatInt ExtrOcamlZInt. | |
| From TH Require Import ExtrNat StoredFast. | |
| Extraction Language OCaml. | |
| Set Extraction Output Directory "extract". | |
| Extraction "storednet.ml" stored_bits_lin. | |