Mukan Erkin Törük
6852832fe8
Some checks failed
CodeQL / Analyze (push) Waiting to run
Docker Build & Push Simapp (main) / docker-build (push) Waiting to run
golangci-lint / lint (push) Waiting to run
Tests / Code Coverage / build (amd64) (push) Waiting to run
Tests / Code Coverage / build (arm64) (push) Waiting to run
Tests / Code Coverage / unit-tests (map[additional-args:-tags="test_e2e" name:e2e path:./e2e]) (push) Waiting to run
Tests / Code Coverage / unit-tests (map[name:08-wasm path:./modules/light-clients/08-wasm]) (push) Waiting to run
Tests / Code Coverage / unit-tests (map[name:ibc-go path:.]) (push) Waiting to run
Deploy to GitHub Pages / Deploy to GitHub Pages (push) Has been cancelled
Buf-Push / push (push) Has been cancelled
50 lines
1.5 KiB
Text
50 lines
1.5 KiB
Text
-------------------------- MODULE denom ----------------------------
|
|
|
|
(**
|
|
The denomination traces interface; please ignore the definition bodies.
|
|
*)
|
|
|
|
EXTENDS identifiers
|
|
|
|
CONSTANT
|
|
Denoms
|
|
|
|
\* A non-account
|
|
NullDenomTrace == "NullDenomTrace"
|
|
|
|
\* All denomination traces
|
|
DenomTraces == {NullDenomTrace}
|
|
|
|
\* Make a new denomination trace from the port/channel prefix and the basic denom
|
|
MakeDenomTrace(port, channel, denom) == NullDenomTrace
|
|
|
|
\* Get the denomination trace port
|
|
GetPort(trace) == NullId
|
|
|
|
\* Get the denomination trace port
|
|
GetChannel(trace) == NullId
|
|
|
|
\* Get the denomination trace basic denomination
|
|
GetDenom(trace) == NullDenomTrace
|
|
|
|
\* Is this denomination trace a native denomination, or is it a prefixed trace
|
|
\* Note that those cases are exclusive, but not exhaustive
|
|
IsNativeDenomTrace(trace) == GetPort(trace) = NullId /\ GetChannel(trace) = NullId
|
|
IsPrefixedDenomTrace(trace) == GetPort(trace) /= NullId /\ GetChannel(trace) /= NullId
|
|
|
|
DenomTypeOK ==
|
|
/\ NullDenomTrace \in DenomTraces
|
|
/\ \A p \in Identifiers, c \in Identifiers, d \in Denoms:
|
|
MakeDenomTrace(p, c, d) \in DenomTraces
|
|
/\ \A t \in DenomTraces:
|
|
/\ GetPort(t) \in Identifiers
|
|
/\ GetChannel(t) \in Identifiers
|
|
/\ GetDenom(t) \in DenomTraces
|
|
|
|
|
|
|
|
|
|
=============================================================================
|
|
\* Modification History
|
|
\* Last modified Thu Nov 05 15:49:23 CET 2020 by andrey
|
|
\* Created Thu Nov 05 13:22:40 CET 2020 by andrey
|