Merge pull request #1323 from cryspen/logand_lemma_plus

Add more facts to logand_lemma
cryspen · Mar 3, 2025 · fa750d3 · fa750d3
2 parents c54a4eb + 1edeb28
commit fa750d3
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/proof-libs/fstar/rust_primitives/Rust_primitives.Integers.fsti b/proof-libs/fstar/rust_primitives/Rust_primitives.Integers.fsti
@@ -262,6 +262,8 @@ val logand_lemma: #t:inttype -> a:int_t t -> b:int_t t ->
          logand zero a == zero /\
          logand a ones == a /\
          logand ones a == a /\
+         (a == b ==> logand a b == a) /\
+         (b == lognot a ==> logand a b == zero) /\
          (v a >= 0 ==> (v (logand a b) >= 0) /\ (v (logand a b) <= v a)) /\
          (v b >= 0 ==> (v (logand a b) >= 0) /\ (v (logand a b) <= v b)))