hypersonic 0.12.0

Formally-verifiable distributed software
Documentation
{-
  Id: stl:FOnI~0yx-bcvd_Wq-~xjW37p-uqzQ3Nq-GGH8AtN-dO64ac8#river-atomic-dallas
  Name: SONIC
  Version: 0.12.0
  Description: Standard library for formally-verifiable distributed contracts
  Author: Dr Maxim Orlovsky <orlovsky@ubideco.org>
  Copyright (C) 2024-2025 Laboratories for Ubiquitous Deterministic Computing (UBIDECO),
                          Institute for Distributed and Cognitive Systems (InDCS), Switzerland.
                          All rights reserved.
  License: Apache-2.0
-}

@context
typelib SONIC

import UltraSONIC#korea-helena-moral
  use StateData#mission-first-owner
  use Consensus#nissan-congo-clark
  use ContractName#value-reform-lesson
  use Genesis#minute-prism-small
  use ContractMeta#element-novel-salute
  use CellLock#jasmine-demo-resume
  use StateValue#kiwi-million-ford
  use Codex#adam-mega-analyze
  use Issue#finance-peru-havana
  use Opid#storm-dragon-brain
  use ContractId#uniform-welcome-papa
  use AuthToken#western-america-patrol
  use CodexId#cargo-season-impact
  use Identity#smart-pioneer-nominal
  use StateCell#tarzan-jordan-camera
  use CellAddr#lecture-vincent-carbon
  use RawData#lima-anvil-karate

import FiniteField#report-canal-convert
  use Fe256#palace-mixer-visual

import Std#delete-roman-hair
  use AsciiPrintable#ultra-sunset-format
  use Bool#oxygen-complex-duet
  use AlphaCapsNum#aladdin-zebra-marble
  use AlphaNumLodash#percent-bingo-caesar
  use AlphaCapsLodash#duet-hammer-labor
  use AlphaSmallLodash#pioneer-eagle-spell

import AluVM#reward-accent-swim
  use Lib#report-gordon-recycle
  use IsaId#mobile-letter-absorb
  use LibId#germany-culture-olivia
  use CoreConfig#ventura-ibiza-special
  use LibSite#polo-macro-elite

import CommitVerify#biology-news-adam
  use ReservedBytes1#origin-roger-relax
  use ReservedBytes2#florida-libra-circus
  use ReservedBytes6#joker-peru-brave
  use ReservedBytes4#young-goblin-academy

import StrictTypes#henry-heart-survive
  use VariantName#theory-austin-before
  use FieldName#present-flute-herman
  use Primitive#deliver-arrow-boxer
  use TySemId#popcorn-super-young
  use FieldSemId#spiral-road-marco
  use TypeName#edgar-carol-mystery
  use UnnamedFieldsSemId#freedom-degree-gregory
  use SemId#logic-absorb-hilton
  use Variant#humor-regard-promise
  use Sizing#courage-alien-salon
  use NamedFieldsSemId#solar-salad-smoke
  use EnumVariants#dispute-natasha-vega
  use VariantInfoSemId#museum-edward-mirror
  use UnionVariantsSemId#santana-address-pepper
  use TypeSystem#adrian-boris-sponsor


@mnemonic(arcade-graph-bruno)
data Aggregator        : none ()
                       | some SubAggregator
                       | take SubAggregator
                       | or (SubAggregator, SubAggregator)
                       | aluVm#255 AluVM.LibSite

@mnemonic(cobra-abraham-bonus)
data Api               : codexId UltraSONIC.CodexId
                       , conforms {U16 ^ ..0xff}
                       , defaultCall CallState?
                       , global {StrictTypes.VariantName -> ^ ..0xff GlobalApi}
                       , owned {StrictTypes.VariantName -> ^ ..0xff OwnedApi}
                       , aggregators {StrictTypes.VariantName -> ^ ..0xff Aggregator}
                       , verifiers {StrictTypes.VariantName -> ^ ..0xff U16}
                       , errors {U256 -> ^ ..0xff [Unicode ^ ..0xff]}

@mnemonic(viva-index-tempo)
data ApisChecksum      : [Byte ^ 4]

