From 1edeb28fe6f06b0b76a287b8b49d3f91faba51f3 Mon Sep 17 00:00:00 2001 From: mamonet Date: Mon, 24 Feb 2025 08:03:43 +0000 Subject: [PATCH] Add more facts to logand_lemma --- proof-libs/fstar/rust_primitives/Rust_primitives.Integers.fsti | 2 ++ 1 file changed, 2 insertions(+) diff --git a/proof-libs/fstar/rust_primitives/Rust_primitives.Integers.fsti b/proof-libs/fstar/rust_primitives/Rust_primitives.Integers.fsti index 19459c7dd..66f6c61d4 100644 --- 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)))