Carolyn Zech

Checking for Community Deletion/Removal

3

What's the policy for when to call `check_community_deleted_or_removed`? I was looking at when `check_community_banned` gets called, and I couldn't figure out why `check_community_deleted_or_removed` was called in some of these places...

Banned Moderators Can Do Actions

6

### Issue Summary `check_community_banned` and `check_community_deleted_or_removed` aren't called in all controllers restricted to mod/admins. This allows for some weird edge cases. For example, the perform trait for BanFromCommunity doesn't enforce...

RFC for List Subcommand

1

RFC for the `kani list` subcommand. I saw the comment [in the template](https://github.com/model-checking/kani/blob/main/rfc/src/template.md#software-design) to leave the Software Design section empty, but I was looking at the raw MD file and...

ICE Resolving `proof_for_contract` target

9

I tried this code: ```rust #[safety::requires(a.is_power_of_two())] pub(crate) const unsafe fn align_offset(p: *const T, a: usize) -> usize { ... #[safety::requires(m.is_power_of_two())] #[safety::requires(x < m)] const unsafe fn mod_inv(x: usize, m: usize)...

`cover_or_fail!` macro

3

This PR adds a `cover_or_fail!` macro to Kani. This macro has the same functionality as the existing `cover!` macro, except it causes verification to fail when the outcome is unsatisfiable...

I tried writing a contract for `char::as_ascii` (in [this file](https://github.com/model-checking/verify-rust-std/blob/main/library/core/src/char/methods.rs)), but Kani couldn't find the implementation of `as_ascii`. I tried this code: ```rust use crate::char; #[kani::proof_for_contract(char::as_ascii)] #[kani::proof_for_contract(char::as_ascii)] fn check_as_ascii_ascii_char() {...

Fail verification if contract is vacuous

2

Fail verification if a contract's preconditions empty the search space. This solution introduces a new Kani intrinsic, `kani::internal::assume_unless_vacuous`, which codegens to this: ```rust Stmt::block( vec![ gcx.codegen_assume(cond, loc), // This `assert(false)`...

Autoharness: Derive `Arbitrary` for structs and enums

1

While generating automatic harnesses, derive `Arbitrary` implementations for structs and enums that don't have implementations. ## Implementation Overview 1. In `automatic_harness_partition`, we mark a function as eligible for autoharness if...

I tried this code: ```rust #[kani::requires(*val != 0)] unsafe fn foo(val: &mut u8) -> &mut u8 { val } #[kani::proof] fn harness() { let mut x: u8 = kani::any(); unsafe...

This PR is not ready for review; I am testing that it passes CI before writing tests. Resolves #ISSUE-NUMBER By submitting this pull request, I confirm that my contribution is...