A mechanism to identify/forbid/"rewrite" non-temporal instructions (and other)

src/trusted/validator_ragel/nacl_unsupported_proof.py

Index: src/trusted/validator_ragel/nacl_unsupported_proof.py
diff --git a/src/trusted/validator_ragel/jecxz_proof.py b/src/trusted/validator_ragel/nacl_unsupported_proof.py
similarity index 53%
copy from src/trusted/validator_ragel/jecxz_proof.py
copy to src/trusted/validator_ragel/nacl_unsupported_proof.py
index b4c6be46772321cf41b4371d5b6cfae1f2921482..d3c140053d27842f8c2718c702bfb4d4c726b466 100644
--- a/src/trusted/validator_ragel/jecxz_proof.py
+++ b/src/trusted/validator_ragel/nacl_unsupported_proof.py
@@ -2,28 +2,17 @@
 # Use of this source code is governed by a BSD-style license that can be
 # found in the LICENSE file.
 
-"""Proof for enabling jecxz"""
+"""Proof that tries do not change when introducing a new attribute
+nacl-unsupported in def files."""
 
 import proof_tools
-from proof_tools import MnemonicOp
-from proof_tools import OpsProd
-
-
-def Instructions(bitness):
-  """Returns 32-bit jecxz variants."""
-  if bitness == 32:
-    jecxz = OpsProd(MnemonicOp('jecxz'))
-    return jecxz
-  return set()
 
 
 def Validate(trie_diffs, bitness):
-  """Validates that 32-bit jecxz variants are added."""
   proof_tools.AssertDiffSetEquals(
       trie_diffs,
-      expected_adds=Instructions(bitness),
+      expected_adds=set(),
       expected_removes=set())
 
-
 if __name__ == '__main__':
   proof_tools.RunProof(proof_tools.ParseStandardOpts(), Validate)