@mnemonic(project-freddie-oasis)
data Articles          : semantics Semantics
                       , sig SigBlob?
                       , issue UltraSONIC.Issue

@mnemonic(pigment-melon-smart)
data ArticlesId        : contractId UltraSONIC.ContractId
                       , version U16
                       , checksum ApisChecksum

@mnemonic(sparta-ginger-analyze)
data CallState         : method StrictTypes.VariantName, owned StrictTypes.VariantName?

@mnemonic(polaris-yellow-public)
data GlobalApi         : semId StrictTypes.SemId
                       , published Std.Bool
                       , convertor StateConvertor
                       , builder StateBuilder
                       , rawConvertor RawConvertor
                       , rawBuilder RawBuilder

@mnemonic(salon-record-hope)
data Issuer            : codex UltraSONIC.Codex
                       , semantics Semantics
                       , sig SigBlob?

@mnemonic(laser-george-europe)
data IssuerId          : codexId UltraSONIC.CodexId
                       , version U16
                       , checksum ApisChecksum

@mnemonic(history-support-manual)
data OwnedApi          : semId StrictTypes.SemId
                       , arithmetics StateArithm
                       , convertor StateConvertor
                       , builder StateBuilder
                       , witnessSemId StrictTypes.SemId
                       , witnessBuilder StateBuilder

@mnemonic(tropic-brenda-reply)
data RawBuilder        : strictEncode StrictTypes.SemId
                       | aluVm#255 AluVM.LibSite

@mnemonic(result-right-amazon)
data RawConvertor      : strictDecode StrictTypes.SemId
                       | aluVm#255 AluVM.LibSite

@mnemonic(senator-flower-guru)
data Semantics         : version U16
                       , default Api
                       , custom {StrictTypes.TypeName -> Api}
                       , codexLibs {AluVM.Lib}
                       , apiLibs {AluVM.Lib}
                       , types StrictTypes.TypeSystem

@mnemonic(insect-cello-avalon)
data SigBlob           : [Byte ^ 1..0x1000]

@mnemonic(pablo-cotton-mirror)
data StateArithm       : fungible ()
                       | nonFungible ()
                       | aluVm#255 AluVM.LibSite

@mnemonic(reverse-delphi-camel)
data StateBuilder      : unit ()
                       | typedEncoder#16 U256
                       | typedFieldEncoder U256
                       | aluVm#255 AluVM.LibSite

@mnemonic(beach-congo-instant)
data StateConvertor    : unit ()
                       | typedEncoder#16 U256
                       | typedFieldEncoder U256
                       | aluVm#255 AluVM.LibSite

@mnemonic(benny-marina-fashion)
data StateSelector     : global (StrictTypes.VariantName, Std.Bool)
                       | aggregated StrictTypes.VariantName

@mnemonic(archer-metal-bison)
data SubAggregator     : const (StrictTypes.SemId, [Byte ^ ..0xff])
                       | theOnly StrictTypes.VariantName
                       | copy StrictTypes.VariantName
                       | unwrap StrictTypes.VariantName
                       | first StrictTypes.VariantName
                       | nth (StrictTypes.VariantName, U16)
                       | last StrictTypes.VariantName
                       | nthBack (StrictTypes.VariantName, U16)
                       | neg#16 StateSelector
                       | add (StateSelector, StateSelector)
                       | sub (StateSelector, StateSelector)
                       | mul (StateSelector, StateSelector)
                       | div (StateSelector, StateSelector)
                       | rem (StateSelector, StateSelector)
                       | exp (StateSelector, StateSelector)
                       | count#32 StrictTypes.VariantName
                       | countUnique StrictTypes.VariantName
                       | setV StrictTypes.VariantName
                       | mapV2u StrictTypes.VariantName
                       | mapV2ListU StrictTypes.VariantName
                       | mapV2SetU StrictTypes.VariantName
                       | sumUnwrap#48 StrictTypes.VariantName
                       | sumOrDefault StrictTypes.VariantName
                       | prodUnwrap StrictTypes.VariantName
                       | prodOrDefault StrictTypes.VariantName

@mnemonic(weekend-street-channel)
data Transition        : opid UltraSONIC.Opid, destroyed {UltraSONIC.CellAddr -> UltraSONIC.StateCell}