Yoshiki Takashima

Hi @hsivonen. Thank you for the analysis on alignment. I agree with you that these are safe behaviors given the nature of the library. With regard to out-of-bound, I should...

@hsivonen Got it. Big thanks to @bjorn3, who suggested the fix.

@stjepang and @RalfJung, I reran with `-Zmiri-disable-stacked-borrows` and it passes fine, no use-after-free, or any other UB except the one we already know. I forgot about this when I rushed...

> I'm not sure why any_slice and any_vec pass in the bound as a const generic. Seems like it'd be best if it were an ordinary parameter. It makes these...

### Replicating linker issue. First, replicate the kani version. ``` git clone https://github.com/YoshikiTakashima/kani.git cd kani git checkout yoshi-proptest-primitive git checkout eac76a7e -- library/proptest/src/sugar.rs cargo clean; cargo build --workspace ``` Then...

Info from deep dive: The following is required for kani to work. Currently, we only provide the `rlib` - `*.rlib` - `symtab.json` Possible `--enable-unstable --c-lib ` where `gotobinary` is `*.goto`

Code changes implemented to link proptest. After cleanup, we can merge.

See the following comment for way to integrate proptest w/o significant changes. https://github.com/model-checking/kani/pull/1435#issuecomment-1215117585

@celinval I think you're right. That's the actual cause. It gave me a "unexpected output" as the message, so I wrongly assumed it was the different input.

More evidence for duplication: It seems proptests are actually running twice: ``` Checking harness sum_lower_than_2020... Report written to: target/report-sum_lower_than_2020/html/index.html Checking harness arbitrary_boolean::arbitrary_boolean... Report written to: target/report-arbitrary_boolean-arbitrary_boolean/html/index.html Checking harness proptest_library_is_linked::successfully_linked_proptest... Report...