Skip to content

Commit fdf96d7

Browse files
feliperodrifeliperodri
authored
Merge branch 'main' into sync-2025-09-09
2 parents 4198ddb + 195e1b6 commit fdf96d7

37 files changed

+11480
-23
lines changed

‎.github/workflows/testable-simd-models.yml‎

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
# This workflow runs the tests for testable simd models.
2+
3+
name: Testable simd models
4+
5+
on:
6+
workflow_dispatch:
7+
merge_group:
8+
pull_request:
9+
branches: [ main ]
10+
push:
11+
paths:
12+
- '.github/workflows/testable-simd-models.yml'
13+
- 'testable-simd-models/**'
14+
15+
defaults:
16+
run:
17+
shell: bash
18+
19+
jobs:
20+
testable-simd-models:
21+
name: Test testable simd models
22+
runs-on: ubuntu-latest
23+
24+
steps:
25+
- name: Checkout Repository
26+
uses: actions/checkout@v4
27+
28+
- name: Run tests
29+
working-directory: testable-simd-models
30+
run: cargo test -- --test-threads=1 --nocapture
31+

‎.gitignore‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -56,3 +56,4 @@ goto-transcoder
5656
# already existing elements were commented out
5757

5858
#/target
59+
testable-simd-models/target

‎README.md‎

