#encoding #strict-encoding #gadt #aluvm #ubideco

bin+lib strict_types

Strict types: confined generalized algebraic data types (GADT)

6 releases

new 1.0.0-beta.6 Mar 19, 2023
1.0.0-beta.5 Mar 10, 2023
1.0.0-beta.3 Feb 4, 2023
1.0.0-beta.1 Jan 30, 2023

#142 in Math

Download history 54/week @ 2023-01-29 212/week @ 2023-02-05 12/week @ 2023-02-12 62/week @ 2023-02-19 18/week @ 2023-02-26 457/week @ 2023-03-05 110/week @ 2023-03-12

648 downloads per month
Used in 3 crates (via rgb-contracts)


4.5K SLoC

Strict types AST and typelib implementation

Protobufs for functional programming

This is a set of libraries for working with abstract syntax trees and libraries of strict types – type system made with category theory which ensures provable properties and bounds for the in-memory and serialized type representation.

Strict types is a formal notation for defining and serializing generalized algebraic data types (GADT) in a deterministic and confined way. It is developed with type theory in mind.

Strict Types are:

  • schema-based (with the schema being strict encoding notation),
  • semantic, i.e. defines types not just as they are layed out in memory, but also depending on their meaning,
  • deterministic, i.e. produces the same result for a given type,
  • portabile, i.e. can run on ahy hardware architecture and OS, including low-performant embedded systems,
  • confined, i.e. provides guarantees and static analysis on a maximum size of the typed data,
  • formally verifiabile.

To learn more about strict encoding read the spec.

Strict types works with type definitions. It allows:

  • static analysis of data types, like
    • defining semantic type ids;
    • specifying exact memory layout;
    • type equivalence in terms of semantics and memory layout;
    • size of serialized data
  • composing types into type libraries;
  • versioning type libraries basing on the semantic types;

The library allows to generate & compile strict type libraries (STL) from rust types implementing StrictEncoding trait -- and ensures that the deserialization with StrictDecode follows the same memory and semantic layout.

Strict Types Library

The library is able to reflect on itself, producing replica of its rust data types in strict types system.

Strict types library id: stl:DYTdc4m4C6HLfM9hQCoavFHbdnwVuFQkWStTHDeHfDZ1#final-olivia-segment

Import this lib by putting in the file header import final_olivia_segment_DYTdc4m4C6HLfM9hQCoavFHbdnwVuFQkWStTHDeHfDZ1 as StrictTypes

Source code can be found in [stl/StrictTypes.sty] file.




The libraries are distributed on the terms of Apache 2.0 license.


~114K SLoC