diff --git a/contest.sh b/contest.sh
index 607f56fea..e8e3ebdf4 100755
--- a/contest.sh
+++ b/contest.sh
@@ -25,9 +25,6 @@ test_dir=$(dirname $file)
 build_dir="$root_dir/build"
 base=$(basename "$file" .json)
 src="$test_dir/$base.solc"
-hull="$build_dir/output1.hull"
-hexfile="$build_dir/$base.hex"
-yulfile="$build_dir/$base.yul"
 
 create=true
 # Allow overriding testrunner location (useful for Nix builds)
@@ -87,16 +84,41 @@ suite=$(echo $presuite | tr -d '"')
 echo "Compiling to Hull..."
 # Allow overriding sol-core command (useful for Nix builds)
 : ${SOLCORE_CMD:="cabal run exe:sol-core --"}
-if ! $SOLCORE_CMD -f "$src"; then
+mkdir -p "$build_dir"
+work_root="$build_dir/.contest-work"
+mkdir -p "$work_root"
+work_dir="$(mktemp -d "$work_root/run.XXXXXX")"
+work_marker="$work_dir/.owned-by-contest"
+touch "$work_marker"
+hull="$work_dir/output1.hull"
+yulfile="$work_dir/output.yul"
+hexfile="$work_dir/output.hex"
+runner_input="$work_dir/runner-input.json"
+runner_output="$work_dir/runner-output.json"
+
+cleanup_work_dir() {
+    if [[ -z "${work_dir:-}" ]]; then
+        return
+    fi
+
+    if [[ "$work_dir" != "$work_root"/run.* || ! -f "$work_marker" ]]; then
+        echo "Error: refusing to clean unverified contest work directory '$work_dir'" >&2
+        return 1
+    fi
+
+    rm -rf -- "$work_dir"
+}
+
+trap cleanup_work_dir EXIT
+trap 'exit 129' HUP
+trap 'exit 130' INT
+trap 'exit 143' TERM
+
+if ! $SOLCORE_CMD -f "$src" -o "$work_dir"; then
     echo "Error: sol-core compilation failed"
     exit 1
 fi
 
-mkdir -p "$build_dir"
-if ls ./output*.hull 1> /dev/null 2>&1; then
-    mv ./output*.hull "$build_dir"/
-fi
-
 if [[ ! -f "$hull" ]]; then
     echo "Error: sol-core did not produce output1.hull"
     exit 1
@@ -122,6 +144,6 @@ fi
 
 echo "Hex output: $hexfile"
 
-jq ".$suite.bytecode |= \"$(cat $hexfile)\" " $file > $build_dir/$suite.json
+jq ".$suite.bytecode |= \"$(cat $hexfile)\" " $file > "$runner_input"
 
-"$testrunner_exe" "$evmone" "$build_dir/$suite.json" "$build_dir/$suite-output.json"
+"$testrunner_exe" "$evmone" "$runner_input" "$runner_output"
diff --git a/run_contests.sh b/run_contests.sh
index 60a7705cb..b928a3d75 100755
--- a/run_contests.sh
+++ b/run_contests.sh
@@ -5,6 +5,8 @@ set -euo pipefail
 root_dir="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
 cd "$root_dir"
 
+bash ./scripts/test_contest_concurrency.sh
+
 bash ./contest.sh test/examples/dispatch/basic.json
 bash ./contest.sh test/examples/dispatch/assembly.json
 bash ./contest.sh test/examples/dispatch/neg.json
