Cast bool to integer?

source/rust_verify/src/fn_call_to_vir.rs

@@ -1053,6 +1053,14 @@ fn verus_item_to_vir<'tcx, 'a>(
                     let expr_vattrs = bctx.ctxt.get_verifier_attrs(expr_attrs)?;
                     Ok(mk_ty_clip(&to_ty, &source_vir, expr_vattrs.truncate))
                 }
+                ((TypX::Bool, _), TypX::Int(_)) => {
+                    let expr_attrs = bctx.ctxt.tcx.hir().attrs(expr.hir_id);
+                    let expr_vattrs = bctx.ctxt.get_verifier_attrs(expr_attrs)?;
+                    let zero = mk_expr(ExprX::Const(vir::ast_util::const_int_from_u128(0)))?;
+                    let one = mk_expr(ExprX::Const(vir::ast_util::const_int_from_u128(1)))?;
+                    let cast_to_integer = mk_expr(ExprX::If(source_vir, one, Some(zero)))?;
+                    Ok(mk_ty_clip(&to_ty, &cast_to_integer, expr_vattrs.truncate))
+                }
                 ((_, true), TypX::Int(IntRange::Int)) => {
                     mk_expr(ExprX::Unary(UnaryOp::CastToInteger, source_vir))
                 }

source/rust_verify/src/rust_to_vir_expr.rs

@@ -1674,6 +1674,12 @@ pub(crate) fn expr_to_vir_innermost<'tcx>(
                 (TypX::Int(_), TypX::Int(_)) => {
                     Ok(mk_ty_clip(&to_vir_ty, &source_vir, expr_vattrs.truncate))
                 }
+                (TypX::Bool, TypX::Int(_)) => {
+                    let zero = mk_expr(ExprX::Const(vir::ast_util::const_int_from_u128(0)))?;
+                    let one = mk_expr(ExprX::Const(vir::ast_util::const_int_from_u128(1)))?;
+                    let cast_to_integer = mk_expr(ExprX::If(source_vir, one, Some(zero)))?;
+                    Ok(mk_ty_clip(&to_vir_ty, &cast_to_integer, expr_vattrs.truncate))
+                }
                 _ => {
                     let source_ty = bctx.types.expr_ty_adjusted(source);
                     let to_ty = bctx.types.expr_ty(expr);

source/rust_verify_test/tests/integers.rs

@@ -496,3 +496,13 @@ test_verify_one_file! {
         }
     } => Ok(())
 }
+
+test_verify_one_file! {
+    #[test] test_bool_to_int verus_code! {
+        fn test1() {
+            assert(true as usize == 1);
+            assert(false as usize == 0);
+            assert(false as int == 0);
+        }
+    } => Ok(())
+}