Proposal for a library for defining packed records

src/Solcore/Backend/Specialise.hs

@@ -355,8 +355,6 @@ specCall i args ty = do
   let name = idName i'
   let argTypes = map typeOfTcExp args
   argTypes' <- atCurrentSubst argTypes
-  let typedArgs = zip args argTypes'
-  args' <- forM typedArgs (uncurry specExp)
   let funType = foldr (:->) ty' argTypes'
   debug ["> specCall: ", show name, " : ", pretty funType]
   mres <- lookupResolution name funType
@@ -376,6 +374,9 @@ specCall i args ty = do
             "\n  This often occurs when a polymorphic-return function (e.g. `require`)",
             "\n  is passed directly to a polymorphic-argument function (e.g. `void`)."
           ]
+      let argTypesForArgs = map (applytv phi) argTypes'
+      let typedArgs = zip args argTypesForArgs
+      args' <- forM typedArgs (uncurry specExp)
       extSpSubst phi
       subst <- getSpSubst
       let ty'' = applytv subst fty
@@ -385,6 +386,8 @@ specCall i args ty = do
       args'' <- atCurrentSubst args'
       return (Id name' ty'', args'')
     Nothing -> do
+      let typedArgs = zip args argTypes'
+      args' <- forM typedArgs (uncurry specExp)
       void $ panics ["! specCall: no resolution found for ", show name, " : ", pretty funType]
       return (i, args')
 
@@ -498,11 +501,19 @@ specStmt stmt@(Let i mty mexp) = do
   debug ["> specStmt (Let): ", pretty i, " : ", pretty (idType i), " @ ", pretty subst]
   i' <- atCurrentSubst i
   let ty' = idType i'
-  ensureClosed ty' stmt subst
   mty' <- atCurrentSubst mty
   case mexp of
-    Nothing -> return $ Let i' mty' Nothing
-    Just e -> Let i' mty' . Just <$> specExp e ty'
+    Nothing -> do
+      ensureClosed ty' stmt subst
+      return $ Let i' mty' Nothing
+    Just e -> do
+      e' <- specExp e ty'
+      i'' <- atCurrentSubst i'
+      let ty'' = idType i''
+      subst' <- getSpSubst
+      ensureClosed ty'' stmt subst'
+      mty'' <- atCurrentSubst mty'
+      return $ Let i'' mty'' (Just e')
 specStmt (Block body) =
   Block <$> specBody body
 specStmt (StmtExp e) = do

src/Solcore/Frontend/Module/Loader.hs

@@ -1592,8 +1592,10 @@ toValidationImportStub (TFunDef (FunDef sig _)) =
   Just (TFunDef (stubFunction (sigName sig)))
 toValidationImportStub (TSym (TySym n _ _)) =
   Just (TSym (stubType n))
-toValidationImportStub d@(TClassDef _) =
-  Just d
+toValidationImportStub (TClassDef (Class bvs _ n pvs mv sigs)) =
+  Just (TClassDef (Class bvs [] n pvs mv (map stripSigContext sigs)))
+  where
+    stripSigContext (Signature vs _ sn ps ret) = Signature vs [] sn ps ret
 toValidationImportStub (TContr (Contract n _ _)) =
   Just (TContr (Contract n [] []))
 toValidationImportStub (TDataDef (DataTy n _ cs)) =

src/Solcore/Frontend/TypeInference/TcEnv.hs

@@ -163,6 +163,8 @@ primCtx =
       primUnit,
       primTrue,
       primFalse,
+      primInl,
+      primInr,
       primInvoke
     ]
 

src/Solcore/Frontend/TypeInference/TcSimplify.hs

@@ -193,10 +193,11 @@ toHnf depth p@(InCls c _ _)
               Nothing -> do
                 info [">>>> No default instance found for:", pretty p]
                 pure [p]
-              Just (_, s) -> do
+              Just (ps', s) -> do
                 info [">>>> Default instance for:", pretty p, " found! (Solved), \n>>> Subst: ", pretty s]
                 _ <- extSubst s
-                pure []
+                ps0 <- withCurrentSubst ps'
+                toHnfs (depth - 1) ps0
   | depth <= 0 = notEnoughFuel [p]
   | otherwise =
       do
@@ -207,16 +208,15 @@ toHnf depth p@(InCls c _ _)
             insts' <- mapM fromANF insts
             info [">>> No matching instance for:", pretty p, " trying a default instance.Defined instances:\n", unlines (map pretty insts')]
             denv <- getDefaultInstEnv
-            -- does c have a default instance?
             case proveDefaulting denv insts p of
               Nothing -> do
                 info [">>>> No default instance found for:", pretty p]
                 pure [p]
-              Just (_, s) -> do
+              Just (ps', s) -> do
                 info [">>>> Default instance for:", pretty p, " found! (Solved), \n>>> Subst: ", pretty s]
-                -- default instances should not have any additional contraints.
                 _ <- extSubst s
-                pure []
+                ps0 <- withCurrentSubst ps'
+                toHnfs (depth - 1) ps0
           Just (ps', s, i) -> do
             info [">>> Found instance for:", pretty p, "\n>>> Instance:", pretty i, "\n>>> Subst:", pretty s]
             _ <- extSubst s

std/Bits.solc

@@ -0,0 +1,65 @@
+export { * };
+
+// Bitwise word operations using EVM assembly.
+
+function band(a : word, b : word) -> word {
+    let res : word;
+    assembly { res := and(a, b) }
+    return res;
+}
+
+function bor(a : word, b : word) -> word {
+    let res : word;
+    assembly { res := or(a, b) }
+    return res;
+}
+
+function bxor(a : word, b : word) -> word {
+    let res : word;
+    assembly { res := xor(a, b) }
+    return res;
+}
+
+function bnot(a : word) -> word {
+    let res : word;
+    assembly { res := not(a) }
+    return res;
+}
+
+// shl(n, x): shift x left by n bits
+function shl_(n : word, x : word) -> word {
+    let res : word;
+    assembly { res := shl(n, x) }
+    return res;
+}
+
+// shr(n, x): logical shift x right by n bits
+function shr_(n : word, x : word) -> word {
+    let res : word;
+    assembly { res := shr(n, x) }
+    return res;
+}
+
+// mask(n): n-bit mask in the least significant positions (bits 0..n-1 set to 1)
+function mask(n : word) -> word {
+    let res : word;
+    assembly { res := sub(shl(n, 1), 1) }
+    return res;
+}
+
+// maxWord(a, b): returns the larger of the two words
+function maxWord(a : word, b : word) -> word {
+    let cond : word;
+    assembly { cond := gt(a, b) }
+    match cond {
+    | 0 => return b;
+    | _ => return a;
+    }
+}
+
+// addWord(a, b): wrapping 256-bit addition
+function addWord(a : word, b : word) -> word {
+    let res : word;
+    assembly { res := add(a, b) }
+    return res;
+}

std/Generic.solc

@@ -0,0 +1,15 @@
+export { * };
+
+// Generic isomorphism class (sum-of-products representation).
+//
+// `a : Generic(rep)` witnesses that type `a` is isomorphic to `rep`,
+// where `rep` is a nested combination of `pair`, `sum`, `()`, `bool`,
+// and `word` — the sum-of-products normal form.
+//
+// Users write exactly one instance per data type; all generic operations
+// (Packable, Storable, ...) follow automatically via the bridge instances.
+
+forall a rep. class a : Generic(rep) {
+    function from(x : a) -> rep;
+    function to(x : rep) -> a;
+}

std/Packable.solc

@@ -0,0 +1,113 @@
+import Bits.{*};
+import Generic.{Generic};
+
+export { * };
+
+// Packable: types that fit in a 256-bit word with a dense bit layout.
+//
+// Invariant: pack(x) uses only the least significant bitWidth(x) bits.
+// bitWidth takes a value so the bridge instance can call Generic.from(x)
+// to resolve the rep type variable before any let-binding needs it.
+
+forall a. class a : Packable {
+    function bitWidth(x : a) -> word;
+    function pack(x : a) -> word;
+    function unpack(w : word) -> a;
+}
+
+instance () : Packable {
+    function bitWidth(x : ()) -> word { return 0; }
+    function pack(x : ()) -> word { return 0; }
+    function unpack(w : word) -> () { return (); }
+}
+
+instance bool : Packable {
+    function bitWidth(x : bool) -> word { return 1; }
+    function pack(x : bool) -> word {
+        match x {
+        | true  => return 1;
+        | false => return 0;
+        }
+    }
+    function unpack(w : word) -> bool {
+        match band(w, 1) {
+        | 0 => return false;
+        | _ => return true;
+        }
+    }
+}
+
+instance word : Packable {
+    function bitWidth(x : word) -> word { return 256; }
+    function pack(x : word) -> word { return x; }
+    function unpack(w : word) -> word { return w; }
+}
+
+// pair: low field a packed in bits 0..bitWidth(a)-1,
+//       high field b packed in bits bitWidth(a)..bitWidth(a)+bitWidth(b)-1
+forall a b. a : Packable, b : Packable =>
+instance pair(a, b) : Packable {
+    function bitWidth(x : pair(a, b)) -> word {
+        match x {
+        | (l, r) => return addWord(Packable.bitWidth(l), Packable.bitWidth(r));
+        }
+    }
+    function pack(x : pair(a, b)) -> word {
+        match x {
+        | (l, r) =>
+            let bw : word = Packable.bitWidth(l);
+            return bor(Packable.pack(l), shl_(bw, Packable.pack(r)));
+        }
+    }
+    function unpack(w : word) -> pair(a, b) {
+        let lo_dummy : a = Packable.unpack(0);
+        let bw : word = Packable.bitWidth(lo_dummy);
+        let lo : a = Packable.unpack(band(w, mask(bw)));
+        let hi : b = Packable.unpack(shr_(bw, w));
+        return (lo, hi);
+    }
+}
+
+// sum: bit 0 is the tag (0 = inl, 1 = inr); payload in the upper bits
+forall a b. a : Packable, b : Packable =>
+instance sum(a, b) : Packable {
+    function bitWidth(x : sum(a, b)) -> word {
+        let la : a = Packable.unpack(0);
+        let lb : b = Packable.unpack(0);
+        return addWord(1, maxWord(Packable.bitWidth(la), Packable.bitWidth(lb)));
+    }
+    function pack(x : sum(a, b)) -> word {
+        match x {
+        | inl(l) => return shl_(1, Packable.pack(l));
+        | inr(r) => return bor(shl_(1, Packable.pack(r)), 1);
+        }
+    }
+    function unpack(w : word) -> sum(a, b) {
+        match band(w, 1) {
+        | 0 => return inl(Packable.unpack(shr_(1, w)):a);
+        | _ => return inr(Packable.unpack(shr_(1, w)):b);
+        }
+    }
+}
+
+// --- Bridge instance ---
+// Any type with a Generic instance is automatically Packable.
+// bitWidth calls Generic.from(x) first so that the rep type variable
+// is resolved into the specialiser substitution before it is needed.
+
+pragma no-patterson-condition Packable;
+pragma no-bounded-variable-condition Packable;
+forall a rep. a : Generic(rep), rep : Packable =>
+default instance a : Packable {
+    function bitWidth(x : a) -> word {
+        let r : rep = Generic.from(x);
+        return Packable.bitWidth(r);
+    }
+    function pack(x : a) -> word {
+        let r : rep = Generic.from(x);
+        return Packable.pack(r);
+    }
+    function unpack(w : word) -> a {
+        return Generic.to(Packable.unpack(w):rep);
+    }
+}

std/Storage.solc

@@ -0,0 +1,30 @@
+import Packable.{Packable};
+
+export { * };
+
+// Storable: EVM storage read/write derived from Packable.
+//
+// The default instance reads/writes the packed word representation.
+// For types with bitWidth > 256 the user must provide a specialised instance
+// that distributes the value across multiple storage slots.
+
+forall a. a : Packable =>
+class a : Storable {
+    function sload(slot : word) -> a;
+    function sstore(slot : word, v : a) -> ();
+}
+
+pragma no-patterson-condition Storable;
+pragma no-bounded-variable-condition Storable;
+forall a. a : Packable =>
+default instance a : Storable {
+    function sload(slot : word) -> a {
+        let raw : word;
+        assembly { raw := sload(slot) }
+        return Packable.unpack(raw);
+    }
+    function sstore(slot : word, v : a) -> () {
+        let w : word = Packable.pack(v);
+        assembly { sstore(slot, w) }
+    }
+}