diff --git a/scripts/test_contest_concurrency.sh b/scripts/test_contest_concurrency.sh
new file mode 100755
index 000000000..b914ff1f4
--- /dev/null
+++ b/scripts/test_contest_concurrency.sh
@@ -0,0 +1,208 @@
+#!/usr/bin/env bash
+
+set -euo pipefail
+
+repo_root="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
+tmp_parent="${TMPDIR:-/tmp}"
+tmp_parent="${tmp_parent%/}"
+test_root="$(mktemp -d "$tmp_parent/solcore-contest-concurrency.XXXXXX")"
+test_marker="$test_root/.owned-by-contest-concurrency-test"
+touch "$test_marker"
+
+cleanup_test_root() {
+    if [[ "$test_root" != "$tmp_parent"/solcore-contest-concurrency.* || ! -f "$test_marker" ]]; then
+        echo "Error: refusing to clean unverified test directory '$test_root'" >&2
+        return 1
+    fi
+
+    rm -rf -- "$test_root"
+}
+
+trap cleanup_test_root EXIT
+trap 'exit 129' HUP
+trap 'exit 130' INT
+trap 'exit 143' TERM
+
+mkdir -p \
+    "$test_root/cases/alpha" \
+    "$test_root/cases/beta" \
+    "$test_root/fake-bin" \
+    "$test_root/state"
+cp "$repo_root/contest.sh" "$test_root/contest.sh"
+chmod +x "$test_root/contest.sh"
+
+printf '%s\n' alpha > "$test_root/cases/alpha/shared.solc"
+printf '%s\n' '{"shared": {}}' > "$test_root/cases/alpha/shared.json"
+printf '%s\n' beta > "$test_root/cases/beta/shared.solc"
+printf '%s\n' '{"shared": {}}' > "$test_root/cases/beta/shared.json"
+printf '%s\n' user-owned-sentinel > "$test_root/output1.hull"
+touch "$test_root/libevmone.so"
+
+cat > "$test_root/fake-bin/tool" <<'EOF'
+#!/usr/bin/env bash
+
+set -euo pipefail
+
+tool="$(basename "$0")"
+
+case "$tool" in
+    sol-core)
+        src=
+        output_dir=
+        while [[ $# -gt 0 ]]; do
+            case "$1" in
+                -f)
+                    src="$2"
+                    shift 2
+                    ;;
+                -o)
+                    output_dir="$2"
+                    shift 2
+                    ;;
+                *)
+                    shift
+                    ;;
+            esac
+        done
+
+        case_name="$FAKE_CASE"
+        [[ "$(<"$src")" == "$case_name" ]]
+        printf '%s\n' "$case_name" > "$output_dir/output1.hull"
+        printf '%s\n' "$output_dir" > "$FAKE_STATE/$case_name.work-dir"
+        touch "$FAKE_STATE/compiler-$case_name.ready"
+
+        deadline=$((SECONDS + 10))
+        until [[ -f "$FAKE_STATE/compiler-alpha.ready" && -f "$FAKE_STATE/compiler-beta.ready" ]]; do
+            if (( SECONDS >= deadline )); then
+                echo "Timed out waiting for both fake compilers" >&2
+                exit 1
+            fi
+            sleep 0.01
+        done
+        ;;
+    yule)
+        hull="$1"
+        shift
+        output=
+        while [[ $# -gt 0 ]]; do
+            case "$1" in
+                -o)
+                    output="$2"
+                    shift 2
+                    ;;
+                *)
+                    shift
+                    ;;
+            esac
+        done
+
+        case_name="$(<"$hull")"
+        printf '%s\n' "$output" > "$FAKE_STATE/$case_name.yul-path"
+        printf '%s\n' "$case_name" > "$output"
+        ;;
+    solc)
+        yul=
+        for arg in "$@"; do
+            yul="$arg"
+        done
+        case_name="$(<"$yul")"
+        [[ "$case_name" == "$FAKE_CASE" ]]
+        printf '%s\n' "$yul" > "$FAKE_STATE/$case_name.solc-input"
+        printf '%s\n' "Binary representation:" "hex-$case_name"
+        ;;
+    jq)
+        if [[ "$1" == "keys[0]" ]]; then
+            printf '%s\n' '"shared"'
+        else
+            [[ "$1" == *"hex-$FAKE_CASE"* ]]
+            printf '{"shared":{"bytecode":"%s","case":"%s"}}\n' \
+                "hex-$FAKE_CASE" "$FAKE_CASE"
+        fi
+        ;;
+    testrunner)
+        [[ -f "$1" ]]
+        [[ -f "$2" ]]
+        command grep -q "\"case\":\"$FAKE_CASE\"" "$2"
+        printf '%s\n' "$2" > "$FAKE_STATE/$FAKE_CASE.runner-input"
+        printf '%s\n' "$3" > "$FAKE_STATE/$FAKE_CASE.runner-output"
+        printf '{"ok":true,"case":"%s"}\n' "$FAKE_CASE" > "$3"
+        ;;
+    *)
+        echo "Unexpected fake tool name: $tool" >&2
+        exit 1
+        ;;
+esac
+EOF
+
+chmod +x "$test_root/fake-bin/tool"
+for tool in sol-core yule solc jq testrunner; do
+    ln -s tool "$test_root/fake-bin/$tool"
+done
+
+run_case() {
+    local case_name="$1"
+
+    PATH="$test_root/fake-bin:$PATH" \
+        SOLCORE_CMD="$test_root/fake-bin/sol-core" \
+        YULE_CMD="$test_root/fake-bin/yule" \
+        testrunner_exe="$test_root/fake-bin/testrunner" \
+        evmone="$test_root/libevmone.so" \
+        FAKE_STATE="$test_root/state" \
+        FAKE_CASE="$case_name" \
+        bash "$test_root/contest.sh" \
+        "$test_root/cases/$case_name/shared.json" \
+        > "$test_root/state/$case_name.log" 2>&1
+}
+
+run_case alpha &
+alpha_pid=$!
+run_case beta &
+beta_pid=$!
+
+failed=0
+if ! wait "$alpha_pid"; then
+    command cat "$test_root/state/alpha.log" >&2
+    failed=1
+fi
+if ! wait "$beta_pid"; then
+    command cat "$test_root/state/beta.log" >&2
+    failed=1
+fi
+if [[ "$failed" != "0" ]]; then
+    exit 1
+fi
+
+alpha_work_dir="$(<"$test_root/state/alpha.work-dir")"
+beta_work_dir="$(<"$test_root/state/beta.work-dir")"
+alpha_yul_path="$(<"$test_root/state/alpha.yul-path")"
+beta_yul_path="$(<"$test_root/state/beta.yul-path")"
+alpha_solc_input="$(<"$test_root/state/alpha.solc-input")"
+beta_solc_input="$(<"$test_root/state/beta.solc-input")"
+alpha_runner_input="$(<"$test_root/state/alpha.runner-input")"
+beta_runner_input="$(<"$test_root/state/beta.runner-input")"
+alpha_runner_output="$(<"$test_root/state/alpha.runner-output")"
+beta_runner_output="$(<"$test_root/state/beta.runner-output")"
+
+[[ "$alpha_work_dir" == "$test_root/build/.contest-work/run."* ]]
+[[ "$beta_work_dir" == "$test_root/build/.contest-work/run."* ]]
+[[ "$alpha_work_dir" != "$beta_work_dir" ]]
+[[ "$alpha_yul_path" == "$alpha_work_dir/output.yul" ]]
+[[ "$beta_yul_path" == "$beta_work_dir/output.yul" ]]
+[[ "$alpha_yul_path" != "$beta_yul_path" ]]
+[[ "$alpha_solc_input" == "$alpha_yul_path" ]]
+[[ "$beta_solc_input" == "$beta_yul_path" ]]
+[[ "$alpha_runner_input" == "$alpha_work_dir/runner-input.json" ]]
+[[ "$beta_runner_input" == "$beta_work_dir/runner-input.json" ]]
+[[ "$alpha_runner_input" != "$beta_runner_input" ]]
+[[ "$alpha_runner_output" == "$alpha_work_dir/runner-output.json" ]]
+[[ "$beta_runner_output" == "$beta_work_dir/runner-output.json" ]]
+[[ "$alpha_runner_output" != "$beta_runner_output" ]]
+[[ ! -e "$alpha_work_dir" ]]
+[[ ! -e "$beta_work_dir" ]]
+[[ "$(<"$test_root/output1.hull")" == "user-owned-sentinel" ]]
+[[ ! -e "$test_root/build/shared.yul" ]]
+[[ ! -e "$test_root/build/shared.hex" ]]
+[[ ! -e "$test_root/build/shared.json" ]]
+[[ ! -e "$test_root/build/shared-output.json" ]]
+
+printf '%s\n' "contest concurrency regression passed"
diff --git a/sol-core.cabal b/sol-core.cabal
index 488357638..e0453a42c 100644
--- a/sol-core.cabal
+++ b/sol-core.cabal
@@ -64,6 +64,7 @@ library
       Solcore.Backend.EmitHull
       Solcore.Backend.Mast
       Solcore.Backend.MastEval
