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/nacl_unsupported_proof.py b/src/trusted/validator_ragel/nacl_unsupported_proof.py
new file mode 100644
index 0000000000000000000000000000000000000000..708f4634e2934daa989b0fc2074ff7eff3fbf105
--- /dev/null
+++ b/src/trusted/validator_ragel/nacl_unsupported_proof.py
@@ -0,0 +1,18 @@
+# Copyright 2015 The Native Client Authors. All rights reserved.
+# Use of this source code is governed by a BSD-style license that can be
+# found in the LICENSE file.
+
+"""Proof that tries do not change when introducing a new attribute
+nacl-unsupported in def files."""
+
+import proof_tools
+
+
+def Validate(trie_diffs, bitness):
+  proof_tools.AssertDiffSetEquals(
+      trie_diffs,
+      expected_adds=set(),
+      expected_removes=set())
+
+if __name__ == '__main__':
+  proof_tools.RunProof(proof_tools.ParseStandardOpts(), Validate)