diff --git a/crucible-jvm/src/Lang/Crucible/JVM/Context.hs b/crucible-jvm/src/Lang/Crucible/JVM/Context.hs
index 2aa479274..bb6f61aef 100644
--- a/crucible-jvm/src/Lang/Crucible/JVM/Context.hs
+++ b/crucible-jvm/src/Lang/Crucible/JVM/Context.hs
@@ -30,7 +30,7 @@ import           Lang.Crucible.JVM.Types
 -- * JVMContext
 
 
-type StaticFieldTable = Map (J.ClassName, J.FieldId) (GlobalVar JVMValueType)
+type StaticFieldTable = Map J.FieldId (GlobalVar JVMValueType)
 type MethodHandleTable = Map (J.ClassName, J.MethodKey) JVMHandleInfo
 
 data JVMHandleInfo where
@@ -41,7 +41,7 @@ data JVMHandleInfo where
 data JVMContext = JVMContext
   { methodHandles :: Map (J.ClassName, J.MethodKey) JVMHandleInfo
       -- ^ Map from static and dynamic methods to Crucible function handles.
-  , staticFields :: Map (J.ClassName, J.FieldId) (GlobalVar JVMValueType)
+  , staticFields :: Map J.FieldId (GlobalVar JVMValueType)
       -- ^ Map from static field names to Crucible global variables.
       -- We know about these fields at translation time so we can allocate
       -- global variables to store them.
diff --git a/crucible-jvm/src/Lang/Crucible/JVM/Simulate.hs b/crucible-jvm/src/Lang/Crucible/JVM/Simulate.hs
index d4e9305e0..25372ef8f 100644
--- a/crucible-jvm/src/Lang/Crucible/JVM/Simulate.hs
+++ b/crucible-jvm/src/Lang/Crucible/JVM/Simulate.hs
@@ -34,7 +34,6 @@ import           Data.Maybe (fromMaybe)
 import qualified Data.Set as Set
 import           Data.String (fromString)
 import           Data.List (isPrefixOf)
-import qualified Data.Text as Text
 import qualified Data.Vector as V
 
 import           System.IO
@@ -345,7 +344,7 @@ declareStaticField halloc c m f = do
   let fieldId = J.FieldId cn fn (J.fieldType f)
   let str = fn ++ show (J.fieldType f)
   gvar <- C.freshGlobalVar halloc (globalVarName cn str) (knownRepr :: TypeRepr JVMValueType)
-  return $ (Map.insert (cn,fieldId) gvar m)
+  return $ Map.insert fieldId gvar m
 
 
 -- | Create the initial 'JVMContext'.
@@ -457,7 +456,7 @@ jvmSimContext sym halloc handle ctx verbosity p =
 -- | Make the initial state for the simulator, binding the function handles so that
 -- they translate method bodies when they are accessed.
 mkSimSt ::
-  -- forall sym .
+  forall sym p ret.
   (IsSymInterface sym) =>
   sym ->
   p ->
@@ -471,8 +470,8 @@ mkSimSt sym p halloc ctx verbosity ret k =
   do globals <- Map.foldrWithKey initField (return globals0) (staticFields ctx)
      return $ C.InitialState simctx globals C.defaultAbortHandler ret k
   where
-    -- initField :: (J.ClassName, J.FieldId) -> GlobalVar JVMValueType -> IO (C.SymGlobalState sym) -> IO (C.SymGlobalState sym)
-    initField (_, fi) var m =
+    initField :: J.FieldId -> GlobalVar JVMValueType -> IO (C.SymGlobalState sym) -> IO (C.SymGlobalState sym)
+    initField fi var m =
       do gs <- m
          z <- zeroValue sym (J.fieldIdType fi)
          return (C.insertGlobal var z gs)
@@ -807,27 +806,48 @@ doAppJVM sym =
   where
     out _verbosity _msg = return () --putStrLn
 
--- | Write a value to a field of an object reference.
+-- | Write a value to a field of an object reference. The 'FieldId'
+-- must have already been resolved (see §5.4.3.2 of the JVM spec).
 doFieldStore ::
   IsSymInterface sym =>
   sym ->
   C.SymGlobalState sym ->
   C.RegValue sym JVMRefType ->
-  String {- ^ field name -} ->
+  J.FieldId ->
   C.RegValue sym JVMValueType ->
   IO (C.SymGlobalState sym)
-doFieldStore sym globals ref fname val =
+doFieldStore sym globals ref fid val =
   do let msg1 = C.GenericSimError "Field store: null reference"
      ref' <- C.readPartExpr sym ref msg1
      obj <- EvalStmt.readRef sym jvmIntrinsicTypes objectRepr ref' globals
      let msg2 = C.GenericSimError "Field store: object is not a class instance"
      inst <- C.readPartExpr sym (C.unVB (C.unroll obj Ctx.! Ctx.i1of2)) msg2
      let tab = C.unRV (inst Ctx.! Ctx.i1of2)
-     let tab' = Map.insert (Text.pack fname) (W4.justPartExpr sym val) tab
+     let tab' = Map.insert (fieldIdText fid) (W4.justPartExpr sym val) tab
      let inst' = Control.Lens.set (Ctx.ixF Ctx.i1of2) (C.RV tab') inst
      let obj' = C.RolledType (C.injectVariant sym knownRepr Ctx.i1of2 inst')
      EvalStmt.alterRef sym jvmIntrinsicTypes objectRepr ref' (W4.justPartExpr sym obj') globals
 