+      Solcore.Backend.NameEncoding
       Solcore.Backend.Specialise
       Solcore.Desugarer.DecisionTreeCompiler
       Solcore.Desugarer.DeriveClasses
@@ -188,6 +189,8 @@ test-suite sol-core-tests
 
   -- cabal-fmt: expand test -Main
   other-modules:
+    BackendBlockScopeTests
+    BackendNameEncodingTests
     Cases
     ContractAbiTests
     DiagnosticCliTests
diff --git a/src/Solcore/Backend/EmitHull.hs b/src/Solcore/Backend/EmitHull.hs
index d878ec332..cb3eb4510 100644
--- a/src/Solcore/Backend/EmitHull.hs
+++ b/src/Solcore/Backend/EmitHull.hs
@@ -15,6 +15,7 @@ import GHC.Stack (HasCallStack)
 import Language.Hull qualified as Hull
 import Language.Yul
 import Solcore.Backend.Mast
+import Solcore.Backend.NameEncoding (encodeBackendName)
 import Solcore.Frontend.Pretty.SolcorePretty
 import Solcore.Frontend.Syntax.Contract (Constr (..), DataTy (..))
 import Solcore.Frontend.Syntax.Name
@@ -271,7 +272,7 @@ translateTCon tycon tas = do
     Just (DataTy _n tvs cs _) -> do
       let subst = zip tvs (map mastToTy tas)
       tys <- mapM (translateDCon subst) cs
-      Hull.TNamed (show tycon) <$> buildSumType tys
+      Hull.TNamed (encodeBackendName tycon) <$> buildSumType tys
     Nothing -> errorsEM ["translateTCon: unknown type ", pretty tycon, "\n", show tycon]
   where
     buildSumType :: [Hull.Type] -> EM Hull.Type
@@ -432,7 +433,9 @@ emitStmt (MastAsm as) = do
     notEVar _ = True
 emitStmt MastBreak = pure [Hull.SBreak]
 emitStmt MastContinue = pure [Hull.SContinue]
-emitStmt (MastSeq stmts) = concat <$> mapM emitStmt stmts
+emitStmt (MastSeq stmts) = withLocalState do
+  body <- concat <$> mapM emitStmt stmts
+  pure [Hull.SBlock body]
 
 emitStmts :: [MastStmt] -> EM [Hull.Stmt]
 emitStmts = concatMapM emitStmt'
diff --git a/src/Solcore/Backend/MastEval.hs b/src/Solcore/Backend/MastEval.hs
index 7ab0c47a4..594bb3829 100644
--- a/src/Solcore/Backend/MastEval.hs
+++ b/src/Solcore/Backend/MastEval.hs
@@ -191,22 +191,17 @@ buildFunTable cu = Map.fromList $ concatMap collectFromTopDecl (mastTopDecls cu)
     collectFromDecl (MastCDataDecl _) = []
 
 -----------------------------------------------------------------------
--- Type registry: pre-scan a function body for all declared MastIds
+-- Type registry: start with function parameters and extend at each declaration
 -----------------------------------------------------------------------
 
 -- | Build a registry from variable names to their full MastIds.
--- Covers function parameters and let-declared variables throughout the body.
--- Used to reconstruct VEnv entries after interpreting an asm block, since
--- a no-init 'let' deletes the variable from VEnv before the asm block runs.
+-- Let-declared variables are registered as their statements are evaluated, so
+-- assembly before a shadowing declaration still resolves to the outer binding.
+-- The registry survives no-init let deletion from VEnv.
 buildTypeReg :: [MastParam] -> [MastStmt] -> TypeReg
-buildTypeReg params stmts =
-  Map.fromList $
+buildTypeReg params _ =
+  Map.fromList
     [(mastParamName p, MastId (mastParamName p) (mastParamType p)) | p <- params]
-      ++ concatMap letIds stmts
-  where
-    letIds (MastLet _ i _ _) = [(mastIdName i, i)]
-    letIds (MastMatch _ alts) = concatMap (concatMap letIds . snd) alts
-    letIds _ = []
 
 -----------------------------------------------------------------------
 -- Evaluate top-level declarations
@@ -283,18 +278,34 @@ evalStmts :: TypeReg -> VEnv -> [MastStmt] -> EvalM (VEnv, [MastStmt])
 evalStmts _ env [] = pure (env, [])
 evalStmts tyReg env (s : ss) = do
   (env', s') <- evalStmt tyReg env s
