make recommended changes for PR #574

crates/flux-refineck/src/sigs/default.rs

@@ -171,12 +171,12 @@ pub(crate) fn mk_not() -> (mir::UnOp, Sig<1>) {
 pub(crate) fn mk_lnot() -> impl IntoIterator<Item = (mir::UnOp, Sig<1>)> {
     let int_lnots = INT_TYS.map(|int_ty| {
         define_btys! { let Int = BaseTy::Int(int_ty); };
-        (mir::UnOp::Not, s!(fn(a: Int) -> Int[E::tt()]))
+        (mir::UnOp::Not, s!(fn(a: Int) -> Int{v: E::tt()}))
     });
 
     let uint_lnots = UINT_TYS.map(|uint_ty| {
         define_btys! { let Uint = BaseTy::Uint(uint_ty); };
-        (mir::UnOp::Not, s!(fn(a: Uint) -> Uint[E::tt()]))
+        (mir::UnOp::Not, s!(fn(a: Uint) -> Uint{v: E::tt()}))
     });
 
     chain!(int_lnots, uint_lnots)

crates/flux-refineck/src/sigs/overflow.rs

@@ -29,6 +29,7 @@ pub(super) static UN_OPS: LazyLock<SigTable<mir::UnOp, 1>> = LazyLock::new(|| {
 
     table.extend(mk_neg());
     table.extend([super::default::mk_not()]);
+    table.extend(super::default::mk_lnot());
 
     table
 });

crates/flux-tests/tests/pos/surface/binop.rs

@@ -64,6 +64,18 @@ pub fn bitwise_shr_u32_u32(a: u32, b: u32) -> u32 {
     a >> b
 }
 
+// Bitwise UnOps
+#[flux::sig(fn(u32{v: v > 0}) -> u32)]
+pub fn bitwise_not_u32(a: u32) -> u32 {
+    !a
+}
+
+#[flux::sig(fn(i32{v: v > 0}) -> i32)]
+pub fn bitwise_not_i32(a: i32) -> i32 {
+    !a
+}
+
+
 // Logical BinOps
 #[flux::sig(fn(a: bool, b: bool) -> bool{v: v == a || v == b})]
 pub fn logical_or(a: bool, b: bool) -> bool {
@@ -79,3 +91,15 @@ pub fn logical_or_ft(a: bool, b: bool) -> bool {
 pub fn logical_or_ff(a: bool, b: bool) -> bool {
     a | b
 }
+
+// Logical UnOps
+#[flux::sig(fn(bool[true]) -> bool[false])]
+pub fn logical_not_t(a: bool) -> bool {
+    !a
+}
+
+#[flux::sig(fn(bool[false]) -> bool[true])]
+pub fn logical_not_f(a: bool) -> bool {
+    !a
+}
+