+-- | Write a value to a static field of a class. The 'FieldId' must
+-- have already been resolved (see §5.4.3.2 of the JVM spec).
+doStaticFieldStore ::
+  IsSymInterface sym =>
+  sym ->
+  JVMContext ->
+  C.SymGlobalState sym ->
+  J.FieldId ->
+  C.RegValue sym JVMValueType ->
+  IO (C.SymGlobalState sym)
+doStaticFieldStore sym jc globals fid val =
+  case Map.lookup fid (staticFields jc) of
+    Nothing -> C.addFailedAssertion sym msg
+    Just gvar ->
+      do putStrLn $ "doStaticFieldStore " ++ fname
+         pure (C.insertGlobal gvar val globals)
+  where
+    fname = J.unClassName (J.fieldIdClass fid) ++ "." ++ J.fieldIdName fid
+    msg = C.GenericSimError $ "Static field store: field not found: " ++ fname
+
 -- | Write a value at an index of an array reference.
 doArrayStore ::
   IsSymInterface sym =>
@@ -849,24 +869,46 @@ doArrayStore sym globals ref idx val =
      let obj' = C.RolledType (C.injectVariant sym knownRepr Ctx.i2of2 arr')
      EvalStmt.alterRef sym jvmIntrinsicTypes objectRepr ref' (W4.justPartExpr sym obj') globals
 
--- | Read a value from a field of an object reference.
+-- | Read a value from a field of an object reference. The 'FieldId'
+-- must have already been resolved (see §5.4.3.2 of the JVM spec).
 doFieldLoad ::
   IsSymInterface sym =>
   sym ->
   C.SymGlobalState sym ->
-  C.RegValue sym JVMRefType -> String {- ^ field name -} ->
+  C.RegValue sym JVMRefType ->
+  J.FieldId ->
   IO (C.RegValue sym JVMValueType)
-doFieldLoad sym globals ref fname =
+doFieldLoad sym globals ref fid =
   do let msg1 = C.GenericSimError "Field load: null reference"
      ref' <- C.readPartExpr sym ref msg1
      obj <- EvalStmt.readRef sym jvmIntrinsicTypes objectRepr ref' globals
      let msg2 = C.GenericSimError "Field load: object is not a class instance"
      inst <- C.readPartExpr sym (C.unVB (C.unroll obj Ctx.! Ctx.i1of2)) msg2
      let tab = C.unRV (inst Ctx.! Ctx.i1of2)
-     let msg3 = C.GenericSimError $ "Field load: field not found: " ++ fname
-     let key = Text.pack fname
+     let msg3 = C.GenericSimError $ "Field load: field not found: " ++ J.fieldIdName fid
+     let key = fieldIdText fid
      C.readPartExpr sym (fromMaybe W4.Unassigned (Map.lookup key tab)) msg3
 
