We've talked about the best way to implement a usage checker for the new occam-pi compiler (without using the current brute-force approach). One option which might have some mileage: prove that functions mapping PAR indices to array indices are actually 1:1 mappings.