-  (env'', ss') <- evalStmts tyReg env' ss
+  (env'', ss') <- evalStmts (registerDeclaration tyReg s) env' ss
   pure (env'', s' <> ss')
 
+-- Process a lexical block while remembering each shadowed binding at the point
+-- its declaration is reached. This preserves earlier updates to outer
+-- variables and restores only declarations owned by this block.
+evalScopedStmts :: TypeReg -> VEnv -> [MastStmt] -> EvalM (VEnv, [MastStmt])
+evalScopedStmts tyReg env = go tyReg env Map.empty
+  where
+    go _ current saved [] =
+      pure (restoreScopedBindings saved current, [])
+    go currentTyReg current saved (s : ss) = do
+      let saved' = saveShadowedBinding saved current s
+      (current', s') <- evalStmt currentTyReg current s
+      (current'', ss') <-
+        go (registerDeclaration currentTyReg s) current' saved' ss
+      pure (current'', s' <> ss')
+
 evalStmt :: TypeReg -> VEnv -> MastStmt -> EvalM (VEnv, [MastStmt])
 evalStmt tyReg env stmt = case stmt of
   MastLet ct i ty mInit -> do
     mInit' <- traverse (if ct then withComptimeMode . evalExp env else evalExp env) mInit
+    let shadowedEnv = deleteBindingsNamed (mastIdName i) env
     let env' = case mInit' of
-          Just e | isKnownValue e -> Map.insert i e env
-          _ -> Map.delete i env -- Shadow/remove any existing binding
-          -- Comptime lets with known values are dead after evaluation: all uses will be
-          -- substituted from VEnv, and EmitHull cannot handle string-typed variables.
+          Just e | isKnownValue e -> Map.insert i e shadowedEnv
+          _ -> shadowedEnv
+    -- Comptime lets with known values are dead after evaluation: all uses will be
+    -- substituted from VEnv, and EmitHull cannot handle string-typed variables.
     let stmts = case mInit' of
           Just e | ct && isKnownValue e -> []
           _ -> [MastLet ct i ty mInit']
@@ -339,7 +350,9 @@ evalStmt tyReg env stmt = case stmt of
         pure (mergeYulStateToVEnv tyReg yulState' env, [MastAsm yul'])
       Nothing ->
         pure (Map.empty, [MastAsm yul'])
-  MastSeq stmts -> evalStmts tyReg env stmts
+  MastSeq stmts -> do
+    (env', stmts') <- evalScopedStmts tyReg env stmts
+    pure (env', [MastSeq stmts'])
   MastBreak -> pure (env, [MastBreak])
   MastContinue -> pure (env, [MastContinue])
   MastFor initStmt cond post body -> do
@@ -366,9 +379,10 @@ evalLoopStmt :: VEnv -> MastStmt -> EvalM (VEnv, MastStmt)
 evalLoopStmt env st = case st of
   MastLet ct i ty mInit -> do
     mInit' <- traverse (evalExp env) mInit
+    let shadowedEnv = deleteBindingsNamed (mastIdName i) env
     let env' = case mInit' of
-          Just e | isKnownValue e -> Map.insert i e env
-          _ -> Map.delete i env
+          Just e | isKnownValue e -> Map.insert i e shadowedEnv
+          _ -> shadowedEnv
     pure (env', MastLet ct i ty mInit')
   MastAssign i e -> do
     e' <- evalExp env e
@@ -400,9 +414,20 @@ evalLoopStmt env st = case st of
   MastBreak -> pure (env, MastBreak)
   MastContinue -> pure (env, MastContinue)
   MastSeq stmts -> do
-    (env', stmts') <- mapAccumM evalLoopStmt env stmts
+    (env', stmts') <- evalScopedLoopStmts env stmts
     pure (env', MastSeq stmts')
 
+evalScopedLoopStmts :: VEnv -> [MastStmt] -> EvalM (VEnv, [MastStmt])
+evalScopedLoopStmts env = go env Map.empty
+  where
+    go current saved [] =
+      pure (restoreScopedBindings saved current, [])
+    go current saved (s : ss) = do
+      let saved' = saveShadowedBinding saved current s
+      (current', s') <- evalLoopStmt current s
+      (current'', ss') <- go current' saved' ss
+      pure (current'', s' : ss')
+
 evalAlt :: TypeReg -> VEnv -> MastAlt -> EvalM MastAlt
 evalAlt tyReg env (pat, body) = do
   -- Pattern bindings shadow existing bindings, but we don't track them
@@ -436,6 +461,51 @@ assignedInStmt (MastFor initStmt _ post body) =
 assignedInStmt (MastSeq stmts) = foldMap assignedInStmt stmts
 assignedInStmt _ = Set.empty
 
+type ScopedBindings = Map.Map Name VEnv
+
+registerDeclaration :: TypeReg -> MastStmt -> TypeReg
+registerDeclaration registry (MastLet _ mastId _ _) =
+  Map.insert (mastIdName mastId) mastId registry
+registerDeclaration registry _ = registry
+
+deleteBindingsNamed :: Name -> VEnv -> VEnv
+deleteBindingsNamed name =
+  Map.filterWithKey (\mastId _ -> mastIdName mastId /= name)
+
+bindingsNamed :: Name -> VEnv -> VEnv
+bindingsNamed name =
+  Map.filterWithKey (\mastId _ -> mastIdName mastId == name)
+
+-- Save a name only at its first direct declaration in this block. The snapshot
+-- is taken immediately before evaluating that declaration, after any earlier
+-- updates to the outer binding.
+saveShadowedBinding :: ScopedBindings -> VEnv -> MastStmt -> ScopedBindings
+saveShadowedBinding saved env (MastLet _ mastId _ _)
+  | Map.member name saved = saved
+  | otherwise = Map.insert name (bindingsNamed name env) saved
+  where
+    name = mastIdName mastId
+saveShadowedBinding saved _ _ = saved
+
+-- Remove every local identity for each declared name, then restore exactly the
+-- identities and known values visible when that declaration was reached.
+restoreScopedBindings :: ScopedBindings -> VEnv -> VEnv
+restoreScopedBindings saved current =
+  Map.foldlWithKey' restore current saved
+  where
+    restore inner name outer =
+      Map.union outer (deleteBindingsNamed name inner)
+
+-- | A scoped prefix that can be evaluated without losing control-flow or
+-- uninterpreted side effects before continuing with the enclosing body.
+isInlineableScopedPrefix :: [MastStmt] -> Bool
+isInlineableScopedPrefix = all inlineable
+  where
+    inlineable MastLet {} = True
+    inlineable MastAssign {} = True
+    inlineable (MastSeq stmts) = isInlineableScopedPrefix stmts
+    inlineable _ = False
+
 -----------------------------------------------------------------------
 -- Evaluate expressions
 -----------------------------------------------------------------------
@@ -874,10 +944,11 @@ evalFunBody _ _ [] = pure Nothing -- No return statement found
 evalFunBody tyReg env (stmt : rest) = case stmt of
   MastLet _ i _ mInit -> do
     mInit' <- traverse (evalExp env) mInit
+    let shadowedEnv = deleteBindingsNamed (mastIdName i) env
     let env' = case mInit' of
-          Just e | isKnownValue e -> Map.insert i e env
-          _ -> Map.delete i env
-    evalFunBody tyReg env' rest
+          Just e | isKnownValue e -> Map.insert i e shadowedEnv
+          _ -> shadowedEnv
+    evalFunBody (registerDeclaration tyReg stmt) env' rest
   MastAssign i e -> do
     e' <- evalExp env e
     let env' =
@@ -906,7 +977,19 @@ evalFunBody tyReg env (stmt : rest) = case stmt of
     case mYulState' of
       Just yulState' -> evalFunBody tyReg (mergeYulStateToVEnv tyReg yulState' env) rest
       Nothing -> pure Nothing
-  MastSeq stmts -> evalFunBody tyReg env stmts
+  MastSeq stmts
+    | isInlineableScopedPrefix stmts -> do
+        (env', _) <- evalScopedStmts tyReg env stmts
+        evalFunBody tyReg env' rest
+    -- A scoped control-flow body may itself return. Evaluate it speculatively:
+    -- a successful return keeps its effects, while failure restores memory,
+    -- fuel, and queued clones before the caller gives up on inlining.
+    | otherwise -> do
+        savedState <- lift get
+        result <- evalFunBody tyReg env stmts
+        case result of
+          Just {} -> pure result
+          Nothing -> lift (put savedState) >> pure Nothing
 
 -- Try to match a known scrutinee against alternatives.
 -- Returns the extended environment and the body of the matching alternative.
diff --git a/src/Solcore/Backend/NameEncoding.hs b/src/Solcore/Backend/NameEncoding.hs
new file mode 100644
index 000000000..a52ce155b
--- /dev/null
+++ b/src/Solcore/Backend/NameEncoding.hs
@@ -0,0 +1,76 @@
+module Solcore.Backend.NameEncoding
+  ( encodeBackendName,
+    encodeSpecialisedName,
+    encodeTypeIdentity,
+  )
+where
+
+import Data.Char (isAlpha, isAlphaNum, ord)
+import Data.List (isInfixOf)
+import Solcore.Frontend.Syntax.Name
+import Solcore.Frontend.Syntax.Ty
+
+-- | Encode a source-level name as a Hull/Yul identifier.
+--
+-- Plain backend-safe names are preserved because entry points and inline
+-- assembly refer to names such as @main@ by their source spelling. Encoded
+-- names use the reserved "$$" namespace; a plain name containing that marker
+-- is escaped, so source and compiler-generated names cannot forge each other.
+encodeBackendName :: Name -> String
+encodeBackendName (Name name)
+  | isBackendIdentifier name && not ("$$" `isInfixOf` name) = name
+  | otherwise = "$$N" ++ encodeSegment name
+encodeBackendName qualified@QualName {} =
+  "$$Q" ++ encodeNamePayload qualified
+
+-- | Form the backend name of a specialised declaration. Source identity and
+-- type-argument boundaries are both retained in the encoding.
+encodeSpecialisedName :: Name -> [Ty] -> Name
+encodeSpecialisedName name [] = Name (encodeBackendName name)
+encodeSpecialisedName name types =
+  Name
+    ( "$$S"
+        ++ encodeField (encodeBackendName name)
+        ++ encodeList (map encodeTypeIdentity types)
+    )
+
+-- | Encode the complete structural identity of a type.
+encodeTypeIdentity :: Ty -> String
+encodeTypeIdentity (TyVar (TVar name)) =
+  "V" ++ encodeField (encodeNamePayload name)
+encodeTypeIdentity (TyVar (Skolem name)) =
+  "K" ++ encodeField (encodeNamePayload name)
+encodeTypeIdentity (Meta (MetaTv name)) =
+  "M" ++ encodeField (encodeNamePayload name)
+encodeTypeIdentity (TyCon name types) =
+  "T"
+    ++ encodeField (encodeNamePayload name)
+    ++ encodeList (map encodeTypeIdentity types)
+
+isBackendIdentifier :: String -> Bool
+isBackendIdentifier [] = False
+isBackendIdentifier (first : rest) =
+  (isAlpha first || first == '_' || first == '$')
+    && all
+      (\char -> isAlphaNum char || char == '_' || char == '$')
+      rest
+
+-- Name constructors and qualification boundaries are retained explicitly.
+-- Code points prevent source spelling from imitating structural delimiters.
+encodeNamePayload :: Name -> String
+encodeNamePayload (Name name) = "N" ++ encodeSegment name
+encodeNamePayload (QualName qualifier leaf) =
+  "Q" ++ encodeField (encodeNamePayload qualifier) ++ encodeSegment leaf
+
+encodeSegment :: String -> String
+encodeSegment value =
+  show (length value)
+    ++ "$"
+    ++ concatMap (\char -> show (ord char) ++ "_") value
+
+encodeField :: String -> String
+encodeField value = show (length value) ++ "$" ++ value
+
+encodeList :: [String] -> String
+encodeList values =
+  show (length values) ++ "$" ++ concatMap encodeField values
diff --git a/src/Solcore/Backend/Specialise.hs b/src/Solcore/Backend/Specialise.hs
index 6f0a78e9f..a39758d08 100644
--- a/src/Solcore/Backend/Specialise.hs
+++ b/src/Solcore/Backend/Specialise.hs
@@ -20,10 +20,11 @@ import Control.Monad
 import Control.Monad.Except
 import Control.Monad.State
 import Data.Generics
-import Data.List (intercalate, union, (\\))
+import Data.List (union, (\\))
 import Data.Map qualified as Map
 import Data.Maybe (fromMaybe)
 import Solcore.Backend.Mast
+import Solcore.Backend.NameEncoding (encodeSpecialisedName)
 import Solcore.Desugarer.IfDesugarer (desugaredBoolTy)
 import Solcore.Frontend.Pretty.ShortName
 import Solcore.Frontend.Pretty.SolcorePretty
@@ -838,22 +839,7 @@ specMatch exps alts = do
       return e'
 
 specName :: Name -> [Ty] -> Name
-specName n [] = Name $ flattenQual n
-specName n ts = Name $ flattenQual n ++ "$" ++ intercalate "_" (map mangleTy ts)
-
-flattenQual :: Name -> String
-flattenQual (Name n) = n
-flattenQual (QualName n s) = flattenQual n ++ "_" ++ s
-
-mangleTy :: Ty -> String
-mangleTy (TyVar (TVar (Name n))) = n
-mangleTy (Meta (MetaTv (Name n))) = n
-mangleTy (TyCon (Name "()") []) = "unit"
--- Contract-local types carry a contract-qualified name (e.g. A.Color); flatten
--- the whole qualified name so the mangled identifier stays unique and Yul-safe.
-mangleTy (TyCon n []) = flattenQual n
-mangleTy (TyCon n ts) = flattenQual n ++ "L" ++ intercalate "_" (map mangleTy ts) ++ "J"
-mangleTy ty = error ("mangleTy - unexpected type: " ++ show ty)
+specName = encodeSpecialisedName
 
 prettyId :: Id -> String
 prettyId = render . pprId
@@ -1199,10 +1185,7 @@ toMastStmt EmptyStmt = MastSeq []
 toMastStmt s = error $ "toMastStmt: unexpected " ++ show s
 
 toMastBody :: [Stmt Id] -> [MastStmt]
-toMastBody = concatMap go
-  where
-    go (Block body) = toMastBody body
-    go stmt = [toMastStmt stmt]
+toMastBody = map toMastStmt
 
 toMastAlt :: ([Pat Id], [Stmt Id]) -> MastAlt
 toMastAlt ([p], body) = (toMastPat p, toMastBody body)
diff --git a/test/BackendBlockScopeTests.hs b/test/BackendBlockScopeTests.hs
new file mode 100644
index 000000000..9f1f63680
--- /dev/null
+++ b/test/BackendBlockScopeTests.hs
@@ -0,0 +1,200 @@
+module BackendBlockScopeTests (backendBlockScopeTests) where
+
+import Language.Hull qualified as Hull
+import Language.Yul (YLiteral (..), YulExp (..), YulStmt (..))
+import Solcore.Backend.Mast
+import Solcore.Backend.MastEval (defaultFuel, evalCompUnit)
+import Solcore.Frontend.Syntax.Name
+import Solcore.Frontend.Syntax.Stmt (Literal (..))
+import Solcore.Pipeline.Options (Option (..), stdOpt)
+import Solcore.Pipeline.SolcorePipeline (compile)
+import System.FilePath ((</>))
+import Test.Tasty
+import Test.Tasty.HUnit
+
+backendBlockScopeTests :: TestTree
+backendBlockScopeTests =
+  testGroup
+    "Backend lexical blocks"
+    [ sourceBlockTests,
+      typeRegistryScopeTest,
+      declarationPointScopeTest,
+      loopBlockScopeTest
+    ]
+
+sourceBlockTests :: TestTree
+sourceBlockTests =
+  testCase "blocks preserve shadowing, outer updates, and inline evaluation" $ do
+    let folder = "./test/examples/cases"
+        path = folder </> "block-shadowing.solc"
+    result <-
+      compile
+        stdOpt
+          { fileName = path,
+            optRootDir = folder,
+            optNoGenDispatch = True
+          }
+    case result of
+      Left err -> assertFailure err
+      Right objects -> assertMain objects
+
+assertMain :: [Hull.Object] -> Assertion
+assertMain objects =
+  case [ body
+       | Hull.Object name code _ <- objects,
+         name == "BlockShadowing",
+         Hull.SFunction "main" _ _ body <- code
+       ] of
+    [body] -> do
+      [value | Hull.SReturn (Hull.EWord value) <- body]
+        @?= [3]
+      assertBinding body "directShadow" 1
+      assertBinding body "inlineShadow" 1
+      assertBinding body "inlineUpdate" 3
+      assertBinding body "updateBeforeShadow" 2
+      mapM_
+        ( \value ->
+            assertBool
+              ("expected assignment " ++ show value ++ " in a nested Hull block")
+              (any (blockAssigns value) body)
+        )
+        [2, 3]
+    bodies ->
+      assertFailure
+        ("expected one BlockShadowing main body, got " ++ show (length bodies))
+
+assertBinding :: [Hull.Stmt] -> Hull.Name -> Integer -> Assertion
+assertBinding body name expected =
+  [value | Hull.SAssign (Hull.EVar actual) (Hull.EWord value) <- body, actual == name]
+    @?= [expected]
+
+blockAssigns :: Integer -> Hull.Stmt -> Bool
+blockAssigns expected (Hull.SBlock body) =
+  any isExpectedAssignment body
+  where
+    isExpectedAssignment
+      (Hull.SAssign (Hull.EVar "x") (Hull.EWord value)) =
+        value == expected
+    isExpectedAssignment _ = False
+blockAssigns _ _ = False
+
+typeRegistryScopeTest :: TestTree
+typeRegistryScopeTest =
+  testCase "assembly uses and updates the block-local identity" $ do
+    evaluatedReturn typeRegistryUnit @?= wordLiteral 1
+    case [ rhs
+         | MastSeq body <- evaluatedBody typeRegistryUnit,
+           MastAsm [YAssign [Name "x"] rhs] <- body
+         ] of
+      [rhs] -> rhs @?= YLit (YulNumber 2)
+      result -> assertFailure ("unexpected evaluated assembly: " ++ show result)
+
+typeRegistryUnit :: MastCompUnit
+typeRegistryUnit =
+  singleFunctionUnit
+    [ MastLet False outerId (Just outerType) (Just (wordLiteral 1)),
+      MastSeq
+        [ MastLet False innerId (Just wordType) (Just (wordLiteral 2)),
+          MastAsm [YAssign [Name "x"] (YIdent (Name "x"))]
+        ],
+      MastReturn (MastVar outerId)
+    ]
+  where
+    -- Keep the outer type ordered after "word" so a name-only Map collapse
+    -- would incorrectly prefer its known value.
+    outerType = MastTyCon (Name "zzOuter") []
+    wordType = MastTyCon (Name "word") []
+    outerId = MastId (Name "x") outerType
+    innerId = MastId (Name "x") wordType
+
+declarationPointScopeTest :: TestTree
+declarationPointScopeTest =
+  testCase "shadow restoration keeps updates made before the declaration" $
+    evaluatedReturn declarationPointUnit @?= wordLiteral 2
+
+declarationPointUnit :: MastCompUnit
+declarationPointUnit =
+  singleFunctionUnit
+    [ MastLet False xId (Just wordType) (Just (wordLiteral 1)),
+      MastSeq
+        [ MastAssign xId (wordLiteral 2),
+          MastLet False xId (Just wordType) (Just (wordLiteral 3))
+        ],
+      MastReturn (MastVar xId)
+    ]
+  where
+    wordType = MastTyCon (Name "word") []
+    xId = MastId (Name "x") wordType
+
+loopBlockScopeTest :: TestTree
+loopBlockScopeTest =
+  testCase "loop-local block shadowing does not change following loop statements" $
+    case evaluatedBody loopScopeUnit of
+      [ _,
+        MastFor
+          _
+          _
+          _
+          [MastSeq _, MastAssign _ (MastLit (IntLit value))],
+        _
+        ] ->
+          value @?= 1
+      body -> assertFailure ("unexpected evaluated loop body: " ++ show body)
+
+loopScopeUnit :: MastCompUnit
+loopScopeUnit =
+  singleFunctionUnit
+    [ MastLet False outerId (Just wordType) (Just (wordLiteral 1)),
+      MastFor
+        (MastSeq [])
+        (wordLiteral 1)
+        (MastSeq [])
+        [ MastSeq
+            [MastLet False outerId (Just wordType) (Just (wordLiteral 2))],
+          MastAssign resultId (MastVar outerId)
+        ],
+      MastReturn (MastVar outerId)
+    ]
+  where
+    wordType = MastTyCon (Name "word") []
+    outerId = MastId (Name "x") wordType
+    resultId = MastId (Name "result") wordType
+
+singleFunctionUnit :: [MastStmt] -> MastCompUnit
+singleFunctionUnit body =
+  MastCompUnit
+    []
+    [ MastTContr
+        ( MastContract
+            (Name "C")
+            [ MastCFunDecl
+                MastFunDef
+                  { mastFunName = Name "main",
+                    mastFunParams = [],
+                    mastFunRetComptime = False,
+                    mastFunReturn = MastTyCon (Name "word") [],
+                    mastFunBody = body
+                  }
+            ]
+        )
+    ]
+
+evaluatedReturn :: MastCompUnit -> MastExp
+evaluatedReturn unit =
+  case reverse (evaluatedBody unit) of
+    MastReturn value : _ -> value
+    body -> error ("missing evaluated return: " ++ show body)
+
+evaluatedBody :: MastCompUnit -> [MastStmt]
+evaluatedBody unit =
+  case evalCompUnit defaultFuel unit of
+    ( MastCompUnit
+        _
+        [MastTContr (MastContract _ (MastCFunDecl function : _))],
+      _
+      ) ->
+        mastFunBody function
+    result -> error ("unexpected evaluated unit: " ++ show result)
+
+wordLiteral :: Integer -> MastExp
+wordLiteral = MastLit . IntLit
diff --git a/test/BackendNameEncodingTests.hs b/test/BackendNameEncodingTests.hs
new file mode 100644
index 000000000..05faee981
--- /dev/null
+++ b/test/BackendNameEncodingTests.hs
@@ -0,0 +1,170 @@
+module BackendNameEncodingTests (backendNameEncodingTests) where
+
+import Common.LightYear (runParserE)
+import Control.Monad (forM_)
+import Data.List (nub)
+import Language.Hull qualified as Hull
+import Language.Hull.Parser (hullObject)
+import Solcore.Backend.EmitHull (emitHull)
+import Solcore.Backend.Mast
+import Solcore.Backend.NameEncoding
+import Solcore.Frontend.Syntax.Contract (Constr (..), DataTy (..))
+import Solcore.Frontend.Syntax.Name
+import Solcore.Frontend.Syntax.Ty
+import Test.Tasty
+import Test.Tasty.HUnit
+
+backendNameEncodingTests :: TestTree
+backendNameEncodingTests =
+  testGroup
+    "Backend name encoding"
+    [ sourceNameTests,
+      typeIdentityTests,
+      specialisedNameTests,
+      hullTypeNameTest
+    ]
+
+sourceNameTests :: TestTree
+sourceNameTests =
+  testGroup
+    "source names"
+    [ testCase "plain backend names retain their spelling" $
+        encodeBackendName (Name "main") @?= "main",
+      testCase "qualification cannot collide with underscore spelling" $ do
+        let names =
+              [ QualName (QualName (Name "A") "B") "C",
+                QualName (Name "A_B") "C",
+                QualName (Name "A") "B_C",
+                Name "A_B_C"
+              ]
+        assertDistinct (map encodeBackendName names),
+      testCase "plain names cannot forge the reserved namespace" $ do
+        let plain = Name "$$Qforged"
+            qualified = QualName (Name "Q") "forged"
+        assertBool
+          "reserved plain and qualified names must differ"
+          (encodeBackendName plain /= encodeBackendName qualified)
+    ]
+
+typeIdentityTests :: TestTree
+typeIdentityTests =
+  testGroup
+    "type identities"
+    [ testCase "constructor arity and argument boundaries remain distinct" $ do
+        let oneArgument =
+              TyCon (Name "Container") [TyCon (Name "A_B") []]
+            twoArguments =
+              TyCon
+                (Name "Container")
+                [TyCon (Name "A") [], TyCon (Name "B") []]
+        assertBool
+          "one structured argument must not equal two arguments"
+          (encodeTypeIdentity oneArgument /= encodeTypeIdentity twoArguments),
+      testCase "qualified and underscore-spelled constructors remain distinct" $ do
+        let qualified = TyCon (QualName (Name "C") "S") []
+            flat = TyCon (Name "C_S") []
+        assertBool
+          "C.S and C_S must have distinct type identities"
+          (encodeTypeIdentity qualified /= encodeTypeIdentity flat),
+      testCase "builtin unit and a source type named unit remain distinct" $ do
+        let builtinUnit = TyCon (Name "()") []
+            sourceUnit = TyCon (Name "unit") []
+        assertBool
+          "() and unit must have distinct type identities"
+          (encodeTypeIdentity builtinUnit /= encodeTypeIdentity sourceUnit),
+      testCase "type representation constructors remain distinct" $ do
+        let name = Name "T"
+            variants =
+              [ TyCon name [],
+                TyVar (TVar name),
+                TyVar (Skolem name),
+                Meta (MetaTv name)
+              ]
+        assertDistinct (map encodeTypeIdentity variants)
+    ]
+
+specialisedNameTests :: TestTree
+specialisedNameTests =
+  testGroup
+    "specialised names"
+    [ testCase "source identity survives specialisation" $ do
+        let ty = TyCon (Name "word") []
+            qualified = encodeSpecialisedName (QualName (Name "C") "f") [ty]
+            flat = encodeSpecialisedName (Name "C_f") [ty]
+        assertBool
+          "C.f and C_f specialisations must differ"
+          (qualified /= flat),
+      testCase "unspecialised and specialised declarations are disjoint" $ do
+        let name = Name "f"
+            ty = TyCon (Name "word") []
+        assertBool
+          "a specialised name must not equal its unspecialised source name"
+          (encodeSpecialisedName name [] /= encodeSpecialisedName name [ty])
+    ]
+
+hullTypeNameTest :: TestTree
+hullTypeNameTest =
+  testCase "Hull type labels use encoded source identities" $ do
+    objects <- emitHull False mastCompUnit
+    case objects of
+      [Hull.Object _ statements _] -> do
+        functionArgumentLabels statements
+          @?= [ ("qualifiedValue", encodeBackendName qualifiedType),
+                ("flatValue", encodeBackendName flatType)
+              ]
+        forM_ objects $ \object ->
+          case runParserE hullObject "<generated Hull>" (show object) of
+            Left err ->
+              assertFailure ("generated Hull must parse successfully:\n" ++ err)
+            Right _ -> pure ()
+      _ -> assertFailure ("unexpected Hull objects: " ++ show objects)
+  where
+    qualifiedType = QualName (Name "C") "S"
+    flatType = Name "C_S"
+
+    mastCompUnit =
+      MastCompUnit
+        []
+        [ MastTContr
+            ( MastContract
+                (Name "C")
+                [ MastCDataDecl (nullaryData qualifiedType),
+                  MastCDataDecl (nullaryData flatType),
+                  identityFunction "qualifiedValue" qualifiedType,
+                  identityFunction "flatValue" flatType
+                ]
+            )
+        ]
+
+    nullaryData name =
+      DataTy
+        { dataName = name,
+          dataParams = [],
+          dataConstrs = [Constr (QualName name "Value") []],
+          dataDerivings = []
+        }
+
+    identityFunction functionName typeName =
+      MastCFunDecl
+        MastFunDef
+          { mastFunName = functionName,
+            mastFunParams = [MastParam "value" False mastType],
+            mastFunRetComptime = False,
+            mastFunReturn = mastType,
+            mastFunBody = [MastReturn (MastVar (MastId "value" mastType))]
+          }
+      where
+        mastType = MastTyCon typeName []
+
+functionArgumentLabels :: [Hull.Stmt] -> [(Hull.Name, String)]
+functionArgumentLabels statements =
+  [ (functionName, label)
+  | Hull.SFunction functionName [Hull.TArg _ (Hull.TNamed label _)] _ _ <- statements
+  ]
+
+assertDistinct :: (Eq a, Show a) => [a] -> Assertion
+assertDistinct values =
+  assertEqual
+    ("expected pairwise-distinct values, got " ++ show values)
+    (length values)
+    (length (nub values))
diff --git a/test/Main.hs b/test/Main.hs
index c5a06387e..1bf74093f 100644
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -1,5 +1,7 @@
 module Main where
 
+import BackendBlockScopeTests
+import BackendNameEncodingTests
 import Cases
 import ContractAbiTests
 import DiagnosticCliTests
@@ -20,7 +22,9 @@ tests :: TestTree
 tests =
   testGroup
     "Tests"
-    [ parserTests,
+    [ backendBlockScopeTests,
+      backendNameEncodingTests,
+      parserTests,
       cases,
       tabledResolution,
       comptime,
diff --git a/test/examples/cases/block-shadowing.solc b/test/examples/cases/block-shadowing.solc
new file mode 100644
index 000000000..c9849534a
--- /dev/null
+++ b/test/examples/cases/block-shadowing.solc
@@ -0,0 +1,41 @@
+contract BlockShadowing {
+  function main() -> word {
+    let x: word = 1;
+    {
+      let x: word = 2;
+    }
+    let directShadow: word = x;
+    let inlineShadow: word = shadowedValue();
+    let inlineUpdate: word = updatedValue();
+    let updateBeforeShadow: word = updatedBeforeShadow();
+    {
+      x = 3;
+    }
+    return x;
+  }
+}
+
+function shadowedValue() -> word {
+  let x: word = 1;
+  {
+    let x: word = 2;
+  }
+  return x;
+}
+
+function updatedValue() -> word {
+  let x: word = 1;
+  {
+    x = 3;
+  }
+  return x;
+}
+
+function updatedBeforeShadow() -> word {
+  let x: word = 1;
+  {
+    x = 2;
+    let x: word = 3;
+  }
+  return x;
+}