Add basic comments

model-checking · jaisnan · Jun 11, 2024 · May 31, 2024 · Jun 3, 2024 · Jun 4, 2024
commit e96d4a74a86a7348871916ee676116f2dfc4e74b
@@ -1,6 +1,12 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
+//! This macro generates implementations of the `Arbitrary` trait for various types. The `Arbitrary` trait defines
+//! methods for generating arbitrary (unconstrained) values of the implementing type.
+//! trivial_arbitrary and nonzero_arbitrary are implementations of Arbitrary for types that can be represented
+//! by an unconstrained symbolic value of their size (e.g., `u8`, `u16`, `u32`, etc.).
+//!
+//! TODO: Use this inside kani library so that we dont have to maintain two copies of the same proc macro for arbitrary.
 #[macro_export]
 macro_rules! generate_arbitrary {
     ($core:path) => {

@@ -47,6 +47,11 @@ macro_rules! kani_lib {
     };
 }
 
+/// Kani intrinsics contains the public APIs used by users to verify their harnesses.
+/// This macro is a part of kani_core as that allows us to verify even libraries that are no_core
+/// such as core in rust's std library itself.
+///
+/// TODO: Use this inside kani library so that we dont have to maintain two copies of the same intrinsics.
 #[macro_export]
 macro_rules! kani_intrinsics {
     () => {