+-- | Read a value from a static field of a class. The 'FieldId' must
+-- have already been resolved (see §5.4.3.2 of the JVM spec).
+doStaticFieldLoad ::
+  IsSymInterface sym =>
+  sym ->
+  JVMContext ->
+  C.SymGlobalState sym ->
+  J.FieldId ->
+  IO (C.RegValue sym JVMValueType)
+doStaticFieldLoad sym jc globals fid =
+  case Map.lookup fid (staticFields jc) of
+    Nothing -> C.addFailedAssertion sym msg
+    Just gvar ->
+      case C.lookupGlobal gvar globals of
+        Nothing -> C.addFailedAssertion sym msg
+        Just v -> pure v
+  where
+    fname = J.unClassName (J.fieldIdClass fid) ++ "." ++ J.fieldIdName fid
+    msg = C.GenericSimError $ "Static field load: field not found: " ++ fname
+
 -- | Read a value at an index of an array reference.
 doArrayLoad ::
   IsSymInterface sym =>
diff --git a/crucible-jvm/src/Lang/Crucible/JVM/Translation/Class.hs b/crucible-jvm/src/Lang/Crucible/JVM/Translation/Class.hs
index 8b590bbec..e5a988df4 100644
--- a/crucible-jvm/src/Lang/Crucible/JVM/Translation/Class.hs
+++ b/crucible-jvm/src/Lang/Crucible/JVM/Translation/Class.hs
@@ -362,10 +362,10 @@ getStaticFieldValue fieldId = do
       let cls = J.fieldIdClass fieldId
       ctx <- gets jsContext
       initializeClass cls
-      case Map.lookup (J.fieldIdClass fieldId, fieldId) (staticFields ctx) of
+      case Map.lookup fieldId (staticFields ctx) of
         Just glob -> do
           r <- readGlobal glob
-          fromJVMDynamic (J.fieldIdType fieldId) r
+          fromJVMDynamic ("getstatic " <> fieldIdText fieldId) (J.fieldIdType fieldId) r
         Nothing ->
           jvmFail $ "getstatic: field " ++ J.fieldIdName fieldId ++ " not found"
 
@@ -374,7 +374,7 @@ setStaticFieldValue :: J.FieldId -> JVMValue s -> JVMGenerator s ret ()
 setStaticFieldValue  fieldId val = do
     ctx <- gets jsContext
     let cName = J.fieldIdClass fieldId
-    case Map.lookup (cName, fieldId) (staticFields ctx) of
+    case Map.lookup fieldId (staticFields ctx) of
          Just glob -> do
            writeGlobal glob (valueToExpr val)
          Nothing ->
@@ -834,12 +834,12 @@ resolveField fieldId =
 getInstanceFieldValue :: JVMObject s -> J.FieldId -> JVMGenerator s ret (JVMValue s)
 getInstanceFieldValue obj fieldId =
   do let uobj = App (UnrollRecursive knownRepr knownRepr obj)
-     inst <- projectVariant Ctx.i1of2 uobj
+     inst <- projectVariant "getfield: expected class instance" Ctx.i1of2 uobj
      let fields = App (GetStruct inst Ctx.i1of2 knownRepr)
      key <- resolveField fieldId
      let mval = App (LookupStringMapEntry knownRepr fields key)
      dyn <- assertedJustExpr mval "Field not present"
-     fromJVMDynamic (J.fieldIdType fieldId) dyn
+     fromJVMDynamic ("getfield " <> fieldIdText fieldId) (J.fieldIdType fieldId) dyn
 
 -- | Update a field of a JVM object (must be a class instance, not an array).
 setInstanceFieldValue :: JVMObject s -> J.FieldId -> JVMValue s -> JVMGenerator s ret (JVMObject s)
@@ -847,7 +847,7 @@ setInstanceFieldValue obj fieldId val =
   do let dyn  = valueToExpr val
      let mdyn = App (JustValue knownRepr dyn)
      let uobj = App (UnrollRecursive knownRepr knownRepr obj)
-     inst <- projectVariant Ctx.i1of2 uobj
+     inst <- projectVariant "setfield: expected class instance" Ctx.i1of2 uobj
      let fields = App (GetStruct inst Ctx.i1of2 knownRepr)
      key <- resolveField fieldId
      let fields' = App (InsertStringMapEntry knownRepr fields key mdyn)
@@ -859,7 +859,7 @@ setInstanceFieldValue obj fieldId val =
 getJVMInstanceClass :: JVMObject s -> JVMGenerator s ret (JVMClass s)
 getJVMInstanceClass obj = do
   let uobj = App (UnrollRecursive knownRepr knownRepr obj)
