Had an advisor meeting. Some things about coverage checking are becoming more clear - however, doing the permutation example in a way that makes coverage manifest seems to require a third-order encoding, which is kind of intimidating.