Terraform-style infrastructure as code in Lean 4: dependently-typed target and observed cloud state, so an unrealisable target is a compile error