Add field element type (#2659)

* Closes #2571 * It is reasonable to finish this PR before tackling #2562, because the field element type is the primary data type in Cairo. * Depends on #2653 Checklist --------- - [x] Add field type and operations to intermediate representations (JuvixCore, JuvixTree, JuvixAsm, JuvixReg). - [x] Add CLI option to choose field size. - [x] Add frontend field builtins. - [x] Automatic conversion of integer literals to field elements. - [x] Juvix standard library support for fields. - [x] Check if field size matches when loading a stored module. - [x] Update the Cairo Assembly (CASM) interpreter to use the field type instead of integer type. - [x] Add field type to VampIR backend. - [x] Tests --------- Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
2024-08-16 11:40:36 +03:00 · 2024-02-27 14:54:43 +01:00 · 2024-02-27 14:54:43 +01:00 · dcea0bbecb
commit dcea0bbecb
parent a091a7f63d
108 changed files with 1195 additions and 159 deletions
--- a/app/Commands/Dev/Core/Eval.hs
+++ b/app/Commands/Dev/Core/Eval.hs
@ -9,9 +9,10 @@ runCommand :: forall r. (Members '[EmbedIO, App] r) => CoreEvalOptions -> Sem r
 runCommand opts = do
  f :: Path Abs File <- fromAppPathFile b
  s <- readFile f
+  gopts <- askGlobalOptions
  case Core.runParser f defaultModuleId mempty s of
    Left err -> exitJuvixError (JuvixError err)
-    Right (tab, Just node) -> do evalAndPrint opts tab node
+    Right (tab, Just node) -> do evalAndPrint gopts opts tab node
    Right (_, Nothing) -> return ()
  where
    b :: AppPath File
--- a/app/Commands/Dev/Core/FromConcrete.hs
+++ b/app/Commands/Dev/Core/FromConcrete.hs
@ -51,14 +51,14 @@ runCommand localOpts = do
            newline

      goEval :: Sem r ()
-      goEval = evalAndPrint localOpts tab' evalNode
+      goEval = evalAndPrint gopts localOpts tab' evalNode
        where
          evalNode :: Core.Node
            | isJust (localOpts ^. coreFromConcreteSymbolName) = getNode' selInfo
            | otherwise = getNode' mainInfo

      goNormalize :: Sem r ()
-      goNormalize = normalizeAndPrint localOpts tab' evalNode
+      goNormalize = normalizeAndPrint gopts localOpts tab' evalNode
        where
          evalNode :: Core.Node
            | isJust (localOpts ^. coreFromConcreteSymbolName) = getNode' selInfo
--- a/app/Commands/Dev/Core/Normalize.hs
+++ b/app/Commands/Dev/Core/Normalize.hs
@ -9,9 +9,10 @@ runCommand :: forall r. (Members '[EmbedIO, App] r) => CoreNormalizeOptions -> S
 runCommand opts = do
  f :: Path Abs File <- fromAppPathFile b
  s <- readFile f
+  gopts <- askGlobalOptions
  case Core.runParser f defaultModuleId mempty s of
    Left err -> exitJuvixError (JuvixError err)
-    Right (tab, Just node) -> do normalizeAndPrint opts tab node
+    Right (tab, Just node) -> do normalizeAndPrint gopts opts tab node
    Right (_, Nothing) -> return ()
  where
    b :: AppPath File
--- a/app/Commands/Dev/Core/Read.hs
+++ b/app/Commands/Dev/Core/Read.hs
@ -30,21 +30,21 @@ runCommand opts = do
  embed (Scoper.scopeTrace tab')
  unless (project opts ^. coreReadNoPrint) $ do
    renderStdOut (Pretty.ppOut opts tab')
-  whenJust (tab' ^. Core.infoMain) $ \sym -> doEval tab' (fromJust $ tab' ^. Core.identContext . at sym)
+  whenJust (tab' ^. Core.infoMain) $ \sym -> doEval gopts tab' (fromJust $ tab' ^. Core.identContext . at sym)
  where
-    doEval :: Core.InfoTable -> Core.Node -> Sem r ()
-    doEval tab' node =
+    doEval :: GlobalOptions -> Core.InfoTable -> Core.Node -> Sem r ()
+    doEval gopts tab' node =
      if
          | project opts ^. coreReadEval -> do
              putStrLn "--------------------------------"
              putStrLn "|            Eval              |"
              putStrLn "--------------------------------"
-              Eval.evalAndPrint opts tab' node
+              Eval.evalAndPrint gopts opts tab' node
          | project opts ^. coreReadNormalize -> do
              putStrLn "--------------------------------"
              putStrLn "|         Normalize            |"
              putStrLn "--------------------------------"
-              Eval.normalizeAndPrint opts tab' node
+              Eval.normalizeAndPrint gopts opts tab' node
          | otherwise -> return ()
    sinputFile :: AppPath File
    sinputFile = project opts ^. coreReadInputFile
--- a/app/Commands/Dev/Core/Repl.hs
+++ b/app/Commands/Dev/Core/Repl.hs
@ -14,6 +14,7 @@ import Juvix.Compiler.Core.Pretty qualified as Core
 import Juvix.Compiler.Core.Transformation.ComputeTypeInfo qualified as Core
 import Juvix.Compiler.Core.Transformation.DisambiguateNames qualified as Core
 import Juvix.Compiler.Core.Translation.FromSource qualified as Core
+import Juvix.Data.Field
 import Juvix.Extra.Paths

 runCommand :: forall r. (Members '[EmbedIO, App] r) => CoreReplOptions -> Sem r ()
@ -98,7 +99,7 @@ runRepl opts tab = do
  where
    replEval :: Bool -> Core.InfoTable -> Core.Node -> Sem r ()
    replEval noIO tab' node = do
-      r <- Core.doEval noIO defaultLoc tab' node
+      r <- Core.doEval Nothing noIO defaultLoc tab' node
      case r of
        Left err -> do
          printJuvixError (JuvixError err)
@ -115,7 +116,7 @@ runRepl opts tab = do
    replNormalize :: Core.InfoTable -> Core.Node -> Sem r ()
    replNormalize tab' node =
      let md' = Core.moduleFromInfoTable tab'
-          node' = normalize md' node
+          node' = normalize (maximum allowedFieldSizes) md' node
       in if
              | Info.member Info.kNoDisplayInfo (Core.getInfo node') ->
                  runRepl opts tab'
--- a/app/Commands/Dev/Core/Strip.hs
+++ b/app/Commands/Dev/Core/Strip.hs
@ -16,7 +16,7 @@ runCommand opts = do
        run $
          runReader (project gopts) $
            runError @JuvixError (Core.toStripped' Core.Identity (Core.moduleFromInfoTable tab) :: Sem '[Error JuvixError, Reader Core.CoreOptions] Core.Module)
-  tab' <- getRight $ mapLeft JuvixError $ mapRight (Stripped.fromCore . Core.computeCombinedInfoTable) r
+  tab' <- getRight $ mapLeft JuvixError $ mapRight (Stripped.fromCore (project gopts ^. Core.optFieldSize) . Core.computeCombinedInfoTable) r
  unless (project opts ^. coreStripNoPrint) $ do
    renderStdOut (Core.ppOut opts tab')
  where
--- a/app/Commands/Eval.hs
+++ b/app/Commands/Eval.hs
@ -22,7 +22,7 @@ runCommand opts@EvalOptions {..} = do
            | otherwise -> getNode tab (mainInfo tab)
  case mevalNode of
    Just evalNode ->
-      Eval.evalAndPrint opts tab evalNode
+      Eval.evalAndPrint gopts opts tab evalNode
    Nothing -> do
      let name = fromMaybe Str.main _evalSymbolName
      printFailureExit ("function not found: " <> name)
--- a/app/Commands/Repl.hs
+++ b/app/Commands/Repl.hs
@ -171,6 +171,7 @@ replCommand opts input_ = catchAll $ do

        eval :: Core.Node -> Repl Core.Node
        eval n = do
+          gopts <- State.gets (^. replStateGlobalOptions)
          ep <- getReplEntryPointFromPrepath (mkPrepath (toFilePath P.replPath))
          let shouldDisambiguate :: Bool
              shouldDisambiguate = not (opts ^. replNoDisambiguate)
@ -182,12 +183,12 @@ replCommand opts input_ = catchAll $ do
              . runState artif
              . runTransformations shouldDisambiguate (opts ^. replTransformations)
              $ n
-          liftIO (doEvalIO' artif' n') >>= replFromEither
+          liftIO (doEvalIO' (project gopts ^. Core.optFieldSize) artif' n') >>= replFromEither

-        doEvalIO' :: Artifacts -> Core.Node -> IO (Either JuvixError Core.Node)
-        doEvalIO' artif' n =
+        doEvalIO' :: Natural -> Artifacts -> Core.Node -> IO (Either JuvixError Core.Node)
+        doEvalIO' fsize artif' n =
          mapLeft (JuvixError @Core.CoreError)
-            <$> Core.doEvalIO False replDefaultLoc (Core.computeCombinedInfoTable $ artif' ^. artifactCoreModule) n
+            <$> Core.doEvalIO (Just fsize) False replDefaultLoc (Core.computeCombinedInfoTable $ artif' ^. artifactCoreModule) n

        compileString :: Repl (Maybe Core.Node)
        compileString = do
--- a/app/CommonOptions.hs
+++ b/app/CommonOptions.hs
@ -11,6 +11,7 @@ import Data.List.NonEmpty qualified as NonEmpty
 import Juvix.Compiler.Core.Data.TransformationId.Parser qualified as Core
 import Juvix.Compiler.Reg.Data.TransformationId.Parser qualified as Reg
 import Juvix.Compiler.Tree.Data.TransformationId.Parser qualified as Tree
+import Juvix.Data.Field
 import Juvix.Data.FileExt
 import Juvix.Prelude
 import Options.Applicative
@ -111,6 +112,23 @@ naturalNumberOpt = eitherReader aux
    aux :: String -> Either String Word
    aux s = maybe (Left $ s <> " is not a nonnegative number") Right (readMaybe s :: Maybe Word)

+fieldSizeOpt :: ReadM (Maybe Natural)
+fieldSizeOpt = eitherReader aux
+  where
+    aux :: String -> Either String (Maybe Natural)
+    aux s = case s of
+      "cairo" -> Right $ Just cairoFieldSize
+      "small" -> Right $ Just smallFieldSize
+      _ ->
+        mapRight Just $
+          either Left checkAllowed $
+            maybe (Left $ s <> " is not a valid field size") Right (readMaybe s :: Maybe Natural)
+
+    checkAllowed :: Natural -> Either String Natural
+    checkAllowed n
+      | n `elem` allowedFieldSizes = Right n
+      | otherwise = Left $ Prelude.show n <> " is not a recognized field size"
+
 extCompleter :: FileExt -> Completer
 extCompleter ext = mkCompleter $ \word -> do
  let cmd = unwords ["compgen", "-o", "plusdirs", "-f", "-X", "!*" <> Prelude.show ext, "--", requote word]
--- a/app/Evaluator.hs
+++ b/app/Evaluator.hs
@ -20,15 +20,16 @@ data EvalOptions = EvalOptions
 makeLenses ''EvalOptions

 evalAndPrint ::
-  forall r a.
-  (Members '[EmbedIO, App] r, CanonicalProjection a EvalOptions, CanonicalProjection a Core.Options) =>
+  forall r a b.
+  (Members '[EmbedIO, App] r, CanonicalProjection a EvalOptions, CanonicalProjection b Core.CoreOptions, CanonicalProjection a Core.Options) =>
+  b ->
  a ->
  Core.InfoTable ->
  Core.Node ->
  Sem r ()
-evalAndPrint opts tab node = do
+evalAndPrint gopts opts tab node = do
  loc <- defaultLoc
-  r <- Core.doEval (project opts ^. evalNoIO) loc tab node
+  r <- Core.doEval (Just $ project gopts ^. Core.optFieldSize) (project opts ^. evalNoIO) loc tab node
  case r of
    Left err -> exitJuvixError (JuvixError err)
    Right node'
@ -50,14 +51,15 @@ evalAndPrint opts tab node = do
    f = project opts ^. evalInputFile

 normalizeAndPrint ::
-  forall r a.
-  (Members '[EmbedIO, App] r, CanonicalProjection a EvalOptions, CanonicalProjection a Core.Options) =>
+  forall r a b.
+  (Members '[EmbedIO, App] r, CanonicalProjection a EvalOptions, CanonicalProjection b Core.CoreOptions, CanonicalProjection a Core.Options) =>
+  b ->
  a ->
  Core.InfoTable ->
  Core.Node ->
  Sem r ()
-normalizeAndPrint opts tab node =
-  let node' = normalize (Core.moduleFromInfoTable tab) node
+normalizeAndPrint gopts opts tab node =
+  let node' = normalize (project gopts ^. Core.optFieldSize) (Core.moduleFromInfoTable tab) node
   in if
          | Info.member Info.kNoDisplayInfo (Core.getInfo node') ->
              return ()
--- a/app/GlobalOptions.hs
+++ b/app/GlobalOptions.hs
@ -11,6 +11,7 @@ import Juvix.Compiler.Pipeline
 import Juvix.Compiler.Pipeline.Root
 import Juvix.Data.Effect.TaggedLock
 import Juvix.Data.Error.GenericError qualified as E
+import Juvix.Data.Field

 data GlobalOptions = GlobalOptions
  { _globalNoColors :: Bool,
@ -23,6 +24,7 @@ data GlobalOptions = GlobalOptions
    _globalNoCoverage :: Bool,
    _globalNoStdlib :: Bool,
    _globalUnrollLimit :: Int,
+    _globalFieldSize :: Maybe Natural,
    _globalOffline :: Bool
  }
  deriving stock (Eq, Show)
@ -46,6 +48,7 @@ instance CanonicalProjection GlobalOptions Core.CoreOptions where
    Core.CoreOptions
      { Core._optCheckCoverage = not _globalNoCoverage,
        Core._optUnrollLimit = _globalUnrollLimit,
+        Core._optFieldSize = fromMaybe defaultFieldSize _globalFieldSize,
        Core._optOptimizationLevel = defaultOptimizationLevel,
        Core._optInliningDepth = defaultInliningDepth
      }
@ -63,6 +66,7 @@ defaultGlobalOptions =
      _globalNoCoverage = False,
      _globalNoStdlib = False,
      _globalUnrollLimit = defaultUnrollLimit,
+      _globalFieldSize = Nothing,
      _globalOffline = False
    }

@ -112,6 +116,13 @@ parseGlobalFlags = do
      ( long "no-stdlib"
          <> help "Do not use the standard library"
      )
+  _globalFieldSize <-
+    option
+      fieldSizeOpt
+      ( long "field-size"
+          <> value Nothing
+          <> help "Field type size [cairo,small,11] (default: small)"
+      )
  _globalUnrollLimit <-
    option
      (fromIntegral <$> naturalNumberOpt)
@ -162,7 +173,8 @@ entryPointFromGlobalOptions root mainFile opts = do
        _entryPointUnrollLimit = opts ^. globalUnrollLimit,
        _entryPointGenericOptions = project opts,
        _entryPointBuildDir = maybe (def ^. entryPointBuildDir) (CustomBuildDir . Abs) mabsBuildDir,
-        _entryPointOffline = opts ^. globalOffline
+        _entryPointOffline = opts ^. globalOffline,
+        _entryPointFieldSize = fromMaybe defaultFieldSize $ opts ^. globalFieldSize
      }
  where
    optBuildDir :: Maybe (Prepath Dir)
@ -184,7 +196,8 @@ entryPointFromGlobalOptionsNoFile root opts = do
        _entryPointUnrollLimit = opts ^. globalUnrollLimit,
        _entryPointGenericOptions = project opts,
        _entryPointBuildDir = maybe (def ^. entryPointBuildDir) (CustomBuildDir . Abs) mabsBuildDir,
-        _entryPointOffline = opts ^. globalOffline
+        _entryPointOffline = opts ^. globalOffline,
+        _entryPointFieldSize = fromMaybe defaultFieldSize $ opts ^. globalFieldSize
      }
  where
    optBuildDir :: Maybe (Prepath Dir)
--- a/examples/milestone/Bank/Bank.juvix
+++ b/examples/milestone/Bank/Bank.juvix
@ -12,12 +12,6 @@ Address : Type := Nat;

 bankAddress : Address := 1234;

--- Some field type.
-axiom Field : Type;
-
--- Equality test for ;Field;.
-axiom eqField : Field -> Field -> Bool;
-
 module Token;
  type Token :=
    --- Arguments are: owner, gates, amount.
@ -47,7 +41,7 @@ module Balances;
    | f n nil := (f, n) :: nil
    | f n ((b, bn) :: bs) :=
      if
-        (eqField f b)
+        (f == b)
        ((b, bn + n) :: bs)
        ((b, bn) :: increment f n bs);

@ -58,7 +52,7 @@ module Balances;
    | _ _ nil := nil
    | f n ((b, bn) :: bs) :=
      if
-        (eqField f b)
+        (f == b)
        ((b, sub bn n) :: bs)
        ((b, bn) :: decrement f n bs);

--- a/include/package-base/Juvix/Builtin/V1/Nat.juvix
+++ b/include/package-base/Juvix/Builtin/V1/Nat.juvix
@ -10,7 +10,5 @@ naturalNatI : Natural Nat :=
  mkNatural@{
    + := (Nat.+);
    * := (Nat.*);
-    div := Nat.div;
-    mod := Nat.mod;
    fromNat (x : Nat) : Nat := x
  };
--- a/include/package-base/Juvix/Builtin/V1/Trait/Natural.juvix
+++ b/include/package-base/Juvix/Builtin/V1/Trait/Natural.juvix
@ -10,8 +10,6 @@ type Natural A :=
    + : A -> A -> A;
    syntax operator * multiplicative;
    * : A -> A -> A;
-    div : A -> A -> A;
-    mod : A -> A -> A;
    builtin from-nat
    fromNat : Nat -> A
  };
--- a/2
+++ b/2
@ -1 +1 @@
-Subproject commit 183d4e9329a648b339ebecf2122b3e9621c99ee8
+Subproject commit 6eb7ac818f8f2e4e28c208fa8ec32ba7411cab04
--- a/runtime/src/vampir/stdlib.pir
+++ b/runtime/src/vampir/stdlib.pir
@ -63,6 +63,19 @@ def mul (x, e1) (y, e2) = {
    (x * y, e1 * e2 * range_check (x * y))
 };

+def fadd (x, e1) (y, e2) = {
+    (x + y, e1 * e2)
+};
+def fsub (x, e1) (y, e2) = {
+    (x - y, e1 * e2)
+};
+def fmul (x, e1) (y, e2) = {
+    (x * y, e1 * e2)
+};
+def fdiv (x, e1) (y, e2) = {
+    (x / y, e1 * e2)
+};
+
 def equal (x, e1) (y, e2) = (isZero (x - y), e1 * e2);

 def if (b, e) (x, e1) (y, e2) = (b * x + (1 - b) * y, e * (b * e1 + (1 - b) * e2));
--- a/runtime/src/vampir/stdlib_unsafe.pir
+++ b/runtime/src/vampir/stdlib_unsafe.pir
@ -41,6 +41,11 @@ def add x y = x + y;
 def sub x y = x - y;
 def mul x y = x * y;

+def fadd x y = x + y;
+def fsub x y = x - y;
+def fmul x y = x * y;
+def fdiv x y = x / y;
+
 def equal x y = isZero (x - y);

 def if b x y = b * x + (1 - b) * y;
--- a/src/Juvix/Compiler/Asm/Extra/Memory.hs
+++ b/src/Juvix/Compiler/Asm/Extra/Memory.hs
@ -104,6 +104,7 @@ getDirectRefType dr mem = case dr of
 getConstantType :: Constant -> Type
 getConstantType = \case
  ConstInt {} -> mkTypeInteger
+  ConstField {} -> TyField
  ConstBool {} -> mkTypeBool
  ConstString {} -> TyString
  ConstUnit -> TyUnit
--- a/src/Juvix/Compiler/Asm/Extra/Recursors.hs
+++ b/src/Juvix/Compiler/Asm/Extra/Recursors.hs
@ -131,14 +131,17 @@ recurse' sig = go True
            Return ->
              return (dropTempStack mem)

-        fixMemIntOp :: Memory -> Sem r Memory
-        fixMemIntOp mem = fixMemBinOp' mem mkTypeInteger mkTypeInteger mkTypeInteger
-
        fixMemBinOp' :: Memory -> Type -> Type -> Type -> Sem r Memory
        fixMemBinOp' mem ty0 ty1 rty = do
          checkValueStack' loc (sig ^. recursorInfoTable) [ty0, ty1] mem
          return $ pushValueStack rty (popValueStack 2 mem)

+        fixMemIntOp :: Memory -> Sem r Memory
+        fixMemIntOp mem = fixMemBinOp' mem mkTypeInteger mkTypeInteger mkTypeInteger
+
+        fixMemFieldOp :: Memory -> Sem r Memory
+        fixMemFieldOp mem = fixMemBinOp' mem TyField TyField TyField
+
        fixMemBinop :: Memory -> BinaryOp -> Sem r Memory
        fixMemBinop mem op = case op of
          OpIntAdd ->
@ -155,6 +158,14 @@ recurse' sig = go True
            fixMemBinOp' mem mkTypeInteger mkTypeInteger mkTypeBool
          OpIntLe ->
            fixMemBinOp' mem mkTypeInteger mkTypeInteger mkTypeBool
+          OpFieldAdd ->
+            fixMemFieldOp mem
+          OpFieldSub ->
+            fixMemFieldOp mem
+          OpFieldMul ->
+            fixMemFieldOp mem
+          OpFieldDiv ->
+            fixMemFieldOp mem
          OpEq ->
            fixMemBinOp' mem TyDynamic TyDynamic mkTypeBool
          OpStrConcat ->
@ -164,15 +175,23 @@ recurse' sig = go True
        fixMemUnop mem op = case op of
          OpShow ->
            return (pushValueStack TyString (popValueStack 1 mem))
-          OpStrToInt -> do
-            checkValueStack' loc (sig ^. recursorInfoTable) [TyString] mem
-            return (pushValueStack mkTypeInteger (popValueStack 1 mem))
+          OpStrToInt ->
+            checkUnop TyString mkTypeInteger
          OpArgsNum -> do
            when (null (mem ^. memoryValueStack)) $
              throw $
                AsmError loc "empty value stack"
            checkFunType (topValueStack' 0 mem)
            return $ pushValueStack mkTypeInteger (popValueStack 1 mem)
+          OpIntToField ->
+            checkUnop mkTypeInteger TyField
+          OpFieldToInt ->
+            checkUnop TyField mkTypeInteger
+          where
+            checkUnop :: Type -> Type -> Sem r Memory
+            checkUnop ty1 ty2 = do
+              checkValueStack' loc (sig ^. recursorInfoTable) [ty1] mem
+              return (pushValueStack ty2 (popValueStack 1 mem))

        fixMemExtendClosure :: Memory -> InstrExtendClosure -> Sem r Memory
        fixMemExtendClosure mem InstrExtendClosure {..} = do
--- a/src/Juvix/Compiler/Asm/Interpreter.hs
+++ b/src/Juvix/Compiler/Asm/Interpreter.hs
@ -159,6 +159,7 @@ runCodeR infoTable funInfo = goCode (funInfo ^. functionCode) >> popLastValueSta
    getConstantVal :: Constant -> Val
    getConstantVal = \case
      ConstInt i -> ValInteger i
+      ConstField f -> ValField f
      ConstBool b -> ValBool b
      ConstString s -> ValString s
      ConstUnit -> ValUnit
--- a/src/Juvix/Compiler/Asm/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Asm/Translation/FromSource.hs
@ -73,6 +73,14 @@ command = do
      return $ mkBinop' loc OpIntLe
    "eq" ->
      return $ mkBinop' loc OpEq
+    "fadd" ->
+      return $ mkBinop' loc OpFieldAdd
+    "fsub" ->
+      return $ mkBinop' loc OpFieldSub
+    "fmul" ->
+      return $ mkBinop' loc OpFieldMul
+    "fdiv" ->
+      return $ mkBinop' loc OpFieldDiv
    "strcat" ->
      return $ mkBinop' loc OpStrConcat
    "show" ->
--- a/src/Juvix/Compiler/Asm/Translation/FromTree.hs
+++ b/src/Juvix/Compiler/Asm/Translation/FromTree.hs
@ -16,7 +16,8 @@ fromTree tab =
    { _infoMainFunction = tab ^. Tree.infoMainFunction,
      _infoFunctions = genCode <$> tab ^. Tree.infoFunctions,
      _infoInductives = tab ^. Tree.infoInductives,
-      _infoConstrs = tab ^. Tree.infoConstrs
+      _infoConstrs = tab ^. Tree.infoConstrs,
+      _infoFieldSize = tab ^. Tree.infoFieldSize
    }

 -- Generate code for a single function.
--- a/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs
+++ b/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs
@ -256,6 +256,9 @@ fromRegInstr bNoStack info = \case
  Reg.Block Reg.InstrBlock {..} ->
    fromRegCode bNoStack info _instrBlockCode
  where
+    unsupported :: Text -> a
+    unsupported x = error ("unsupported: " <> x)
+
    fromBinaryOp :: Reg.InstrBinop -> Statement
    fromBinaryOp Reg.InstrBinop {..} =
      StatementExpr $
@ -277,6 +280,10 @@ fromRegInstr bNoStack info = \case
      Reg.OpIntLe -> "JUVIX_INT_LE"
      Reg.OpEq -> "JUVIX_VAL_EQ"
      Reg.OpStrConcat -> "JUVIX_STR_CONCAT"
+      Reg.OpFieldAdd -> unsupported "field type"
+      Reg.OpFieldSub -> unsupported "field type"
+      Reg.OpFieldMul -> unsupported "field type"
+      Reg.OpFieldDiv -> unsupported "field type"

    fromUnaryOp :: Reg.InstrUnop -> Statement
    fromUnaryOp Reg.InstrUnop {..} =
@ -292,6 +299,8 @@ fromRegInstr bNoStack info = \case
      Reg.OpShow -> "JUVIX_SHOW"
      Reg.OpStrToInt -> "JUVIX_STR_TO_INT"
      Reg.OpArgsNum -> "JUVIX_ARGS_NUM"
+      Reg.OpFieldToInt -> unsupported "field type"
+      Reg.OpIntToField -> unsupported "field type"

    fromVarRef :: Reg.VarRef -> Expression
    fromVarRef Reg.VarRef {..} =
@ -322,6 +331,7 @@ fromRegInstr bNoStack info = \case
    fromConst :: Reg.Constant -> Expression
    fromConst = \case
      Reg.ConstInt x -> macroCall "make_smallint" [integer x]
+      Reg.ConstField {} -> impossible
      Reg.ConstBool True -> macroVar "BOOL_TRUE"
      Reg.ConstBool False -> macroVar "BOOL_FALSE"
      Reg.ConstString x -> macroCall "GET_CONST_CSTRING" [integer (getStringId info x)]
--- a/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs
+++ b/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs
@ -156,6 +156,7 @@ fromCore tab = case tab ^. Core.infoMain of
    convertConstant :: Core.Constant -> Trans Morphism
    convertConstant Core.Constant {..} = case _constantValue of
      Core.ConstInteger n -> return $ MorphismInteger (BitChoice {_bitChoice = n})
+      Core.ConstField {} -> unsupported
      Core.ConstString {} -> unsupported

    convertApp :: Core.App -> Trans Morphism
@ -543,6 +544,7 @@ fromCore tab = case tab ^. Core.infoMain of
      case _typePrimPrimitive of
        Core.PrimInteger {} -> ObjectInteger
        Core.PrimBool {} -> objectBool
+        Core.PrimField {} -> unsupported
        Core.PrimString -> unsupported

    convertInductive :: Symbol -> Object
--- a/src/Juvix/Compiler/Backend/VampIR/Language.hs
+++ b/src/Juvix/Compiler/Backend/VampIR/Language.hs
@ -16,6 +16,10 @@ data OpCode
  | OpMul
  | OpDiv
  | OpMod
+  | OpFieldAdd
+  | OpFieldSub
+  | OpFieldMul
+  | OpFieldDiv
  | OpEq
  | OpLt
  | OpLe
--- a/src/Juvix/Compiler/Backend/VampIR/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Backend/VampIR/Pretty/Base.hs
@ -29,6 +29,10 @@ instance PrettyCode OpCode where
    OpMul -> return kwMul
    OpDiv -> return kwDiv
    OpMod -> return kwMod
+    OpFieldAdd -> return kwFieldAdd
+    OpFieldSub -> return kwFieldSub
+    OpFieldMul -> return kwFieldMul
+    OpFieldDiv -> return kwFieldDiv
    OpEq -> return kwEqual
    OpLt -> return kwLessThan
    OpLe -> return kwLessOrEqual
--- a/src/Juvix/Compiler/Backend/VampIR/Pretty/Keywords.hs
+++ b/src/Juvix/Compiler/Backend/VampIR/Pretty/Keywords.hs
@ -31,6 +31,18 @@ kwDiv = keyword Str.vampirDiv
 kwMod :: Doc Ann
 kwMod = keyword Str.vampirMod

+kwFieldAdd :: Doc Ann
+kwFieldAdd = keyword Str.fadd
+
+kwFieldSub :: Doc Ann
+kwFieldSub = keyword Str.fsub
+
+kwFieldMul :: Doc Ann
+kwFieldMul = keyword Str.fmul
+
+kwFieldDiv :: Doc Ann
+kwFieldDiv = keyword Str.fdiv
+
 kwEqual :: Doc Ann
 kwEqual = keyword Str.vampirEqual

--- a/src/Juvix/Compiler/Backend/VampIR/Translation/FromCore.hs
+++ b/src/Juvix/Compiler/Backend/VampIR/Translation/FromCore.hs
@ -92,11 +92,18 @@ fromCoreNode ii node =
            OpIntMod -> OpMod
            OpIntLt -> OpLt
            OpIntLe -> OpLe
+            Core.OpFieldAdd -> VampIR.OpFieldAdd
+            Core.OpFieldSub -> VampIR.OpFieldSub
+            Core.OpFieldMul -> VampIR.OpFieldMul
+            Core.OpFieldDiv -> VampIR.OpFieldDiv
            Core.OpEq -> VampIR.OpEq
            _ -> impossible
-      _ -> case _builtinAppOp of
+      [x] -> case _builtinAppOp of
        OpFail -> ExpressionFail
+        OpFieldToInt -> convertExpr x
+        OpFieldFromInt -> convertExpr x
        _ -> impossible
+      _ -> impossible

    goConstructor :: Constr -> Expression
    goConstructor Constr {..} = case _constrTag of
--- a/src/Juvix/Compiler/Builtins.hs
+++ b/src/Juvix/Compiler/Builtins.hs
@ -6,6 +6,7 @@ module Juvix.Compiler.Builtins
    module Juvix.Compiler.Builtins.Bool,
    module Juvix.Compiler.Builtins.List,
    module Juvix.Compiler.Builtins.String,
+    module Juvix.Compiler.Builtins.Field,
    module Juvix.Compiler.Builtins.Debug,
    module Juvix.Compiler.Builtins.Control,
  )
@ -15,6 +16,7 @@ import Juvix.Compiler.Builtins.Bool
 import Juvix.Compiler.Builtins.Control
 import Juvix.Compiler.Builtins.Debug
 import Juvix.Compiler.Builtins.Effect
+import Juvix.Compiler.Builtins.Field
 import Juvix.Compiler.Builtins.IO
 import Juvix.Compiler.Builtins.Int
 import Juvix.Compiler.Builtins.List
--- a/src/Juvix/Compiler/Builtins/Field.hs
+++ b/src/Juvix/Compiler/Builtins/Field.hs
@ -0,0 +1,55 @@
+module Juvix.Compiler.Builtins.Field where
+
+import Juvix.Compiler.Builtins.Effect
+import Juvix.Compiler.Internal.Extra
+import Juvix.Prelude
+
+registerField :: (Member Builtins r) => AxiomDef -> Sem r ()
+registerField d = do
+  unless (isSmallUniverse' (d ^. axiomType)) (error "String should be in the small universe")
+  registerBuiltin BuiltinField (d ^. axiomName)
+
+registerFieldEq :: (Member Builtins r) => AxiomDef -> Sem r ()
+registerFieldEq f = do
+  field_ <- getBuiltinName (getLoc f) BuiltinField
+  bool_ <- getBuiltinName (getLoc f) BuiltinBool
+  unless (f ^. axiomType === (field_ --> field_ --> bool_)) (error "field equality has the wrong type signature")
+  registerBuiltin BuiltinFieldEq (f ^. axiomName)
+
+registerFieldAdd :: (Member Builtins r) => AxiomDef -> Sem r ()
+registerFieldAdd f = do
+  field_ <- getBuiltinName (getLoc f) BuiltinField
+  unless (f ^. axiomType === (field_ --> field_ --> field_)) (error "field addition has the wrong type signature")
+  registerBuiltin BuiltinFieldAdd (f ^. axiomName)
+
+registerFieldSub :: (Member Builtins r) => AxiomDef -> Sem r ()
+registerFieldSub f = do
+  field_ <- getBuiltinName (getLoc f) BuiltinField
+  unless (f ^. axiomType === (field_ --> field_ --> field_)) (error "field subtraction has the wrong type signature")
+  registerBuiltin BuiltinFieldSub (f ^. axiomName)
+
+registerFieldMul :: (Member Builtins r) => AxiomDef -> Sem r ()
+registerFieldMul f = do
+  field_ <- getBuiltinName (getLoc f) BuiltinField
+  unless (f ^. axiomType === (field_ --> field_ --> field_)) (error "field multiplication has the wrong type signature")
+  registerBuiltin BuiltinFieldMul (f ^. axiomName)
+
+registerFieldDiv :: (Member Builtins r) => AxiomDef -> Sem r ()
+registerFieldDiv f = do
+  field_ <- getBuiltinName (getLoc f) BuiltinField
+  unless (f ^. axiomType === (field_ --> field_ --> field_)) (error "field division has the wrong type signature")
+  registerBuiltin BuiltinFieldDiv (f ^. axiomName)
+
+registerFieldFromInt :: (Member Builtins r) => AxiomDef -> Sem r ()
+registerFieldFromInt f = do
+  field_ <- getBuiltinName (getLoc f) BuiltinField
+  int_ <- getBuiltinName (getLoc f) BuiltinInt
+  unless (f ^. axiomType === (int_ --> field_)) (error "integer to field conversion has the wrong type signature")
+  registerBuiltin BuiltinFieldFromInt (f ^. axiomName)
+
+registerFieldToNat :: (Member Builtins r) => AxiomDef -> Sem r ()
+registerFieldToNat f = do
+  field_ <- getBuiltinName (getLoc f) BuiltinField
+  nat_ <- getBuiltinName (getLoc f) BuiltinNat
+  unless (f ^. axiomType === (field_ --> nat_)) (error "field to nat conversion has the wrong type signature")
+  registerBuiltin BuiltinFieldToNat (f ^. axiomName)
--- a/src/Juvix/Compiler/Casm/Interpreter.hs
+++ b/src/Juvix/Compiler/Casm/Interpreter.hs
@ -15,11 +15,12 @@ import Juvix.Compiler.Casm.Data.LabelInfo
 import Juvix.Compiler.Casm.Error
 import Juvix.Compiler.Casm.Interpreter.Error
 import Juvix.Compiler.Casm.Language hiding (ap)
+import Juvix.Data.Field

-type Memory s = MV.MVector s (Maybe Integer)
+type Memory s = MV.MVector s (Maybe FField)

 -- | Runs Cairo Assembly. Returns the value of `[ap - 1]` at program exit.
-runCode :: LabelInfo -> [Instruction] -> Integer
+runCode :: LabelInfo -> [Instruction] -> FField
 runCode (LabelInfo labelInfo) instrs0 = runST goCode
  where
    instrs :: Vec.Vector Instruction
@ -28,7 +29,10 @@ runCode (LabelInfo labelInfo) instrs0 = runST goCode
    initialMemSize :: Int
    initialMemSize = 1024

-    goCode :: ST s Integer
+    fsize :: Natural
+    fsize = cairoFieldSize
+
+    goCode :: ST s FField
    goCode = do
      mem <- MV.replicate initialMemSize Nothing
      go 0 0 0 mem
@ -38,7 +42,7 @@ runCode (LabelInfo labelInfo) instrs0 = runST goCode
      Address ->
      Address ->
      Memory s ->
-      ST s Integer
+      ST s FField
    go pc ap fp mem
      | Vec.length instrs <= pc = do
          when (Vec.length instrs < pc) $
@ -81,14 +85,14 @@ runCode (LabelInfo labelInfo) instrs0 = runST goCode
      Ap -> ap
      Fp -> fp

-    readMem :: Memory s -> Address -> ST s Integer
+    readMem :: Memory s -> Address -> ST s FField
    readMem mem addr = do
      mv <- MV.read mem addr
      case mv of
        Just v -> return v
        Nothing -> throwRunError ("reading uninitialized memory at address " <> show addr)

-    writeMem :: Memory s -> Address -> Integer -> ST s (Memory s)
+    writeMem :: Memory s -> Address -> FField -> ST s (Memory s)
    writeMem mem addr v = do
      let len = MV.length mem
      mem' <-
@ -104,59 +108,62 @@ runCode (LabelInfo labelInfo) instrs0 = runST goCode
      MV.write mem' addr (Just v)
      return mem'

-    writeMemRef :: Address -> Address -> Memory s -> MemRef -> Integer -> ST s (Memory s)
+    writeMemRef :: Address -> Address -> Memory s -> MemRef -> FField -> ST s (Memory s)
    writeMemRef ap fp mem MemRef {..} v = do
      let r = readReg ap fp _memRefReg
          off :: Int = fromIntegral _memRefOff
      writeMem mem (r + off) v

-    readMemRef :: Address -> Address -> Memory s -> MemRef -> ST s Integer
+    readMemRef :: Address -> Address -> Memory s -> MemRef -> ST s FField
    readMemRef ap fp mem MemRef {..} = do
      let r = readReg ap fp _memRefReg
          off :: Int = fromIntegral _memRefOff
      readMem mem (r + off)

-    readLabel :: LabelRef -> Integer
+    readLabel :: LabelRef -> FField
    readLabel LabelRef {..} =
-      fromIntegral $ fromMaybe (throwRunError "invalid label") $ HashMap.lookup _labelRefSymbol labelInfo
+      fieldFromInteger fsize $
+        fromIntegral $
+          fromMaybe (throwRunError "invalid label") $
+            HashMap.lookup _labelRefSymbol labelInfo

-    readValue :: Address -> Address -> Memory s -> Value -> ST s Integer
+    readValue :: Address -> Address -> Memory s -> Value -> ST s FField
    readValue ap fp mem = \case
-      Imm v -> return v
+      Imm v -> return $ fieldFromInteger fsize v
      Ref r -> readMemRef ap fp mem r
      Lab l -> return $ readLabel l

-    readLoadValue :: Address -> Address -> Memory s -> LoadValue -> ST s Integer
+    readLoadValue :: Address -> Address -> Memory s -> LoadValue -> ST s FField
    readLoadValue ap fp mem LoadValue {..} = do
      src <- readMemRef ap fp mem _loadValueSrc
      let off :: Int = fromIntegral _loadValueOff
-          addr :: Int = fromInteger src + off
+          addr :: Int = fromInteger (fieldToInteger src) + off
      readMem mem addr

-    readBinopValue :: Address -> Address -> Memory s -> BinopValue -> ST s Integer
+    readBinopValue :: Address -> Address -> Memory s -> BinopValue -> ST s FField
    readBinopValue ap fp mem BinopValue {..} = do
      v1 <- readMemRef ap fp mem _binopValueArg1
      v2 <- readValue ap fp mem _binopValueArg2
      return $ goOp v1 v2 _binopValueOpcode
      where
-        goOp :: Integer -> Integer -> Opcode -> Integer
+        goOp :: FField -> FField -> Opcode -> FField
        goOp x y = \case
-          FieldAdd -> x + y
-          FieldMul -> x * y
+          FieldAdd -> fieldAdd x y
+          FieldMul -> fieldMul x y

-    readRValue :: Address -> Address -> Memory s -> RValue -> ST s Integer
+    readRValue :: Address -> Address -> Memory s -> RValue -> ST s FField
    readRValue ap fp mem = \case
      Val x -> readValue ap fp mem x
      Load x -> readLoadValue ap fp mem x
      Binop x -> readBinopValue ap fp mem x

-    goAssign :: InstrAssign -> Address -> Address -> Address -> Memory s -> ST s Integer
+    goAssign :: InstrAssign -> Address -> Address -> Address -> Memory s -> ST s FField
    goAssign InstrAssign {..} pc ap fp mem = do
      v <- readRValue ap fp mem _instrAssignValue
      mem' <- writeMemRef ap fp mem _instrAssignResult v
      go (pc + 1) (ap + fromEnum _instrAssignIncAp) fp mem'

-    goExtraBinop :: InstrExtraBinop -> Address -> Address -> Address -> Memory s -> ST s Integer
+    goExtraBinop :: InstrExtraBinop -> Address -> Address -> Address -> Memory s -> ST s FField
    goExtraBinop InstrExtraBinop {..} pc ap fp mem = do
      v1 <- readMemRef ap fp mem _instrExtraBinopArg1
      v2 <- readValue ap fp mem _instrExtraBinopArg2
@ -164,51 +171,61 @@ runCode (LabelInfo labelInfo) instrs0 = runST goCode
      mem' <- writeMemRef ap fp mem _instrExtraBinopResult v
      go (pc + 1) (ap + fromEnum _instrExtraBinopIncAp) fp mem'
      where
-        goOp :: Integer -> Integer -> ExtraOpcode -> Integer
+        goOp :: FField -> FField -> ExtraOpcode -> FField
        goOp x y = \case
-          FieldSub -> x - y
-          IntAdd -> x + y
-          IntSub -> x - y
-          IntMul -> x * y
-          IntDiv -> x `quot` y
-          IntMod -> x `rem` y
-          IntLt -> if x < y then 1 else 0
+          FieldSub -> fieldSub x y
+          FieldDiv -> fieldDiv x y
+          IntAdd -> fieldAdd x y
+          IntSub -> fieldSub x y
+          IntMul -> fieldMul x y
+          IntDiv -> fieldFromInteger fsize (fieldToInt x `quot` fieldToInt y)
+          IntMod -> fieldFromInteger fsize (fieldToInt x `rem` fieldToInt y)
+          IntLt ->
+            fieldFromInteger fsize $
+              if fieldToInt x < fieldToInt y then 1 else 0

-    goJump :: InstrJump -> Address -> Address -> Address -> Memory s -> ST s Integer
+        fieldToInt :: FField -> Integer
+        fieldToInt f
+          | v < fromIntegral fsize `div` 2 = v
+          | otherwise = v - fromIntegral fsize
+          where
+            v = fieldToInteger f
+
+    goJump :: InstrJump -> Address -> Address -> Address -> Memory s -> ST s FField
    goJump InstrJump {..} _ ap fp mem = do
      tgt <- readValue ap fp mem _instrJumpTarget
-      go (fromInteger tgt) (ap + fromEnum _instrJumpIncAp) fp mem
+      go (fromInteger (fieldToInteger tgt)) (ap + fromEnum _instrJumpIncAp) fp mem

-    goJumpIf :: InstrJumpIf -> Address -> Address -> Address -> Memory s -> ST s Integer
+    goJumpIf :: InstrJumpIf -> Address -> Address -> Address -> Memory s -> ST s FField
    goJumpIf InstrJumpIf {..} pc ap fp mem = do
      tgt <- readValue ap fp mem _instrJumpIfTarget
      v <- readMemRef ap fp mem _instrJumpIfValue
-      go (if v /= 0 then fromInteger tgt else pc + 1) (ap + fromEnum _instrJumpIfIncAp) fp mem
+      go (if fieldToInteger v /= 0 then fromInteger (fieldToInteger tgt) else pc + 1) (ap + fromEnum _instrJumpIfIncAp) fp mem

-    goJumpRel :: InstrJumpRel -> Address -> Address -> Address -> Memory s -> ST s Integer
+    goJumpRel :: InstrJumpRel -> Address -> Address -> Address -> Memory s -> ST s FField
    goJumpRel InstrJumpRel {..} pc ap fp mem = do
      tgt <- readRValue ap fp mem _instrJumpRelTarget
-      go (pc + fromInteger tgt) (ap + fromEnum _instrJumpRelIncAp) fp mem
+      go (pc + fromInteger (fieldToInteger tgt)) (ap + fromEnum _instrJumpRelIncAp) fp mem

-    goCall :: InstrCall -> Address -> Address -> Address -> Memory s -> ST s Integer
+    goCall :: InstrCall -> Address -> Address -> Address -> Memory s -> ST s FField
    goCall InstrCall {..} pc ap fp mem = do
      tgt <- readValue ap fp mem _instrCallTarget
-      mem' <- writeMem mem ap (fromIntegral fp)
-      mem'' <- writeMem mem' (ap + 1) (fromIntegral pc + 1)
-      go (fromInteger tgt) (ap + 2) (ap + 2) mem''
+      mem' <- writeMem mem ap (fieldFromInteger fsize (fromIntegral fp))
+      mem'' <- writeMem mem' (ap + 1) (fieldFromInteger fsize (fromIntegral pc + 1))
+      go (fromInteger (fieldToInteger tgt)) (ap + 2) (ap + 2) mem''

-    goReturn :: Address -> Address -> Address -> Memory s -> ST s Integer
+    goReturn :: Address -> Address -> Address -> Memory s -> ST s FField
    goReturn _ ap fp mem = do
      pc' <- readMem mem (fp - 1)
      fp' <- readMem mem (fp - 2)
-      go (fromInteger pc') ap (fromInteger fp') mem
+      go (fromInteger (fieldToInteger pc')) ap (fromInteger (fieldToInteger fp')) mem

-    goAlloc :: InstrAlloc -> Address -> Address -> Address -> Memory s -> ST s Integer
+    goAlloc :: InstrAlloc -> Address -> Address -> Address -> Memory s -> ST s FField
    goAlloc InstrAlloc {..} pc ap fp mem = do
      v <- readRValue ap fp mem _instrAllocSize
-      go (pc + 1) (ap + fromInteger v) fp mem
+      go (pc + 1) (ap + fromInteger (fieldToInteger v)) fp mem

-    goTrace :: InstrTrace -> Address -> Address -> Address -> Memory s -> ST s Integer
+    goTrace :: InstrTrace -> Address -> Address -> Address -> Memory s -> ST s FField
    goTrace InstrTrace {..} pc ap fp mem = do
      v <- readRValue ap fp mem _instrTraceValue
      GHC.unsafePerformIO (print v >> return (pure ()))
--- a/src/Juvix/Compiler/Casm/Keywords.hs
+++ b/src/Juvix/Compiler/Casm/Keywords.hs
@ -12,6 +12,7 @@ import Juvix.Data.Keyword.All
    kwApPlusPlus,
    kwCall,
    kwColon,
+    kwDiv,
    kwEq,
    kwFp,
    kwIf,
@ -43,6 +44,7 @@ allKeywords =
    kwApPlusPlus,
    kwCall,
    kwColon,
+    kwDiv,
    kwEq,
    kwFp,
    kwIf,
--- a/src/Juvix/Compiler/Casm/Language.hs
+++ b/src/Juvix/Compiler/Casm/Language.hs
@ -72,6 +72,7 @@ data RValue
 -- `ap` arbitrarily.
 data ExtraOpcode
  = FieldSub
+  | FieldDiv
  | IntAdd
  | IntSub
  | IntMul
--- a/src/Juvix/Compiler/Casm/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Casm/Pretty/Base.hs
@ -69,6 +69,7 @@ instance PrettyCode Opcode where
 instance PrettyCode ExtraOpcode where
  ppCode = \case
    FieldSub -> return Str.minus
+    FieldDiv -> return Str.div
    IntAdd -> return Str.iadd
    IntSub -> return Str.isub
    IntMul -> return Str.imul
--- a/src/Juvix/Compiler/Casm/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Casm/Translation/FromSource.hs
@ -253,6 +253,7 @@ parseAssign = do
    parseExtraValue :: ExtraOpcode -> ParsecS r Value
    parseExtraValue = \case
      FieldSub -> Ref <$> parseMemRef
+      FieldDiv -> Ref <$> parseMemRef
      _ -> parseValue

 registerAP :: ParsecS r Reg
@ -276,6 +277,7 @@ opcode =
 extraOpcode :: ParsecS r ExtraOpcode
 extraOpcode =
  (kw kwMinus >> return FieldSub)
+    <|> (kw kwDiv >> return FieldDiv)
    <|> (kw kwIntAdd >> return IntAdd)
    <|> (kw kwIntSub >> return IntSub)
    <|> (kw kwIntMul >> return IntMul)
--- a/src/Juvix/Compiler/Concrete/Data/Builtins.hs
+++ b/src/Juvix/Compiler/Concrete/Data/Builtins.hs
@ -161,6 +161,14 @@ data BuiltinAxiom
  | BuiltinStringEq
  | BuiltinStringToNat
  | BuiltinBoolPrint
+  | BuiltinFieldEq
+  | BuiltinFieldAdd
+  | BuiltinFieldSub
+  | BuiltinFieldMul
+  | BuiltinFieldDiv
+  | BuiltinField
+  | BuiltinFieldFromInt
+  | BuiltinFieldToNat
  | BuiltinString
  | BuiltinIO
  | BuiltinIOSequence
@ -183,6 +191,14 @@ instance Pretty BuiltinAxiom where
    BuiltinStringConcat -> Str.stringConcat
    BuiltinStringEq -> Str.stringEq
    BuiltinStringToNat -> Str.stringToNat
+    BuiltinFieldEq -> Str.fieldEq
+    BuiltinFieldAdd -> Str.fieldAdd
+    BuiltinFieldSub -> Str.fieldSub
+    BuiltinFieldMul -> Str.fieldMul
+    BuiltinFieldDiv -> Str.fieldDiv
+    BuiltinField -> Str.field
+    BuiltinFieldFromInt -> Str.fieldFromInt
+    BuiltinFieldToNat -> Str.fieldToNat
    BuiltinBoolPrint -> Str.boolPrint
    BuiltinIO -> Str.io
    BuiltinString -> Str.string
--- a/src/Juvix/Compiler/Core/Data/Stripped/InfoTable.hs
+++ b/src/Juvix/Compiler/Core/Data/Stripped/InfoTable.hs
@ -7,7 +7,8 @@ data InfoTable = InfoTable
  { _infoMain :: Maybe Symbol,
    _infoFunctions :: HashMap Symbol FunctionInfo,
    _infoInductives :: HashMap Symbol InductiveInfo,
-    _infoConstructors :: HashMap Tag ConstructorInfo
+    _infoConstructors :: HashMap Tag ConstructorInfo,
+    _infoFieldSize :: Natural
  }

 data FunctionInfo = FunctionInfo
--- a/src/Juvix/Compiler/Core/Evaluator.hs
+++ b/src/Juvix/Compiler/Core/Evaluator.hs
@ -12,12 +12,14 @@ import Juvix.Compiler.Core.Extra
 import Juvix.Compiler.Core.Info qualified as Info
 import Juvix.Compiler.Core.Info.NoDisplayInfo
 import Juvix.Compiler.Core.Pretty
+import Juvix.Data.Field
 import Text.Read qualified as T

 data EvalOptions = EvalOptions
  { _evalOptionsNormalize :: Bool,
    _evalOptionsNoFailure :: Bool,
-    _evalOptionsSilent :: Bool
+    _evalOptionsSilent :: Bool,
+    _evalOptionsFieldSize :: Natural
  }

 makeLenses ''EvalOptions
@ -27,7 +29,8 @@ defaultEvalOptions =
  EvalOptions
    { _evalOptionsNormalize = False,
      _evalOptionsNoFailure = False,
-      _evalOptionsSilent = False
+      _evalOptionsSilent = False,
+      _evalOptionsFieldSize = defaultFieldSize
    }

 data EvalError = EvalError
@ -169,6 +172,12 @@ geval opts herr ctx env0 = eval' env0
      OpIntMul -> binNumOp (*)
      OpIntLt -> binNumCmpOp (<)
      OpIntLe -> binNumCmpOp (<=)
+      OpFieldAdd -> binFieldOp fieldAdd
+      OpFieldSub -> binFieldOp fieldSub
+      OpFieldMul -> binFieldOp fieldMul
+      OpFieldDiv -> binFieldOp fieldDiv
+      OpFieldFromInt -> fieldFromIntOp
+      OpFieldToInt -> fieldToIntOp
      OpEq -> eqOp
      OpIntDiv -> divOp quot
      OpIntMod -> divOp rem
@ -223,6 +232,30 @@ geval opts herr ctx env0 = eval' env0
        binNumOp = binOp nodeFromInteger integerFromNode
        {-# INLINE binNumOp #-}

+        binFieldOp :: (FField -> FField -> FField) -> [Node] -> Node
+        binFieldOp = binOp nodeFromField fieldFromNode
+        {-# INLINE binFieldOp #-}
+
+        fieldFromIntOp :: [Node] -> Node
+        fieldFromIntOp =
+          unary $ \node ->
+            let !v = eval' env node
+             in nodeFromField $
+                  fieldFromInteger (opts ^. evalOptionsFieldSize) $
+                    fromMaybe (evalError "expected integer" v) $
+                      integerFromNode v
+        {-# INLINE fieldFromIntOp #-}
+
+        fieldToIntOp :: [Node] -> Node
+        fieldToIntOp =
+          unary $ \node ->
+            let !v = eval' env node
+             in nodeFromInteger $
+                  fieldToInteger $
+                    fromMaybe (evalError "expected field element" v) $
+                      fieldFromNode v
+        {-# INLINE fieldToIntOp #-}
+
        eqOp :: [Node] -> Node
        eqOp
          | opts ^. evalOptionsNormalize =
@ -285,6 +318,10 @@ geval opts herr ctx env0 = eval' env0
    nodeFromInteger !int = mkConstant' (ConstInteger int)
    {-# INLINE nodeFromInteger #-}

+    nodeFromField :: FField -> Node
+    nodeFromField !fld = mkConstant' (ConstField fld)
+    {-# INLINE nodeFromField #-}
+
    nodeFromBool :: Bool -> Node
    nodeFromBool b = mkConstr' (BuiltinTag tag) []
      where
@ -299,6 +336,12 @@ geval opts herr ctx env0 = eval' env0
      _ -> Nothing
    {-# INLINE integerFromNode #-}

+    fieldFromNode :: Node -> Maybe FField
+    fieldFromNode = \case
+      NCst (Constant _ (ConstField fld)) -> Just fld
+      _ -> Nothing
+    {-# INLINE fieldFromNode #-}
+
    printNode :: Node -> Text
    printNode = \case
      NCst (Constant _ (ConstString s)) -> s
@ -395,22 +438,30 @@ evalIO = hEvalIO stderr stdin stdout
 doEval ::
  forall r.
  (MonadIO (Sem r)) =>
+  Maybe Natural ->
  Bool ->
  Interval ->
  InfoTable ->
  Node ->
  Sem r (Either CoreError Node)
-doEval noIO loc tab node
+doEval mfsize noIO loc tab node
  | noIO = catchEvalError loc (eval stderr (tab ^. identContext) [] node)
-  | otherwise = liftIO (catchEvalErrorIO loc (evalIO (tab ^. identContext) [] node))
+  | otherwise = liftIO (catchEvalErrorIO loc (hEvalIO' opts stderr stdin stdout (tab ^. identContext) [] node))
+  where
+    opts =
+      maybe
+        defaultEvalOptions
+        (\fsize -> defaultEvalOptions {_evalOptionsFieldSize = fsize})
+        mfsize

 doEvalIO ::
+  Maybe Natural ->
  Bool ->
  Interval ->
  InfoTable ->
  Node ->
  IO (Either CoreError Node)
-doEvalIO noIO i tab node = runM (doEval noIO i tab node)
+doEvalIO mfsize noIO i tab node = runM (doEval mfsize noIO i tab node)

 -- | Catch EvalError and convert it to CoreError. Needs a default location in case
 -- no location is available in EvalError.
--- a/src/Juvix/Compiler/Core/Extra/Base.hs
+++ b/src/Juvix/Compiler/Core/Extra/Base.hs
@ -188,6 +188,12 @@ mkTypeString i = mkTypePrim i PrimString
 mkTypeString' :: Type
 mkTypeString' = mkTypeString Info.empty

+mkTypeField :: Info -> Type
+mkTypeField i = mkTypePrim i PrimField
+
+mkTypeField' :: Type
+mkTypeField' = mkTypeField Info.empty
+
 mkDynamic :: Info -> Type
 mkDynamic i = NDyn (Dynamic i)

--- a/src/Juvix/Compiler/Core/Extra/Utils.hs
+++ b/src/Juvix/Compiler/Core/Extra/Utils.hs
@ -410,6 +410,12 @@ builtinOpArgTypes = \case
  OpIntMod -> [mkTypeInteger', mkTypeInteger']
  OpIntLt -> [mkTypeInteger', mkTypeInteger']
  OpIntLe -> [mkTypeInteger', mkTypeInteger']
+  OpFieldAdd -> [mkTypeField', mkTypeField']
+  OpFieldSub -> [mkTypeField', mkTypeField']
+  OpFieldMul -> [mkTypeField', mkTypeField']
+  OpFieldDiv -> [mkTypeField', mkTypeField']
+  OpFieldFromInt -> [mkTypeInteger']
+  OpFieldToInt -> [mkTypeField']
  OpEq -> [mkDynamic', mkDynamic']
  OpShow -> [mkDynamic']
  OpStrConcat -> [mkTypeString', mkTypeString']
--- a/src/Juvix/Compiler/Core/Keywords.hs
+++ b/src/Juvix/Compiler/Core/Keywords.hs
@ -21,6 +21,10 @@ import Juvix.Data.Keyword.All
    kwElse,
    kwEq,
    kwFail,
+    kwFieldAdd,
+    kwFieldDiv,
+    kwFieldMul,
+    kwFieldSub,
    kwGe,
    kwGt,
    kwIf,
@ -67,6 +71,10 @@ allKeywords =
    kwDiv,
    kwElse,
    kwEq,
+    kwFieldAdd,
+    kwFieldDiv,
+    kwFieldMul,
+    kwFieldSub,
    kwIf,
    kwIn,
    kwInductive,
--- a/src/Juvix/Compiler/Core/Language/Builtins.hs
+++ b/src/Juvix/Compiler/Core/Language/Builtins.hs
@ -13,6 +13,12 @@ data BuiltinOp
  | OpIntMod
  | OpIntLt
  | OpIntLe
+  | OpFieldAdd
+  | OpFieldSub
+  | OpFieldMul
+  | OpFieldDiv
+  | OpFieldFromInt
+  | OpFieldToInt
  | OpEq
  | OpShow
  | OpStrConcat
@ -47,6 +53,12 @@ builtinOpArgsNum = \case
  OpIntMod -> 2
  OpIntLt -> 2
  OpIntLe -> 2
+  OpFieldAdd -> 2
+  OpFieldSub -> 2
+  OpFieldMul -> 2
+  OpFieldDiv -> 2
+  OpFieldFromInt -> 1
+  OpFieldToInt -> 1
  OpEq -> 2
  OpShow -> 1
  OpStrConcat -> 2
--- a/src/Juvix/Compiler/Core/Language/Nodes.hs
+++ b/src/Juvix/Compiler/Core/Language/Nodes.hs
@ -11,6 +11,7 @@ import Data.Serialize
 import Juvix.Compiler.Core.Language.Base
 import Juvix.Compiler.Core.Language.Builtins
 import Juvix.Compiler.Core.Language.Primitives
+import Juvix.Data.Field

 -- | De Bruijn index of a locally bound variable.
 data Var' i = Var
@ -35,6 +36,7 @@ data Constant' i = Constant

 data ConstantValue
  = ConstInteger !Integer
+  | ConstField !FField
  | ConstString !Text
  deriving stock (Eq, Generic)

--- a/src/Juvix/Compiler/Core/Language/Primitives.hs
+++ b/src/Juvix/Compiler/Core/Language/Primitives.hs
@ -14,6 +14,7 @@ data Primitive
  = PrimInteger PrimIntegerInfo
  | PrimBool PrimBoolInfo
  | PrimString
+  | PrimField
  deriving stock (Eq, Generic)

 -- | Info about a type represented as an integer.
--- a/src/Juvix/Compiler/Core/Normalizer.hs
+++ b/src/Juvix/Compiler/Core/Normalizer.hs
@ -20,8 +20,8 @@ makeLenses ''NormEnv

 type Norm = Sem '[Reader NormEnv, InfoTableBuilder]

-normalize :: Module -> Node -> Node
-normalize md = run . evalInfoTableBuilder md . runReader normEnv . normalize'
+normalize :: Natural -> Module -> Node -> Node
+normalize fsize md = run . evalInfoTableBuilder md . runReader normEnv . normalize'
  where
    normEnv =
      NormEnv
@ -43,7 +43,8 @@ normalize md = run . evalInfoTableBuilder md . runReader normEnv . normalize'
      where
        opts =
          defaultEvalOptions
-            { _evalOptionsNormalize = True
+            { _evalOptionsNormalize = True,
+              _evalOptionsFieldSize = fsize
            }

    go :: Node -> Norm Node
--- a/src/Juvix/Compiler/Core/Options.hs
+++ b/src/Juvix/Compiler/Core/Options.hs
@ -1,13 +1,15 @@
 module Juvix.Compiler.Core.Options where

 import Juvix.Compiler.Pipeline.EntryPoint
+import Juvix.Data.Field
 import Juvix.Prelude

 data CoreOptions = CoreOptions
  { _optCheckCoverage :: Bool,
    _optUnrollLimit :: Int,
    _optOptimizationLevel :: Int,
-    _optInliningDepth :: Int
+    _optInliningDepth :: Int,
+    _optFieldSize :: Natural
  }

 makeLenses ''CoreOptions
@ -18,7 +20,8 @@ defaultCoreOptions =
    { _optCheckCoverage = True,
      _optUnrollLimit = defaultUnrollLimit,
      _optOptimizationLevel = defaultOptimizationLevel,
-      _optInliningDepth = defaultInliningDepth
+      _optInliningDepth = defaultInliningDepth,
+      _optFieldSize = defaultFieldSize
    }

 fromEntryPoint :: EntryPoint -> CoreOptions
@ -27,5 +30,6 @@ fromEntryPoint EntryPoint {..} =
    { _optCheckCoverage = not _entryPointNoCoverage,
      _optUnrollLimit = _entryPointUnrollLimit,
      _optOptimizationLevel = _entryPointOptimizationLevel,
-      _optInliningDepth = _entryPointInliningDepth
+      _optInliningDepth = _entryPointInliningDepth,
+      _optFieldSize = _entryPointFieldSize
    }
--- a/src/Juvix/Compiler/Core/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Core/Pretty/Base.hs
@ -39,6 +39,12 @@ instance PrettyCode BuiltinOp where
    OpIntMod -> return primMod
    OpIntLt -> return primLess
    OpIntLe -> return primLessEquals
+    OpFieldAdd -> return primFieldAdd
+    OpFieldSub -> return primFieldSub
+    OpFieldMul -> return primFieldMul
+    OpFieldDiv -> return primFieldDiv
+    OpFieldFromInt -> return primFieldFromInt
+    OpFieldToInt -> return primFieldToInt
    OpEq -> return primEquals
    OpShow -> return primShow
    OpStrConcat -> return primStrConcat
@ -64,6 +70,7 @@ instance PrettyCode Tag where
 instance PrettyCode Primitive where
  ppCode = \case
    PrimInteger _ -> return $ annotate (AnnKind KNameInductive) (pretty ("Int" :: String))
+    PrimField -> return $ annotate (AnnKind KNameInductive) (pretty ("Field" :: String))
    PrimBool _ -> return $ annotate (AnnKind KNameInductive) (pretty ("Bool" :: String))
    PrimString -> return $ annotate (AnnKind KNameInductive) (pretty ("String" :: String))

@ -88,11 +95,16 @@ instance PrettyCode ConstantValue where
  ppCode = \case
    ConstInteger int ->
      return $ annotate AnnLiteralInteger (pretty int)
+    ConstField fld ->
+      return $ annotate AnnLiteralInteger (pretty fld)
    ConstString txt ->
      return $ annotate AnnLiteralString (pretty (show txt :: String))

 instance PrettyCode (Constant' i) where
-  ppCode Constant {..} = ppCode _constantValue
+  ppCode Constant {..} = case _constantValue of
+    ConstField fld ->
+      return $ annotate AnnLiteralInteger (pretty fld <> "F")
+    _ -> ppCode _constantValue

 instance (PrettyCode a, HasAtomicity a) => PrettyCode (App' i a) where
  ppCode App {..} = do
@ -695,6 +707,24 @@ kwUnnamedConstr = keyword Str.exclamation
 kwQuestion :: Doc Ann
 kwQuestion = keyword Str.questionMark

+primFieldAdd :: Doc Ann
+primFieldAdd = primitive Str.fadd
+
+primFieldSub :: Doc Ann
+primFieldSub = primitive Str.fsub
+
+primFieldMul :: Doc Ann
+primFieldMul = primitive Str.fmul
+
+primFieldDiv :: Doc Ann
+primFieldDiv = primitive Str.fdiv
+
+primFieldFromInt :: Doc Ann
+primFieldFromInt = primitive Str.itof
+
+primFieldToInt :: Doc Ann
+primFieldToInt = primitive Str.ftoi
+
 primLess :: Doc Ann
 primLess = primitive Str.less

--- a/src/Juvix/Compiler/Core/Transformation.hs
+++ b/src/Juvix/Compiler/Core/Transformation.hs
@ -77,7 +77,7 @@ applyTransformations ts tbl = foldM (flip appTrans) tbl ts
      CheckExec -> mapError (JuvixError @CoreError) . checkExec
      CheckVampIR -> mapError (JuvixError @CoreError) . checkVampIR
      CheckAnoma -> mapError (JuvixError @CoreError) . checkAnoma
-      Normalize -> return . normalize
+      Normalize -> normalize
      LetFolding -> return . letFolding
      LambdaFolding -> return . lambdaFolding
      LetHoisting -> return . letHoisting
--- a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs
+++ b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs
@ -32,6 +32,7 @@ computeNodeTypeInfo md = umapL go
      NCst Constant {..} ->
        case _constantValue of
          ConstInteger {} -> mkTypeInteger'
+          ConstField {} -> mkTypeField'
          ConstString {} -> mkTypeString'
      NApp {} ->
        let (fn, args) = unfoldApps' node
@ -48,6 +49,12 @@ computeNodeTypeInfo md = umapL go
          OpIntMod -> mkTypeInteger'
          OpIntLt -> mkTypeBool'
          OpIntLe -> mkTypeBool'
+          OpFieldAdd -> mkTypeField'
+          OpFieldSub -> mkTypeField'
+          OpFieldMul -> mkTypeField'
+          OpFieldDiv -> mkTypeField'
+          OpFieldFromInt -> mkTypeField'
+          OpFieldToInt -> mkTypeInteger'
          OpEq -> mkTypeBool'
          OpShow -> mkTypeString'
          OpStrConcat -> mkTypeString'
--- a/src/Juvix/Compiler/Core/Transformation/ConvertBuiltinTypes.hs
+++ b/src/Juvix/Compiler/Core/Transformation/ConvertBuiltinTypes.hs
@ -18,6 +18,7 @@ convertNode md = umap go
          Just (BuiltinTypeInductive BuiltinNat) -> mkTypeInteger'
          Just (BuiltinTypeInductive BuiltinInt) -> mkTypeInteger'
          Just (BuiltinTypeAxiom BuiltinString) -> mkTypeString'
+          Just (BuiltinTypeAxiom BuiltinField) -> mkTypeField'
          _ -> node
        where
          ii = lookupInductiveInfo md _typeConstrSymbol
--- a/src/Juvix/Compiler/Core/Transformation/Normalize.hs
+++ b/src/Juvix/Compiler/Core/Transformation/Normalize.hs
@ -2,14 +2,17 @@ module Juvix.Compiler.Core.Transformation.Normalize where

 import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Core.Normalizer qualified as Normalizer
+import Juvix.Compiler.Core.Options
 import Juvix.Compiler.Core.Transformation.Base

-normalize :: Module -> Module
-normalize md =
-  pruneInfoTable $
-    set (moduleInfoTable . identContext) (HashMap.singleton sym node) $
-      set (moduleInfoTable . infoIdentifiers) (HashMap.singleton sym ii) md
+normalize :: (Member (Reader CoreOptions) r) => Module -> Sem r Module
+normalize md = do
+  opts <- ask
+  let node = Normalizer.normalize (opts ^. optFieldSize) md (lookupIdentifierNode md sym)
+  return $
+    pruneInfoTable $
+      set (moduleInfoTable . identContext) (HashMap.singleton sym node) $
+        set (moduleInfoTable . infoIdentifiers) (HashMap.singleton sym ii) md
  where
    sym = fromJust $ getInfoMain md
-    node = Normalizer.normalize md (lookupIdentifierNode md sym)
    ii = lookupIdentifierInfo md sym
--- a/src/Juvix/Compiler/Core/Transformation/Optimize/ConstantFolding.hs
+++ b/src/Juvix/Compiler/Core/Transformation/Optimize/ConstantFolding.hs
@ -5,10 +5,11 @@ import Juvix.Compiler.Core.Data.IdentDependencyInfo
 import Juvix.Compiler.Core.Evaluator
 import Juvix.Compiler.Core.Extra
 import Juvix.Compiler.Core.Info.FreeVarsInfo as Info
+import Juvix.Compiler.Core.Options
 import Juvix.Compiler.Core.Transformation.Base

-convertNode :: HashSet Symbol -> InfoTable -> Module -> Node -> Node
-convertNode nonRecSyms tab md = umap go
+convertNode :: CoreOptions -> HashSet Symbol -> InfoTable -> Module -> Node -> Node
+convertNode opts nonRecSyms tab md = umap go
  where
    go :: Node -> Node
    go node = case node of
@ -54,24 +55,27 @@ convertNode nonRecSyms tab md = umap go
      _ -> isType' node

    doEval' :: Node -> Node
-    doEval' = removeClosures . geval opts stderr (tab ^. identContext) []
+    doEval' = removeClosures . geval eopts stderr (tab ^. identContext) []
      where
-        opts =
+        eopts =
          defaultEvalOptions
            { _evalOptionsNoFailure = True,
-              _evalOptionsSilent = True
+              _evalOptionsSilent = True,
+              _evalOptionsFieldSize = opts ^. optFieldSize
            }

-constantFolding' :: HashSet Symbol -> InfoTable -> Module -> Module
-constantFolding' nonRecSyms tab md =
+constantFolding' :: CoreOptions -> HashSet Symbol -> InfoTable -> Module -> Module
+constantFolding' opts nonRecSyms tab md =
  mapAllNodes
    ( removeInfo kFreeVarsInfo
-        . convertNode nonRecSyms tab md
+        . convertNode opts nonRecSyms tab md
        . computeFreeVarsInfo
    )
    md

-constantFolding :: Module -> Module
-constantFolding md = constantFolding' (nonRecursiveIdents' tab) tab md
+constantFolding :: (Member (Reader CoreOptions) r) => Module -> Sem r Module
+constantFolding md = do
+  opts <- ask
+  return $ constantFolding' opts (nonRecursiveIdents' tab) tab md
  where
    tab = computeCombinedInfoTable md
--- a/src/Juvix/Compiler/Core/Transformation/Optimize/Phase/Main.hs
+++ b/src/Juvix/Compiler/Core/Transformation/Optimize/Phase/Main.hs
@ -16,7 +16,7 @@ import Juvix.Compiler.Core.Transformation.Optimize.SimplifyIfs
 import Juvix.Compiler.Core.Transformation.Optimize.SpecializeArgs

 optimize' :: CoreOptions -> Module -> Module
-optimize' CoreOptions {..} md =
+optimize' opts@CoreOptions {..} md =
  filterUnreachable
    . compose
      (4 * _optOptimizationLevel)
@ -40,7 +40,7 @@ optimize' CoreOptions {..} md =
    nonRecs = nonRecursiveIdents' tab

    doConstantFolding :: Module -> Module
-    doConstantFolding md' = constantFolding' nonRecs' tab' md'
+    doConstantFolding md' = constantFolding' opts nonRecs' tab' md'
      where
        tab' = computeCombinedInfoTable md'
        nonRecs'
--- a/src/Juvix/Compiler/Core/Transformation/Optimize/SimplifyArithmetic.hs
+++ b/src/Juvix/Compiler/Core/Transformation/Optimize/SimplifyArithmetic.hs
@ -2,6 +2,7 @@ module Juvix.Compiler.Core.Transformation.Optimize.SimplifyArithmetic (simplifyA

 import Juvix.Compiler.Core.Extra
 import Juvix.Compiler.Core.Transformation.Base
+import Juvix.Data.Field

 convertNode :: Node -> Node
 convertNode = dmap go
@ -58,6 +59,67 @@ convertNode = dmap go
        | _builtinAppOp == OpIntMul,
          [NCst (Constant _ (ConstInteger 1)), x] <- _builtinAppArgs ->
            x
+      NBlt BuiltinApp {..}
+        | _builtinAppOp == OpFieldAdd,
+          [NBlt blt', n] <- _builtinAppArgs,
+          blt' ^. builtinAppOp == OpFieldSub,
+          [x, m] <- blt' ^. builtinAppArgs,
+          m == n ->
+            x
+      NBlt BuiltinApp {..}
+        | _builtinAppOp == OpFieldSub,
+          [NBlt blt', n] <- _builtinAppArgs,
+          blt' ^. builtinAppOp == OpFieldAdd,
+          [x, m] <- blt' ^. builtinAppArgs ->
+            if
+                | m == n ->
+                    x
+                | x == n ->
+                    m
+                | otherwise ->
+                    node
+      NBlt BuiltinApp {..}
+        | _builtinAppOp == OpFieldAdd,
+          [n, NBlt blt'] <- _builtinAppArgs,
+          blt' ^. builtinAppOp == OpFieldSub,
+          [x, m] <- blt' ^. builtinAppArgs,
+          m == n ->
+            x
+      NBlt BuiltinApp {..}
+        | _builtinAppOp == OpFieldAdd || _builtinAppOp == OpFieldSub,
+          [x, NCst (Constant _ (ConstField f))] <- _builtinAppArgs,
+          fieldToInteger f == 0 ->
+            x
+      NBlt BuiltinApp {..}
+        | _builtinAppOp == OpFieldAdd,
+          [NCst (Constant _ (ConstField f)), x] <- _builtinAppArgs,
+          fieldToInteger f == 0 ->
+            x
+      NBlt BuiltinApp {..}
+        | _builtinAppOp == OpFieldMul,
+          [_, c@(NCst (Constant _ (ConstField f)))] <- _builtinAppArgs,
+          fieldToInteger f == 0 ->
+            c
+      NBlt BuiltinApp {..}
+        | _builtinAppOp == OpFieldMul,
+          [c@(NCst (Constant _ (ConstField f))), _] <- _builtinAppArgs,
+          fieldToInteger f == 0 ->
+            c
+      NBlt BuiltinApp {..}
+        | _builtinAppOp == OpFieldMul,
+          [x, NCst (Constant _ (ConstField f))] <- _builtinAppArgs,
+          fieldToInteger f == 1 ->
+            x
+      NBlt BuiltinApp {..}
+        | _builtinAppOp == OpFieldMul,
+          [NCst (Constant _ (ConstField f)), x] <- _builtinAppArgs,
+          fieldToInteger f == 1 ->
+            x
+      NBlt BuiltinApp {..}
+        | _builtinAppOp == OpFieldDiv,
+          [x, NCst (Constant _ (ConstField f))] <- _builtinAppArgs,
+          fieldToInteger f == 1 ->
+            x
      _ -> node

 simplifyArithmetic :: Module -> Module
--- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs
@ -559,6 +559,7 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive
      Internal.BuiltinBoolPrint -> return ()
      Internal.BuiltinIOSequence -> return ()
      Internal.BuiltinIOReadline -> return ()
+      Internal.BuiltinField -> registerInductiveAxiom (Just BuiltinField) []
      Internal.BuiltinString -> registerInductiveAxiom (Just BuiltinString) []
      Internal.BuiltinIO -> registerInductiveAxiom (Just BuiltinIO) builtinIOConstrs
      Internal.BuiltinTrace -> return ()
@ -569,6 +570,13 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive
      Internal.BuiltinNatToString -> return ()
      Internal.BuiltinIntToString -> return ()
      Internal.BuiltinIntPrint -> return ()
+      Internal.BuiltinFieldEq -> return ()
+      Internal.BuiltinFieldAdd -> return ()
+      Internal.BuiltinFieldSub -> return ()
+      Internal.BuiltinFieldMul -> return ()
+      Internal.BuiltinFieldDiv -> return ()
+      Internal.BuiltinFieldFromInt -> return ()
+      Internal.BuiltinFieldToNat -> return ()

    registerInductiveAxiom :: Maybe BuiltinAxiom -> [(Tag, Text, Type -> Type, Maybe BuiltinConstructor)] -> Sem r ()
    registerInductiveAxiom ax ctrs = do
@ -649,6 +657,21 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin)
        natName <- getNatName
        natSym <- getNatSymbol
        registerAxiomDef (mkLambda' (mkTypeConstr (setInfoName natName mempty) natSym []) (mkBuiltinApp' OpShow [mkVar' 0]))
+      Internal.BuiltinField -> return ()
+      Internal.BuiltinFieldEq ->
+        registerAxiomDef (mkLambda' mkTypeField' (mkLambda' mkTypeField' (mkBuiltinApp' OpEq [mkVar' 1, mkVar' 0])))
+      Internal.BuiltinFieldAdd ->
+        registerAxiomDef (mkLambda' mkTypeField' (mkLambda' mkTypeField' (mkBuiltinApp' OpFieldAdd [mkVar' 1, mkVar' 0])))
+      Internal.BuiltinFieldSub ->
+        registerAxiomDef (mkLambda' mkTypeField' (mkLambda' mkTypeField' (mkBuiltinApp' OpFieldSub [mkVar' 1, mkVar' 0])))
+      Internal.BuiltinFieldMul ->
+        registerAxiomDef (mkLambda' mkTypeField' (mkLambda' mkTypeField' (mkBuiltinApp' OpFieldMul [mkVar' 1, mkVar' 0])))
+      Internal.BuiltinFieldDiv ->
+        registerAxiomDef (mkLambda' mkTypeField' (mkLambda' mkTypeField' (mkBuiltinApp' OpFieldDiv [mkVar' 1, mkVar' 0])))
+      Internal.BuiltinFieldFromInt ->
+        registerAxiomDef (mkLambda' mkTypeInteger' (mkBuiltinApp' OpFieldFromInt [mkVar' 0]))
+      Internal.BuiltinFieldToNat ->
+        registerAxiomDef (mkLambda' mkTypeField' (mkBuiltinApp' OpFieldToInt [mkVar' 0]))
      Internal.BuiltinString -> return ()
      Internal.BuiltinIO -> return ()
      Internal.BuiltinTrace -> return ()
@ -1025,6 +1048,18 @@ goApplication a = do
        Just Internal.BuiltinFail -> app
        Just Internal.BuiltinIntToString -> app
        Just Internal.BuiltinIntPrint -> app
+        Just Internal.BuiltinField -> app
+        Just Internal.BuiltinFieldEq -> app
+        Just Internal.BuiltinFieldAdd -> app
+        Just Internal.BuiltinFieldSub -> app
+        Just Internal.BuiltinFieldMul -> app
+        Just Internal.BuiltinFieldDiv -> app
+        Just Internal.BuiltinFieldFromInt -> do
+          as <- exprArgs
+          case as of
+            [x] -> return $ mkBuiltinApp' OpFieldFromInt [x]
+            _ -> app
+        Just Internal.BuiltinFieldToNat -> app
        Nothing -> app
    Internal.ExpressionIden (Internal.IdenFunction n) -> do
      funInfoBuiltin <- Internal.getFunctionBuiltinInfo n
--- a/src/Juvix/Compiler/Core/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromSource.hs
@ -17,6 +17,7 @@ import Juvix.Compiler.Core.Info.LocationInfo as LocationInfo
 import Juvix.Compiler.Core.Info.NameInfo as NameInfo
 import Juvix.Compiler.Core.Transformation.Eta
 import Juvix.Compiler.Core.Translation.FromSource.Lexer
+import Juvix.Data.Field
 import Juvix.Extra.Strings qualified as Str
 import Juvix.Parser.Error
 import Text.Megaparsec qualified as P
@ -559,6 +560,10 @@ builtinAppExpr varsNum vars = do
      <|> (kw kwDiv $> OpIntDiv)
      <|> (kw kwMul $> OpIntMul)
      <|> (kw kwMod $> OpIntMod)
+      <|> (kw kwFieldAdd $> OpFieldAdd)
+      <|> (kw kwFieldSub $> OpFieldSub)
+      <|> (kw kwFieldMul $> OpFieldMul)
+      <|> (kw kwFieldDiv $> OpFieldDiv)
      <|> (kw kwShow $> OpShow)
      <|> (kw kwStrConcat $> OpStrConcat)
      <|> (kw kwStrToInt $> OpStrToInt)
@ -583,7 +588,8 @@ atom ::
  HashMap Text Level ->
  ParsecS r Node
 atom varsNum vars =
-  exprConstInt
+  exprConstField
+    <|> exprConstInt
    <|> exprConstString
    <|> exprUniverse
    <|> exprDynamic
@ -609,6 +615,11 @@ exprConstString = P.try $ do
  (s, i) <- string
  return $ mkConstant (Info.singleton (LocationInfo i)) (ConstString s)

+exprConstField :: ParsecS r Node
+exprConstField = P.try $ do
+  (n, i) <- field
+  return $ mkConstant (Info.singleton (LocationInfo i)) (ConstField (fieldFromInteger defaultFieldSize n))
+
 exprUniverse :: ParsecS r Type
 exprUniverse = do
  kw kwType
@ -1090,6 +1101,7 @@ exprNamed varsNum vars = do
  (txt, i) <- identifierL
  case txt of
    "Int" -> return mkTypeInteger'
+    "Field" -> return mkTypeField'
    "String" -> return mkTypeString'
    _ ->
      case HashMap.lookup txt vars of
--- a/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs
@ -30,6 +30,9 @@ kw = void . lexeme . kw'
 decimal :: (Num n) => ParsecS r (n, Interval)
 decimal = lexemeInterval L.decimal

+field :: ParsecS r (Integer, Interval)
+field = lexemeInterval field'
+
 integer :: ParsecS r (Integer, Interval)
 integer = integer' decimal

--- a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
+++ b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
@ -9,13 +9,14 @@ import Juvix.Compiler.Core.Info.NameInfo
 import Juvix.Compiler.Core.Language.Stripped qualified as Stripped
 import Juvix.Compiler.Core.Pretty

-fromCore :: InfoTable -> Stripped.InfoTable
-fromCore tab =
+fromCore :: Natural -> InfoTable -> Stripped.InfoTable
+fromCore fsize tab =
  Stripped.InfoTable
    { _infoMain = tab ^. infoMain,
      _infoFunctions = fmap (translateFunctionInfo tab) (tab' ^. infoIdentifiers),
      _infoInductives = fmap translateInductiveInfo (tab' ^. infoInductives),
-      _infoConstructors = fmap translateConstructorInfo (tab' ^. infoConstructors)
+      _infoConstructors = fmap translateConstructorInfo (tab' ^. infoConstructors),
+      _infoFieldSize = fsize
    }
  where
    tab' =
@ -78,6 +79,14 @@ fromCore tab =
        BuiltinStringToNat -> False
        BuiltinBoolPrint -> False
        BuiltinString -> False
+        BuiltinField -> False
+        BuiltinFieldEq -> False
+        BuiltinFieldAdd -> False
+        BuiltinFieldSub -> False
+        BuiltinFieldMul -> False
+        BuiltinFieldDiv -> False
+        BuiltinFieldFromInt -> False
+        BuiltinFieldToNat -> False
        BuiltinIOSequence -> False
        BuiltinIOReadline -> False
        BuiltinTrace -> False
--- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
@ -574,6 +574,14 @@ registerBuiltinAxiom d = \case
  BuiltinStringConcat -> registerStringConcat d
  BuiltinStringEq -> registerStringEq d
  BuiltinStringToNat -> registerStringToNat d
+  BuiltinField -> registerField d
+  BuiltinFieldEq -> registerFieldEq d
+  BuiltinFieldAdd -> registerFieldAdd d
+  BuiltinFieldSub -> registerFieldSub d
+  BuiltinFieldMul -> registerFieldMul d
+  BuiltinFieldDiv -> registerFieldDiv d
+  BuiltinFieldFromInt -> registerFieldFromInt d
+  BuiltinFieldToNat -> registerFieldToNat d
  BuiltinBoolPrint -> registerBoolPrint d
  BuiltinTrace -> registerTrace d
  BuiltinFail -> registerFail d
--- a/src/Juvix/Compiler/Nockma/Translation/FromTree.hs
+++ b/src/Juvix/Compiler/Nockma/Translation/FromTree.hs
@ -321,6 +321,7 @@ compile = \case
      Tree.ConstString {} -> stringsErr
      Tree.ConstUnit -> OpQuote # constUnit
      Tree.ConstVoid -> OpQuote # constVoid
+      Tree.ConstField {} -> fieldErr

    goSave :: Tree.NodeSave -> Sem r (Term Natural)
    goSave Tree.NodeSave {..} = do
@ -367,6 +368,8 @@ compile = \case
      Tree.OpArgsNum ->
        let getF f = getClosureField f arg
         in sub (getF ClosureTotalArgsNum) (getF ClosureArgsNum)
+      Tree.OpIntToField -> fieldErr
+      Tree.OpFieldToInt -> fieldErr

    goTrace :: Term Natural -> Sem r (Term Natural)
    goTrace arg = do
@ -395,6 +398,10 @@ compile = \case
          Tree.OpIntLe -> return (callStdlib StdlibLe args)
          Tree.OpEq -> testEq _nodeBinopArg1 _nodeBinopArg2
          Tree.OpStrConcat -> stringsErr
+          Tree.OpFieldAdd -> fieldErr
+          Tree.OpFieldSub -> fieldErr
+          Tree.OpFieldMul -> fieldErr
+          Tree.OpFieldDiv -> fieldErr

    goAllocClosure :: Tree.NodeAllocClosure -> Sem r (Term Natural)
    goAllocClosure Tree.NodeAllocClosure {..} = do
@ -554,6 +561,9 @@ unsupported thing = error ("The Nockma backend does not support " <> thing)
 stringsErr :: a
 stringsErr = unsupported "strings"

+fieldErr :: a
+fieldErr = unsupported "the field type"
+
 -- | Computes a - b
 sub :: Term Natural -> Term Natural -> Term Natural
 sub a b = callStdlib StdlibSub [a, b]
--- a/src/Juvix/Compiler/Pipeline.hs
+++ b/src/Juvix/Compiler/Pipeline.hs
@ -130,19 +130,16 @@ upToCoreTypecheck ::
 upToCoreTypecheck =
  upToCore >>= \r -> Core.toTypechecked (r ^. Core.coreResultModule) >>= \md -> return r {Core._coreResultModule = md}

--------------------------------------------------------------------------------
-- Workflows from stripped Core
--------------------------------------------------------------------------------
-
-strippedCoreToTree :: Core.Module -> Sem r Tree.InfoTable
-strippedCoreToTree = return . Tree.fromCore . Stripped.fromCore . Core.computeCombinedInfoTable
-
 --------------------------------------------------------------------------------
 -- Workflows from stored Core
 --------------------------------------------------------------------------------

 storedCoreToTree :: (Members '[Error JuvixError, Reader EntryPoint] r) => Core.TransformationId -> Core.Module -> Sem r Tree.InfoTable
-storedCoreToTree checkId = Core.toStripped checkId >=> strippedCoreToTree
+storedCoreToTree checkId md = do
+  fsize <- asks (^. entryPointFieldSize)
+  Core.toStripped checkId
+    >=> return . Tree.fromCore . Stripped.fromCore fsize . Core.computeCombinedInfoTable
+    $ md

 storedCoreToAnoma :: (Members '[Error JuvixError, Reader EntryPoint] r) => Core.Module -> Sem r (Nockma.Cell Natural)
 storedCoreToAnoma = storedCoreToTree Core.CheckAnoma >=> treeToAnoma
--- a/src/Juvix/Compiler/Pipeline/Driver.hs
+++ b/src/Juvix/Compiler/Pipeline/Driver.hs
@ -206,7 +206,8 @@ processModule' (EntryIndex entry) = do
  case m of
    Just info
      | info ^. Store.moduleInfoSHA256 == sha256
-          && info ^. Store.moduleInfoOptions == opts -> do
+          && info ^. Store.moduleInfoOptions == opts
+          && info ^. Store.moduleInfoFieldSize == entry ^. entryPointFieldSize -> do
          (changed, mtab) <- processImports'' entry (info ^. Store.moduleInfoImports)
          -- We need to check whether any of the recursive imports is fragile,
          -- not only the direct ones, because identifiers may be re-exported
@ -247,7 +248,8 @@ processModule'' sha256 entry = over pipelineResult mkModuleInfo <$> processFileT
          _moduleInfoImports = map (^. importModulePath) $ scoperResult ^. Scoper.resultParserResult . Parser.resultParserState . parserStateImports,
          _moduleInfoOptions = StoredOptions.fromEntryPoint entry,
          _moduleInfoFragile = Core.moduleIsFragile _coreResultModule,
-          _moduleInfoSHA256 = sha256
+          _moduleInfoSHA256 = sha256,
+          _moduleInfoFieldSize = entry ^. entryPointFieldSize
        }
      where
        scoperResult = _coreResultInternalTypedResult ^. InternalTyped.resultInternal . Internal.resultScoper
--- a/src/Juvix/Compiler/Pipeline/EntryPoint.hs
+++ b/src/Juvix/Compiler/Pipeline/EntryPoint.hs
@ -7,6 +7,7 @@ where
 import Juvix.Compiler.Backend
 import Juvix.Compiler.Pipeline.Package.Base
 import Juvix.Compiler.Pipeline.Root.Base
+import Juvix.Data.Field
 import Juvix.Prelude

 -- | An option specifying how symbols should be pruned in the Internal to Core translation
@ -38,7 +39,8 @@ data EntryPoint = EntryPoint
    _entryPointGenericOptions :: GenericOptions,
    _entryPointModulePath :: Maybe (Path Abs File),
    _entryPointSymbolPruningMode :: SymbolPruningMode,
-    _entryPointOffline :: Bool
+    _entryPointOffline :: Bool,
+    _entryPointFieldSize :: Natural
  }
  deriving stock (Eq, Show)

@ -72,7 +74,8 @@ defaultEntryPointNoFile pkg root =
      _entryPointInliningDepth = defaultInliningDepth,
      _entryPointModulePath = Nothing,
      _entryPointSymbolPruningMode = FilterUnreachable,
-      _entryPointOffline = False
+      _entryPointOffline = False,
+      _entryPointFieldSize = defaultFieldSize
    }

 defaultUnrollLimit :: Int
--- a/src/Juvix/Compiler/Pipeline/Package/Loader/EvalEff/IO.hs
+++ b/src/Juvix/Compiler/Pipeline/Package/Loader/EvalEff/IO.hs
@ -71,7 +71,7 @@ runEvalFileEffIO = interpretScopedAs allocator handler

        evalNode :: Node -> Sem r Node
        evalNode n = do
-          n' <- doEval False packageLoc tab n
+          n' <- doEval Nothing False packageLoc tab n
          case n' of
            Left e -> do
              throw
--- a/src/Juvix/Compiler/Reg/Interpreter.hs
+++ b/src/Juvix/Compiler/Reg/Interpreter.hs
@ -68,6 +68,7 @@ runFunction hout infoTable args0 info0 = do
    readConst :: Constant -> Val
    readConst = \case
      ConstInt i -> ValInteger i
+      ConstField f -> ValField f
      ConstBool b -> ValBool b
      ConstString s -> ValString s
      ConstUnit -> ValUnit
--- a/src/Juvix/Compiler/Reg/Keywords.hs
+++ b/src/Juvix/Compiler/Reg/Keywords.hs
@ -6,7 +6,43 @@ module Juvix.Compiler.Reg.Keywords
 where

 import Juvix.Compiler.Tree.Keywords.Base
-import Juvix.Data.Keyword.All (kwAdd_, kwAlloc, kwArgsNum, kwAtoi, kwBr, kwCAlloc, kwCCall, kwCCallTail, kwCExtend, kwCall, kwCallTail, kwCase, kwDefault, kwDiv_, kwDollar, kwDump, kwEq, kwEq_, kwFail, kwLe_, kwLive, kwLt_, kwMod_, kwMul_, kwNop, kwPrealloc, kwRet, kwShow, kwStrcat, kwSub_, kwTrace)
+import Juvix.Data.Keyword.All
+  ( kwAdd_,
+    kwAlloc,
+    kwArgsNum,
+    kwAtoi,
+    kwBr,
+    kwCAlloc,
+    kwCCall,
+    kwCCallTail,
+    kwCExtend,
+    kwCall,
+    kwCallTail,
+    kwCase,
+    kwDefault,
+    kwDiv_,
+    kwDollar,
+    kwDump,
+    kwEq,
+    kwEq_,
+    kwFail,
+    kwFieldAdd,
+    kwFieldDiv,
+    kwFieldMul,
+    kwFieldSub,
+    kwLe_,
+    kwLive,
+    kwLt_,
+    kwMod_,
+    kwMul_,
+    kwNop,
+    kwPrealloc,
+    kwRet,
+    kwShow,
+    kwStrcat,
+    kwSub_,
+    kwTrace,
+  )
 import Juvix.Prelude

 allKeywordStrings :: HashSet Text
@ -24,6 +60,10 @@ allKeywords =
         kwLt_,
         kwLe_,
         kwEq_,
+         kwFieldAdd,
+         kwFieldDiv,
+         kwFieldMul,
+         kwFieldSub,
         kwStrcat,
         kwEq,
         kwShow,
--- a/src/Juvix/Compiler/Reg/Translation/FromAsm.hs
+++ b/src/Juvix/Compiler/Reg/Translation/FromAsm.hs
@ -14,7 +14,8 @@ fromAsm tab =
    { _infoFunctions = HashMap.map convertFun (tab ^. Asm.infoFunctions),
      _infoConstrs = HashMap.map convertConstr (tab ^. Asm.infoConstrs),
      _infoInductives = HashMap.map convertInductive (tab ^. Asm.infoInductives),
-      _infoMainFunction = tab ^. Asm.infoMainFunction
+      _infoMainFunction = tab ^. Asm.infoMainFunction,
+      _infoFieldSize = tab ^. Asm.infoFieldSize
    }
  where
    convertFun :: Asm.FunctionInfo -> FunctionInfo
--- a/src/Juvix/Compiler/Reg/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Reg/Translation/FromSource.hs
@ -96,6 +96,10 @@ instrBinop vref =
    <|> parseBinaryOp kwLt_ OpIntLt vref
    <|> parseBinaryOp kwLe_ OpIntLe vref
    <|> parseBinaryOp kwEq_ OpEq vref
+    <|> parseBinaryOp kwFieldAdd OpFieldAdd vref
+    <|> parseBinaryOp kwFieldSub OpFieldSub vref
+    <|> parseBinaryOp kwFieldMul OpFieldMul vref
+    <|> parseBinaryOp kwFieldDiv OpFieldDiv vref
    <|> parseBinaryOp kwStrcat OpStrConcat vref

 parseBinaryOp ::
--- a/src/Juvix/Compiler/Store/Language.hs
+++ b/src/Juvix/Compiler/Store/Language.hs
@ -17,7 +17,8 @@ data ModuleInfo = ModuleInfo
    -- | True if any module depending on this module requires recompilation
    -- whenever this module is changed
    _moduleInfoFragile :: Bool,
-    _moduleInfoSHA256 :: Text
+    _moduleInfoSHA256 :: Text,
+    _moduleInfoFieldSize :: Natural
  }
  deriving stock (Generic)

--- a/src/Juvix/Compiler/Tree/Data/InfoTable/Base.hs
+++ b/src/Juvix/Compiler/Tree/Data/InfoTable/Base.hs
@ -9,12 +9,14 @@ import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Tree.Language
 import Juvix.Compiler.Tree.Language.Rep
 import Juvix.Compiler.Tree.Language.Type
+import Juvix.Data.Field

 data InfoTable' code extra = InfoTable
  { _infoFunctions :: HashMap Symbol (FunctionInfo' code extra),
    _infoConstrs :: HashMap Tag ConstructorInfo,
    _infoInductives :: HashMap Symbol InductiveInfo,
-    _infoMainFunction :: Maybe Symbol
+    _infoMainFunction :: Maybe Symbol,
+    _infoFieldSize :: Natural
  }

 data FunctionInfo' code extra = FunctionInfo
@ -70,7 +72,8 @@ emptyInfoTable =
    { _infoFunctions = mempty,
      _infoConstrs = mempty,
      _infoInductives = mempty,
-      _infoMainFunction = Nothing
+      _infoMainFunction = Nothing,
+      _infoFieldSize = defaultFieldSize
    }

 lookupFunInfo :: InfoTable' a e -> Symbol -> FunctionInfo' a e
--- a/src/Juvix/Compiler/Tree/Evaluator.hs
+++ b/src/Juvix/Compiler/Tree/Evaluator.hs
@ -83,6 +83,7 @@ hEval hout tab = eval' [] mempty
        goConstant :: NodeConstant -> Value
        goConstant NodeConstant {..} = case _nodeConstant of
          ConstInt i -> ValInteger i
+          ConstField f -> ValField f
          ConstBool b -> ValBool b
          ConstString s -> ValString s
          ConstUnit -> ValUnit
@ -215,6 +216,7 @@ hEval hout tab = eval' [] mempty
 valueToNode :: Value -> Node
 valueToNode = \case
  ValInteger i -> mkConst $ ConstInt i
+  ValField f -> mkConst $ ConstField f
  ValBool b -> mkConst $ ConstBool b
  ValString s -> mkConst $ ConstString s
  ValUnit -> mkConst ConstUnit
--- a/src/Juvix/Compiler/Tree/Evaluator/Builtins.hs
+++ b/src/Juvix/Compiler/Tree/Evaluator/Builtins.hs
@ -4,6 +4,7 @@ import Juvix.Compiler.Tree.Data.InfoTable.Base
 import Juvix.Compiler.Tree.Language.Builtins
 import Juvix.Compiler.Tree.Language.Value
 import Juvix.Compiler.Tree.Pretty.Base
+import Juvix.Data.Field
 import Juvix.Data.PPOutput
 import Juvix.Prelude
 import Text.Read qualified as T
@ -23,6 +24,13 @@ evalBinop op arg1 arg2 = case op of
    | otherwise -> goIntBinop rem arg1 arg2
  OpIntLe -> goIntCmpBinop (<=) arg1 arg2
  OpIntLt -> goIntCmpBinop (<) arg1 arg2
+  OpFieldAdd -> goFieldBinop fieldAdd arg1 arg2
+  OpFieldSub -> goFieldBinop fieldSub arg1 arg2
+  OpFieldMul -> goFieldBinop fieldMul arg1 arg2
+  OpFieldDiv -> case arg2 of
+    ValField arg2'
+      | fieldToInteger arg2' == 0 -> Left "division by zero"
+    _ -> goFieldBinop fieldDiv arg1 arg2
  OpEq
    | arg1 == arg2 -> Right $ ValBool True
    | otherwise -> Right $ ValBool False
@ -38,6 +46,11 @@ evalBinop op arg1 arg2 = case op of
      (ValInteger i1, ValInteger i2) -> Right $ ValBool (f i1 i2)
      _ -> Left "expected two integer arguments"

+    goFieldBinop :: (FField -> FField -> FField) -> Value -> Value -> Either ErrorMsg Value
+    goFieldBinop f v1 v2 = case (v1, v2) of
+      (ValField i1, ValField i2) -> Right $ ValField (f i1 i2)
+      _ -> Left "expected two field elements as arguments"
+
    goStrConcat :: Value -> Value -> Either ErrorMsg Value
    goStrConcat v1 v2 = case (v1, v2) of
      (ValString s1, ValString s2) -> Right $ ValString (s1 <> s2)
@ -47,6 +60,8 @@ evalUnop :: InfoTable' t e -> UnaryOp -> Value -> Either ErrorMsg Value
 evalUnop tab op v = case op of
  OpShow -> Right $ ValString (printValue tab v)
  OpStrToInt -> goStringUnop strToInt v
+  OpFieldToInt -> goFieldToInt v
+  OpIntToField -> goIntToField v
  OpArgsNum -> goArgsNum v
  where
    strToInt :: Text -> Either ErrorMsg Value
@ -71,6 +86,20 @@ evalUnop tab op v = case op of
      _ ->
        Left "expected a closure"

+    goFieldToInt :: Value -> Either ErrorMsg Value
+    goFieldToInt = \case
+      ValField f ->
+        Right $ ValInteger $ fieldToInteger f
+      _ ->
+        Left "expected a field element"
+
+    goIntToField :: Value -> Either ErrorMsg Value
+    goIntToField = \case
+      ValInteger i ->
+        Right $ ValField $ fieldFromInteger (tab ^. infoFieldSize) i
+      _ ->
+        Left "expected an integer"
+
 printValue :: InfoTable' t e -> Value -> Text
 printValue tab = \case
  ValString s -> s
--- a/src/Juvix/Compiler/Tree/EvaluatorEff.hs
+++ b/src/Juvix/Compiler/Tree/EvaluatorEff.hs
@ -79,6 +79,7 @@ eval tab = E.runReader emptyEvalCtx . eval'
        goConstant :: NodeConstant -> Value
        goConstant NodeConstant {..} = case _nodeConstant of
          ConstInt i -> ValInteger i
+          ConstField f -> ValField f
          ConstBool b -> ValBool b
          ConstString s -> ValString s
          ConstUnit -> ValUnit
--- a/src/Juvix/Compiler/Tree/EvaluatorSem.hs
+++ b/src/Juvix/Compiler/Tree/EvaluatorSem.hs
@ -77,6 +77,7 @@ eval tab = runReader emptyEvalCtx . eval'
        goConstant :: NodeConstant -> Value
        goConstant NodeConstant {..} = case _nodeConstant of
          ConstInt i -> ValInteger i
+          ConstField f -> ValField f
          ConstBool b -> ValBool b
          ConstString s -> ValString s
          ConstUnit -> ValUnit
--- a/src/Juvix/Compiler/Tree/Extra/Type.hs
+++ b/src/Juvix/Compiler/Tree/Extra/Type.hs
@ -76,6 +76,7 @@ isSubtype ty1 ty2 = case (ty1, ty2) of
      checkBounds cmp (Just x) (Just y) = cmp x y
  (TyBool {}, TyBool {}) -> True
  (TyString, TyString) -> True
+  (TyField, TyField) -> True
  (TyUnit, TyUnit) -> True
  (TyVoid, TyVoid) -> True
  (TyInductive {}, TyInductive {}) -> ty1 == ty2
@ -87,6 +88,8 @@ isSubtype ty1 ty2 = case (ty1, ty2) of
  (_, TyInteger {}) -> False
  (TyString, _) -> False
  (_, TyString) -> False
+  (TyField, _) -> False
+  (_, TyField) -> False
  (TyBool {}, _) -> False
  (_, TyBool {}) -> False
  (TyFun {}, _) -> False
@ -142,6 +145,7 @@ unifyTypes ty1 ty2 = case (ty1, ty2) of
  (TyBool {}, TyBool {})
    | ty1 == ty2 -> return ty1
  (TyString, TyString) -> return TyString
+  (TyField, TyField) -> return TyField
  (TyUnit, TyUnit) -> return TyUnit
  (TyVoid, TyVoid) -> return TyVoid
  (TyInductive {}, TyInductive {})
@ -154,6 +158,8 @@ unifyTypes ty1 ty2 = case (ty1, ty2) of
  (_, TyInteger {}) -> err
  (TyString, _) -> err
  (_, TyString) -> err
+  (TyField, _) -> err
+  (_, TyField) -> err
  (TyBool {}, _) -> err
  (_, TyBool {}) -> err
  (TyFun {}, _) -> err
--- a/src/Juvix/Compiler/Tree/Keywords.hs
+++ b/src/Juvix/Compiler/Tree/Keywords.hs
@ -20,6 +20,10 @@ import Juvix.Data.Keyword.All
    kwDiv_,
    kwEq_,
    kwFail,
+    kwFieldAdd,
+    kwFieldDiv,
+    kwFieldMul,
+    kwFieldSub,
    kwLe_,
    kwLt_,
    kwMod_,
@ -45,6 +49,10 @@ allKeywords =
         kwDiv_,
         kwLt_,
         kwLe_,
+         kwFieldAdd,
+         kwFieldSub,
+         kwFieldMul,
+         kwFieldDiv,
         kwSeq_,
         kwEq_,
         kwStrcat,
--- a/src/Juvix/Compiler/Tree/Language/Base.hs
+++ b/src/Juvix/Compiler/Tree/Language/Base.hs
@ -5,6 +5,7 @@ module Juvix.Compiler.Tree.Language.Base
 where

 import Juvix.Compiler.Core.Language.Base
+import Juvix.Data.Field

 -- | Offset of a data field or an argument
 type Offset = Int
@ -14,6 +15,7 @@ data Constant
  = ConstInt Integer
  | ConstBool Bool
  | ConstString Text
+  | ConstField FField
  | ConstUnit
  | ConstVoid
  deriving stock (Eq)
--- a/src/Juvix/Compiler/Tree/Language/Builtins.hs
+++ b/src/Juvix/Compiler/Tree/Language/Builtins.hs
@ -10,6 +10,10 @@ data BinaryOp
  | OpIntMod
  | OpIntLt
  | OpIntLe
+  | OpFieldAdd
+  | OpFieldSub
+  | OpFieldMul
+  | OpFieldDiv
  | OpEq
  | OpStrConcat
  deriving stock (Eq)
@ -19,6 +23,10 @@ data UnaryOp
    OpShow
  | -- | Convert a string to an integer. JV* opcode: `atoi`.
    OpStrToInt
+  | -- | Convert an integer to a field element. JV* opcode: `itof`.
+    OpIntToField
+  | -- | Convert a field element to an integer. JV* opcode: `ftoi`.
+    OpFieldToInt
  | -- | Compute the number of expected arguments for the given closure. JV*
    -- opcode: `argsnum`.
    OpArgsNum
--- a/src/Juvix/Compiler/Tree/Language/Type.hs
+++ b/src/Juvix/Compiler/Tree/Language/Type.hs
@ -7,6 +7,7 @@ data Type
  | TyInteger TypeInteger
  | TyBool TypeBool
  | TyString
+  | TyField
  | TyUnit
  | TyVoid
  | TyInductive TypeInductive
@ -77,6 +78,7 @@ instance HasAtomicity Type where
    TyInteger x -> atomicity x
    TyBool x -> atomicity x
    TyString -> Atom
+    TyField -> Atom
    TyUnit -> Atom
    TyVoid -> Atom
    TyInductive x -> atomicity x
--- a/src/Juvix/Compiler/Tree/Language/Value.hs
+++ b/src/Juvix/Compiler/Tree/Language/Value.hs
@ -1,11 +1,13 @@
 module Juvix.Compiler.Tree.Language.Value where

 import Juvix.Compiler.Tree.Language.Base
+import Juvix.Data.Field

 {-
  A value may be one of:

  - Integer (arbitrary precision)
+  - Field element
  - Boolean
  - String
  - Constructor data
@ -14,6 +16,7 @@ import Juvix.Compiler.Tree.Language.Base

 data Value
  = ValInteger Integer
+  | ValField FField
  | ValBool Bool
  | ValString Text
  | ValUnit
@ -50,6 +53,7 @@ instance HasAtomicity Closure where
 instance HasAtomicity Value where
  atomicity = \case
    ValInteger {} -> Atom
+    ValField {} -> Atom
    ValBool {} -> Atom
    ValString {} -> Atom
    ValUnit -> Atom
--- a/src/Juvix/Compiler/Tree/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Tree/Pretty/Base.hs
@ -83,6 +83,8 @@ instance PrettyCode Value where
  ppCode = \case
    ValInteger i ->
      return $ integer i
+    ValField i ->
+      return $ integer i
    ValBool True ->
      return $ annotate (AnnKind KNameConstructor) (pretty (Str.true_ :: String))
    ValBool False ->
@ -137,6 +139,8 @@ instance PrettyCode Type where
      return $ annotate (AnnKind KNameInductive) Str.mul
    TyInteger {} ->
      return $ annotate (AnnKind KNameInductive) Str.integer
+    TyField {} ->
+      return $ annotate (AnnKind KNameInductive) Str.field
    TyBool {} ->
      return $ annotate (AnnKind KNameInductive) Str.bool
    TyString ->
@ -181,6 +185,8 @@ instance PrettyCode Constant where
  ppCode = \case
    ConstInt v ->
      return $ annotate AnnLiteralInteger (pretty v)
+    ConstField v ->
+      return $ annotate AnnLiteralInteger (pretty v <> "F")
    ConstBool True ->
      return $ annotate (AnnKind KNameConstructor) Str.true_
    ConstBool False ->
@ -201,6 +207,10 @@ instance PrettyCode BinaryOp where
    OpIntMod -> Str.instrMod
    OpIntLt -> Str.instrLt
    OpIntLe -> Str.instrLe
+    OpFieldAdd -> Str.fadd
+    OpFieldSub -> Str.fsub
+    OpFieldMul -> Str.fmul
+    OpFieldDiv -> Str.fdiv
    OpEq -> Str.instrEq
    OpStrConcat -> Str.instrStrConcat

@ -220,6 +230,8 @@ instance PrettyCode UnaryOp where
  ppCode op = return $ primitive $ case op of
    OpShow -> Str.instrShow
    OpStrToInt -> Str.instrStrToInt
+    OpFieldToInt -> Str.instrFieldToInt
+    OpIntToField -> Str.instrIntToField
    OpArgsNum -> Str.instrArgsNum

 instance PrettyCode UnaryOpcode where
--- a/src/Juvix/Compiler/Tree/Transformation/Validate.hs
+++ b/src/Juvix/Compiler/Tree/Transformation/Validate.hs
@ -52,6 +52,10 @@ inferType tab funInfo = goInfer mempty
          OpIntMod -> checkBinop mkTypeInteger mkTypeInteger mkTypeInteger
          OpIntLt -> checkBinop mkTypeInteger mkTypeInteger mkTypeBool
          OpIntLe -> checkBinop mkTypeInteger mkTypeInteger mkTypeBool
+          OpFieldAdd -> checkBinop TyField TyField TyField
+          OpFieldSub -> checkBinop TyField TyField TyField
+          OpFieldMul -> checkBinop TyField TyField TyField
+          OpFieldDiv -> checkBinop TyField TyField TyField
          OpEq -> checkBinop TyDynamic TyDynamic mkTypeBool
          OpStrConcat -> checkBinop TyString TyString TyString

@ -74,12 +78,15 @@ inferType tab funInfo = goInfer mempty
          OpShow -> checkUnop TyDynamic TyString
          OpStrToInt -> checkUnop TyString mkTypeInteger
          OpArgsNum -> checkUnop TyDynamic mkTypeInteger
+          OpIntToField -> checkUnop mkTypeInteger TyField
+          OpFieldToInt -> checkUnop TyField mkTypeInteger

    goConst :: BinderList Type -> NodeConstant -> Sem r Type
    goConst _ NodeConstant {..} = case _nodeConstant of
      ConstInt {} -> return mkTypeInteger
      ConstBool {} -> return mkTypeBool
      ConstString {} -> return TyString
+      ConstField {} -> return TyField
      ConstUnit {} -> return TyUnit
      ConstVoid {} -> return TyVoid

--- a/src/Juvix/Compiler/Tree/Translation/FromAsm.hs
+++ b/src/Juvix/Compiler/Tree/Translation/FromAsm.hs
@ -23,7 +23,8 @@ fromAsm tab = do
      { _infoMainFunction = tab ^. Asm.infoMainFunction,
        _infoFunctions = fns,
        _infoInductives = tab ^. Asm.infoInductives,
-        _infoConstrs = tab ^. Asm.infoConstrs
+        _infoConstrs = tab ^. Asm.infoConstrs,
+        _infoFieldSize = tab ^. Asm.infoFieldSize
      }

 goFunction :: (Member (Error TreeError) r') => Asm.InfoTable -> Asm.FunctionInfo -> Sem r' FunctionInfo
--- a/src/Juvix/Compiler/Tree/Translation/FromCore.hs
+++ b/src/Juvix/Compiler/Tree/Translation/FromCore.hs
@ -17,7 +17,8 @@ fromCore tab =
    { _infoMainFunction = tab ^. Core.infoMain,
      _infoFunctions = genCode tab <$> tab ^. Core.infoFunctions,
      _infoInductives = translateInductiveInfo <$> tab ^. Core.infoInductives,
-      _infoConstrs = translateConstructorInfo <$> tab ^. Core.infoConstructors
+      _infoConstrs = translateConstructorInfo <$> tab ^. Core.infoConstructors,
+      _infoFieldSize = tab ^. Core.infoFieldSize
    }

 -- Generate code for a single function.
@ -82,6 +83,8 @@ genCode infoTable fi =
        mkConst (ConstInt i)
      Core.Constant _ (Core.ConstString s) ->
        mkConst (ConstString s)
+      Core.Constant _ (Core.ConstField fld) ->
+        mkConst (ConstField fld)

    goApps :: Int -> BinderList MemRef -> Core.Apps -> Node
    goApps tempSize refs Core.Apps {..} =
@ -268,6 +271,10 @@ genCode infoTable fi =
      Core.OpIntMod -> PrimBinop OpIntMod
      Core.OpIntLt -> PrimBinop OpIntLt
      Core.OpIntLe -> PrimBinop OpIntLe
+      Core.OpFieldAdd -> PrimBinop OpFieldAdd
+      Core.OpFieldSub -> PrimBinop OpFieldSub
+      Core.OpFieldMul -> PrimBinop OpFieldMul
+      Core.OpFieldDiv -> PrimBinop OpFieldDiv
      Core.OpEq -> PrimBinop OpEq
      Core.OpStrConcat -> PrimBinop OpStrConcat
      Core.OpSeq -> OpSeq
@ -277,6 +284,8 @@ genCode infoTable fi =
    genUnOp = \case
      Core.OpShow -> PrimUnop OpShow
      Core.OpStrToInt -> PrimUnop OpStrToInt
+      Core.OpFieldFromInt -> PrimUnop OpIntToField
+      Core.OpFieldToInt -> PrimUnop OpFieldToInt
      Core.OpTrace -> OpTrace
      Core.OpFail -> OpFail
      _ -> impossible
@ -314,6 +323,8 @@ convertPrimitiveType = \case
    TyBool (TypeBool _infoTrueTag _infoFalseTag)
  Core.PrimString ->
    TyString
+  Core.PrimField ->
+    TyField

 -- | `convertNestedType` ensures that the conversion of a type with Dynamic in the
 -- target is curried. The result of `convertType 0 ty` is always uncurried.
--- a/src/Juvix/Compiler/Tree/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Tree/Translation/FromSource.hs
@ -75,6 +75,10 @@ parseBinop =
    <|> parseBinaryOp kwMod_ (PrimBinop OpIntMod)
    <|> parseBinaryOp kwLt_ (PrimBinop OpIntLt)
    <|> parseBinaryOp kwLe_ (PrimBinop OpIntLe)
+    <|> parseBinaryOp kwFieldAdd (PrimBinop OpFieldAdd)
+    <|> parseBinaryOp kwFieldSub (PrimBinop OpFieldSub)
+    <|> parseBinaryOp kwFieldMul (PrimBinop OpFieldMul)
+    <|> parseBinaryOp kwFieldDiv (PrimBinop OpFieldDiv)
    <|> parseBinaryOp kwEq_ (PrimBinop OpEq)
    <|> parseBinaryOp kwStrcat (PrimBinop OpStrConcat)
    <|> parseBinaryOp kwSeq_ OpSeq
--- a/src/Juvix/Compiler/Tree/Translation/FromSource/Base.hs
+++ b/src/Juvix/Compiler/Tree/Translation/FromSource/Base.hs
@ -23,6 +23,7 @@ import Juvix.Compiler.Tree.Keywords.Base
 import Juvix.Compiler.Tree.Language.Base
 import Juvix.Compiler.Tree.Translation.FromSource.Lexer.Base
 import Juvix.Compiler.Tree.Translation.FromSource.Sig
+import Juvix.Data.Field
 import Juvix.Parser.Error
 import Text.Megaparsec qualified as P

@ -306,6 +307,7 @@ typeNamed = do
  txt <- identifier @t @e @d
  case txt of
    "integer" -> return mkTypeInteger
+    "field" -> return TyField
    "bool" -> return mkTypeBool
    "string" -> return TyString
    "unit" -> return TyUnit
@ -316,7 +318,12 @@ typeNamed = do
        _ -> parseFailure off ("not a type: " ++ fromText txt)

 constant :: ParsecS r Constant
-constant = integerValue <|> boolValue <|> stringValue <|> unitValue <|> voidValue
+constant = fieldValue <|> integerValue <|> boolValue <|> stringValue <|> unitValue <|> voidValue
+
+fieldValue :: ParsecS r Constant
+fieldValue = P.try $ do
+  (i, _) <- field
+  return $ ConstField (fieldFromInteger defaultFieldSize i)

 integerValue :: ParsecS r Constant
 integerValue = do
--- a/src/Juvix/Compiler/Tree/Translation/FromSource/Lexer/Base.hs
+++ b/src/Juvix/Compiler/Tree/Translation/FromSource/Lexer/Base.hs
@ -31,6 +31,9 @@ integer = integer' decimal
 number :: Int -> Int -> ParsecS r (Int, Interval)
 number = number' integer

+field :: ParsecS r (Integer, Interval)
+field = lexemeInterval field'
+
 string :: ParsecS r (Text, Interval)
 string = lexemeInterval string'

--- a/src/Juvix/Data/Field.hs
+++ b/src/Juvix/Data/Field.hs
@ -0,0 +1,106 @@
+module Juvix.Data.Field where
+
+import Data.Serialize as S
+import Data.Singletons.Decide
+import GHC.Show qualified as S
+import GHC.TypeLits.Singletons ()
+import Juvix.Data.FiniteField.PrimeField
+import Juvix.Prelude hiding (toInteger)
+import Juvix.Prelude.Pretty
+
+newtype FField = FField
+  { _unFField :: Sigma Natural (TyCon1 PrimeField)
+  }
+  deriving stock (Generic)
+
+makeLenses ''FField
+
+defaultFieldSize :: Natural
+defaultFieldSize = smallFieldSize
+
+cairoFieldSize :: Natural
+cairoFieldSize = 3618502788666131213697322783095070105623107215331596699973092056135872020481
+
+smallFieldSize :: Natural
+smallFieldSize = 2147483647
+
+allowedFieldSizes :: [Natural]
+allowedFieldSizes = [11, smallFieldSize, cairoFieldSize]
+
+instance Serialize FField where
+  put f = S.put (fieldSize f, fieldToInteger f)
+
+  get = do
+    (n, f) <- S.get
+    return $ fieldFromInteger n f
+
+instance Pretty FField where
+  pretty (FField (_ :&: f)) = pretty (toInteger f)
+
+instance Show FField where
+  show (FField (_ :&: f)) = show (toInteger f)
+
+fieldAdd :: FField -> FField -> FField
+fieldAdd
+  (FField ((n1 :: Sing (p :: Natural)) :&: (f1 :: PrimeField p)))
+  (FField ((n2 :: Sing (r :: Natural)) :&: (f2 :: PrimeField r))) =
+    let x = decideEquality n1 n2
+     in case x :: Maybe (p :~: r) of
+          Just Refl -> FField (n1 :&: withSingI n1 (f1 + f2))
+          Nothing -> impossible
+
+fieldSub :: FField -> FField -> FField
+fieldSub
+  (FField ((n1 :: Sing (p :: Natural)) :&: (f1 :: PrimeField p)))
+  (FField ((n2 :: Sing (r :: Natural)) :&: (f2 :: PrimeField r))) =
+    let x = decideEquality n1 n2
+     in case x :: Maybe (p :~: r) of
+          Just Refl -> FField (n1 :&: withSingI n1 (f1 - f2))
+          Nothing -> impossible
+
+fieldMul :: FField -> FField -> FField
+fieldMul
+  (FField ((n1 :: Sing (p :: Natural)) :&: (f1 :: PrimeField p)))
+  (FField ((n2 :: Sing (r :: Natural)) :&: (f2 :: PrimeField r))) =
+    let x = decideEquality n1 n2
+     in case x :: Maybe (p :~: r) of
+          Just Refl -> FField (n1 :&: withSingI n1 (f1 * f2))
+          Nothing -> impossible
+
+fieldDiv :: FField -> FField -> FField
+fieldDiv
+  (FField ((n1 :: Sing (p :: Natural)) :&: (f1 :: PrimeField p)))
+  (FField ((n2 :: Sing (r :: Natural)) :&: (f2 :: PrimeField r))) =
+    let x = decideEquality n1 n2
+     in case x :: Maybe (p :~: r) of
+          Just Refl -> FField (n1 :&: withSingI n1 (f1 / f2))
+          Nothing -> impossible
+
+fieldFromInteger :: Natural -> Integer -> FField
+fieldFromInteger fsize n =
+  FField (withSomeSing fsize $ \s -> s :&: withSingI s (fromInteger n))
+
+fieldSize :: FField -> Natural
+fieldSize
+  (FField ((n :: Sing (p :: Natural)) :&: (_ :: PrimeField p))) =
+    fromSing n
+
+fieldToInteger :: FField -> Integer
+fieldToInteger
+  (FField ((_ :: Sing (p :: Natural)) :&: (f1 :: PrimeField p))) =
+    toInteger f1
+
+fieldResize :: Natural -> FField -> FField
+fieldResize n f = fieldFromInteger n (fieldToInteger f)
+
+fieldEq :: FField -> FField -> Bool
+fieldEq
+  (FField ((n1 :: Sing (p :: Natural)) :&: (f1 :: PrimeField p)))
+  (FField ((n2 :: Sing (r :: Natural)) :&: (f2 :: PrimeField r))) =
+    let x = decideEquality n1 n2
+     in case x :: Maybe (p :~: r) of
+          Just Refl -> f1 == f2
+          Nothing -> False
+
+instance Eq FField where
+  (==) = fieldEq
--- a/src/Juvix/Data/FiniteField/Base.hs
+++ b/src/Juvix/Data/FiniteField/Base.hs
@ -0,0 +1,18 @@
+module Juvix.Data.FiniteField.Base where
+
+import Juvix.Prelude.Base
+
+class (Fractional k) => FiniteField k where
+  -- | The order is number of elements of a finite field @k@.
+  -- It of the form @p^n@, where @p@ is  prime number called the characteristic
+  -- of the field, and @n@ is a positive integer.
+  order :: k -> Integer
+
+  -- | The characteristic of a field, @p@.
+  char :: k -> Integer
+
+  -- | The inverse of Frobenius endomorphism @x@ ↦ @x^p@.
+  pthRoot :: k -> k
+
+  -- | All values of a field
+  allValues :: [k]
--- a/src/Juvix/Data/FiniteField/PrimeField.hs
+++ b/src/Juvix/Data/FiniteField/PrimeField.hs
@ -0,0 +1,142 @@
+-----------------------------------------------------------------------------
+
+-----------------------------------------------------------------------------
+
+-- |
+-- Module      :  Data.FiniteField.PrimeField
+-- Copyright   :  (c) Masahiro Sakai 2013-2014
+-- License     :  BSD-style
+--
+-- Maintainer  :  masahiro.sakai@gmail.com
+-- Stability   :  provisional
+-- Portability :  non-portable (ScopedTypeVariables, MultiParamTypeClasses, DeriveDataTypeable, TemplateHaskell, BangPatterns)
+--
+-- Finite field of prime order p, Fp = Z/pZ.
+--
+-- References:
+--
+-- * <http://en.wikipedia.org/wiki/Finite_field>
+module Juvix.Data.FiniteField.PrimeField
+  ( PrimeField,
+    toInteger,
+
+    -- * Template haskell utilities
+    -- $TH
+    primeField,
+  )
+where
+
+import Data.Hashable
+import Data.Ratio (denominator, numerator)
+import Data.Singletons
+import GHC.TypeLits
+import GHC.TypeLits.Singletons ()
+import Juvix.Data.FiniteField.Base
+import Language.Haskell.TH qualified as TH
+import Prelude hiding (toInteger)
+
+-- | Finite field of prime order p, Fp = Z/pZ.
+--
+-- NB: Primality of @p@ is assumed, but not checked.
+newtype PrimeField (p :: Natural)
+  = PrimeField Integer
+  deriving stock (Eq)
+
+-- | conversion to 'Integer'
+toInteger :: PrimeField p -> Integer
+toInteger (PrimeField a) = a
+
+toInt :: (Integral a) => PrimeField p -> a
+toInt = fromInteger . toInteger
+
+instance Show (PrimeField p) where
+  showsPrec n (PrimeField x) = showsPrec n x
+
+instance (SingI p) => Read (PrimeField p) where
+  readsPrec n s = [(fromInteger a, s') | (a, s') <- readsPrec n s]
+
+instance (SingI p) => Num (PrimeField p) where
+  PrimeField a + PrimeField b = fromInteger $ a + b
+  PrimeField a * PrimeField b = fromInteger $ a * b
+  PrimeField a - PrimeField b = fromInteger $ a - b
+  negate (PrimeField a) = fromInteger $ negate a
+  abs a = a
+  signum _ = 1
+  fromInteger a = ret
+    where
+      ret = PrimeField $ a `mod` char ret
+
+instance (SingI p) => Fractional (PrimeField p) where
+  fromRational r = fromInteger (numerator r) / fromInteger (denominator r)
+
+  --  recip a = a ^ (char a - 2 :: Integer)
+  recip x@(PrimeField a) =
+    case exgcd a p of
+      (_, r, _) -> fromInteger r
+    where
+      p :: Integer
+      p = char x
+
+instance (SingI p) => Bounded (PrimeField p) where
+  minBound = PrimeField 0
+  maxBound = ret
+    where
+      ret :: PrimeField p
+      ret = PrimeField (char ret - 1)
+
+instance (SingI p) => Enum (PrimeField p) where
+  toEnum x
+    | toInteger (minBound :: PrimeField p) <= x' && x' <= toInteger (maxBound :: PrimeField p) = PrimeField x'
+    | otherwise = error "PrimeField.toEnum: bad argument"
+    where
+      x' = fromIntegral x
+  fromEnum = toInt
+
+instance Ord (PrimeField p) where
+  PrimeField a `compare` PrimeField b = a `compare` b
+
+instance (SingI (p :: Natural)) => FiniteField (PrimeField p) where
+  order x = char x
+
+  -- char _    = natVal (Proxy :: Proxy p)
+  char _ =
+    let c :: Natural
+        c = demote @p
+     in fromIntegral c
+  pthRoot a = a
+  allValues = [minBound .. maxBound]
+
+instance (SingI p) => Hashable (PrimeField p) where
+  hashWithSalt s x@(PrimeField a) =
+    s `hashWithSalt` char x `hashWithSalt` a
+
+-- | Extended GCD algorithm
+exgcd :: (Integral a) => a -> a -> (a, a, a)
+exgcd f1 f2 = f $ go f1 f2 1 0 0 1
+  where
+    go :: forall t. (Integral t) => t -> t -> t -> t -> t -> t -> (t, t, t)
+    go !r0 !r1 !s0 !s1 !t0 !t1
+      | r1 == 0 = (r0, s0, t0)
+      | otherwise = go r1 r2 s1 s2 t1 t2
+      where
+        (q, r2) = r0 `divMod` r1
+        s2 = s0 - q * s1
+        t2 = t0 - q * t1
+    f :: forall a b c. (Ord a, Num a, Num b, Num c) => (a, b, c) -> (a, b, c)
+    f (g, u, v)
+      | g < 0 = (-g, -u, -v)
+      | otherwise = (g, u, v)
+
+-- ---------------------------------------------------------------------------
+
+-- | Create a PrimeField type
+primeField :: Integer -> TH.TypeQ
+primeField n
+  | n <= 0 = error "primeField: negative value"
+  | otherwise = [t|PrimeField $(TH.litT (TH.numTyLit n))|]
+
+-- $TH
+-- Here is usage example for primeField:
+--
+-- > a :: $(primeField 15485867)
+-- > a = 1
--- a/src/Juvix/Data/Keyword/All.hs
+++ b/src/Juvix/Data/Keyword/All.hs
@ -343,6 +343,18 @@ kwLt_ = asciiKw Str.lt_
 kwLe_ :: Keyword
 kwLe_ = asciiKw Str.le_

+kwFieldAdd :: Keyword
+kwFieldAdd = asciiKw Str.fadd
+
+kwFieldSub :: Keyword
+kwFieldSub = asciiKw Str.fsub
+
+kwFieldMul :: Keyword
+kwFieldMul = asciiKw Str.fmul
+
+kwFieldDiv :: Keyword
+kwFieldDiv = asciiKw Str.fdiv
+
 kwSeq_ :: Keyword
 kwSeq_ = asciiKw Str.sseq_

--- a/src/Juvix/Extra/Strings.hs
+++ b/src/Juvix/Extra/Strings.hs
@ -179,6 +179,30 @@ int_ = "int"
 boolPrint :: (IsString s) => s
 boolPrint = "bool-print"

+fieldEq :: (IsString s) => s
+fieldEq = "field-eq"
+
+fieldAdd :: (IsString s) => s
+fieldAdd = "field-add"
+
+fieldSub :: (IsString s) => s
+fieldSub = "field-sub"
+
+fieldMul :: (IsString s) => s
+fieldMul = "field-mul"
+
+fieldDiv :: (IsString s) => s
+fieldDiv = "field-div"
+
+field :: (IsString s) => s
+field = "field"
+
+fieldFromInt :: (IsString s) => s
+fieldFromInt = "field-from-int"
+
+fieldToNat :: (IsString s) => s
+fieldToNat = "field-to-nat"
+
 io :: (IsString s) => s
 io = "IO"

@ -302,6 +326,24 @@ any = "Any"
 questionMark :: (IsString s) => s
 questionMark = "?"

+fadd :: (IsString s) => s
+fadd = "fadd"
+
+fsub :: (IsString s) => s
+fsub = "fsub"
+
+fmul :: (IsString s) => s
+fmul = "fmul"
+
+fdiv :: (IsString s) => s
+fdiv = "fdiv"
+
+ftoi :: (IsString s) => s
+ftoi = "ftoi"
+
+itof :: (IsString s) => s
+itof = "itof"
+
 delimiter :: (IsString s) => s
 delimiter = "delimiter"

@ -674,6 +716,12 @@ instrStrConcat = "strcat"
 instrStrToInt :: (IsString s) => s
 instrStrToInt = "atoi"

+instrFieldToInt :: (IsString s) => s
+instrFieldToInt = "ftoi"
+
+instrIntToField :: (IsString s) => s
+instrIntToField = "itof"
+
 instrShow :: (IsString s) => s
 instrShow = "show"

--- a/src/Juvix/Parser/Lexer.hs
+++ b/src/Juvix/Parser/Lexer.hs
@ -136,6 +136,12 @@ number' int mn mx = do
 string' :: ParsecS r Text
 string' = pack <$> (char '"' >> manyTill L.charLiteral (char '"'))

+field' :: ParsecS r Integer
+field' = do
+  d <- L.decimal
+  P.chunk "F"
+  return d
+
 -- | The caller is responsible of consuming space after it.
 delim' :: Text -> ParsecS r Interval
 delim' d = P.label (unpack d) . fmap snd . interval $ chunk d
--- a/test/Casm/Run/Base.hs
+++ b/test/Casm/Run/Base.hs
@ -5,6 +5,7 @@ import Juvix.Compiler.Casm.Error
 import Juvix.Compiler.Casm.Interpreter
 import Juvix.Compiler.Casm.Translation.FromSource
 import Juvix.Compiler.Casm.Validate
+import Juvix.Data.Field
 import Juvix.Data.PPOutput
 import Juvix.Parser.Error

@ -65,5 +66,5 @@ parseFile f = do
 doRun ::
  LabelInfo ->
  Code ->
-  IO (Either CasmError Integer)
+  IO (Either CasmError FField)
 doRun labi instrs = catchRunErrorIO (runCode labi instrs)
--- a/test/Casm/Run/Positive.hs
+++ b/test/Casm/Run/Positive.hs
@ -99,5 +99,10 @@ tests =
      "Test013: Currying and uncurrying"
      $(mkRelDir ".")
      $(mkRelFile "test013.casm")
-      $(mkRelFile "out/test013.out")
+      $(mkRelFile "out/test013.out"),
+    PosTest
+      "Test014: Field arithmetic"
+      $(mkRelDir ".")
+      $(mkRelFile "test014.casm")
+      $(mkRelFile "out/test014.out")
  ]
--- a/test/Compilation/Positive.hs
+++ b/test/Compilation/Positive.hs
@ -440,5 +440,10 @@ tests =
        "Test073: Import and use a syntax alias"
        $(mkRelDir "test073")
        $(mkRelFile "test073.juvix")
-        $(mkRelFile "out/test073.out")
+        $(mkRelFile "out/test073.out"),
+      posTestEval
+        "Test074: Fields"
+        $(mkRelDir ".")
+        $(mkRelFile "test074.juvix")
+        $(mkRelFile "out/test074.out")
    ]
--- a/test/Core/Asm/Base.hs
+++ b/test/Core/Asm/Base.hs
@ -12,6 +12,7 @@ import Juvix.Compiler.Core.Pipeline
 import Juvix.Compiler.Core.Translation.FromSource
 import Juvix.Compiler.Core.Translation.Stripped.FromCore qualified as Stripped
 import Juvix.Compiler.Tree.Translation.FromCore qualified as Tree
+import Juvix.Data.Field
 import Juvix.Data.PPOutput

 newtype Test = Test
@ -55,5 +56,5 @@ coreAsmAssertion mainFile expectedFile step = do
      case run $ runReader defaultCoreOptions $ runError $ toStored' >=> toStripped' Identity $ moduleFromInfoTable $ setupMainFunction defaultModuleId tabIni node of
        Left err -> assertFailure (show (pretty (fromJuvixError @GenericError err)))
        Right m -> do
-          let tab = Asm.fromTree $ Tree.fromCore $ Stripped.fromCore $ computeCombinedInfoTable m
+          let tab = Asm.fromTree $ Tree.fromCore $ Stripped.fromCore (maximum allowedFieldSizes) $ computeCombinedInfoTable m
          Asm.asmRunAssertion' tab expectedFile step
--- a/test/Core/Compile/Base.hs
+++ b/test/Core/Compile/Base.hs
@ -15,6 +15,7 @@ import Juvix.Compiler.Core.Pipeline
 import Juvix.Compiler.Core.Translation.FromSource
 import Juvix.Compiler.Core.Translation.Stripped.FromCore qualified as Stripped
 import Juvix.Compiler.Tree.Translation.FromCore qualified as Tree
+import Juvix.Data.Field
 import Juvix.Data.PPOutput

 newtype Test = Test
@ -54,7 +55,7 @@ coreCompileAssertion' optLevel tab mainFile expectedFile stdinText step = do
    Right m -> do
      let tab0 = computeCombinedInfoTable m
      assertBool "Check info table" (checkInfoTable tab0)
-      let tab' = Asm.fromTree . Tree.fromCore $ Stripped.fromCore tab0
+      let tab' = Asm.fromTree . Tree.fromCore $ Stripped.fromCore (maximum allowedFieldSizes) tab0
      length (fromText (Asm.ppPrint tab' tab') :: String) `seq`
        Asm.asmCompileAssertion' optLevel tab' mainFile expectedFile stdinText step
  where
--- a/test/Core/Compile/Positive.hs
+++ b/test/Core/Compile/Positive.hs
@ -7,7 +7,7 @@ import Core.Eval.Positive qualified as Eval
 allTests :: TestTree
 allTests = testGroup "JuvixCore compilation tests" (map liftTest (Eval.filterOutTests ignoredTests Eval.compilableTests))

-- Arbitrary precision integers not yet supported
+-- Arbitrary precision integers and fields not yet supported
 ignoredTests :: [String]
 ignoredTests =
  [ "Test011: Tail recursion: Fibonacci numbers in linear time",
@ -15,7 +15,8 @@ ignoredTests =
    "Test025: Mutual recursion",
    "Test026: Nested 'case', 'let' and 'if' with variable capture",
    "Test036: Big numbers",
-    "Test040: LetRec - fib, fact"
+    "Test040: LetRec - fib, fact",
+    "Test061: Fields"
  ]

 liftTest :: Eval.PosTest -> TestTree
--- a/test/Core/Eval/Positive.hs
+++ b/test/Core/Eval/Positive.hs
@ -342,5 +342,10 @@ tests =
      "Test060: Bottom"
      $(mkRelDir ".")
      $(mkRelFile "test060.jvc")
-      $(mkRelFile "out/test060.out")
+      $(mkRelFile "out/test060.out"),
+    PosTest
+      "Test061: Fields"
+      $(mkRelDir ".")
+      $(mkRelFile "test061.jvc")
+      $(mkRelFile "out/test061.out")
  ]
--- a/Show More
+++ b/Show More