diff --git a/docs/SUMMARY.md b/docs/SUMMARY.md
index e32839a2..3b3e2c78 100644
--- a/docs/SUMMARY.md
+++ b/docs/SUMMARY.md
@@ -10,7 +10,7 @@
   - [Zama Devnet](getting_started/faucet/devnet.md)
   - [Local node](getting_started/faucet/local.md)
 
-## Writing contract
+## Writing contracts
 
 - [Getting started](solidity/getting_started.md)
   - [Hardhat](solidity/getting_started/hardhat.md)
diff --git a/docs/solidity/functions.md b/docs/solidity/functions.md
index 5980bb82..de7a905a 100644
--- a/docs/solidity/functions.md
+++ b/docs/solidity/functions.md
@@ -21,12 +21,9 @@ In this case, operators can take as input operands of the following types
 - `uint32`
 
 under the condition that the size of the `uint` operand is at most the size of the `euint` operand.
-For example, `add(uint8 a, euint8 b)` is defined but `add(uint16 a, euint16 b)` is not.
+For example, `add(uint8 a, euint8 b)` is defined but `add(uint32 a, euint16 b)` is not.
 Note that these ciphertext-plaintext operations may take less time to compute than ciphertext-ciphertext operations.
 
-In the backend, FHE operations are only defined on same-type operands.
-Therefore, the `TFHE` Solidity library will do implicit upcasting if necessary.
-
 ## `asEuint`
 
 The `asEuint` functions serve three purposes:
