Formal Theory of Applications

-- Asymmetric key agreement
agree   : PrivKey × PubKey → SharedSecret

-- Key derivation
kdf     : SharedSecret × Context → SymKey
derive  : Key × Label → Key

-- Symmetric authenticated encryption
encrypt : SymKey × τ → Cipher
decrypt : SymKey × Cipher → Option τ

-- Digital signatures
sign    : PrivKey × τ → Sig
verify  : PubKey × τ × Sig → Bool

-- Hashing & secret sharing
hash    : τ → Digest
split   : Key × K × N → [Key]
combine : [Key] → Option Key

-- Canonical asymmetric → symmetric path:
symKey = kdf(agree(my_priv, their_pub), context)

agree_sym        : agree(a_priv, B_pub) = agree(b_priv, A_pub)
encrypt_rt       : decrypt(k, encrypt(k, m)) = Some m
hash_cr          : collision resistant (idealized as injective)
derive_oneway    : derive(k, l) does not reveal k
derive_sep       : l ≠ l' → derive(k, l) ≠ derive(k, l')
split_threshold  : |keys| < k → combine keys = None
split_sufficient : |keys| ≥ k → ∃ key, combine keys = Some key
valid_iff        : valid (s,e) now ⟺ s ≤ now ≤ e

Id = Anon                          -- no key, strength 0
   | Hold    Public                -- I have the private half, strength 1
   | Share   Public K              -- I hold one shard, strength 0
   | Attest  Public Sig Nonce      -- I just proved it, strength 2

session : Id → Label → Window → Option Session
session Anon _ _           = None
session (Hold k) label w   = Some (derive(k, label), w)
session (Share k _) label w = Some (derive(k, label), w)
session (Attest k _ _) l w = Some (derive(k, l), w)

Origin = Unsigned
       | Signed    Public Sig
       | Endorsed  (Public, Sig) (Public, Sig, Nat, Time)
       | CoSigned  [(Public, Sig)] K
       | Logged    Digest BundleIndex

-- Endorsed = author signs, endorser co-signs with seq + time
-- Logged   = included in append-only verifiable log

-- Replay protection: commit hash is deterministic replay identifier
-- Verifier checks: time ∈ skew window, hash not previously accepted, seq monotonic

Entry = (τ, Nat, Time, Origin)     -- (data, seq, time, origin)

wellFormed : [Entry] → Bool
wellFormed log = consecutive(seq) ∧ nonDecreasing(time) ∧ allVerified(origin)

consistent : [Entry] → [Entry] → Bool
consistent(l1, l2) = ∃ proof, verify_consistency(root(l1), root(l2), proof) = true
-- l1's CT root is a prefix of l2's CT root

Claim = Has Digest τ | Missing Digest
      | Included Entry Digest | Consistent Digest Digest

Transport  = Direct                    -- 1:1, shared = agree(my, their)
             | Tree Nat                 -- 1:N, secret = root(tree), O(log N) update

Evolution  = Static                    -- key never changes
             | Epoch                    -- key per group change: keyₙ = derive(epoch, seq)
             | Ratchet                  -- key per use, forward only:
                                         -- keyₙ = derive(stateₙ, "use")
                                         -- stateₙ₊₁ = derive(stateₙ, "next"), delete stateₙ

Scheme     = (Transport, Evolution, Option Window, Option Window)
--                                       ↑ TTL          ↑ Rotation

-- Instances:
Plaintext        = (Direct,  Static,  ∅, ∅)
DH_Session       = (Direct,  Epoch,   ∅, ∅)
Ratchet_DM       = (Direct,  Ratchet, ∅, ∅)
Group_Lazy       = (Tree N,  Epoch,   24h, 24h)
Group_Secure     = (Tree N,  Ratchet, ∅, ∅)
Group_Ephemeral  = (Tree N,  Epoch,   1h, 1h)

S = G × L × P × B

G : { id : Id, schema : Schema, ... }   -- global, shared
L : Scope → τ                           -- local, per view
P : String → τ                          -- persisted across sessions
B : Binding → Life                       -- data binding lifecycle

-- Persistence:
get(k, p) : Option τ
set(k, v, p) : P
del(k, p) : P

Life = Idle
     | Pending Time                -- waiting, with deadline
     | Active  τ Time              -- has data, received at
     | Failed  Err Time            -- error, occurred at
     | Stale   τ Time              -- data expired
     | Done    Reason              -- terminated

Reason = Completed | Revoked | Expired | Closed | Timeout | Error Err

-- Transitions:
Idle --> Pending t
Pending t --> Active       (if now <= t)
Pending t --> Failed       (if now > t, MANDATORY -- Theorem 48)
Active --> Stale --> Pending t --> Active
Active | Pending | Failed | Stale --> Done

