add docs to stdlib

src/stdlib/native/bits/lib.no

@@ -1,34 +1,77 @@
+/// a hint function (unconstrained) to extracts the `nth` bit from a given `value`.
+/// Its current implementation points to `std::bits::nth_bit`. So it has an empty body in definition.
+/// 
+/// # Parameters
+/// - `value`: The `Field` value from which to extract the bit.
+/// - `nth`: The position of the bit to extract (0-indexed).
+/// 
+/// # Returns
+/// - `Field`: The value of the `nth` bit (0 or 1).
+/// 
 hint fn nth_bit(value: Field, const nth: Field) -> Field;
 
-// Convert a bit array to a Field
+/// Converts an array of boolean values (`bits`) into a `Field` value.
+///
+/// # Parameters
+/// - `bits`: An array of `Bool` values representing bits, where each `true` represents `1` and `false` represents `0`.
+///
+/// # Returns
+/// - `Field`: A `Field` value that represents the integer obtained from the binary representation of `bits`.
+///
+/// # Example
+/// ```
+/// let bits = [true, false, true]; // Represents the binary value 101
+/// let result = from_bits(bits);
+/// `result` should be 5 as 101 in binary equals 5 in decimal.
+/// ```
 fn from_bits(bits: [Bool; LEN]) -> Field {
     let mut lc1 = 0;
     let mut e2 = 1;
     let zero = 0;
 
     for index in 0..LEN {
-        lc1 = lc1 + if bits[index] {e2} else {zero};
+        lc1 = lc1 + if bits[index] { e2 } else { zero };
         e2 = e2 + e2;
     }
     return lc1;
 }
 
-// Convert a Field to a bit array
+/// Converts a `Field` value into an array of boolean values (`bits`) representing its binary form.
+///
+/// # Parameters
+/// - `LEN`: The length of the resulting bit array. Determines how many bits are considered in the conversion.
+/// - `value`: The `Field` value to convert into binary representation.
+///
+/// # Returns
+/// - `[Bool; LEN]`: An array of boolean values where each `true` represents `1` and `false` represents `0`.
+///
+/// # Example
+/// ```
+/// let value = 5; // Binary representation: 101
+/// let bits = to_bits(3, value);
+/// `bits` should be [true, false, true] corresponding to the binary 101.
+/// ```
+/// 
+/// # Panics
+/// - The function asserts that `from_bits(bits)` equals `value`, ensuring the conversion is correct.
 fn to_bits(const LEN: Field, value: Field) -> [Bool; LEN] {
     let mut bits = [false; LEN];
     let mut lc1 = 0;
     let mut e2 = 1;
 
-    // todo: ITE should allow literals
+    // TODO: ITE should allow literals.
     let true_val = true;
     let false_val = false;
 
     for index in 0..LEN {
         let bit_num = unsafe nth_bit(value, index);
 
-        bits[index] = if bit_num == 1 {true_val} else {false_val};
+        // constraint the bit values to booleans
+        bits[index] = if bit_num == 1 { true_val } else { false_val };
     }
 
+    // constraint the accumulative contributions of bits to be equal to the value
     assert_eq(from_bits(bits), value);
+
     return bits;
 }

src/stdlib/native/comparator/lib.no

@@ -1,39 +1,54 @@
 use std::bits;
 
-// Instead of comparing bit by bit, we check the carry bit:
-// lhs + (1 << LEN) - rhs
-// proof:
-// lhs + (1 << LEN) will add a carry bit, valued 1, to the bit array representing lhs, 
-// resulted in a bit array of length LEN + 1, named as sum_bits.
-// if `lhs < rhs``, then `lhs - rhs < 0`, thus `(1 << LEN) + lhs - rhs < (1 << LEN)`
-// then, the carry bit of sum_bits is 0.
-// otherwise, the carry bit of sum_bits is 1.
+/// Checks if `lhs` is less than `rhs` by evaluating the carry bit after addition and subtraction.
+/// 
+/// # Parameters
+/// - `LEN`: The assumped bit length of both `lhs` and `rhs`.
+/// - `lhs`: The left-hand side `Field` value to be compared.
+/// - `rhs`: The right-hand side `Field` value to be compared.
+///
+/// # Returns
+/// - `Bool`: `true` if `lhs` is less than `rhs`, otherwise `false`.
+///
+/// # Proof
+/// - Adding `pow2` to `lhs` ensures a carry bit is added to the result, creating a bit array of length `LEN + 1`.
+/// - If `lhs < rhs`, then `lhs - rhs < 0`, making `(1 << LEN) + lhs - rhs` less than `1 << LEN`, resulting in a carry bit of `0`.
+/// - Otherwise, the carry bit will be `1`.
+///
 fn less_than(const LEN: Field, lhs: Field, rhs: Field) -> Bool {
     let carry_bit_len = LEN + 1;
 
-    // 1 << LEN
+    // Calculate 2^LEN using bit shifts.
     let mut pow2 = 1;
     for ii in 0..LEN {
         pow2 = pow2 + pow2;
     }
 
+    // Calculate the adjusted sum to determine the carry bit.
     let sum = (pow2 + lhs) - rhs;
     let sum_bit = bits::to_bits(carry_bit_len, sum);
 
-    // todo: modify the ife to allow literals
     let b1 = false;
     let b2 = true;
     let res = if sum_bit[LEN] { b1 } else { b2 };
 
     return res;
 }
 
-// Less than or equal to.
-// based on the proof of less_than():
-// adding 1 to the rhs, can upper bound by 1 for the lhs:
-// lhs < rhs + 1
-// is equivalent to
-// lhs <= rhs
+/// Checks if `lhs` is less than or equal to `rhs` using the `less_than` function.
+/// 
+/// # Parameters
+/// - `LEN`: The assumped bit length of both `lhs` and `rhs`.
+/// - `lhs`: The left-hand side `Field` value to be compared.
+/// - `rhs`: The right-hand side `Field` value to be compared.
+///
+/// # Returns
+/// - `Bool`: `true` if `lhs` is less than or equal to `rhs`, otherwise `false`.
+///
+/// # Proof
+/// By adding 1 to rhs can increase upper bound by 1 for the lhs.
+/// Thus, `lhs < lhs + 1` => `lhs <= rhs`.
+/// ```
 fn less_eq_than(const LEN: Field, lhs: Field, rhs: Field) -> Bool {
     return less_than(LEN, lhs, rhs + 1);
 }