# VTS: Verified TypeS

[![Continuous integration](https://github.com/input-output-hk/ce-vts/actions/workflows/rust.yml/badge.svg?branch=main)](https://github.com/input-output-hk/ce-vts/actions/workflows/rust.yml)

This started as a simple thought about implementing a new type system where
we can represent a type with its underlying specification.

```nocompile
type NewType = BaseType
    where constraint;
```

The `NewType` is defined as a wrapper around `BaseType` with the `constraint` attached to it.

For example once could define the following:

```rust
vts::vts!{
    /// String that have been already validated against the constraint that
    /// all the characters of the string are valid hexadecimal digits
    ///
    /// For example:
    ///
    /// * `00`
    /// * `a`
    /// * `0123456789abcdef`
    ///
    #[derive(Debug, Clone, PartialEq, Eq, Hash)]
    pub type HexaString = String
        where self.chars().all(|c| c.is_ascii_hexdigit());
}
```

So here we say that the `HexaString` is a `String` where all the characters
comply with the given `constraint` : all chars are ASCII hexadecimal characters.

In the context of the Rust implementation, this is only a convenient way
to wrap a base type and to add some constraint to the lifting. In essence the
generated code will look like the following:

```rust
struct HexaString(String);
struct HexaStringConstraintError;

impl HexaString {
    pub fn new(value: String) -> Result<Self, HexaStringConstraintError> {
        let value = Self(value);
        if value.__constraint() {
            Ok(value)
        } else {
            Err(HexaStringConstraintError)
        }
    }

    fn __constraint(&self) -> bool {
        self.chars().all(|c| c.is_ascii_hexdigit())
    }
}

impl std::ops::Deref for HexaString {
    type Target = String;
    fn deref(&self) -> &Self::Target {
        &self.0
    }
}
```