From f86ba2fb3174cf4c84c38a78d5862d3f6e591def Mon Sep 17 00:00:00 2001
From: Edward Amsden <edward@blackriversoft.com>
Date: Wed, 8 Mar 2023 15:43:26 -0600
Subject: [PATCH] [ska] prototypes for initialization

---
 hoon/codegen/lib/ska.hoon | 491 +++++++++++++++++++++++---------------
 hoon/codegen/lib/sky.hoon | 129 ++++++++++
 2 files changed, 433 insertions(+), 187 deletions(-)
 create mode 100644 hoon/codegen/lib/sky.hoon

diff --git a/hoon/codegen/lib/ska.hoon b/hoon/codegen/lib/ska.hoon
index 18ba078..0a99bf1 100644
--- a/hoon/codegen/lib/ska.hoon
+++ b/hoon/codegen/lib/ska.hoon
@@ -1,5 +1,19 @@
 /-  *sock
+!:
 |%
+++  trip
+  |=  toob=$<(%boom boot)
+  ^-  (unit *)
+  ?-  -.toob
+    %safe  (stub sure.toob)
+    %risk  (stub hope.toob)
+  ==
+++  stub
+  |=  =sock
+  ^-  (unit *)
+  ?:  ?=(%know -.sock)
+    `know.sock
+  ~
 :: Split an axis into a sock into safe and unsafe components
 ++  punt
   |=  [axe=@ =sock]
@@ -244,11 +258,11 @@
   ?:  ?&(?=([%know *] a) ?=([%know *] b))
     ?:  =(know.a know.b)
       a
-    $(a (fray a), b (fray b))
+    $(a (fray know.a), b (fray know.b))
   ?:  ?=([%know *] a)
-    $(a (fray a))
+    $(a (fray know.a))
   ?:  ?=([%know *] b)
-    $(b (fray b))
+    $(b (fray know.b))
   ?:  ?&(?=([%bets *] a) ?=([%bets *] b))
     [%bets $(a hed.a, b hed.b) $(a tal.a, b tal.b)]
   ?:  ?&(?=([%dice ~] a) ?|(?=([%dice ~] b) ?=([%flip ~] b)))
@@ -364,209 +378,312 @@
 ++  wash
   |=  [subj=sock form=*]
   ^-  boot
-  =+  ward=(map [sock *] boot)
-  ?+  form  [%boom ~]
-      ::
-      [[* *] *]
-    (cobb $(form -.form) $(form +.form))
-      ::
-      [%0 @]
-    (pull +.form subj)
-      ::
-      [%1 *]
-    [%safe %know +.form]
-      ::
-      [%2 * *]
-    =/  subn  $(form +<.form)
-    ?:  ?=([%boom ~] subn)
-      [%boom ~]
-    =/  forn  $(form +>.form)
-    ?:  ?=([%boom ~] forn)
-      [%boom ~]
-    ?:  ?=  [%safe %dice ~]  forn
-      [%boom ~]
-    ?:  ?=  [%safe %flip ~]  forn
-      [%boom ~]
-    ?:  ?=  [%risk %dice ~]  forn
-      [%boom ~]
-    ?:  ?=  [%risk %flip ~]  forn
-      [%boom ~]
-    ?+  forn  [%risk %toss ~]
+  =|  ward=(map [sock *] boot)
+  =.  ward  (~(put by ward) [subj form] [%risk %toss ~])
+  |^
+    -:swab
+  ++  swab
+    |-
+    ^-  [boot _ward]
+    ?>  ?=(^ form)
+    ?+  form  [[%boom ~] ward]
         ::
-        [%safe %know *]
-      ?-  subn
-          ::
-          [%safe *]
-        $(subj sure.subn, form know.sure.forn)
-          ::
-          [%risk *]
-        (dare $(subj hope.subn, form know.sure.forn))
-      ==
+        [[* *] *]
+      =^  l  ward  $(form -.form)
+      =^  r  ward  $(form +.form)
+      :_  ward
+      (cobb l r)
         ::
-        [%risk %know *]
-      ?-  subn
-          ::
-          [%safe *]
-        (dare $(subj sure.subn, form know.hope.forn))
-          ::
-          [%risk *]
-        (dare $(subj hope.subn, form know.hope.forn))
-      ==
-    ==
-      ::
-      [%3 *]
-    (ques $(form +.form))
-      ::
-      [%4 *]
-    (pile $(form +.form))
-      ::
-      [%5 * *]
-    (bopp $(form +<.form) $(form +>.form))
-      ::
-      [%6 * * *]
-    =/  cond  $(form +<.form)
-    ?+  cond  [%boom ~]
+        [%0 @]
+      :_  ward
+      (pull +.form subj)
         ::
-        [%safe *]
-      ?+  sure.cond  [%boom ~]
-          ::
-          [%know %0]
-        $(form +>-.form)
-          ::
-          [%know %1]
-        $(form +>+.form)
-          ::
-          [%flip ~]
-        (gnaw $(form +>-.form) $(form +>+.form))
-          ::
-          [%dice ~]
-        (dare (gnaw $(form +>-.form) $(form +>+.form)))
-          ::
-          [%toss ~]
-        (dare (gnaw $(form +>-.form) $(form +>+.form)))
-      ==
+        [%1 *]
+      :_  ward
+      [%safe %know +.form]
         ::
-        [%risk *]
-      ?+  hope.cond  [%boom ~]
-          ::
-          [%know %0]
-        (dare $(form +>-.form))
-          ::
-          [%know %1]
-        (dare $(form +>+.form))
-          ::
-          [%flip ~]
-        (dare (gnaw $(form +>-.form) $(form +>+.form)))
-          ::
-          [%dice ~]
-        (dare (gnaw $(form +>-.form) $(form +>+.form)))
-          ::
-          [%toss ~]
-        (dare (gnaw $(form +>-.form) $(form +>+.form)))
-      ==
-    ==
-      ::
-      [%7 * *]
-    =/  news  $(form +<.form)
-    ?+  news  [%boom ~]
-        ::
-        [%safe *]
-      $(subj sure.news, form +>.form)
-        ::
-        [%risk *]
-      (dare $(subj hope.news, form +>.form))
-    ==
-      ::
-      [%8 * *]
-    =/  news  $(form +<.form)
-    ?+  news  [%boom ~]
-        ::
-        [%safe *]
-      $(subj (knit sure.news subj), form +>.form)
-        ::
-        [%risk *]
-      (dare $(subj (knit hope.news subj), form +>.form))
-    ==
-      ::
-      [%9 @ *]
-    =/  news  $(form +>.form)
-    ?+  news  [%boom ~]
-        ::
-        [%safe *]
-      =/  newf  (pull +<.form sure.news)
-      ?+  newf  [%boom ~]
+        [%2 * *]
+      =^  subn  ward  $(form +<.form)
+      ?:  ?=([%boom ~] subn)
+        [[%boom ~] ward]
+      =^  forn  ward  $(form +>.form)
+      ?:  ?=([%boom ~] forn)
+        [[%boom ~] ward]
+      ?:  ?=  [%safe %dice ~]  forn
+        [[%boom ~] ward]
+      ?:  ?=  [%safe %flip ~]  forn
+        [[%boom ~] ward]
+      ?:  ?=  [%risk %dice ~]  forn
+        [[%boom ~] ward]
+      ?:  ?=  [%risk %flip ~]  forn
+        [[%boom ~] ward]
+      ?+  forn  [[%risk %toss ~] ward]
           ::
           [%safe %know *]
-        $(subj sure.news, form know.sure.newf)
+        ?-  subn
+            ::
+            [%safe *]
+          =/  nubs  sure.subn
+          =/  norm  know.sure.forn
+          =/  mem  (~(get by ward) [nubs norm])
+          ?.  ?=(~ mem)  [u.mem ward]
+          =.  ward  (~(put by ward) [nubs norm] [%risk %toss ~])
+          =^  r  ward  $(subj nubs, form norm)
+          [r (~(put by ward) [nubs norm] r)]
+            ::
+            [%risk *]
+          =/  nubs  hope.subn
+          =/  norm  know.sure.forn
+          =/  mem  (~(get by ward) [nubs norm])
+          ?.  ?=(~ mem)  [u.mem ward]
+          =.  ward  (~(put by ward) [nubs norm] [%risk %toss ~])
+          =^  r  ward  $(subj nubs, form norm)
+          [(dare r) (~(put by ward) [nubs norm] (dare r))]
+        ==
           ::
           [%risk %know *]
-        (dare $(subj sure.news, form know.hope.newf))
-          ::
-          [%safe *]
-        [%risk %toss ~]
-          ::
-          [%risk *]
-        [%risk %toss ~]
+        ?-  subn
+            ::
+            [%safe *]
+          =/  nubs  sure.subn
+          =/  norm  know.hope.forn
+          =/  mem  (~(get by ward) [nubs norm])
+          ?.  ?=(~ mem)  [u.mem ward]
+          =.  ward  (~(put by ward) [nubs norm] [%risk %toss ~])
+          =^  r  ward  $(subj nubs, form norm)
+          [(dare r) (~(put by ward) [nubs norm] (dare r))]
+            ::
+            [%risk *]
+          =/  nubs  hope.subn
+          =/  norm  know.hope.forn
+          =/  mem  (~(get by ward) [nubs norm])
+          ?.  ?=(~ mem)  [u.mem ward]
+          =.  ward  (~(put by ward) [nubs norm] [%risk %toss ~])
+          =^  r  ward  $(subj nubs, form norm)
+          [(dare r) (~(put by ward) [nubs norm] (dare r))]
+        ==
       ==
         ::
-        [%risk *]
-      =/  newf  (pull +<.form hope.news)
-      ?+  newf  [%boom ~]
-          ::
-          [%safe %know *]
-        (dare $(subj hope.news, form know.sure.newf))
-          ::
-          [%risk %know *]
-        (dare $(subj hope.news, form know.hope.newf))
+        [%3 *]
+      =^  s  ward  $(form +.form)
+      :_  ward
+      (ques s)
+        ::
+        [%4 *]
+      =^  s  ward  $(form +.form)
+      :_  ward
+      (pile s)
+        ::
+        [%5 * *]
+      =^  l  ward  $(form +<.form)
+      =^  r  ward  $(form +>.form)
+      :_  ward
+      (bopp l r)
+        ::
+        [%6 * * *]
+      =^  cond  ward  $(form +<.form)
+      ?+  cond  [[%boom ~] ward]
           ::
           [%safe *]
-        [%risk %toss ~]
+        ?+  sure.cond  [[%boom ~] ward]
+            ::
+            [%know %0]
+          $(form +>-.form)
+            ::
+            [%know %1]
+          $(form +>+.form)
+            ::
+            [%flip ~]
+          =^  t  ward  $(form +>-.form)
+          =^  f  ward  $(form +>+.form)
+          :_  ward
+          (gnaw t f)
+            ::
+            [%dice ~]
+          =^  t  ward  $(form +>-.form)
+          =^  f  ward  $(form +>+.form)
+          :_  ward
+          (dare (gnaw t f))
+            ::
+            [%toss ~]
+          =^  t  ward  $(form +>-.form)
+          =^  f  ward  $(form +>+.form)
+          :_  ward
+          (dare (gnaw t f))
+        ==
           ::
           [%risk *]
-        [%risk %toss ~]
+        ?+  hope.cond  [[%boom ~] ward]
+            ::
+            [%know %0]
+          =^  t  ward  $(form +>-.form)
+          :_  ward
+          (dare t)
+            ::
+            [%know %1]
+          =^  f  ward  $(form +>+.form)
+          :_  ward
+          (dare f)
+            ::
+            [%flip ~]
+          =^  t  ward  $(form +>-.form)
+          =^  f  ward  $(form +>+.form)
+          :_  ward
+          (dare (gnaw t f))
+            ::
+            [%dice ~]
+          =^  t  ward  $(form +>-.form)
+          =^  f  ward  $(form +>+.form)
+          :_  ward
+          (dare (gnaw t f))
+            ::
+            [%toss ~]
+          =^  t  ward  $(form +>-.form)
+          =^  f  ward  $(form +>+.form)
+          :_  ward
+          (dare (gnaw t f))
+        ==
       ==
-    ==
-      ::
-      [%10 [@ *] *]
-    (welt +<-.form $(form +<+.form) $(form +>.form))
-      ::
-      [%11 @ *]
-    $(form +>.form)
-      ::
-      [%11 [* *] *]
-    =/  hint  $(form +<+.form)
-    ?+  hint  [%boom ~]
         ::
-        [%safe *]
+        [%7 * *]
+      =^  news  ward  $(form +<.form)
+      ?+  news  [[%boom ~] ward]
+          ::
+          [%safe *]
+        $(subj sure.news, form +>.form)
+          ::
+          [%risk *]
+        =^  r  ward  $(subj hope.news, form +>.form)
+        :_  ward
+        (dare r)
+      ==
+        ::
+        [%8 * *]
+      =^  news  ward  $(form +<.form)
+      ?+  news  [[%boom ~] ward]
+          ::
+          [%safe *]
+        $(subj (knit sure.news subj), form +>.form)
+          ::
+          [%risk *]
+        =^  r  ward  $(subj (knit hope.news subj), form +>.form)
+        :_  ward
+        (dare r)
+      ==
+        ::
+        [%9 @ *]
+      =^  news  ward  $(form +>.form)
+      ?+  news  [[%boom ~] ward]
+          ::
+          [%safe *]
+        =/  newf  (pull +<.form sure.news)
+        ?+  newf  [[%boom ~] ward]
+            ::
+            [%safe %know *]
+          =/  nubs  sure.news
+          =/  norm  know.sure.newf
+          =/  mem  (~(get by ward) [nubs norm])
+          ?.  ?=(~ mem)  [u.mem ward]
+          =.  ward  (~(put by ward) [nubs norm] [%risk %toss ~])
+          =^  r  ward  $(subj nubs, form norm)
+          :_  (~(put by ward) [nubs norm] r)
+          r
+            ::
+            [%risk %know *]
+          =/  nubs  sure.news
+          =/  norm  know.hope.newf
+          =/  mem  (~(get by ward) [nubs norm])
+          ?.  ?=(~ mem)  [u.mem ward]
+          =.  ward  (~(put by ward) [nubs norm] [%risk %toss ~])
+          =^  r  ward  $(subj nubs, form norm)
+          :_  (~(put by ward) [nubs norm] (dare r))
+          (dare r)
+            ::
+            [%safe *]
+          [[%risk %toss ~] ward]
+            ::
+            [%risk *]
+          [[%risk %toss ~] ward]
+        ==
+          ::
+          [%risk *]
+        =/  newf  (pull +<.form hope.news)
+        ?+  newf  [[%boom ~] ward]
+            ::
+            [%safe %know *]
+          =/  nubs  hope.news
+          =/  norm  know.sure.newf
+          =/  mem  (~(get by ward) [nubs norm])
+          ?.  ?=(~ mem)  [u.mem ward]
+          =.  ward  (~(put by ward) [nubs norm] [%risk %toss ~])
+          =^  r  ward  $(subj nubs, form norm)
+          :_  (~(put by ward) [nubs norm] (dare r))
+          (dare r)
+            ::
+            [%risk %know *]
+          =/  nubs  hope.news
+          =/  norm  know.hope.newf
+          =/  mem  (~(get by ward) [nubs norm])
+          ?.  ?=(~ mem)  [u.mem ward]
+          =.  ward  (~(put by ward) [nubs norm] [%risk %toss ~])
+          =^  r  ward  $(subj nubs, form norm)
+          :_  (~(put by ward) [nubs norm] (dare r))
+          (dare r)
+            ::
+            [%safe *]
+          [[%risk %toss ~] ward]
+            ::
+            [%risk *]
+          [[%risk %toss ~] ward]
+        ==
+      ==
+        ::
+        [%10 [@ *] *]
+      =^  p  ward  $(form +<+.form)
+      =^  w  ward  $(form +>.form)
+      :_  ward
+      (welt +<-.form p w)
+        ::
+        [%11 @ *]
       $(form +>.form)
         ::
-        [%risk *]
-      (dare $(form +>.form))
+        [%11 [* *] *]
+      =^  hint  ward  $(form +<+.form)
+      ?+  hint  [[%boom ~] ward]
+          ::
+          [%safe *]
+        $(form +>.form)
+          ::
+          [%risk *]
+        =^  r  ward  $(form +<.form)
+        :_  ward
+        (dare r)
+      ==
+        ::
+        [%12 *]
+      [[%risk %toss ~] ward]
     ==
+  --
+++  cuff
+  |=  =sock
+  =/  axe  1
+  |-
+  ^-  (list @)
+  ?-  sock
       ::
-      [%12 *]
-    [%risk %toss ~]
+      [%know *]
+    (limo [axe ~])
+      ::
+      [%bets *]
+    (weld $(axe (add axe axe), sock hed.sock) $(axe (add (add axe axe) 1), sock tal.sock))
+      ::
+      [%dice ~]
+    (limo [axe ~])
+      ::
+      [%flip ~]
+    (limo [axe ~])
+      ::
+      [%toss ~]
+    (limo [axe ~])
   ==
-  ++  cuff
-    |=  =sock
-    =/  axe  1
-    |-
-    ^-  (list @)
-    ?-  sock
-        ::
-        [%know *]
-      (limo [axe ~])
-        ::
-        [%bets *]
-      (weld $(axe (add axe axe), sock hed.sock) $(axe (add (add axe axe) 1), sock tal.sock))
-        ::
-        [%dice ~]
-      (limo [axe ~])
-        ::
-        [%flip ~]
-      (limo [axe ~])
-        ::
-        [%toss ~]
-      (limo [axe ~])
-    ==
 --
diff --git a/hoon/codegen/lib/sky.hoon b/hoon/codegen/lib/sky.hoon
new file mode 100644
index 0000000..617c231
--- /dev/null
+++ b/hoon/codegen/lib/sky.hoon
@@ -0,0 +1,129 @@
+/-  *sock
+/+  ska
+|%
+:: mask axes in a noun to make a sock
+++  dope
+  |=  [mask=(list @) non=noun]
+  ^-  boot
+  =/  sack=boot  [%safe %know non]
+  |-
+  ^-  boot
+  ?~  mask  sack
+  $(sack (welt:ska i.mask [%safe %toss ~] sack), mask t.mask)
+:: turn a hoon type into a boot
+++  wove
+  |=  kine=type
+  ^-  boot
+  ?@  kine
+    ?-  kine
+      %noun  [%risk %toss ~]
+      %void  [%boom ~]
+    ==
+  ?-  -.kine
+      %atom
+    ?~  q.kine
+      [%risk %dice ~]
+    [%risk %know u.q.kine]
+  ::
+      %cell
+    (cobb:ska $(kine p.kine) $(kine q.kine))
+  ::
+      %core
+    %+  cobb:ska
+      (spry p.r.q.kine) :: compiled battery
+    $(kine p.kine) :: current payload
+  ::
+      %face
+    $(kine q.kine)
+  ::
+      %fork
+    =/  tins  ~(tap in p.kine)
+    ?~  tins  [%risk %toss ~]
+    =/  hypo  $(kine i.tins)
+    =/  tons  t.tins
+    |-
+    ^-  boot
+    ?~  tons  hypo
+    $(hypo (gnaw:ska ^$(kine i.tons) hypo))
+  ::
+      %hint
+    $(kine q.kine)
+  ::
+      %hold
+    $(kine p.kine)
+  ==
+:: turn a seminoun into a sock
+++  spry
+  |=  seminoun
+  ^-  boot
+  ?-  -.mask
+      %half
+    ?>  ?=(^ data)
+    (cobb:ska $(mask left.mask, data -.data) $(mask rite.mask, data +.data))
+  ::
+      %full
+    ?~  blocks.mask
+      [%risk %know data]
+    [%risk %toss ~]
+  ::
+      %lazy
+    [%risk %toss ~]
+  ==
+::  for a stateful core, figure out what we can assume across all state
+::  transitions
+::  
+::  step is a list of arm axes and result axes which are expected to produce gates
+::  the gates will be simul-slammed with %toss
+::  then the result axis will be intersected with the stateful core
+::  knowledge
+::  
+::  fixed point termination argument: we can only know the same or less
+::  than what we knew last time (intersection cannot add knowledge)
+::  if we know the same, we stop now. We can only subtract finitely many
+::  axes of knowledge from the tree before we know [%boom ~] or
+::  [%risk %gues ~] at which point we will learn the same thing twice
+::  and terminate
+++  arid
+  |=  [muck=boot step=(list [@ @])]
+  ^-  boot
+  =/  yuck  muck
+  =/  stop  step
+  ?:  ?=(%boom -.muck)
+    [%boom ~]
+  |-
+  ^-  boot
+  ?~  stop
+    ?:  =(yuck muck)
+      yuck
+    ^$(muck yuck)
+  =/  erm  (yank:ska -.i.stop muck)
+  ?:  ?=(%boom -.erm)
+    $(stop t.stop, yuck (gnaw:ska [%boom ~] yuck))
+  =/  arm  (trip:ska erm)
+  ?~  arm
+    $(stop t.stop, yuck (gnaw:ska [%risk %toss ~] yuck))
+  =/  cor
+    ?-  -.muck
+      %safe  sure.muck
+      %risk  hope.muck
+    ==
+  =/  mat  (wash:ska cor u.arm)
+  ?:  ?=(%boom -.mat)
+    $(stop t.stop, yuck (gnaw:ska [%boom ~] yuck))
+  =/  ear  (yank:ska 2 mat)
+  ?:  ?=(%boom -.ear)
+    $(stop t.stop, yuck (gnaw:ska [%boom ~] yuck))
+  =/  gar  (trip:ska ear)
+  ?~  gar
+    $(stop t.stop, yuck (gnaw:ska [%risk %toss ~] yuck))
+  =/  mar  (welt:ska 6 [%risk %toss ~] mat)
+  ?:  ?=(%boom -.mar)
+    $(stop t.stop, yuck (gnaw:ska [%boom ~] yuck))
+  =/  gor
+    ?-  -.mar
+      %safe  sure.mar
+      %risk  hope.mar
+    ==
+  =/  beg  (wash:ska gor u.gar)
+  $(stop t.stop, yuck (gnaw:ska (yank:ska +.i.stop beg) yuck))
+--