add some default.nix files
check each arithmetic expression for overflow
add requires/ensures
manually insert requires for Ix types for now
add proc environment to check `call` statement