Using Coq 8.12 as indicated, I cannot compile the coq proof, on none of the branch version.
Specifically for the most complete(closest to the Microsoft CheckedC) version of formalization among them, that is the one in the master branch, the complained error is that Coq cannot find stack_grow_prop.