-  inst <- projectVariant Ctx.i1of2 uobj
+  inst <- projectVariant "invokeinterface: expected class instance" Ctx.i1of2 uobj
   return $ App (GetStruct inst Ctx.i2of2 knownRepr)
 
 
diff --git a/crucible-jvm/src/Lang/Crucible/JVM/Translation/Monad.hs b/crucible-jvm/src/Lang/Crucible/JVM/Translation/Monad.hs
index a0326d1ee..d8e0935d0 100644
--- a/crucible-jvm/src/Lang/Crucible/JVM/Translation/Monad.hs
+++ b/crucible-jvm/src/Lang/Crucible/JVM/Translation/Monad.hs
@@ -18,6 +18,7 @@ import           Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
 import           Control.Monad.State.Strict
 import           Control.Lens hiding (op, (:>))
+import qualified Data.Text as Text
 
 -- jvm-parser
 import qualified Language.JVM.Parser as J
@@ -39,6 +40,7 @@ import           Lang.Crucible.Panic
 import           Lang.Crucible.JVM.Types
 import           Lang.Crucible.JVM.Context
 -- what4
+import           What4.Interface (StringLiteral(..))
 import           What4.ProgramLoc (Position(InternalPos))
 
 import Debug.Trace
@@ -187,12 +189,14 @@ valueToExpr (RValue x) = App $ InjectVariant knownRepr tagR x
 
 projectVariant ::
   KnownRepr (Ctx.Assignment TypeRepr) ctx =>
+  Text.Text ->
   Ctx.Index ctx tp ->
   Expr JVM s (VariantType ctx) ->
   JVMGenerator s ret (Expr JVM s tp)
-projectVariant tag var =
+projectVariant msg tag var =
   do let mx = App (ProjectVariant knownRepr tag var)
-     assertedJustExpr mx "incorrect variant"
+     let str = App $ StringLit $ UnicodeLiteral ("read failed: " <> msg)
+     assertedJustExpr mx str
 
 injectVariant ::
   KnownRepr (Ctx.Assignment TypeRepr) ctx =>
@@ -202,19 +206,20 @@ injectVariant ::
 injectVariant tag val = App (InjectVariant knownRepr tag val)
 
 
-fromJVMDynamic :: J.Type -> Expr JVM s JVMValueType -> JVMGenerator s ret (JVMValue s)
-fromJVMDynamic ty dyn =
+fromJVMDynamic ::
+  Text.Text -> J.Type -> Expr JVM s JVMValueType -> JVMGenerator s ret (JVMValue s)
+fromJVMDynamic msg ty dyn =
   case ty of
-    J.BooleanType -> IValue <$> projectVariant tagI dyn
-    J.ArrayType _ -> RValue <$> projectVariant tagR dyn
-    J.ByteType    -> IValue <$> projectVariant tagI dyn
-    J.CharType    -> IValue <$> projectVariant tagI dyn
-    J.ClassType _ -> RValue <$> projectVariant tagR dyn
-    J.DoubleType  -> DValue <$> projectVariant tagD dyn
-    J.FloatType   -> FValue <$> projectVariant tagF dyn
-    J.IntType     -> IValue <$> projectVariant tagI dyn
-    J.LongType    -> LValue <$> projectVariant tagL dyn
-    J.ShortType   -> IValue <$> projectVariant tagI dyn
+    J.BooleanType -> IValue <$> projectVariant msg tagI dyn
+    J.ArrayType _ -> RValue <$> projectVariant msg tagR dyn
+    J.ByteType    -> IValue <$> projectVariant msg tagI dyn
+    J.CharType    -> IValue <$> projectVariant msg tagI dyn
+    J.ClassType _ -> RValue <$> projectVariant msg tagR dyn
+    J.DoubleType  -> DValue <$> projectVariant msg tagD dyn
+    J.FloatType   -> FValue <$> projectVariant msg tagF dyn
+    J.IntType     -> IValue <$> projectVariant msg tagI dyn
+    J.LongType    -> LValue <$> projectVariant msg tagL dyn
+    J.ShortType   -> IValue <$> projectVariant msg tagI dyn
 
 toJVMDynamic :: J.Type -> JVMValue s -> JVMGenerator s ret (Expr JVM s JVMValueType)
 toJVMDynamic ty val =