Locality WIP and notes

frontend/src/Language/Granule/Checker/Constraints.hs

@@ -246,6 +246,11 @@ freshSolverVarScoped quant name (TyCon conName) q k =
                     .|| solverVar .== literal publicRepresentation
                     .|| solverVar .== literal unusedRepresentation
                       , SLevel solverVar)
+          "Locality" -> k (solverVar .== literal arbitraryRep
+                      .|| solverVar .== literal globalRep
+                      .|| solverVar .== literal localRep
+                      .|| solverVar .== literal unusedRep
+                        , SLocality solverVar)
           "LNL"    -> k (solverVar .== literal zeroRep
                     .|| solverVar .== literal oneRep
                     .|| solverVar .== literal manyRep
@@ -408,6 +413,15 @@ compileCoeffect (TyCon name) (TyCon (internalName -> "Level")) _ = do
 
   return (SLevel . fromInteger . toInteger $ n, sTrue)
 
+compileCoeffect (TyCon name) (TyCon (internalName -> "Locality")) _ = do
+  let n = case internalName name of
+            "Arb"    -> arbitraryRep
+            "Global" -> globalRep
+            "Local"  -> localRep
+            c        -> error $ "Cannot compile " <> show c
+
+  return (SLocality . fromInteger . toInteger $ n, sTrue)
+
 compileCoeffect (TyCon name) (TyCon (internalName -> "LNL")) _ = do
   let n = case internalName name of
             "Zero"    -> zeroRep
@@ -533,6 +547,7 @@ compileCoeffect (TyGrade k' 0) k vars = do
     (TyCon k') ->
       case internalName k' of
         "Level"     -> return (SLevel (literal unusedRepresentation), sTrue)
+        "Locality"  -> return (SLocality (literal unusedRep), sTrue) -- ???
         "Sec"       -> return (SSec hiRepresentation, sTrue)
         "Nat"       -> return (SNat 0, sTrue)
         "Q"         -> return (SFloat (fromRational 0), sTrue)
@@ -572,6 +587,7 @@ compileCoeffect (TyGrade k' 1) k vars = do
     TyCon k ->
       case internalName k of
         "Level"     -> return (SLevel (literal privateRepresentation), sTrue)
+        "Locality"  -> return (SLocality (literal localRep), sTrue) -- ???
         "Sec"       -> return (SSec loRepresentation, sTrue)
         "Nat"       -> return (SNat 1, sTrue)
         "Q"         -> return (SFloat (fromRational 1), sTrue)
@@ -634,6 +650,7 @@ eqConstraint :: SGrade -> SGrade -> Symbolic SBool
 eqConstraint (SNat n) (SNat m)     = return $ n .== m
 eqConstraint (SFloat n) (SFloat m) = return $ n .== m
 eqConstraint (SLevel l) (SLevel k) = return $ l .== k
+eqConstraint (SLocality s) (SLocality t) = return $ s .== t
 eqConstraint u@(SUnknown{}) u'@(SUnknown{}) = symGradeEq u u'
 eqConstraint (SExtNat x) (SExtNat y) = return $ x .== y
 eqConstraint SPoint SPoint           = return sTrue
@@ -683,6 +700,15 @@ approximatedByOrEqualConstraint (SLevel l) (SLevel k) =
   --        $ ite (l .== literal privateRepresentation) sTrue
   --        $ ite (k .== literal publicRepresentation) sTrue sFalse
 
+-- TODO: ???
+approximatedByOrEqualConstraint (SLocality l) (SLocality k) =
+  return $ ltCase localRep  globalRep
+         $ ltCase localRep  arbitraryRep
+         $ ltCase globalRep arbitraryRep
+         $ ite (l .== k) sTrue
+         sFalse
+  where ltCase a b = ite ((l .== literal a) .&& (k .== literal b)) sTrue
+
 approximatedByOrEqualConstraint (SSec a) (SSec b) =
   -- Lo <= Lo   (False <= False)
   -- Hi <= Hi   (True <= True)

frontend/src/Language/Granule/Checker/Constraints/SymbolicGrades.hs

@@ -29,6 +29,7 @@ data SGrade =
      | SFraction { sFraction :: SFrac }
      | SFloat    SFloat
      | SLevel    SInteger
+     | SLocality SInteger
      | SSec      SBool -- Hi = True, Lo = False
      | SSet      Polarity (SSet SSetElem)
      | SExtNat   { sExtNat :: SNatX }
@@ -61,6 +62,12 @@ publicRepresentation  = 3
 unusedRepresentation  = 0
 dunnoRepresentation   = 2
 
+localRep, globalRep, arbitraryRep, unusedRep :: Integer
+localRep     = 0
+globalRep    = 1
+arbitraryRep = 2
+unusedRep    = 3
+
 -- Representation for `Sec`
 hiRepresentation, loRepresentation :: SBool
 hiRepresentation = sTrue
@@ -139,6 +146,7 @@ match (SNat _) (SNat _) = True
 match (SFloat _) (SFloat _) = True
 match (SFraction _) (SFraction _) = True
 match (SLevel _) (SLevel _) = True
+match (SLocality _) (SLocality _) = True
 match (SSet p _) (SSet p' _) | p == p' = True
 match (SExtNat _) (SExtNat _) = True
 match (SInterval s1 s2) (SInterval t1 t2) = match s1 t1 && match s2 t2
@@ -189,6 +197,7 @@ instance Mergeable SGrade where
   symbolicMerge s sb (SFloat n) (SFloat n') = SFloat (symbolicMerge s sb n n')
   symbolicMerge s sb (SFraction f) (SFraction f') = SFraction (symbolicMerge s sb f f')
   symbolicMerge s sb (SLevel n) (SLevel n') = SLevel (symbolicMerge s sb n n')
+  symbolicMerge s sb (SLocality n) (SLocality n') = SLocality (symbolicMerge s sb n n')
   symbolicMerge s sb (SSet _ n) (SSet _ n') = error "Can't symbolic merge sets yet"
   symbolicMerge s sb (SExtNat n) (SExtNat n') = SExtNat (symbolicMerge s sb n n')
   symbolicMerge s sb (SInterval lb1 ub1) (SInterval lb2 ub2) =
@@ -228,6 +237,13 @@ symGradeLess (SLevel n) (SLevel n') =
          $ ite (n .== n') sTrue                               -- Refl
          sFalse
   where ltCase a b = ite ((n .== literal a) .&& (n' .== literal b)) sTrue
+
+symGradeLess (SLocality l) (SLocality k) =
+    return $ ltCase globalRep  localRep -- ???
+           sFalse
+    where ltCase a b = ite ((l .== literal a) .&& (k .== literal b)) sTrue
+
+
 symGradeLess (SSet _ n) (SSet _ n')  = solverError "Can't do < on sets"
 symGradeLess (SExtNat n) (SExtNat n') = return $ n .< n'
 symGradeLess SPoint SPoint            = return sTrue
@@ -276,6 +292,7 @@ symGradeEq (SFloat n) (SFloat n') = return $ n .== n'
 symGradeEq (SFraction f) (SFraction f') = return $ f .== f'
 
 symGradeEq (SLevel n) (SLevel n') = return $ n .== n'
+symGradeEq (SLocality n) (SLocality n') = return $ n .== n'
 symGradeEq (SSet p n) (SSet p' n') | p == p' = return $ n .== n'
 
 symGradeEq (SExtNat n@(SNatX ni)) (SNat n') =
@@ -319,6 +336,9 @@ symGradeMeet (SLevel s) (SLevel t) =
                         (s .== literal dunnoRepresentation))     -- join x Dunno = Dunno
                         (literal dunnoRepresentation)
                   $ literal publicRepresentation -- join Public Public = Public
+
+symGradeMeet (SLocality s) (SLocality t) = solverError "TODO"
+
 symGradeMeet (SFloat n1) (SFloat n2) = return $ SFloat $ n1 `smin` n2
 symGradeMeet (SFraction f) (SFraction f') = return $ SFraction $
   ite (isUniq f) f' (ite (isUniq f') f (SFrac (fVal f `smin` fVal f')))
@@ -357,6 +377,7 @@ symGradeJoin (SLevel s) (SLevel t) =
                         (s .== literal privateRepresentation))
                         (literal privateRepresentation)
                   $ literal dunnoRepresentation -- meet Dunno Private = meet Private Dunno = meet Dunno Dunno = Dunno
+symGradeJoin (SLocality s) (SLocality t) = solverError "TODO"
 symGradeJoin (SFloat n1) (SFloat n2) = return $ SFloat (n1 `smax` n2)
 symGradeJoin (SFraction f) (SFraction f') = return $ SFraction $
   ite (isUniq f .|| isUniq f') star (SFrac (fVal f `smax` fVal f'))
@@ -398,6 +419,18 @@ symGradePlus (SNat n1) (SNat n2) = return $ SNat (n1 + n2)
 symGradePlus (SSet Normal s) (SSet Normal t) = return $ SSet Normal $ S.intersection s t
 symGradePlus (SSet Opposite s) (SSet Opposite t) = return $ SSet Opposite $ S.union s t
 symGradePlus (SLevel lev1) (SLevel lev2) = symGradeJoin (SLevel lev1) (SLevel lev2)
+symGradePlus (SLocality s) (SLocality t) =
+    return $ SLocality
+        $ ite (s .== literal unusedRep) t                           -- Unused + y      = y
+        $ ite (t .== literal unusedRep) s                           -- y      + Unused = y
+        $ ite ((s .== literal localRep) .&&                         -- Local
+                (t .== literal localRep)) (literal localRep)        --        + Local  = Local
+        $ ite (s .== literal arbitraryRep) (literal arbitraryRep)   -- Arb    + y      = Arb
+        $ ite (t .== literal arbitraryRep) (literal arbitraryRep)   -- y      + Arb    = Arb
+        $ ite (s .== literal globalRep) (literal globalRep)         -- Global + y      = Global
+        $ ite (t .== literal globalRep) (literal globalRep)         -- y      + Global = Global
+        $ literal unusedRep                                         -- ?      + ?      = ?
+
 symGradePlus (SFloat n1) (SFloat n2) = return $ SFloat $ n1 + n2
 symGradePlus (SFraction f) (SFraction f') = return $ SFraction (f + f')
 symGradePlus (SExtNat x) (SExtNat y) = return $ SExtNat (x + y)
@@ -448,6 +481,18 @@ symGradeTimes (SExtNat (SNatX n1)) (SNat n2) = return $ SExtNat $ SNatX (n1 * n2
 symGradeTimes (SSet Normal s) (SSet Normal t) = return $ SSet Normal $ S.union s t
 symGradeTimes (SSet Opposite s) (SSet Opposite t) = return $ SSet Opposite $ S.intersection s t
 symGradeTimes (SLevel lev1) (SLevel lev2) = symGradeJoin (SLevel lev1) (SLevel lev2)
+symGradeTimes (SLocality s) (SLocality t) =
+    return $ SLocality
+        $ ite (s .== literal unusedRep) (literal unusedRep)       -- Unused * y      = Unused
+        $ ite (t .== literal unusedRep) (literal unusedRep)       -- y      * Unused = Unused
+        $ ite ((s .== literal localRep) .&&                       -- Local
+                (t .== literal localRep)) (literal localRep)      --        * Local  = Local
+        $ ite (s .== literal arbitraryRep) (literal arbitraryRep) -- Arb    * y      = Arb
+        $ ite (t .== literal arbitraryRep) (literal arbitraryRep) -- y      * Arb    = Arb
+        $ ite (s .== literal globalRep) (literal globalRep)       -- Global * y      = Global
+        $ ite (t .== literal globalRep) (literal globalRep)       -- y      * Global = Global
+        $ literal unusedRep                                       -- ?      * ?      = ?
+
 symGradeTimes (SFloat n1) (SFloat n2) = return $ SFloat $ n1 * n2
 symGradeTimes (SFraction f) (SFraction f') = return $ SFraction (f * f')
 symGradeTimes (SExtNat x) (SExtNat y) = return $ SExtNat (x * y)

frontend/src/Language/Granule/Checker/Primitives.hs

@@ -112,6 +112,11 @@ typeConstructors =
     , (mkId "Sec",  (kcoeffect, [], []))
     , (mkId "Hi",    (tyCon "Sec", [], []))
     , (mkId "Lo",    (tyCon "Sec", [], []))
+    -- Locality
+    , (mkId "Locality", (kcoeffect, [], []))
+    , (mkId "Arb", (tyCon "Locality", [], []))
+    , (mkId "Local", (tyCon "Locality", [], []))
+    , (mkId "Global", (tyCon "Locality", [], []))
     -- Uniqueness
     , (mkId "Uniqueness", (kguarantee, [], []))
     , (mkId "Unique", (tyCon "Uniqueness", [], []))

work-in-progress/locality/examples.gr

@@ -0,0 +1,63 @@
+g2g : Int [Global] -> Int [Global]
+g2g x = x
+
+g2l : Int [Global] -> Int [Local]
+g2l x = x
+
+l2l : Int [Local] -> Int [Local]
+l2l x = x
+
+a2l : Int [Arb] -> Int [Local]
+a2l x = x
+
+a2g : Int [Arb] -> Int [Global]
+a2g x = x
+
+-- this should be okay
+fine1 : forall {a : Type} . a [Global] -> a [Global]
+fine1 [x] = [x]
+
+-- bad1 : forall {a : Type} . a [Local] -> a [Global]
+-- bad1 [x] = [x]
+
+-- Disallowed by Agda
+--
+--    ---------------------- :: var
+--    x : Local a |- x : a
+--    --------------------- :: box_i
+--    x : Local a |- [x] : a [Local]
+--    ---------------------- :: box_i
+--    x : Global x |- [[x]] : a [Global]
+
+-- bad2 : forall {a : Type} . a [Local] -> (a [Local]) [Global]
+-- bad2 [x] = [[x]]
+
+local : Int [Local]
+local = [42]
+
+bad3 : ∀ {a : Type} . a [Local] -> (a, a [Global])
+bad3 [x] = (x, [x])
+
+main : (Int, Int [Global])
+main = bad3 local
+
+
+-- these should be ok
+
+-- (+') : Int [Local] -> Int [Local] -> Int
+-- (+') : Int [Arb] -> Int [Arb] -> Int [Global]
+
+-- BUILTIN
+-- moveToHeap : forall (a : Type) . a -> a [Global]
+
+-- these are not ok!
+
+-- l2g : Int [Local] -> Int [Global]
+-- l2g x = x
+
+-- l2a : Int [Local] -> Int [Arb]
+-- l2a x = x
+
+-- -- this is fine on Jane Street
+-- g2a : Int [Global] -> Int [Arb]
+-- g2a x = x

work-in-progress/locality/examples.ml

@@ -0,0 +1,19 @@
+let g2g : string @ global -> string @ global = fun x -> x
+
+let g2l : string @ global -> string @ local = fun x -> x
+
+let l2l : string @ local -> string @ local = fun x -> x
+
+let a2l : string -> string @ local = fun x -> x
+
+let a2g : string -> string @ global = fun x -> x
+
+(* not ok
+let l2g : 'a @ local -> 'a @ global = fun x -> x 
+  *)
+
+(* not ok
+let l2a : string @ local -> string = fun x -> x 
+  *)
+
+let g2a : string @ global -> string = fun x -> x

work-in-progress/locality/notes.md

@@ -0,0 +1,79 @@
+WIP notes
+
+## Desired behaviour
+
+Simple lifetimes, save on GC
+
+- Local values are not heap allocated (safely!)
+  - call stack? "locals stack" - locals need to survive across call frames
+- Global values are heap allocated
+- Global is default
+
+In JSOCaml:
+
+- a Global can be used in Local context (G < L)
+- a Local cannot escape it's "region" (?? function body / scope / loop body / ref)
+- a local parameter is a promise that the function will not escape the parameter
+- a local return is a promise that the caller will not escape the return
+- quirks?
+  - utility to end regions early, "exclave"
+  - tail positions special treatment, e.g. ret `drop local` not ok but ret `drop local ; ()` ok
+
+## Notes
+
+Need examples of what is and is not fine
+
+Needs rules for safety
+
+Will require annotating builtins especially mutable refs
+
+Extension for promotions?
+
+Locals need to live beyond their stack frame
+
+Fine-grained lifetimes e.g. this local can live 0..2 call frames - nonsense?
+
+In JS Locality is combined with Uniqueness/Affinity for borrows
+
+Some behavioural similarity here with Private / Public - i.e. private does not escape to public context, public can be used in private
+
+Should we drop Arb? Do we need it? Global as default. For formalisation do we need Unused as in Locality1?
+
+ok: (a : Global, b : Global) : Local
+notok: (a : Local, b : Local) : Global
+
+why is this useful?
+
+- intensive computations without GC pause
+- non-leaky (withFile : io -> path -> (handle : Local -> a) -> a)
+
+how much of the desired behaviour could we achieve with linearity/reuse bounds + uniqueness?
+
+## Locality2
+
+This is the implementation in frontend, expected behaviour in simple cases (see examples) - order is reverse of what I expect and not clear on route to formalisation - 0 is Local and 1 is Arb.
+
+Local < Global < Arb
+
+meet Local x = Local
+meet x Local = Local
+meet Global x = Global
+meet x Global = Global
+meet Arb Arb = Arb
+
+join Arb x = Arb
+join x Arb = Arb
+join Global x = Global
+join x Global = Global
+join Local Local = Local
+
+plus = join (?)
+times = meet (?)
+
+## Resources
+
+[Oxidizing OCaml with Modal Memory Management](https://dl.acm.org/doi/pdf/10.1145/3674642) (JS)
+
+[LocalGlobal.agda](https://github.com/granule-project/security-coeffects-mechanization/blob/4c0ae9ed41da2ede42e02f7baaa1cbfef78d9814/LocalGlobal.agda) (Locality1)
+
+[OCaml with Jane Street extensions](https://github.com/janestreet/opam-repository/tree/with-extensions) (JSOCaml)