@@ -180,3 +177,27 @@ Note that since we work with unsigned integers, the result of negation is interp
 The `not` operator returns the value obtained after flipping all the bits of the operand.
 
 > **_NOTE:_** More information about the behavior of these operators can be found at the [TFHE-rs docs](https://docs.zama.ai/tfhe-rs/getting-started/operations#arithmetic-operations.).
+
+## Generating random encrypted integers
+
+Random encrypted integers of types `euint8`, `euint16` or `euint32` can be generated fully on-chain.
+
+That can only be done during transactions and not on an `eth_call` RPC method, because PRNG state needs to be mutated on-chain during generation.
+
+> **_IMPORTANT:_** Not for use in production! Currently, integers are generated in the plain via a PRNG whose seed and state are public, with the state being on-chain. An FHE-based PRNG is coming soon, where the seed and state will be encrypted.
+
+> **_NOTE:_** As of now, there is a separate PRNG per smart contract. That might change when the FHE-based PRNG is implemented.
+
+### Examples
+
+```solidity
+// random euint8
+function randEuint8() internal view returns (euint8)
+
+// random euint16
+function randEuint16() internal view returns (euint16)
+
+// random euint32
+function randEuint32() internal view returns (euint32)
+
+```
\ No newline at end of file
diff --git a/docs/solidity/library.md b/docs/solidity/library.md
index 14f28889..d3615e41 100644
--- a/docs/solidity/library.md
+++ b/docs/solidity/library.md
@@ -1,55 +1,84 @@
 # Library
 
-The library exposes utility functions for TFHE operations.
-The goal of the library is to provide a seamless developer experience for writing smart contracts that can operate on confidential data.
+The TFHE library exposes functions for:
+ - homomorphic operations involving TFHE ciphertexts
+ - decrypting or reencrypting TFHE ciphertexts
+
+Its goal is to provide a seamless developer experience for writing smart contracts that operate on confidential data.
+
+It is under active development and some features are implemented, some are mockups and others are coming soon.
 
 ## Types
 
-The library provides a type system that is checked both at compile time and at run time.
-The structure and operations related to these types are described in this sections.
+The TFHE library provides encrypted integer types and a type system that is checked both at compile time and at run time.
 
-We currently support encrypted integers of bit length up to 32 bits.
+Encrypted integers behave as much as possible as Solidity's integer types. Currently, however, behaviour such as "revert on overflow" is not supported as this would leak some information about the encrypted value. Therefore, arithmetic on `euint` types is [unchecked](https://docs.soliditylang.org/en/latest/control-structures.html#checked-or-unchecked-arithmetic), i.e. there is wrap-around on overlow.
 
-<!-- Support for up to 256 bits is on our roadmap.  -->
+Encrypted integers with overflow checking are coming soon to the THFE library. They will allow reversal in case of an overflow, but will
+leak some information about the operands.
 
-Our library provides the following types :
+In terms of implementation in the backend, encrypted integers take the form of TFHE ciphertexts.
+The TFHE library abstracts away that and, instead, exposes ciphertext handles to the smart contract developer.
+The `euint` types are _wrappers_ over these handles.
 
-- `ebool`
-- `euint8`
-- `euint16`
-- `euint32`
+The following TFHE data types are defined:
 
-These encrypted integers behave as much as possible as Solidity's integer types. However, behaviour such as "revert on overflow" is not supported as this would leak some information of the encrypted integers. Therefore, arithmetic on `euint` types is [unchecked](https://docs.soliditylang.org/en/latest/control-structures.html#checked-or-unchecked-arithmetic), i.e. there is wrap-around on overlow.
+| type                  | supported       |
+| --------------------- | ----------------|
+| `ebool`               | yes (1)         |
+| `euint8`              | yes             |
+| `euint16`             | yes             |
+| `euint32`             | yes             |
+| `euint64`             | no, coming soon |
+| `euint128`            | no              |
+| `euint256`            | no              |
+| `eint8`               | no, coming soon |
+| `eint16`              | no, coming soon |
+| `eint32`              | no, coming soon |
+| `eint64`              | no, coming soon |
+| `eint128`             | no              |
+| `eint256`             | no              |
 
-In the back-end, encrypted integers are TFHE ciphertexts.
-The library abstracts away the ciphertexts and presents pointers to ciphertexts, or ciphertext handles, to the smart contract developer.
-The `euint` types are _wrappers_ over these handles.
+> **_NOTE 1:_** The `ebool` type is currently implemented as an `euint8`. A more optimized native boolean type will replace `euint8`.
 
 ## Operations
 
-The library exposes utility functions for operations on TFHE ciphertexts.
-The list of supported operations is presented below.
-
-| name                  | function name | type   |
-| --------------------- | ------------- | ------ |
-| Add                   | `TFHE.add`    | Binary |
-| Sub                   | `TFHE.sub`    | Binary |
-| Mul                   | `TFHE.mul`    | Binary |
-| BitAnd                | `TFHE.and`    | Binary |
-| BitOr                 | `TFHE.or`     | Binary |
-| BitXor                | `TFHE.xor`    | Binary |
-| Shift Right           | `TFHE.shr`    | Binary |
-| Shift Left            | `TFHE.shl`    | Binary |
-| Equal                 | `TFHE.eq`     | Binary |
-| Not equal             | `TFHE.ne`     | Binary |
-| Greater than or equal | `TFHE.ge`     | Binary |
-| Greater than          | `TFHE.gt`     | Binary |
-| Less than or equal    | `TFHE.le`     | Binary |
-| Less than             | `TFHE.lt`     | Binary |
-| Min                   | `TFHE.min`    | Binary |
-| Max                   | `TFHE.max`    | Binary |
-| Neg                   | `TFHE.neg`    | Unary  |
-| Not                   | `TFHE.not`    | Unary  |
-| Cmux                  | `TFHE.cmux`   | Ternary|
+The TFHE library exposes the following operations involving TFHE ciphertexts:
+
+| name                  | function name       | type         | supported            |
+| --------------------- | ------------------- | ------------ | -------------------- |
+| Add                   | `TFHE.add`          | Binary       | yes                  |
+| Add w/ Overflow Check | `TFHE.safeAdd`      | Binary       | no, coming soon      |
+| Sub                   | `TFHE.sub`          | Binary       | yes                  |
+| Sub w/ Overflow Check | `TFHE.safeSub`      | Binary       | no, coming soon      |
+| Mul                   | `TFHE.mul`          | Binary       | yes                  |
+| Mul w/ Overflow Check | `TFHE.safeMul`      | Binary       | no, coming soon      |
+| BitAnd                | `TFHE.and`          | Binary       | yes                  |
+| BitOr                 | `TFHE.or`           | Binary       | yes                  |
+| BitXor                | `TFHE.xor`          | Binary       | yes                  |
+| Shift Right           | `TFHE.shr`          | Binary       | yes                  |
+| Shift Left            | `TFHE.shl`          | Binary       | yes                  |
+| Equal                 | `TFHE.eq`           | Binary       | yes                  |
+| Not equal             | `TFHE.ne`           | Binary       | yes                  |
+| Greater than or equal | `TFHE.ge`           | Binary       | yes                  |
+| Greater than          | `TFHE.gt`           | Binary       | yes                  |
+| Less than or equal    | `TFHE.le`           | Binary       | yes                  |
+| Less than             | `TFHE.lt`           | Binary       | yes                  |
+| Min                   | `TFHE.min`          | Binary       | yes                  |
+| Max                   | `TFHE.max`          | Binary       | yes                  |
+| Neg                   | `TFHE.neg`          | Unary        | yes                  |
+| Not                   | `TFHE.not`          | Unary        | yes                  |
+| Cmux                  | `TFHE.cmux`         | Ternary      | yes (1)              |
+| Decrypt               | `TFHE.decrypt()`    | Decryption   | yes (2)              |
+| Reencrypt             | `TFHE.reencrypt()`  | Reencryption | yes (2)              |
+| Optimistic Require    | `TFHE.optReq()`     | Decryption   | yes (1)              |
+| Random unsigned int   | `TFHE.randEuintX()` | Random       | mockup (3)           |
+| Random signed int     | `TFHE.randEintX()`  | Random       | mockup coming soon   |
+
+> **_NOTE 1:_**
+
+> **_NOTE 2:_**
+
+> **_NOTE 3:_**
 
 More information about the supported operations can be found at the [TFHE-rs docs](https://docs.zama.ai/tfhe-rs/getting-started/operations#arithmetic-operations.).