Storage = {
  ops         : [Op],           -- {Get, Put, Del, Scan, Batch, ...}
  atomicity   : None | Record | Global,
  consistency : Eventual | Strong | Causal,
  provable    : Bool            -- provides inclusion proofs?
}

Op = Read Query | Write Mutation
Query = Select | Get | Scan | List
Mutation = Insert | Put | Del | Batch

Store = {
  storage   : Storage,
  interface : [Interface],      -- REST | GraphQL | WebSocket | Local
  auth      : [Auth],           -- None | Bearer | ApiKey | Sig | OAuth
  protect   : Protection
}

Protection = (Scope, Scheme, Signing)
Scope      = Open | Content | Record | Field (Name → Scope)
Signing    = Unsigned | Signed Key | Multi [Key] K | Chain

Binding = {
  store   : Store,                         -- App satisfies Store
  via     : Interface ∈ store.interface,    -- checked: Theorem 31
  auth    : Auth ∈ store.auth,             -- checked: Theorem 32
  mode    : Pull Query Trigger | Push Query Session,
  parse   : τ → Option τ,
  target  : Path S,
  guard   : Id × Schema → Bool
}

Trigger = Init | Tick Duration | On Event | Change Path
Session = derive(id.key, label) + Window

-- Every datum passes through trust:
-- Inbound:  guard → auth → request → [transport] → verify(origin)
--           → verify(claim)? → decrypt(scheme) → parse → state
-- Outbound: guard → sign → encrypt(scheme) → request → [transport]

Action = Set Path τ            -- set value at path in S
       | Del Path               -- delete value at path
       | Bind Binding Life      -- update binding lifecycle

reduce : S × Action → S
reduce(s, a) = if access(s.id, a, s.schema)
               then apply(s, a)
               else s              -- Theorem 4: Guard

Event = Click | Input | Select | Submit
      | Nav | Scroll | Gesture | Custom String

V = El Tag [Attr] [V] | Text String | Empty

Attr = Class String | On Event Action | Bind Path
     | Prop String τ | If (S → Bool) | Key τ

render : S → V       -- pure, total, no IO

Env = { time : Time }             -- explicit external inputs

Effect = Fetch   Binding Op (τ → Action)  -- read or write store
       | Open    Binding (Life → Action)   -- open push connection
       | Close   Binding                    -- close connection
       | Route   String                     -- navigate
       | Sync    P                          -- persist
       | Batch   [Effect]                   -- parallel
       | None

effect  : S × Action × Env → [Effect]   -- pure
execute : Effect → IO ()                -- impure, outside guarantee

App = (S₀, B, reduce, effect, render)

S₀     : S                          -- initial state
B      : [Binding]                   -- all data bindings
reduce : S × Action → S             -- pure state transition
effect : S × Action × Env → [Effect] -- pure effect description
render : S → V                       -- pure view function

       Inbound                                Outbound
       =======                                ========

                      +-------------------+
 Store --[pull]------>|                   |--[write]--> Store
                      |  access           |
 Store ==[push]======>|  verify           |--[route]--> URL
       (stream)    |  |  prove?           |
                   |  |  decrypt          |--[sync]---> Device
 User --[event]---+-->|  parse            |
                      |  reduce           |
 Key  --[sign]------->|  render           |--[view]---> DOM
                      |  effect           |
                      |                   |
                      |  G x L x P x B    |
                      |      proven       |
                      +-------------------+

      In:  access -> verify -> prove? -> decrypt(scheme) -> parse
      Out: sign -> encrypt(scheme) -> write(origin)

-- Outbound (alice sends):
  1. guard:     access(alice, Chat_Message, schema) -> true (Member, C)
  2. sign:      sig = schnorr(commit_hash, alice_priv)
  3. encrypt:   key = MLS.deriveMessageKey(epochSecret)
                    cipher = encrypt(key, plaintext)
  4. commit:    hash = H(0x10, enclave, alice_pub, "Chat_Message", cipher, exp, tags)
  5. transport: ECDH(signer_priv, seq_pub) + HKDF("enc:query") + XChaCha20

-- Inbound (bob receives via push):
  1. transport: ECDH(seq_priv, bob_signer_pub) + HKDF("enc:push")
  2. verify:    check sig (alice) + seq_sig (node)
  3. decrypt:   MLS.decrypt(epochKey, cipher) -> plaintext
  4. parse:     parse(ChatMessage) -> Some msg
  5. state:     reduce(s, Set L.messages (append msg))

seq=0  Manifest              -> epoch 0 (alice, bob initial members)
seq=1  Grant Member carol    -> MLS.addMember(carol)    -> epoch 1
seq=2  Chat_Message (alice)  -> encrypted with epoch 1 key
seq=3  Revoke Member carol   -> MLS.removeMember(carol) -> epoch 2
seq=4  Chat_Message (bob)    -> encrypted with epoch 2 key
                               carol CANNOT decrypt (forward secrecy)