From e47a37e3f0622e3f4acbb3a9ce984f65666771e9 Mon Sep 17 00:00:00 2001
From: Tony Garnock-Jones <tonyg@leastfixedpoint.com>
Date: Thu, 27 May 2021 10:36:35 +0200
Subject: [PATCH] First steps to an actual novy implementation

---
 .gitignore               |  1 +
 box-protocol.prs         |  9 +++++++++
 dataspace.prs            |  9 +++++++++
 gatekeeper.prs           |  5 +++++
 protocol.prs             | 14 +++++++++++++
 secure-chat-protocol.prs | 14 +++++++++++++
 simple-chat-protocol.prs |  5 +++++
 sturdy.prs               | 43 ++++++++++++++++++++++++++++++++++++++++
 worker.prs               |  4 ++++
 9 files changed, 104 insertions(+)
 create mode 100644 .gitignore
 create mode 100644 box-protocol.prs
 create mode 100644 dataspace.prs
 create mode 100644 gatekeeper.prs
 create mode 100644 protocol.prs
 create mode 100644 secure-chat-protocol.prs
 create mode 100644 simple-chat-protocol.prs
 create mode 100644 sturdy.prs
 create mode 100644 worker.prs

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..e8e450b
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+gen/
diff --git a/box-protocol.prs b/box-protocol.prs
new file mode 100644
index 0000000..d200d54
--- /dev/null
+++ b/box-protocol.prs
@@ -0,0 +1,9 @@
+version 1 .
+embeddedType Actor.Ref .
+
+BoxState = <BoxState @value int>.
+SetBox = <SetBox @value int>.
+
+; BoxCap = BoxState / <Observe =SetBox @observer embedded>.
+; ClientCap = SetBox / <Observe =BoxState @observer embedded>.
+.
diff --git a/dataspace.prs b/dataspace.prs
new file mode 100644
index 0000000..eadbd9a
--- /dev/null
+++ b/dataspace.prs
@@ -0,0 +1,9 @@
+version 1 .
+embeddedType Actor.Ref .
+
+;As implemented
+Observe = <Observe @label symbol @observer embedded>.
+
+; ;As will be implemented soon
+; Observe = <Observe @pattern Pattern @observer embedded>.
+.
diff --git a/gatekeeper.prs b/gatekeeper.prs
new file mode 100644
index 0000000..7673518
--- /dev/null
+++ b/gatekeeper.prs
@@ -0,0 +1,5 @@
+version 1 .
+embeddedType Actor.Ref .
+
+Resolve = <resolve @sturdyref sturdy.SturdyRef @observer embedded>.
+Bind = <bind @oid any @key bytes @target embedded>.
diff --git a/protocol.prs b/protocol.prs
new file mode 100644
index 0000000..1fe9c20
--- /dev/null
+++ b/protocol.prs
@@ -0,0 +1,14 @@
+version 1 .
+embeddedType sturdy.WireRef .
+
+Assertion = any .
+Handle    = int .
+Event     = Assert / Retract / Message / Sync .
+Oid       = int .
+Turn      = [TurnEvent ...].
+TurnEvent = [@oid Oid @event Event].
+
+Assert = <assert @assertion Assertion @handle Handle>.
+Retract = <retract @handle Handle>.
+Message = <message @body Assertion>.
+Sync = <sync @peer embedded>.
diff --git a/secure-chat-protocol.prs b/secure-chat-protocol.prs
new file mode 100644
index 0000000..951e950
--- /dev/null
+++ b/secure-chat-protocol.prs
@@ -0,0 +1,14 @@
+version 1 .
+embeddedType Actor.Ref .
+
+UserId = int .
+
+Join = <joinedUser @uid UserId @handle embedded>.
+
+NickClaim = <claimNick @uid UserId @name string @k embedded>.
+
+UserInfo = <user @uid UserId @name string>.
+
+Says = <says @who UserId @what string>.
+
+NickConflict = <nickConflict>.
diff --git a/simple-chat-protocol.prs b/simple-chat-protocol.prs
new file mode 100644
index 0000000..987c1f4
--- /dev/null
+++ b/simple-chat-protocol.prs
@@ -0,0 +1,5 @@
+version 1 .
+embeddedType Actor.Ref .
+
+Present = <Present @username string>.
+Says = <Says @who string @what string>.
diff --git a/sturdy.prs b/sturdy.prs
new file mode 100644
index 0000000..630f395
--- /dev/null
+++ b/sturdy.prs
@@ -0,0 +1,43 @@
+version 1 .
+
+; Each Attenuation is a stage. The sequence of Attenuations is run RIGHT-TO-LEFT.
+; That is, the newest Attenuations are at the right.
+SturdyRef = <ref @oid any @caveatChain [Attenuation ...] @sig bytes>.
+
+; An individual Attenuation is run RIGHT-TO-LEFT.
+; That is, the newest Caveats are at the right.
+Attenuation = [Caveat ...].
+
+; embodies 1st-party caveats over assertion structure, but nothing else
+; can add 3rd-party caveats and richer predicates later
+Caveat = Rewrite / Alts .
+Rewrite = <rewrite @pattern Pattern @template Template>.
+Alts = <or @alternatives [Rewrite ...]>.
+
+Oid = int .
+WireRef = @mine [0 @oid Oid] / @yours [1 @oid Oid @attenuation Caveat ...].
+
+;---------------------------------------------------------------------------
+
+ConstructorSpec = CRec / CArr / CDict .
+CRec = <rec @label any @arity int>.
+CArr = <arr @arity int>.
+CDict = <dict>.
+
+Lit = <lit @value any>.
+
+Pattern = PDiscard / PAtom / PEmbedded / PBind / PAnd / PNot / Lit / PCompound .
+PDiscard = <_>.
+PAtom = =Boolean / =Float / =Double / =SignedInteger / =String / =ByteString / =Symbol .
+PEmbedded = =Embedded .
+PBind = <bind @name symbol @pattern Pattern>.
+PAnd = <and @patterns [Pattern ...]>.
+PNot = <not @pattern Pattern>.
+PCompound = <compound @ctor ConstructorSpec @members PCompoundMembers>.
+PCompoundMembers = { any: Pattern ...:... }.
+
+Template = TRef / Lit / TCompound .
+TRef = <ref @name symbol>.
+TCompound = <compound @ctor ConstructorSpec @members TCompoundMembers>.
+TCompoundMembers = { any: Template ...:... }.
+
diff --git a/worker.prs b/worker.prs
new file mode 100644
index 0000000..e35abd9
--- /dev/null
+++ b/worker.prs
@@ -0,0 +1,4 @@
+version 1 .
+embeddedType Actor.Ref .
+
+Instance = <Instance @name string @argument any>.