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 Net Host. | |
| Extraction Language OCaml. | |
| Set Extraction Output Directory "extract". | |
| Extraction "hostnet.ml" host_units host_next nH. | |