Lines changed: 23 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -29,29 +29,29 @@ These are the challenges:
2929
| [2: Verify the memory safety of core intrinsics using raw pointers](https://model-checking.github.io/verify-rust-std/challenges/0002-intrinsics-memory.html) | N/A | Open | |
3030
| [3: Verifying Raw Pointer Arithmetic Operations](https://model-checking.github.io/verify-rust-std/challenges/0003-pointer-arithmentic.html) | N/A | [Resolved](https://github.com/model-checking/verify-rust-std/pull/212) | [Kani](https://github.com/model-checking/verify-rust-std/pull/212/files) |
3131
| [4: Memory safety of BTreeMap's `btree::node` module](https://model-checking.github.io/verify-rust-std/challenges/0004-btree-node.html) | 10,000 USD | Open | |
32-
| [5: Verify functions iterating over inductive data type: `linked_list`](./challenges/0005-linked-list.md) | 5,000 USD | [Resolved](https://github.com/model-checking/verify-rust-std/pull/238) | [VeriFast](https://github.com/model-checking/verify-rust-std/tree/main/verifast-proofs/alloc/collections/linked_list.rs) |
33-
| [6: Safety of `NonNull`](./challenges/0006-nonnull.md) | N/A | [Resolved](https://github.com/model-checking/verify-rust-std/pull/247) | [Kani](https://github.com/model-checking/verify-rust-std/blob/main/library/core/src/ptr/non_null.rs) |
34-
| [7: Safety of Methods for Atomic Types & Atomic Intrinsics](./challenges/0007-atomic-types.md) | 10,000 USD | Open | |
35-
| [8: Contracts for SmallSort](./challenges/0008-smallsort.md) | 10,000 USD | Open | |
36-
| [9: Safe abstractions for `core::time::Duration`](./challenges/0009-duration.md) | N/A | [Resolved](https://github.com/model-checking/verify-rust-std/pull/136) | [Kani](https://github.com/model-checking/verify-rust-std/blob/main/library/core/src/time.rs) |
37-
| [10: Memory safety of String](./challenges/0010-string.md) | N/A | Open | |
38-
| [11: Safety of Methods for Numeric Primitive Types](./challenges/0011-floats-ints.md) | N/A | [Resolved](https://github.com/model-checking/verify-rust-std/issues/59) | [Kani](https://github.com/model-checking/verify-rust-std/tree/main/library/core/src/num) |
39-
| [12: Safety of `NonZero`](./challenges/0012-nonzero.md) | N/A | Open | |
40-
| [13: Safety of `CStr`](./challenges/0013-cstr.md) | N/A | Open | |
41-
| [14: Safety of Primitive Conversions](./challenges/0014-convert-num.md) | TBD | [Resolved](https://github.com/model-checking/verify-rust-std/pull/247) | [Kani](https://github.com/model-checking/verify-rust-std/blob/main/library/core/src/convert/num.rs) |
42-
| [15: Contracts and Tests for SIMD Intrinsics](./challenges/0015-intrinsics-simd.md) | | Open | |
43-
| [16: Verify the safety of Iterator functions](./challenges/0016-iter.md) | 10,000 USD | Open | |
44-
| [17: Verify the safety of slice functions](./challenges/0017-slice.md) | 10,000 USD | Open | |
45-
| [18: Verify the safety of slice iter functions](./challenges/0018-slice-iter.md) | 10,000 USD | Open | |
46-
| [19: Safety of `RawVec`](./challenges/0019-rawvec.md) | 10,000 USD | [Resolved](https://github.com/model-checking/verify-rust-std/pull/422) | [VeriFast](https://github.com/model-checking/verify-rust-std/tree/main/verifast-proofs/alloc/raw_vec/mod.rs) |
47-
| [20: Verify the safety of char-related functions in str::pattern](./challenges/0020-str-pattern-pt1.md) | 25,000 USD | Open | |
48-
| [21: Verify the safety of substring-related functions in str::pattern](./challenges/0021-str-pattern-pt2.md) | 25,000 USD | Open | |
49-
| [22: Verify the safety of str iter functions](./challenges/0022-str-iter.md) | 10,000 USD | Open | |
50-
| [23: Verify the safety of Vec functions part 1](./challenges/0023-vec-pt1.md) | 15,000 USD | Open | |
51-
| [24: Verify the safety of Vec functions part 2](./challenges/0024-vec-pt2.md) | 15,000 USD | Open | |
52-
| [25: Verify the safety of `VecDeque` functions](./challenges/0025-vecdeque.md) | 10,000 USD | Open | |
53-
| [26: Verify reference-counted Cell implementation](./challenges/0026-rc.md) | 10,000 USD | Open | |
54-
| [27: Verify atomically reference-counted Cell implementation](./challenges/0027-arc.md) | 10,000 USD | Open | |
32+
| [5: Verify functions iterating over inductive data type: `linked_list`](https://model-checking.github.io/verify-rust-std/challenges/0005-linked-list.html) | 5,000 USD | [Resolved](https://github.com/model-checking/verify-rust-std/pull/238) | [VeriFast](https://github.com/model-checking/verify-rust-std/tree/main/verifast-proofs/alloc/collections/linked_list.rs) |
33+
| [6: Safety of `NonNull`](https://model-checking.github.io/verify-rust-std/challenges/0006-nonnull.html) | N/A | [Resolved](https://github.com/model-checking/verify-rust-std/pull/247) | [Kani](https://github.com/model-checking/verify-rust-std/blob/main/library/core/src/ptr/non_null.rs) |
34+
| [7: Safety of Methods for Atomic Types & Atomic Intrinsics](https://model-checking.github.io/verify-rust-std/challenges/0007-atomic-types.html) | 10,000 USD | Open | |
35+
| [8: Contracts for SmallSort](https://model-checking.github.io/verify-rust-std/challenges/0008-smallsort.html) | 10,000 USD | Open | |
36+
| [9: Safe abstractions for `core::time::Duration`](https://model-checking.github.io/verify-rust-std/challenges/0009-duration.html) | N/A | [Resolved](https://github.com/model-checking/verify-rust-std/pull/136) | [Kani](https://github.com/model-checking/verify-rust-std/blob/main/library/core/src/time.rs) |
37+
| [10: Memory safety of String](https://model-checking.github.io/verify-rust-std/challenges/0010-string.html) | N/A | Open | |
38+
| [11: Safety of Methods for Numeric Primitive Types](https://model-checking.github.io/verify-rust-std/challenges/0011-floats-ints.html) | N/A | [Resolved](https://github.com/model-checking/verify-rust-std/issues/59) | [Kani](https://github.com/model-checking/verify-rust-std/tree/main/library/core/src/num) |
39+
| [12: Safety of `NonZero`](https://model-checking.github.io/verify-rust-std/challenges/0012-nonzero.html) | N/A | Open | |
40+
| [13: Safety of `CStr`](https://model-checking.github.io/verify-rust-std/challenges/0013-cstr.html) | N/A | Open | |
41+
| [14: Safety of Primitive Conversions](https://model-checking.github.io/verify-rust-std/challenges/0014-convert-num.html) | TBD | [Resolved](https://github.com/model-checking/verify-rust-std/pull/247) | [Kani](https://github.com/model-checking/verify-rust-std/blob/main/library/core/src/convert/num.rs) |
42+
| [15: Contracts and Tests for SIMD Intrinsics](https://model-checking.github.io/verify-rust-std/challenges/0015-intrinsics-simd.html) | | Open | |
43+
| [16: Verify the safety of Iterator functions](https://model-checking.github.io/verify-rust-std/challenges/0016-iter.html) | 10,000 USD | Open | |
44+
| [17: Verify the safety of slice functions](https://model-checking.github.io/verify-rust-std/challenges/0017-slice.html) | 10,000 USD | Open | |
45+
| [18: Verify the safety of slice iter functions](https://model-checking.github.io/verify-rust-std/challenges/0018-slice-iter.html) | 10,000 USD | Open | |
46+
| [19: Safety of `RawVec`](https://model-checking.github.io/verify-rust-std/challenges/0019-rawvec.html) | 10,000 USD | [Resolved](https://github.com/model-checking/verify-rust-std/pull/422) | [VeriFast](https://github.com/model-checking/verify-rust-std/tree/main/verifast-proofs/alloc/raw_vec/mod.rs) |
47+
| [20: Verify the safety of char-related functions in str::pattern](https://model-checking.github.io/verify-rust-std/challenges/0020-str-pattern-pt1.html) | 25,000 USD | Open | |
48+
| [21: Verify the safety of substring-related functions in str::pattern](https://model-checking.github.io/verify-rust-std/challenges/0021-str-pattern-pt2.html) | 25,000 USD | Open | |
49+
| [22: Verify the safety of str iter functions](https://model-checking.github.io/verify-rust-std/challenges/0022-str-iter.html) | 10,000 USD | Open | |
50+
| [23: Verify the safety of Vec functions part 1](https://model-checking.github.io/verify-rust-std/challenges/0023-vec-pt1.html) | 15,000 USD | Open | |
51+
| [24: Verify the safety of Vec functions part 2](https://model-checking.github.io/verify-rust-std/challenges/0024-vec-pt2.html) | 15,000 USD | Open | |
52+
| [25: Verify the safety of `VecDeque` functions](https://model-checking.github.io/verify-rust-std/challenges/0025-vecdeque.html) | 10,000 USD | Open | |
53+
| [26: Verify reference-counted Cell implementation](https://model-checking.github.io/verify-rust-std/challenges/0026-rc.html) | 10,000 USD | Open | |
54+
| [27: Verify atomically reference-counted Cell implementation](https://model-checking.github.io/verify-rust-std/challenges/0027-arc.html) | 10,000 USD | Open | |
5555

5656
See [our book](https://model-checking.github.io/verify-rust-std/intro.html) for more details on the challenge rules.
5757

‎scripts/kani-std-analysis/metrics-data-core.json‎

Lines changed: 88 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -644,6 +644,94 @@
644644
"verified_safe_fns_under_contract": 111,
645645
"verified_safe_fns_with_loop_under_contract": 0,
646646
"total_functions_under_contract_all_crates": 417
647+
},
648+
{
649+
"date": "2025-09-14",
650+
"total_unsafe_fns": 7190,
651+
"total_unsafe_fns_with_loop": 22,
652+
"total_safe_abstractions": 1888,
653+
"total_safe_abstractions_with_loop": 88,
654+
"total_safe_fns": 15871,
655+
"total_safe_fns_with_loop": 750,
656+
"unsafe_fns_under_contract": 284,
657+
"unsafe_fns_with_loop_under_contract": 3,
658+
"verified_unsafe_fns_under_contract": 253,
659+
"verified_unsafe_fns_with_loop_under_contract": 1,
660+
"safe_abstractions_under_contract": 77,
661+
"safe_abstractions_with_loop_under_contract": 0,
662+
"verified_safe_abstractions_under_contract": 77,
663+
"verified_safe_abstractions_with_loop_under_contract": 0,
664+
"safe_fns_under_contract": 114,
665+
"safe_fns_with_loop_under_contract": 0,
666+
"verified_safe_fns_under_contract": 111,
667+
"verified_safe_fns_with_loop_under_contract": 0,
668+
"total_functions_under_contract_all_crates": 417
669+
},
670+
{
671+
"date": "2025-09-21",
672+
"total_unsafe_fns": 7190,
673+
"total_unsafe_fns_with_loop": 22,
674+
"total_safe_abstractions": 1888,
675+
"total_safe_abstractions_with_loop": 88,
676+
"total_safe_fns": 15871,
677+
"total_safe_fns_with_loop": 750,
678+
"unsafe_fns_under_contract": 284,
679+
"unsafe_fns_with_loop_under_contract": 3,
680+
"verified_unsafe_fns_under_contract": 253,
681+
"verified_unsafe_fns_with_loop_under_contract": 1,
682+
"safe_abstractions_under_contract": 77,
683+
"safe_abstractions_with_loop_under_contract": 0,
684+
"verified_safe_abstractions_under_contract": 77,
685+
"verified_safe_abstractions_with_loop_under_contract": 0,
686+
"safe_fns_under_contract": 114,
687+
"safe_fns_with_loop_under_contract": 0,
688+
"verified_safe_fns_under_contract": 111,
689+
"verified_safe_fns_with_loop_under_contract": 0,
690+
"total_functions_under_contract_all_crates": 417
691+
},
692+
{
693+
"date": "2025-09-28",
694+
"total_unsafe_fns": 7190,
695+
"total_unsafe_fns_with_loop": 22,
696+
"total_safe_abstractions": 1888,
697+
"total_safe_abstractions_with_loop": 88,
698+
"total_safe_fns": 15871,
699+
"total_safe_fns_with_loop": 750,
700+
"unsafe_fns_under_contract": 284,
701+
"unsafe_fns_with_loop_under_contract": 3,
702+
"verified_unsafe_fns_under_contract": 253,
703+
"verified_unsafe_fns_with_loop_under_contract": 1,
704+
"safe_abstractions_under_contract": 77,
705+
"safe_abstractions_with_loop_under_contract": 0,
706+
"verified_safe_abstractions_under_contract": 77,
707+
"verified_safe_abstractions_with_loop_under_contract": 0,
708+
"safe_fns_under_contract": 114,
709+
"safe_fns_with_loop_under_contract": 0,
710+
"verified_safe_fns_under_contract": 111,
711+
"verified_safe_fns_with_loop_under_contract": 0,
712+
"total_functions_under_contract_all_crates": 417
713+
},
714+
{
715+
"date": "2025-10-05",
716+
"total_unsafe_fns": 7190,
717+
"total_unsafe_fns_with_loop": 22,
718+
"total_safe_abstractions": 1888,
719+
"total_safe_abstractions_with_loop": 88,
720+
"total_safe_fns": 15871,
721+
"total_safe_fns_with_loop": 750,
722+
"unsafe_fns_under_contract": 284,
723+
"unsafe_fns_with_loop_under_contract": 3,
724+
"verified_unsafe_fns_under_contract": 253,
725+
"verified_unsafe_fns_with_loop_under_contract": 1,
726+
"safe_abstractions_under_contract": 77,
727+
"safe_abstractions_with_loop_under_contract": 0,
728+
"verified_safe_abstractions_under_contract": 77,
729+
"verified_safe_abstractions_with_loop_under_contract": 0,
730+
"safe_fns_under_contract": 114,
731+
"safe_fns_with_loop_under_contract": 0,
732+
"verified_safe_fns_under_contract": 111,
733+
"verified_safe_fns_with_loop_under_contract": 0,
734+
"total_functions_under_contract_all_crates": 417
647735
}
648736
]
649737
}

‎scripts/kani-std-analysis/metrics-data-std.json‎

Lines changed: 88 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -527,6 +527,94 @@
527527
"verified_safe_fns_under_contract": 0,
528528
"verified_safe_fns_with_loop_under_contract": 0,
529529
"total_functions_under_contract_all_crates": 417
530+
},
531+
{
532+
"date": "2025-09-14",
533+
"total_unsafe_fns": 186,
534+
"total_unsafe_fns_with_loop": 12,
535+
"total_safe_abstractions": 528,
536+
"total_safe_abstractions_with_loop": 47,
537+
"total_safe_fns": 4222,
538+
"total_safe_fns_with_loop": 190,
539+
"unsafe_fns_under_contract": 10,
540+
"unsafe_fns_with_loop_under_contract": 1,
541+
"verified_unsafe_fns_under_contract": 7,
542+
"verified_unsafe_fns_with_loop_under_contract": 0,
543+
"safe_abstractions_under_contract": 0,
544+
"safe_abstractions_with_loop_under_contract": 0,
545+
"verified_safe_abstractions_under_contract": 0,
546+
"verified_safe_abstractions_with_loop_under_contract": 0,
547+
"safe_fns_under_contract": 0,
548+
"safe_fns_with_loop_under_contract": 0,
549+
"verified_safe_fns_under_contract": 0,
550+
"verified_safe_fns_with_loop_under_contract": 0,
551+
"total_functions_under_contract_all_crates": 417
552+
},
553+
{
554+
"date": "2025-09-21",
555+
"total_unsafe_fns": 186,
556+
"total_unsafe_fns_with_loop": 12,
557+
"total_safe_abstractions": 528,
558+
"total_safe_abstractions_with_loop": 47,
559+
"total_safe_fns": 4222,
560+
"total_safe_fns_with_loop": 190,
561+
"unsafe_fns_under_contract": 10,
562+
"unsafe_fns_with_loop_under_contract": 1,
563+
"verified_unsafe_fns_under_contract": 7,
564+
"verified_unsafe_fns_with_loop_under_contract": 0,
565+
"safe_abstractions_under_contract": 0,
566+
"safe_abstractions_with_loop_under_contract": 0,
567+
"verified_safe_abstractions_under_contract": 0,
568+
"verified_safe_abstractions_with_loop_under_contract": 0,
569+
"safe_fns_under_contract": 0,
570+
"safe_fns_with_loop_under_contract": 0,
571+
"verified_safe_fns_under_contract": 0,
572+
"verified_safe_fns_with_loop_under_contract": 0,
573+
"total_functions_under_contract_all_crates": 417
574+
},
575+
{
576+
"date": "2025-09-28",
577+
"total_unsafe_fns": 186,
578+
"total_unsafe_fns_with_loop": 12,
579+
"total_safe_abstractions": 528,
580+
"total_safe_abstractions_with_loop": 47,
581+
"total_safe_fns": 4222,
582+
"total_safe_fns_with_loop": 190,
583+
"unsafe_fns_under_contract": 10,
584+
"unsafe_fns_with_loop_under_contract": 1,
585+
"verified_unsafe_fns_under_contract": 7,
586+
"verified_unsafe_fns_with_loop_under_contract": 0,
587+
"safe_abstractions_under_contract": 0,
588+
"safe_abstractions_with_loop_under_contract": 0,
589+
"verified_safe_abstractions_under_contract": 0,
590+
"verified_safe_abstractions_with_loop_under_contract": 0,
591+
"safe_fns_under_contract": 0,
592+
"safe_fns_with_loop_under_contract": 0,
593+
"verified_safe_fns_under_contract": 0,
594+
"verified_safe_fns_with_loop_under_contract": 0,
595+
"total_functions_under_contract_all_crates": 417
596+
},
597+
{
598+
"date": "2025-10-05",
599+
"total_unsafe_fns": 186,
600+
"total_unsafe_fns_with_loop": 12,
601+
"total_safe_abstractions": 528,
602+
"total_safe_abstractions_with_loop": 47,
603+
"total_safe_fns": 4222,
604+
"total_safe_fns_with_loop": 190,
605+
"unsafe_fns_under_contract": 10,
606+
"unsafe_fns_with_loop_under_contract": 1,
607+
"verified_unsafe_fns_under_contract": 7,
608+
"verified_unsafe_fns_with_loop_under_contract": 0,
609+
"safe_abstractions_under_contract": 0,
610+
"safe_abstractions_with_loop_under_contract": 0,
611+
"verified_safe_abstractions_under_contract": 0,
612+
"verified_safe_abstractions_with_loop_under_contract": 0,
613+
"safe_fns_under_contract": 0,
614+
"safe_fns_with_loop_under_contract": 0,
615+
"verified_safe_fns_under_contract": 0,
616+
"verified_safe_fns_with_loop_under_contract": 0,
617+
"total_functions_under_contract_all_crates": 417
530618
}
531619
]
532620
}

‎testable-simd-models/Cargo.toml‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
[package]
2+
name = "testable-simd-models"
3+
version = "0.0.2"
4+
authors = ["Cryspen"]
5+
license = "Apache-2.0"
6+
homepage = "https://github.com/cryspen/verify-rust-std/testable-simd-models"
7+
edition = "2021"
8+
repository = "https://github.com/cryspen/verify-rust-std/testable-simd-models"
9+
readme = "README.md"
10+
11+
[dependencies]
12+
rand = "0.9"
13+
pastey = "0.1.0"
14+
15+
[lints.rust]
16+
unexpected_cfgs = { level = "warn" }

0 commit comments

Comments
 (0)