MCPcopy Create free account
hub / github.com/BasisResearch/lean.py / test_rotate_left_proof

Method test_rotate_left_proof

tests/test_z3_compat.py:1213–1217  ·  view source on GitHub ↗

rotateLeft(x, 0) == x for 8-bit.

(self, kernel)

Source from the content-addressed store, hash-verified

1211 assert r.size() == 8
1212
1213 def test_rotate_left_proof(self, kernel):
1214 """rotateLeft(x, 0) == x for 8-bit."""
1215 x = BitVec("x", 8)
1216 claim = ForAll(x, RotateLeft(x, 0) == x)
1217 assert _try_prove(claim)
1218
1219 def test_rotate_right_proof(self, kernel):
1220 """rotateRight(x, 0) == x for 8-bit."""

Callers

nothing calls this directly

Calls 4

BitVecFunction · 0.90
ForAllFunction · 0.90
RotateLeftFunction · 0.90
_try_proveFunction · 0.90

Tested by

no test coverage detected