Repository: bytecodealliance/wasmtime
Pull request #7274 (2023-10-17 22:00:35)

PCC: initial end-to-end integration with Wasmtime's static memories.
This PR wires up end-to-end support for validating the compilation of accesses to static memories in Wasmtime. It creates "memory types" for the vmcontext struct and the memories it points to, and it adds PCC annotations to the relevant memory pointers. On aarch64 (where instruction semantics for PCC are implemented), this validates a simple `i32.load` function body with default memory configuration.

Note that facts are not yet propagated through egraph rewrites, so optimization has to be disabled for this to work; that support will come next.

Co-authored-by: Nick Fitzgerald <fitzgen@gmail.com>

cfallin: Just a heads-up that the last commit has a few blessed expected-output changes on the Wasm memory access tests, because we had removed the special case `vmctx` GV lowering (so there are a few more aliases now). No functional change so I think it should be fine...
github-actions[bot]: #### Subscribe to Label Action

cc @peterhuene

<details>
This issue or pull request has been labeled: "cranelift", "cranelift:area:aarch64", "cranelift:area:machinst", "cranelift:meta", "cranelift:wasm", "wasmtime:api", "wasmtime:config"

Thus the following users have been cc'd because of the following labels:

* peterhuene: wasmtime:api

To subscribe or unsubscribe from this label, edit the <code>.github/subscribe-to-label.json</code> configuration file.

[Learn more.](https://github.com/bytecodealliance/subscribe-to-label-action)
</details>
github-actions[bot]: #### Label Messager: wasmtime:config

It looks like you are changing Wasmtime's configuration options. Make sure to
complete this check list:

* [ ] If you added a new `Config` method, you wrote extensive documentation for
      it.

  <details>

  Our documentation should be of the following form:

  ```text
  Short, simple summary sentence.

  More details. These details can be multiple paragraphs. There should be
  information about not just the method, but its parameters and results as
  well.

  Is this method fallible? If so, when can it return an error?

  Can this method panic? If so, when does it panic?

  # Example

  Optional example here.
  ```

  </details>

* [ ] If you added a new `Config` method, or modified an existing one, you
  ensured that this configuration is exercised by the fuzz targets.

  <details>

  For example, if you expose a new strategy for allocating the next instance
  slot inside the pooling allocator, you should ensure that at least one of our
  fuzz targets exercises that new strategy.

  Often, all that is required of you is to ensure that there is a knob for this
  configuration option in [`wasmtime_fuzzing::Config`][fuzzing-config] (or one
  of its nested `struct`s).

  Rarely, this may require authoring a new fuzz target to specifically test this
  configuration. See [our docs on fuzzing][fuzzing-docs] for more details.

  </details>

* [ ] If you are enabling a configuration option by default, make sure that it
  has been fuzzed for at least two weeks before turning it on by default.

[fuzzing-config]: https://github.com/bytecodealliance/wasmtime/blob/ca0e8d0a1d8cefc0496dba2f77a670571d8fdcab/crates/fuzzing/src/generators.rs#L182-L194
[fuzzing-docs]: https://docs.wasmtime.dev/contributing-fuzzing.html


--------------------------------------------------------------------------------

<details>

To modify this label's message, edit the <code>.github/label-messager/wasmtime-config.md</code> file.

To add new label messages or remove existing label messages, edit the
<code>.github/label-messager.json</code> configuration file.

[Learn more.](https://github.com/bytecodealliance/label-messager-action)

</details>

Patch:
diff --git a/cranelift/codegen/meta/src/shared/settings.rs b/cranelift/codegen/meta/src/shared/settings.rs
index e97708873..f63228014 100644
--- a/cranelift/codegen/meta/src/shared/settings.rs
+++ b/cranelift/codegen/meta/src/shared/settings.rs
@@ -67,7 +67,12 @@ pub(crate) fn define() -> SettingGroup {
         "enable_pcc",
         "Enable proof-carrying code translation validation.",
         r#"
-            This adds a proof-carrying code mode. TODO ADD MORE
+            This adds a proof-carrying-code mode. Proof-carrying code (PCC) is a strategy to verify
+            that the compiler preserves certain properties or invariants in the compiled code.
+            For example, a frontend that translates WebAssembly to CLIF can embed PCC facts in
+            the CLIF, and Cranelift will verify that the final machine code satisfies the stated
+            facts at each intermediate computed value. Loads and stores can be marked as "checked"
+            and their memory effects can be verified as safe.
         "#,
         false,
     );
diff --git a/cranelift/codegen/src/ir/function.rs b/cranelift/codegen/src/ir/function.rs
index 081ef15b2..5d91e705e 100644
--- a/cranelift/codegen/src/ir/function.rs
+++ b/cranelift/codegen/src/ir/function.rs
@@ -5,10 +5,10 @@
 
 use crate::entity::{PrimaryMap, SecondaryMap};
 use crate::ir::{
-    self, Block, DataFlowGraph, DynamicStackSlot, DynamicStackSlotData, DynamicStackSlots,
-    DynamicType, ExtFuncData, FuncRef, GlobalValue, GlobalValueData, Inst, JumpTable,
-    JumpTableData, Layout, MemoryType, MemoryTypeData, Opcode, SigRef, Signature, SourceLocs,
-    StackSlot, StackSlotData, StackSlots, Table, TableData, Type,
+    self, pcc::Fact, Block, DataFlowGraph, DynamicStackSlot, DynamicStackSlotData,
+    DynamicStackSlots, DynamicType, ExtFuncData, FuncRef, GlobalValue, GlobalValueData, Inst,
+    JumpTable, JumpTableData, Layout, MemoryType, MemoryTypeData, Opcode, SigRef, Signature,
+    SourceLocs, StackSlot, StackSlotData, StackSlots, Table, TableData, Type,
 };
 use crate::isa::CallConv;
 use crate::write::write_function;
@@ -172,6 +172,9 @@ pub struct FunctionStencil {
     /// Global values referenced.
     pub global_values: PrimaryMap<ir::GlobalValue, ir::GlobalValueData>,
 
+    /// Global value proof-carrying-code facts.
+    pub global_value_facts: SecondaryMap<ir::GlobalValue, Option<Fact>>,
+
     /// Memory types for proof-carrying code.
     pub memory_types: PrimaryMap<ir::MemoryType, ir::MemoryTypeData>,
 
@@ -204,6 +207,7 @@ impl FunctionStencil {
         self.sized_stack_slots.clear();
         self.dynamic_stack_slots.clear();
         self.global_values.clear();
+        self.global_value_facts.clear();
         self.memory_types.clear();
         self.tables.clear();
         self.dfg.clear();
@@ -417,6 +421,7 @@ impl Function {
                 sized_stack_slots: StackSlots::new(),
                 dynamic_stack_slots: DynamicStackSlots::new(),
                 global_values: PrimaryMap::new(),
+                global_value_facts: SecondaryMap::new(),
                 memory_types: PrimaryMap::new(),
                 tables: PrimaryMap::new(),
                 dfg: DataFlowGraph::new(),
diff --git a/cranelift/codegen/src/ir/globalvalue.rs b/cranelift/codegen/src/ir/globalvalue.rs
index 530875641..438a13e50 100644
--- a/cranelift/codegen/src/ir/globalvalue.rs
+++ b/cranelift/codegen/src/ir/globalvalue.rs
@@ -1,7 +1,7 @@
 //! Global values.
 
 use crate::ir::immediates::{Imm64, Offset32};
-use crate::ir::{ExternalName, GlobalValue, Type};
+use crate::ir::{ExternalName, GlobalValue, MemFlags, Type};
 use crate::isa::TargetIsa;
 use core::fmt;
 
@@ -31,9 +31,8 @@ pub enum GlobalValueData {
         /// Type of the loaded value.
         global_type: Type,
 
-        /// Specifies whether the memory that this refers to is readonly, allowing for the
-        /// elimination of redundant loads.
-        readonly: bool,
+        /// Specifies the memory flags to be used by the load. Guaranteed to be notrap and aligned.
+        flags: MemFlags,
     },
 
     /// Value is an offset from another global value.
@@ -111,15 +110,8 @@ impl fmt::Display for GlobalValueData {
                 base,
                 offset,
                 global_type,
-                readonly,
-            } => write!(
-                f,
-                "load.{} notrap aligned {}{}{}",
-                global_type,
-                if readonly { "readonly " } else { "" },
-                base,
-                offset
-            ),
+                flags,
+            } => write!(f, "load.{}{} {}{}", global_type, flags, base, offset),
             Self::IAddImm {
                 global_type,
                 base,
diff --git a/cranelift/codegen/src/ir/pcc.rs b/cranelift/codegen/src/ir/pcc.rs
index 7502610a5..406228000 100644
--- a/cranelift/codegen/src/ir/pcc.rs
+++ b/cranelift/codegen/src/ir/pcc.rs
@@ -53,6 +53,10 @@
 //! - Support bounds-checking-type operations for dynamic memories and
 //!   tables.
 //!
+//! More checks:
+//! - Check that facts on `vmctx` GVs are subsumed by the actual facts
+//!   on the vmctx arg in block0 (function arg).
+//!
 //! Generality:
 //! - facts on outputs (in func signature)?
 //! - Implement checking at the CLIF level as well.
@@ -79,6 +83,7 @@ use crate::ir;
 use crate::ir::types::*;
 use crate::isa::TargetIsa;
 use crate::machinst::{BlockIndex, LowerBackend, MachInst, VCode};
+use crate::trace;
 use regalloc2::Function as _;
 use std::fmt;
 
@@ -440,6 +445,13 @@ impl<'a> FactContext<'a> {
         // support positive offsets.
         let offset = u64::try_from(offset).ok()?;
 
+        trace!(
+            "FactContext::offset: {:?} + {} in width {}",
+            fact,
+            offset,
+            width
+        );
+
         match fact {
             Fact::Range {
                 bit_width,
@@ -460,8 +472,8 @@ impl<'a> FactContext<'a> {
                 min_offset: mem_min_offset,
                 max_offset: mem_max_offset,
             } => {
-                let min_offset = mem_min_offset.checked_sub(offset)?;
-                let max_offset = mem_max_offset.checked_sub(offset)?;
+                let min_offset = mem_min_offset.checked_add(offset)?;
+                let max_offset = mem_max_offset.checked_add(offset)?;
                 Some(Fact::Mem {
                     ty: *ty,
                     min_offset,
diff --git a/cranelift/codegen/src/isa/aarch64/pcc.rs b/cranelift/codegen/src/isa/aarch64/pcc.rs
index 83a039ec6..5c43ae053 100644
--- a/cranelift/codegen/src/isa/aarch64/pcc.rs
+++ b/cranelift/codegen/src/isa/aarch64/pcc.rs
@@ -346,9 +346,7 @@ fn check_addr<'a>(
             let rm = get_fact_or_default(vcode, rm)?;
             let rm_extended = fail_if_missing(extend_fact(ctx, rm, extendop))?;
             let sum = fail_if_missing(ctx.add(&rn, &rm_extended, 64))?;
-            trace!("rn = {rn:?} rm = {rm:?} rm_extended = {rm_extended:?} sum = {sum:?}");
             check(&sum, ty)?;
-            trace!(" -> checks out!");
             Ok(())
         }
         &AMode::Unscaled { rn, simm9 } => {
@@ -358,11 +356,13 @@ fn check_addr<'a>(
         }
         &AMode::UnsignedOffset { rn, uimm12 } => {
             let rn = get_fact_or_default(vcode, rn)?;
-            // Safety: this will not overflow: `size` should be at
-            // most 32 or 64 for large vector ops, and the `uimm12`'s
-            // value is at most 4095.
-            let uimm12: u64 = uimm12.value.into();
-            let offset: u64 = uimm12.checked_mul(ty.bytes().into()).unwrap();
+            // N.B.: the architecture scales the immediate in the
+            // encoded instruction by the size of the loaded type, so
+            // e.g. an offset field of 4095 can mean a load of offset
+            // 32760 (= 4095 * 8) for I64s. The `UImm12Scaled` type
+            // stores the *scaled* value, so we don't need to multiply
+            // (again) by the type's size here.
+            let offset: u64 = uimm12.value.into();
             // This `unwrap()` will always succeed because the value
             // will always be positive and much smaller than
             // `i64::MAX` (see above).
diff --git a/cranelift/codegen/src/legalizer/globalvalue.rs b/cranelift/codegen/src/legalizer/globalvalue.rs
index 57fa29e1f..4ab5a4ad2 100644
--- a/cranelift/codegen/src/legalizer/globalvalue.rs
+++ b/cranelift/codegen/src/legalizer/globalvalue.rs
@@ -21,7 +21,7 @@ pub fn expand_global_value(
     );
 
     match func.global_values[global_value] {
-        ir::GlobalValueData::VMContext => vmctx_addr(inst, func),
+        ir::GlobalValueData::VMContext => vmctx_addr(global_value, inst, func),
         ir::GlobalValueData::IAddImm {
             base,
             offset,
@@ -31,8 +31,8 @@ pub fn expand_global_value(
             base,
             offset,
             global_type,
-            readonly,
-        } => load_addr(inst, func, base, offset, global_type, readonly, isa),
+            flags,
+        } => load_addr(inst, func, base, offset, global_type, flags, isa),
         ir::GlobalValueData::Symbol { tls, .. } => symbol(inst, func, global_value, isa, tls),
         ir::GlobalValueData::DynScaleTargetConst { vector_type } => {
             const_vector_scale(inst, func, vector_type, isa)
@@ -52,7 +52,7 @@ fn const_vector_scale(inst: ir::Inst, func: &mut ir::Function, ty: ir::Type, isa
 }
 
 /// Expand a `global_value` instruction for a vmctx global.
-fn vmctx_addr(inst: ir::Inst, func: &mut ir::Function) {
+fn vmctx_addr(global_value: ir::GlobalValue, inst: ir::Inst, func: &mut ir::Function) {
     // Get the value representing the `vmctx` argument.
     let vmctx = func
         .special_param(ir::ArgumentPurpose::VMContext)
@@ -63,6 +63,15 @@ fn vmctx_addr(inst: ir::Inst, func: &mut ir::Function) {
     func.dfg.clear_results(inst);
     func.dfg.change_to_alias(result, vmctx);
     func.layout.remove_inst(inst);
+
+    // If there was a fact on the GV, then copy it to the vmctx arg
+    // blockparam def.
+    if let Some(fact) = &func.global_value_facts[global_value] {
+        if func.dfg.facts[vmctx].is_none() {
+            let fact = fact.clone();
+            func.dfg.facts[vmctx] = Some(fact);
+        }
+    }
 }
 
 /// Expand a `global_value` instruction for an iadd_imm global.
@@ -75,15 +84,11 @@ fn iadd_imm_addr(
 ) {
     let mut pos = FuncCursor::new(func).at_inst(inst);
 
-    // Get the value for the lhs. For tidiness, expand VMContext here so that we avoid
-    // `vmctx_addr` which creates an otherwise unneeded value alias.
-    let lhs = if let ir::GlobalValueData::VMContext = pos.func.global_values[base] {
-        pos.func
-            .special_param(ir::ArgumentPurpose::VMContext)
-            .expect("Missing vmctx parameter")
-    } else {
-        pos.ins().global_value(global_type, base)
-    };
+    // Get the value for the lhs.
+    let lhs = pos.ins().global_value(global_type, base);
+    if let Some(fact) = &pos.func.global_value_facts[base] {
+        pos.func.dfg.facts[lhs] = Some(fact.clone());
+    }
 
     // Simply replace the `global_value` instruction with an `iadd_imm`, reusing the result value.
     pos.func.dfg.replace(inst).iadd_imm(lhs, offset);
@@ -96,7 +101,7 @@ fn load_addr(
     base: ir::GlobalValue,
     offset: ir::immediates::Offset32,
     global_type: ir::Type,
-    readonly: bool,
+    flags: ir::MemFlags,
     isa: &dyn TargetIsa,
 ) {
     // We need to load a pointer from the `base` global value, so insert a new `global_value`
@@ -106,27 +111,17 @@ fn load_addr(
     let mut pos = FuncCursor::new(func).at_inst(inst);
     pos.use_srcloc(inst);
 
-    // Get the value for the base. For tidiness, expand VMContext here so that we avoid
-    // `vmctx_addr` which creates an otherwise unneeded value alias.
-    let base_addr = if let ir::GlobalValueData::VMContext = pos.func.global_values[base] {
-        pos.func
-            .special_param(ir::ArgumentPurpose::VMContext)
-            .expect("Missing vmctx parameter")
-    } else {
-        pos.ins().global_value(ptr_ty, base)
-    };
-
-    // Global-value loads are always notrap and aligned. They may be readonly.
-    let mut mflags = ir::MemFlags::trusted();
-    if readonly {
-        mflags.set_readonly();
+    // Get the value for the base.
+    let base_addr = pos.ins().global_value(ptr_ty, base);
+    if let Some(fact) = &pos.func.global_value_facts[base] {
+        pos.func.dfg.facts[base_addr] = Some(fact.clone());
     }
 
     // Perform the load.
     pos.func
         .dfg
         .replace(inst)
-        .load(global_type, mflags, base_addr, offset);
+        .load(global_type, flags, base_addr, offset);
 }
 
 /// Expand a `global_value` instruction for a symbolic name global.
diff --git a/cranelift/codegen/src/machinst/abi.rs b/cranelift/codegen/src/machinst/abi.rs
index fd0e71add..afeedec7d 100644
--- a/cranelift/codegen/src/machinst/abi.rs
+++ b/cranelift/codegen/src/machinst/abi.rs
@@ -1319,7 +1319,7 @@ fn generate_gv<M: ABIMachineSpec>(
             base,
             offset,
             global_type: _,
-            readonly: _,
+            flags: _,
         } => {
             let base = generate_gv::<M>(f, sigs, sig, base, insts);
             let into_reg = Writable::from_reg(M::get_stacklimit_reg(f.stencil.signature.call_conv));
diff --git a/cranelift/codegen/src/print_errors.rs b/cranelift/codegen/src/print_errors.rs
index e3fe73661..679ce12a2 100644
--- a/cranelift/codegen/src/print_errors.rs
+++ b/cranelift/codegen/src/print_errors.rs
@@ -4,6 +4,7 @@ use crate::entity::SecondaryMap;
 use crate::ir;
 use crate::ir::entities::{AnyEntity, Block, Inst, Value};
 use crate::ir::function::Function;
+use crate::ir::pcc::Fact;
 use crate::result::CodegenError;
 use crate::verifier::{VerifierError, VerifierErrors};
 use crate::write::{decorate_function, FuncWriter, PlainWriter};
@@ -71,8 +72,9 @@ impl<'a> FuncWriter for PrettyVerifierError<'a> {
         func: &Function,
         entity: AnyEntity,
         value: &dyn fmt::Display,
+        maybe_fact: Option<&Fact>,
     ) -> fmt::Result {
-        pretty_preamble_error(w, func, entity, value, &mut *self.0, self.1)
+        pretty_preamble_error(w, func, entity, value, maybe_fact, &mut *self.0, self.1)
     }
 }
 
@@ -156,11 +158,12 @@ fn pretty_preamble_error(
     func: &Function,
     entity: AnyEntity,
     value: &dyn fmt::Display,
+    maybe_fact: Option<&Fact>,
     func_w: &mut dyn FuncWriter,
     errors: &mut Vec<VerifierError>,
 ) -> fmt::Result {
     let mut s = String::new();
-    func_w.write_entity_definition(&mut s, func, entity, value)?;
+    func_w.write_entity_definition(&mut s, func, entity, value, maybe_fact)?;
     write!(w, "{}", s)?;
 
     // TODO: Use drain_filter here when it gets stabilized
diff --git a/cranelift/codegen/src/write.rs b/cranelift/codegen/src/write.rs
index a550af4f3..3bfc4d770 100644
--- a/cranelift/codegen/src/write.rs
+++ b/cranelift/codegen/src/write.rs
@@ -5,6 +5,7 @@
 
 use crate::entity::SecondaryMap;
 use crate::ir::entities::AnyEntity;
+use crate::ir::pcc::Fact;
 use crate::ir::{Block, DataFlowGraph, Function, Inst, SigRef, Type, Value, ValueDef};
 use crate::packed_option::ReservedValue;
 use alloc::string::{String, ToString};
@@ -43,28 +44,29 @@ pub trait FuncWriter {
 
         for (ss, slot) in func.dynamic_stack_slots.iter() {
             any = true;
-            self.write_entity_definition(w, func, ss.into(), slot)?;
+            self.write_entity_definition(w, func, ss.into(), slot, None)?;
         }
 
         for (ss, slot) in func.sized_stack_slots.iter() {
             any = true;
-            self.write_entity_definition(w, func, ss.into(), slot)?;
+            self.write_entity_definition(w, func, ss.into(), slot, None)?;
         }
 
         for (gv, gv_data) in &func.global_values {
             any = true;
-            self.write_entity_definition(w, func, gv.into(), gv_data)?;
+            let maybe_fact = func.global_value_facts[gv].as_ref();
+            self.write_entity_definition(w, func, gv.into(), gv_data, maybe_fact)?;
         }
 
         for (mt, mt_data) in &func.memory_types {
             any = true;
-            self.write_entity_definition(w, func, mt.into(), mt_data)?;
+            self.write_entity_definition(w, func, mt.into(), mt_data, None)?;
         }
 
         for (table, table_data) in &func.tables {
             if !table_data.index_type.is_invalid() {
                 any = true;
-                self.write_entity_definition(w, func, table.into(), table_data)?;
+                self.write_entity_definition(w, func, table.into(), table_data, None)?;
             }
         }
 
@@ -72,7 +74,7 @@ pub trait FuncWriter {
         // signatures.
         for (sig, sig_data) in &func.dfg.signatures {
             any = true;
-            self.write_entity_definition(w, func, sig.into(), &sig_data)?;
+            self.write_entity_definition(w, func, sig.into(), &sig_data, None)?;
         }
 
         for (fnref, ext_func) in &func.dfg.ext_funcs {
@@ -83,18 +85,19 @@ pub trait FuncWriter {
                     func,
                     fnref.into(),
                     &ext_func.display(Some(&func.params)),
+                    None,
                 )?;
             }
         }
 
         for (&cref, cval) in func.dfg.constants.iter() {
             any = true;
-            self.write_entity_definition(w, func, cref.into(), cval)?;
+            self.write_entity_definition(w, func, cref.into(), cval, None)?;
         }
 
         if let Some(limit) = func.stack_limit {
             any = true;
-            self.write_entity_definition(w, func, AnyEntity::StackLimit, &limit)?;
+            self.write_entity_definition(w, func, AnyEntity::StackLimit, &limit, None)?;
         }
 
         Ok(any)
@@ -107,8 +110,9 @@ pub trait FuncWriter {
         func: &Function,
         entity: AnyEntity,
         value: &dyn fmt::Display,
+        maybe_fact: Option<&Fact>,
     ) -> fmt::Result {
-        self.super_entity_definition(w, func, entity, value)
+        self.super_entity_definition(w, func, entity, value, maybe_fact)
     }
 
     /// Default impl of `write_entity_definition`
@@ -119,8 +123,13 @@ pub trait FuncWriter {
         func: &Function,
         entity: AnyEntity,
         value: &dyn fmt::Display,
+        maybe_fact: Option<&Fact>,
     ) -> fmt::Result {
-        writeln!(w, "    {} = {}", entity, value)
+        if let Some(fact) = maybe_fact {
+            writeln!(w, "    {} ! {} = {}", entity, fact, value)
+        } else {
+            writeln!(w, "    {} = {}", entity, value)
+        }
     }
 }
 
diff --git a/cranelift/reader/src/parser.rs b/cranelift/reader/src/parser.rs
index 16baa3588..b088af004 100644
--- a/cranelift/reader/src/parser.rs
+++ b/cranelift/reader/src/parser.rs
@@ -305,7 +305,13 @@ impl Context {
     }
 
     // Allocate a global value slot.
-    fn add_gv(&mut self, gv: GlobalValue, data: GlobalValueData, loc: Location) -> ParseResult<()> {
+    fn add_gv(
+        &mut self,
+        gv: GlobalValue,
+        data: GlobalValueData,
+        maybe_fact: Option<Fact>,
+        loc: Location,
+    ) -> ParseResult<()> {
         self.map.def_gv(gv, loc)?;
         while self.function.global_values.next_key().index() <= gv.index() {
             self.function.create_global_value(GlobalValueData::Symbol {
@@ -316,6 +322,9 @@ impl Context {
             });
         }
         self.function.global_values[gv] = data;
+        if let Some(fact) = maybe_fact {
+            self.function.global_value_facts[gv] = Some(fact);
+        }
         Ok(())
     }
 
@@ -1468,7 +1477,7 @@ impl<'a> Parser<'a> {
                 Some(Token::GlobalValue(..)) => {
                     self.start_gathering_comments();
                     self.parse_global_value_decl()
-                        .and_then(|(gv, dat)| ctx.add_gv(gv, dat, self.loc))
+                        .and_then(|(gv, dat, maybe_fact)| ctx.add_gv(gv, dat, maybe_fact, self.loc))
                 }
                 Some(Token::MemoryType(..)) => {
                     self.start_gathering_comments();
@@ -1574,16 +1583,25 @@ impl<'a> Parser<'a> {
 
     // Parse a global value decl.
     //
-    // global-val-decl ::= * GlobalValue(gv) "=" global-val-desc
+    // global-val-decl ::= * GlobalValue(gv) [ "!" fact ] "=" global-val-desc
     // global-val-desc ::= "vmctx"
     //                   | "load" "." type "notrap" "aligned" GlobalValue(base) [offset]
     //                   | "iadd_imm" "(" GlobalValue(base) ")" imm64
     //                   | "symbol" ["colocated"] name + imm64
     //                   | "dyn_scale_target_const" "." type
     //
-    fn parse_global_value_decl(&mut self) -> ParseResult<(GlobalValue, GlobalValueData)> {
+    fn parse_global_value_decl(
+        &mut self,
+    ) -> ParseResult<(GlobalValue, GlobalValueData, Option<Fact>)> {
         let gv = self.match_gv("expected global value number: gv«n»")?;
 
+        let fact = if self.token() == Some(Token::Bang) {
+            self.consume();
+            Some(self.parse_fact()?)
+        } else {
+            None
+        };
+
         self.match_token(Token::Equal, "expected '=' in global value declaration")?;
 
         let data = match self.match_any_identifier("expected global value kind")? {
@@ -1605,7 +1623,7 @@ impl<'a> Parser<'a> {
                     base,
                     offset,
                     global_type,
-                    readonly: flags.readonly(),
+                    flags,
                 }
             }
             "iadd_imm" => {
@@ -1654,7 +1672,7 @@ impl<'a> Parser<'a> {
         self.token();
         self.claim_gathered_comments(gv);
 
-        Ok((gv, data))
+        Ok((gv, data, fact))
     }
 
     // Parse one field definition in a memory-type struct decl.
diff --git a/cranelift/wasm/src/code_translator.rs b/cranelift/wasm/src/code_translator.rs
index 6a0090c10..ef6946150 100644
--- a/cranelift/wasm/src/code_translator.rs
+++ b/cranelift/wasm/src/code_translator.rs
@@ -2811,6 +2811,11 @@ where
     let mut flags = MemFlags::new();
     flags.set_endianness(ir::Endianness::Little);
 
+    if heap.memory_type.is_some() {
+        // Proof-carrying code is enabled; check this memory access.
+        flags.set_checked();
+    }
+
     // The access occurs to the `heap` disjoint category of abstract
     // state. This may allow alias analysis to merge redundant loads,
     // etc. when heap accesses occur interleaved with other (table,
diff --git a/cranelift/wasm/src/code_translator/bounds_checks.rs b/cranelift/wasm/src/code_translator/bounds_checks.rs
index 5b4d48e03..531a1bcd7 100644
--- a/cranelift/wasm/src/code_translator/bounds_checks.rs
+++ b/cranelift/wasm/src/code_translator/bounds_checks.rs
@@ -23,6 +23,7 @@ use super::Reachability;
 use crate::{FuncEnvironment, HeapData, HeapStyle};
 use cranelift_codegen::{
     cursor::{Cursor, FuncCursor},
+    ir::pcc::Fact,
     ir::{self, condcodes::IntCC, InstBuilder, RelSourceLoc},
 };
 use cranelift_frontend::FunctionBuilder;
@@ -56,6 +57,7 @@ where
     );
     let offset_and_size = offset_plus_size(offset, access_size);
     let spectre_mitigations_enabled = env.heap_access_spectre_mitigation();
+    let pcc = env.proof_carrying_code();
 
     // We need to emit code that will trap (or compute an address that will trap
     // when accessed) if
@@ -95,6 +97,7 @@ where
                 index,
                 offset,
                 spectre_mitigations_enabled,
+                pcc,
                 oob,
             ))
         }
@@ -134,6 +137,7 @@ where
                 index,
                 offset,
                 spectre_mitigations_enabled,
+                pcc,
                 oob,
             ))
         }
@@ -158,6 +162,7 @@ where
                 index,
                 offset,
                 spectre_mitigations_enabled,
+                pcc,
                 oob,
             ))
         }
@@ -187,6 +192,7 @@ where
                 index,
                 offset,
                 spectre_mitigations_enabled,
+                pcc,
                 oob,
             ))
         }
@@ -254,6 +260,7 @@ where
                 env.pointer_type(),
                 index,
                 offset,
+                pcc,
             ))
         }
 
@@ -283,6 +290,7 @@ where
                 index,
                 offset,
                 spectre_mitigations_enabled,
+                pcc,
                 oob,
             ))
         }
@@ -332,6 +340,8 @@ fn explicit_check_oob_condition_and_compute_addr(
     offset: u32,
     // Whether Spectre mitigations are enabled for heap accesses.
     spectre_mitigations_enabled: bool,
+    // Whether we're emitting PCC facts.
+    pcc: bool,
     // The `i8` boolean value that is non-zero when the heap access is out of
     // bounds (and therefore we should trap) and is zero when the heap access is
     // in bounds (and therefore we can proceed).
@@ -342,7 +352,7 @@ fn explicit_check_oob_condition_and_compute_addr(
             .trapnz(oob_condition, ir::TrapCode::HeapOutOfBounds);
     }
 
-    let mut addr = compute_addr(pos, heap, addr_ty, index, offset);
+    let mut addr = compute_addr(pos, heap, addr_ty, index, offset, pcc);
 
     if spectre_mitigations_enabled {
         let null = pos.ins().iconst(addr_ty, 0);
@@ -364,11 +374,42 @@ fn compute_addr(
     addr_ty: ir::Type,
     index: ir::Value,
     offset: u32,
+    pcc: bool,
 ) -> ir::Value {
     debug_assert_eq!(pos.func.dfg.value_type(index), addr_ty);
 
     let heap_base = pos.ins().global_value(addr_ty, heap.base);
+
+    let pcc_memtype = if pcc {
+        Some(
+            heap.memory_type
+                .expect("A memory type is required when PCC is enabled"),
+        )
+    } else {
+        None
+    };
+
+    if let Some(ty) = pcc_memtype {
+        pos.func.dfg.facts[heap_base] = Some(Fact::Mem {
+            ty,
+            min_offset: 0,
+            max_offset: 0,
+        });
+    }
+
     let base_and_index = pos.ins().iadd(heap_base, index);
+
+    if let Some(ty) = pcc_memtype {
+        // TODO: handle memory64 as well. For now we assert that we
+        // have a 32-bit `heap.index_type`.
+        assert_eq!(heap.index_type, ir::types::I32);
+        pos.func.dfg.facts[base_and_index] = Some(Fact::Mem {
+            ty,
+            min_offset: 0,
+            max_offset: u64::from(u32::MAX),
+        });
+    }
+
     if offset == 0 {
         base_and_index
     } else {
@@ -376,7 +417,19 @@ fn compute_addr(
         // `select_spectre_guard`, if any. If it happens after, then we
         // potentially are letting speculative execution read the whole first
         // 4GiB of memory.
-        pos.ins().iadd_imm(base_and_index, offset as i64)
+        let result = pos.ins().iadd_imm(base_and_index, offset as i64);
+        if let Some(ty) = pcc_memtype {
+            pos.func.dfg.facts[result] = Some(Fact::Mem {
+                ty,
+                min_offset: u64::from(offset),
+                // Safety: can't overflow -- two u32s summed in a
+                // 64-bit add. TODO: when memory64 is supported here,
+                // `u32::MAX` is no longer true, and we'll need to
+                // handle overflow here.
+                max_offset: u64::from(u32::MAX) + u64::from(offset),
+            });
+        }
+        result
     }
 }
 
diff --git a/cranelift/wasm/src/environ/dummy.rs b/cranelift/wasm/src/environ/dummy.rs
index 95f9fecec..aacaeb18a 100644
--- a/cranelift/wasm/src/environ/dummy.rs
+++ b/cranelift/wasm/src/environ/dummy.rs
@@ -261,6 +261,10 @@ impl<'dummy_environment> TargetEnvironment for DummyFuncEnvironment<'dummy_envir
     fn heap_access_spectre_mitigation(&self) -> bool {
         false
     }
+
+    fn proof_carrying_code(&self) -> bool {
+        false
+    }
 }
 
 impl<'dummy_environment> FuncEnvironment for DummyFuncEnvironment<'dummy_environment> {
@@ -297,7 +301,7 @@ impl<'dummy_environment> FuncEnvironment for DummyFuncEnvironment<'dummy_environ
             base: addr,
             offset: Offset32::new(0),
             global_type: self.pointer_type(),
-            readonly: true,
+            flags: ir::MemFlags::trusted().with_readonly(),
         });
 
         Ok(self.heaps.push(HeapData {
@@ -308,6 +312,7 @@ impl<'dummy_environment> FuncEnvironment for DummyFuncEnvironment<'dummy_environ
                 bound: 0x1_0000_0000,
             },
             index_type: I32,
+            memory_type: None,
         }))
     }
 
@@ -318,13 +323,14 @@ impl<'dummy_environment> FuncEnvironment for DummyFuncEnvironment<'dummy_environ
             base: vmctx,
             offset: Offset32::new(0),
             global_type: self.pointer_type(),
-            readonly: true, // when tables in wasm become "growable", revisit whether this can be readonly or not.
+            // When tables in wasm become "growable", revisit whether this can be readonly or not.
+            flags: ir::MemFlags::trusted().with_readonly(),
         });
         let bound_gv = func.create_global_value(ir::GlobalValueData::Load {
             base: vmctx,
             offset: Offset32::new(0),
             global_type: I32,
-            readonly: true,
+            flags: ir::MemFlags::trusted().with_readonly(),
         });
 
         Ok(func.create_table(ir::TableData {
@@ -710,6 +716,10 @@ impl TargetEnvironment for DummyEnvironment {
     fn heap_access_spectre_mitigation(&self) -> bool {
         false
     }
+
+    fn proof_carrying_code(&self) -> bool {
+        false
+    }
 }
 
 impl<'data> ModuleEnvironment<'data> for DummyEnvironment {
diff --git a/cranelift/wasm/src/environ/spec.rs b/cranelift/wasm/src/environ/spec.rs
index 5d7c82ff3..967839ce1 100644
--- a/cranelift/wasm/src/environ/spec.rs
+++ b/cranelift/wasm/src/environ/spec.rs
@@ -51,6 +51,9 @@ pub trait TargetEnvironment: TypeConvert {
     /// Whether to enable Spectre mitigations for heap accesses.
     fn heap_access_spectre_mitigation(&self) -> bool;
 
+    /// Whether to add proof-carrying-code facts to verify memory accesses.
+    fn proof_carrying_code(&self) -> bool;
+
     /// Get the Cranelift integer type to use for native pointers.
     ///
     /// This returns `I64` for 64-bit architectures and `I32` for 32-bit architectures.
diff --git a/cranelift/wasm/src/heap.rs b/cranelift/wasm/src/heap.rs
index b253c62dc..bab1f7e9a 100644
--- a/cranelift/wasm/src/heap.rs
+++ b/cranelift/wasm/src/heap.rs
@@ -1,6 +1,6 @@
 //! Heaps to implement WebAssembly linear memories.
 
-use cranelift_codegen::ir::{GlobalValue, Type};
+use cranelift_codegen::ir::{GlobalValue, MemoryType, Type};
 use cranelift_entity::entity_impl;
 
 /// An opaque reference to a [`HeapData`][crate::HeapData].
@@ -82,6 +82,9 @@ pub struct HeapData {
 
     /// The index type for the heap.
     pub index_type: Type,
+
+    /// The memory type for the pointed-to memory, if using proof-carrying code.
+    pub memory_type: Option<MemoryType>,
 }
 
 /// Style of heap including style-specific information.
diff --git a/crates/cli-flags/src/lib.rs b/crates/cli-flags/src/lib.rs
index 13efde1dc..63ef2491d 100644
--- a/crates/cli-flags/src/lib.rs
+++ b/crates/cli-flags/src/lib.rs
@@ -88,6 +88,8 @@ wasmtime_option_group! {
         pub cache_config: Option<String>,
         /// Whether or not to enable parallel compilation of modules.
         pub parallel_compilation: Option<bool>,
+        /// Whether to enable proof-carrying code (PCC)-based validation.
+        pub enable_pcc: Option<bool>,
 
         #[prefixed = "cranelift"]
         /// Set a cranelift-specific option. Use `wasmtime settings` to see
@@ -369,6 +371,9 @@ impl CommonOptions {
         if let Some(enable) = self.wasm.nan_canonicalization {
             config.cranelift_nan_canonicalization(enable);
         }
+        if let Some(enable) = self.codegen.enable_pcc {
+            config.cranelift_pcc(enable);
+        }
 
         self.enable_wasm_features(&mut config)?;
 
diff --git a/crates/cranelift/src/compiler.rs b/crates/cranelift/src/compiler.rs
index 9bc954a4c..b9457f8ad 100644
--- a/crates/cranelift/src/compiler.rs
+++ b/crates/cranelift/src/compiler.rs
@@ -197,7 +197,7 @@ impl wasmtime_environ::Compiler for Compiler {
                 .unwrap()
                 .into(),
             global_type: isa.pointer_type(),
-            readonly: true,
+            flags: MemFlags::trusted().with_readonly(),
         });
         let stack_limit = context.func.create_global_value(ir::GlobalValueData::Load {
             base: interrupts_ptr,
@@ -205,7 +205,7 @@ impl wasmtime_environ::Compiler for Compiler {
                 .unwrap()
                 .into(),
             global_type: isa.pointer_type(),
-            readonly: false,
+            flags: MemFlags::trusted(),
         });
         context.func.stack_limit = Some(stack_limit);
         let FunctionBodyData { validator, body } = input;
diff --git a/crates/cranelift/src/func_environ.rs b/crates/cranelift/src/func_environ.rs
index 39df50fb0..189de51c2 100644
--- a/crates/cranelift/src/func_environ.rs
+++ b/crates/cranelift/src/func_environ.rs
@@ -3,11 +3,13 @@ use cranelift_codegen::cursor::FuncCursor;
 use cranelift_codegen::ir;
 use cranelift_codegen::ir::condcodes::*;
 use cranelift_codegen::ir::immediates::{Imm64, Offset32, Uimm64};
+use cranelift_codegen::ir::pcc::Fact;
 use cranelift_codegen::ir::types::*;
 use cranelift_codegen::ir::{
-    AbiParam, ArgumentPurpose, Function, InstBuilder, Signature, UserFuncName, Value,
+    AbiParam, ArgumentPurpose, Function, InstBuilder, MemFlags, Signature, UserFuncName, Value,
 };
 use cranelift_codegen::isa::{self, CallConv, TargetFrontendConfig, TargetIsa};
+use cranelift_entity::SecondaryMap;
 use cranelift_entity::{EntityRef, PrimaryMap};
 use cranelift_frontend::FunctionBuilder;
 use cranelift_frontend::Variable;
@@ -121,6 +123,14 @@ pub struct FuncEnvironment<'module_environment> {
     /// The Cranelift global holding the vmctx address.
     vmctx: Option<ir::GlobalValue>,
 
+    /// The PCC memory type describing the vmctx layout, if we're
+    /// using PCC.
+    pcc_vmctx_memtype: Option<ir::MemoryType>,
+
+    /// The PCC memory type describing the data for each memory, if
+    /// we're using PCC.
+    pcc_memory_memtypes: SecondaryMap<MemoryIndex, Option<ir::MemoryType>>,
+
     /// Caches of signatures for builtin functions.
     builtin_function_signatures: BuiltinFunctionSignatures,
 
@@ -188,6 +198,8 @@ impl<'module_environment> FuncEnvironment<'module_environment> {
             types,
             heaps: PrimaryMap::default(),
             vmctx: None,
+            pcc_vmctx_memtype: None,
+            pcc_memory_memtypes: SecondaryMap::new(),
             builtin_function_signatures,
             offsets: VMOffsets::new(isa.pointer_bytes(), &translation.module),
             tunables,
@@ -212,6 +224,68 @@ impl<'module_environment> FuncEnvironment<'module_environment> {
     fn vmctx(&mut self, func: &mut Function) -> ir::GlobalValue {
         self.vmctx.unwrap_or_else(|| {
             let vmctx = func.create_global_value(ir::GlobalValueData::VMContext);
+            if self.isa.flags().enable_pcc() {
+                let mut fields = vec![];
+                for (memory_idx, plan) in &self.module.memory_plans {
+                    // For now, we only do PCC on defined, owned (non-shared), static, 32-bit memories (whew!).
+                    if plan.memory.shared || plan.memory.memory64 {
+                        continue;
+                    }
+                    let static_bound_wasm_pages = match &plan.style {
+                        MemoryStyle::Dynamic { .. } => continue,
+                        MemoryStyle::Static { bound } => *bound,
+                    };
+                    let static_bound = static_bound_wasm_pages.checked_mul(0x1_0000).unwrap();
+                    let def_memory_idx = match self.module.defined_memory_index(memory_idx) {
+                        Some(i) => i,
+                        None => continue,
+                    };
+                    let owned_memory_idx = self.module.owned_memory_index(def_memory_idx);
+
+                    let base_field_offset = self
+                        .offsets
+                        .vmctx_vmmemory_definition_base(owned_memory_idx);
+                    // Create a new "blob" memory type to represent the pointed-to memory.
+                    let data_mt = func.create_memory_type(ir::MemoryTypeData::Memory {
+                        size: static_bound
+                            .checked_add(plan.offset_guard_size)
+                            .expect("Memory plan has overflowing size plus guard"),
+                    });
+
+                    self.pcc_memory_memtypes[memory_idx] = Some(data_mt);
+
+                    fields.push(ir::MemoryTypeField {
+                        offset: u64::from(base_field_offset),
+                        ty: self.isa.pointer_type(),
+                        // Read-only field from the PoV of PCC checks:
+                        // don't allow stores to this field. (Even if
+                        // it is a dynamic memory whose base can
+                        // change, that update happens inside the
+                        // runtime, not in generated code.)
+                        readonly: true,
+                        fact: Some(Fact::Mem {
+                            ty: data_mt,
+                            min_offset: 0,
+                            max_offset: 0,
+                        }),
+                    });
+                }
+                let size = fields
+                    .iter()
+                    .map(|field| field.offset + u64::from(self.isa.pointer_type().bytes()))
+                    .max()
+                    .unwrap_or(0);
+
+                let vmctx_memtype =
+                    func.create_memory_type(ir::MemoryTypeData::Struct { size, fields });
+
+                self.pcc_vmctx_memtype = Some(vmctx_memtype);
+                func.global_value_facts[vmctx] = Some(Fact::Mem {
+                    ty: vmctx_memtype,
+                    min_offset: 0,
+                    max_offset: 0,
+                });
+            }
             self.vmctx = Some(vmctx);
             vmctx
         })
@@ -352,7 +426,7 @@ impl<'module_environment> FuncEnvironment<'module_environment> {
                 base: vmctx,
                 offset: Offset32::new(i32::try_from(from_offset).unwrap()),
                 global_type: pointer_type,
-                readonly: true,
+                flags: MemFlags::trusted().with_readonly(),
             });
             (global, 0)
         }
@@ -1197,6 +1271,10 @@ impl<'module_environment> TargetEnvironment for FuncEnvironment<'module_environm
     fn heap_access_spectre_mitigation(&self) -> bool {
         self.isa.flags().enable_heap_access_spectre_mitigation()
     }
+
+    fn proof_carrying_code(&self) -> bool {
+        self.isa.flags().enable_pcc()
+    }
 }
 
 impl<'module_environment> cranelift_wasm::FuncEnvironment for FuncEnvironment<'module_environment> {
@@ -1237,7 +1315,7 @@ impl<'module_environment> cranelift_wasm::FuncEnvironment for FuncEnvironment<'m
                     base: vmctx,
                     offset: Offset32::new(i32::try_from(from_offset).unwrap()),
                     global_type: pointer_type,
-                    readonly: true,
+                    flags: MemFlags::trusted().with_readonly(),
                 });
                 let base_offset = i32::from(self.offsets.vmtable_definition_base());
                 let current_elements_offset =
@@ -1250,7 +1328,7 @@ impl<'module_environment> cranelift_wasm::FuncEnvironment for FuncEnvironment<'m
             base: ptr,
             offset: Offset32::new(base_offset),
             global_type: pointer_type,
-            readonly: false,
+            flags: MemFlags::trusted(),
         });
         let bound_gv = func.create_global_value(ir::GlobalValueData::Load {
             base: ptr,
@@ -1259,7 +1337,7 @@ impl<'module_environment> cranelift_wasm::FuncEnvironment for FuncEnvironment<'m
                 u16::from(self.offsets.size_of_vmtable_definition_current_elements()) * 8,
             )
             .unwrap(),
-            readonly: false,
+            flags: MemFlags::trusted(),
         });
 
         let element_size = u64::from(
@@ -1774,7 +1852,7 @@ impl<'module_environment> cranelift_wasm::FuncEnvironment for FuncEnvironment<'m
                         base: vmctx,
                         offset: Offset32::new(i32::try_from(from_offset).unwrap()),
                         global_type: pointer_type,
-                        readonly: true,
+                        flags: MemFlags::trusted().with_readonly(),
                     });
                     let base_offset = i32::from(self.offsets.ptr.vmmemory_definition_base());
                     let current_length_offset =
@@ -1797,7 +1875,7 @@ impl<'module_environment> cranelift_wasm::FuncEnvironment for FuncEnvironment<'m
                     base: vmctx,
                     offset: Offset32::new(i32::try_from(from_offset).unwrap()),
                     global_type: pointer_type,
-                    readonly: true,
+                    flags: MemFlags::trusted().with_readonly(),
                 });
                 let base_offset = i32::from(self.offsets.ptr.vmmemory_definition_base());
                 let current_length_offset =
@@ -1819,7 +1897,7 @@ impl<'module_environment> cranelift_wasm::FuncEnvironment for FuncEnvironment<'m
                     base: ptr,
                     offset: Offset32::new(current_length_offset),
                     global_type: pointer_type,
-                    readonly: false,
+                    flags: MemFlags::trusted(),
                 });
                 (
                     offset_guard_size,
@@ -1843,18 +1921,32 @@ impl<'module_environment> cranelift_wasm::FuncEnvironment for FuncEnvironment<'m
             ),
         };
 
+        let mut flags = MemFlags::trusted().with_checked();
+        if readonly_base {
+            flags.set_readonly();
+        }
         let heap_base = func.create_global_value(ir::GlobalValueData::Load {
             base: ptr,
             offset: Offset32::new(base_offset),
             global_type: pointer_type,
-            readonly: readonly_base,
+            flags,
         });
+        let memory_type = self.pcc_memory_memtypes[index];
+        if let Some(ty) = memory_type {
+            func.global_value_facts[heap_base] = Some(Fact::Mem {
+                ty,
+                min_offset: 0,
+                max_offset: 0,
+            });
+        }
+
         Ok(self.heaps.push(HeapData {
             base: heap_base,
             min_size,
             offset_guard_size,
             style: heap_style,
             index_type: self.memory_index_type(index),
+            memory_type,
         }))
     }
 
diff --git a/crates/wasmtime/src/config.rs b/crates/wasmtime/src/config.rs
index c3b88e5e6..b3797dd95 100644
--- a/crates/wasmtime/src/config.rs
+++ b/crates/wasmtime/src/config.rs
@@ -967,6 +967,29 @@ impl Config {
         self
     }
 
+    /// Controls whether proof-carrying code (PCC) is used to validate
+    /// lowering of Wasm sandbox checks.
+    ///
+    /// Proof-carrying code carries "facts" about program values from
+    /// the IR all the way to machine code, and checks those facts
+    /// against known machine-instruction semantics. This guards
+    /// against bugs in instruction lowering that might create holes
+    /// in the Wasm sandbox.
+    ///
+    /// PCC is designed to be fast: it does not require complex
+    /// solvers or logic engines to verify, but only a linear pass
+    /// over a trail of "breadcrumbs" or facts at each intermediate
+    /// value. Thus, it is appropriate to enable in production.
+    #[cfg(any(feature = "cranelift", feature = "winch"))]
+    #[cfg_attr(nightlydoc, doc(cfg(any(feature = "cranelift", feature = "winch"))))]
+    pub fn cranelift_pcc(&mut self, enable: bool) -> &mut Self {
+        let val = if enable { "true" } else { "false" };
+        self.compiler_config
+            .settings
+            .insert("enable_pcc".to_string(), val.to_string());
+        self
+    }
+
     /// Allows setting a Cranelift boolean flag or preset. This allows
     /// fine-tuning of Cranelift settings.
     ///


Test patch:
diff --git a/cranelift/filetests/filetests/pcc/succeed/gv_fact.clif b/cranelift/filetests/filetests/pcc/succeed/gv_fact.clif
new file mode 100644
index 000000000..bc2f39c93
--- /dev/null
+++ b/cranelift/filetests/filetests/pcc/succeed/gv_fact.clif
@@ -0,0 +1,57 @@
+test compile
+set enable_pcc=true
+target aarch64
+
+function %f0(i64 vmctx) -> i64 {
+    mt0 = struct 16 { 8: i64 ! mem(mt1, 0, 0) }
+    mt1 = memory 0x1_0000_0000
+    gv0 ! mem(mt0, 0, 0) = vmctx
+    gv1 ! mem(mt1, 0, 0) = load.i64 notrap aligned checked gv0+8
+    
+block0(v0 ! mem(mt0, 0, 0): i64):
+    v1 ! mem(mt1, 0, 0) = global_value.i64 gv1
+    return v1
+}
+
+function %f1(i64 vmctx) -> i64 {
+    mt0 = struct 16 { 8: i64 ! mem(mt1, 0, 0) }
+    mt1 = struct 8 { 0: i64 ! mem(mt2, 0, 0) }
+    mt2 = memory 0x1_0000_0000
+    gv0 ! mem(mt0, 0, 0) = vmctx
+    gv1 ! mem(mt1, 0, 0) = load.i64 notrap aligned checked gv0+8
+    gv2 ! mem(mt2, 0, 0) = load.i64 notrap aligned checked gv1+0
+    
+block0(v0 ! mem(mt0, 0, 0): i64):
+    v1 ! mem(mt2, 0, 0) = global_value.i64 gv2
+    return v1
+}
+
+function %f1(i64 vmctx) -> i64 {
+    mt0 = struct 16 { 8: i64 ! mem(mt1, 0, 0) }
+    mt1 = struct 8 { 0: i64 ! mem(mt2, 0, 0) }
+    mt2 = memory 0x1_0000_0000
+    gv0 ! mem(mt0, 0, 0) = vmctx
+    gv1 ! mem(mt1, 0, 0) = load.i64 notrap aligned checked gv0+8
+    gv2 ! mem(mt2, 0, 0) = load.i64 notrap aligned checked gv1+0
+    gv3 ! mem(mt2, 8, 8) = iadd_imm.i64 gv2, 8
+    
+block0(v0 ! mem(mt0, 0, 0): i64):
+    v1 ! mem(mt2, 8, 8) = global_value.i64 gv3
+    return v1
+}
+
+function %f2(i64 vmctx) -> i64 {
+    mt0 = struct 16 { 8: i64 ! mem(mt1, 0, 0) }
+    mt1 = struct 8 { 0: i64 ! mem(mt2, 0, 0) }
+    mt2 = memory 0x1_0000_0000
+    gv0 ! mem(mt0, 0, 0) = vmctx
+    gv1 ! mem(mt1, 0, 0) = load.i64 notrap aligned checked gv0+8
+    gv2 ! mem(mt2, 0, 0) = load.i64 notrap aligned checked gv1+0
+    gv3 ! mem(mt2, 8, 8) = iadd_imm.i64 gv2, 8
+
+    ;; like the above, but with no fact provided on `v0`; it should
+    ;; get copied from the GV.
+block0(v0: i64):
+    v1 ! mem(mt2, 8, 8) = global_value.i64 gv3
+    return v1
+}
diff --git a/cranelift/filetests/filetests/pcc/succeed/load.clif b/cranelift/filetests/filetests/pcc/succeed/load.clif
index 276eab361..90b8e030d 100644
--- a/cranelift/filetests/filetests/pcc/succeed/load.clif
+++ b/cranelift/filetests/filetests/pcc/succeed/load.clif
@@ -62,3 +62,23 @@ block0(v0 ! mem(mt0, 0, 0): i64, v1 ! range(64, 0, 0xfff): i64):
     v5 = load.i64 checked v4
     return v5
 }
+
+;; UnsignedOffset mode on aarch64.
+function %f6(i64) -> i64 {
+    mt0 = memory 0x8000
+block0(v0 ! mem(mt0, 0, 0): i64):
+    v2 = iconst.i64 8
+    v3 ! mem(mt0, 8, 8) = iadd.i64 v0, v2
+    v4 = load.i64 checked v3
+    return v4
+}
+
+;; Unscaled mode on aarch64.
+function %f6(i64) -> i64 {
+    mt0 = memory 0x8000
+block0(v0 ! mem(mt0, 8, 8): i64):
+    v2 = iconst.i64 8
+    v3 ! mem(mt0, 0, 0) = isub.i64 v0, v2
+    v4 = load.i64 checked v3
+    return v4
+}
diff --git a/cranelift/filetests/filetests/wasm/duplicate-loads-dynamic-memory.wat b/cranelift/filetests/filetests/wasm/duplicate-loads-dynamic-memory.wat
index 7d00c81bf..915a8187a 100644
--- a/cranelift/filetests/filetests/wasm/duplicate-loads-dynamic-memory.wat
+++ b/cranelift/filetests/filetests/wasm/duplicate-loads-dynamic-memory.wat
@@ -48,6 +48,10 @@
 ;;     gv2 = load.i64 notrap aligned gv0
 ;;
 ;;                                 block0(v0: i32, v1: i64):
+;;                                     v20 -> v1
+;;                                     v21 -> v1
+;;                                     v22 -> v1
+;;                                     v23 -> v1
 ;; @0057                               v5 = load.i64 notrap aligned v1+8
 ;; @0057                               v7 = load.i64 notrap aligned v1
 ;; @0057                               v4 = uextend.i64 v0
@@ -69,14 +73,18 @@
 ;;     gv2 = load.i64 notrap aligned gv0
 ;;
 ;;                                 block0(v0: i32, v1: i64):
+;;                                     v22 -> v1
+;;                                     v23 -> v1
+;;                                     v25 -> v1
+;;                                     v26 -> v1
 ;; @0064                               v5 = load.i64 notrap aligned v1+8
 ;; @0064                               v7 = load.i64 notrap aligned v1
 ;; @0064                               v4 = uextend.i64 v0
 ;; @0064                               v6 = icmp ugt v4, v5
 ;; @0064                               v10 = iconst.i64 0
 ;; @0064                               v8 = iadd v7, v4
-;;                                     v22 = iconst.i64 1234
-;; @0064                               v9 = iadd v8, v22  ; v22 = 1234
+;;                                     v24 = iconst.i64 1234
+;; @0064                               v9 = iadd v8, v24  ; v24 = 1234
 ;; @0064                               v11 = select_spectre_guard v6, v10, v9  ; v10 = 0
 ;; @0064                               v12 = load.i32 little heap v11
 ;;                                     v2 -> v12
diff --git a/cranelift/filetests/filetests/wasm/duplicate-loads-static-memory.wat b/cranelift/filetests/filetests/wasm/duplicate-loads-static-memory.wat
index 16a4fe413..ec8b71033 100644
--- a/cranelift/filetests/filetests/wasm/duplicate-loads-static-memory.wat
+++ b/cranelift/filetests/filetests/wasm/duplicate-loads-static-memory.wat
@@ -43,6 +43,8 @@
 ;;     gv1 = load.i64 notrap aligned readonly gv0
 ;;
 ;;                                 block0(v0: i32, v1: i64):
+;;                                     v12 -> v1
+;;                                     v13 -> v1
 ;; @0057                               v5 = load.i64 notrap aligned readonly v1
 ;; @0057                               v4 = uextend.i64 v0
 ;; @0057                               v6 = iadd v5, v4
@@ -59,11 +61,13 @@
 ;;     gv1 = load.i64 notrap aligned readonly gv0
 ;;
 ;;                                 block0(v0: i32, v1: i64):
+;;                                     v14 -> v1
+;;                                     v16 -> v1
 ;; @0064                               v5 = load.i64 notrap aligned readonly v1
 ;; @0064                               v4 = uextend.i64 v0
 ;; @0064                               v6 = iadd v5, v4
-;;                                     v14 = iconst.i64 1234
-;; @0064                               v7 = iadd v6, v14  ; v14 = 1234
+;;                                     v15 = iconst.i64 1234
+;; @0064                               v7 = iadd v6, v15  ; v15 = 1234
 ;; @0064                               v8 = load.i32 little heap v7
 ;;                                     v2 -> v8
 ;; @006e                               jump block1
diff --git a/cranelift/filetests/filetests/wasm/dynamic-memory-no-spectre-access-same-index-different-offsets.wat b/cranelift/filetests/filetests/wasm/dynamic-memory-no-spectre-access-same-index-different-offsets.wat
index d3f19dfe5..3d47fe4dd 100644
--- a/cranelift/filetests/filetests/wasm/dynamic-memory-no-spectre-access-same-index-different-offsets.wat
+++ b/cranelift/filetests/filetests/wasm/dynamic-memory-no-spectre-access-same-index-different-offsets.wat
@@ -61,6 +61,12 @@
 ;;     gv2 = load.i64 notrap aligned gv0
 ;;
 ;;                                 block0(v0: i32, v1: i64):
+;;                                     v27 -> v1
+;;                                     v28 -> v1
+;;                                     v29 -> v1
+;;                                     v30 -> v1
+;;                                     v32 -> v1
+;;                                     v33 -> v1
 ;; @0047                               v6 = load.i64 notrap aligned v1+8
 ;; @0047                               v5 = uextend.i64 v0
 ;; @0047                               v7 = icmp ugt v5, v6
@@ -80,8 +86,8 @@
 ;; @004c                               trap heap_oob
 ;;
 ;;                                 block5:
-;;                                     v27 = iconst.i64 4
-;; @004c                               v16 = iadd.i64 v9, v27  ; v27 = 4
+;;                                     v31 = iconst.i64 4
+;; @004c                               v16 = iadd.i64 v9, v31  ; v31 = 4
 ;; @004c                               v17 = load.i32 little heap v16
 ;;                                     v3 -> v17
 ;; @0051                               v19 = iconst.i64 0x0010_0003
@@ -95,8 +101,8 @@
 ;;                                 block7:
 ;; @0051                               v23 = load.i64 notrap aligned v1
 ;; @0051                               v24 = iadd v23, v5
-;;                                     v28 = iconst.i64 0x000f_ffff
-;; @0051                               v25 = iadd v24, v28  ; v28 = 0x000f_ffff
+;;                                     v34 = iconst.i64 0x000f_ffff
+;; @0051                               v25 = iadd v24, v34  ; v34 = 0x000f_ffff
 ;; @0051                               v26 = load.i32 little heap v25
 ;;                                     v4 -> v26
 ;; @0056                               jump block1
@@ -111,6 +117,12 @@
 ;;     gv2 = load.i64 notrap aligned gv0
 ;;
 ;;                                 block0(v0: i32, v1: i32, v2: i32, v3: i32, v4: i64):
+;;                                     v24 -> v4
+;;                                     v25 -> v4
+;;                                     v26 -> v4
+;;                                     v27 -> v4
+;;                                     v29 -> v4
+;;                                     v30 -> v4
 ;; @005d                               v6 = load.i64 notrap aligned v4+8
 ;; @005d                               v5 = uextend.i64 v0
 ;; @005d                               v7 = icmp ugt v5, v6
@@ -129,8 +141,8 @@
 ;; @0064                               trap heap_oob
 ;;
 ;;                                 block5:
-;;                                     v24 = iconst.i64 4
-;; @0064                               v15 = iadd.i64 v9, v24  ; v24 = 4
+;;                                     v28 = iconst.i64 4
+;; @0064                               v15 = iadd.i64 v9, v28  ; v28 = 4
 ;; @0064                               store.i32 little heap v2, v15
 ;; @006b                               v17 = iconst.i64 0x0010_0003
 ;; @006b                               v18 = uadd_overflow_trap.i64 v5, v17, heap_oob  ; v17 = 0x0010_0003
@@ -143,8 +155,8 @@
 ;;                                 block7:
 ;; @006b                               v21 = load.i64 notrap aligned v4
 ;; @006b                               v22 = iadd v21, v5
-;;                                     v25 = iconst.i64 0x000f_ffff
-;; @006b                               v23 = iadd v22, v25  ; v25 = 0x000f_ffff
+;;                                     v31 = iconst.i64 0x000f_ffff
+;; @006b                               v23 = iadd v22, v31  ; v31 = 0x000f_ffff
 ;; @006b                               store.i32 little heap v3, v23
 ;; @0070                               jump block1
 ;;
diff --git a/cranelift/filetests/filetests/wasm/dynamic-memory-yes-spectre-access-same-index-different-offsets.wat b/cranelift/filetests/filetests/wasm/dynamic-memory-yes-spectre-access-same-index-different-offsets.wat
index c31b82338..a509d268f 100644
--- a/cranelift/filetests/filetests/wasm/dynamic-memory-yes-spectre-access-same-index-different-offsets.wat
+++ b/cranelift/filetests/filetests/wasm/dynamic-memory-yes-spectre-access-same-index-different-offsets.wat
@@ -61,6 +61,12 @@
 ;;     gv2 = load.i64 notrap aligned gv0
 ;;
 ;;                                 block0(v0: i32, v1: i64):
+;;                                     v33 -> v1
+;;                                     v34 -> v1
+;;                                     v35 -> v1
+;;                                     v36 -> v1
+;;                                     v38 -> v1
+;;                                     v39 -> v1
 ;; @0047                               v6 = load.i64 notrap aligned v1+8
 ;; @0047                               v8 = load.i64 notrap aligned v1
 ;; @0047                               v5 = uextend.i64 v0
@@ -70,16 +76,16 @@
 ;; @0047                               v11 = select_spectre_guard v7, v10, v9  ; v10 = 0
 ;; @0047                               v12 = load.i32 little heap v11
 ;;                                     v2 -> v12
-;;                                     v33 = iconst.i64 4
-;; @004c                               v18 = iadd v9, v33  ; v33 = 4
+;;                                     v37 = iconst.i64 4
+;; @004c                               v18 = iadd v9, v37  ; v37 = 4
 ;; @004c                               v20 = select_spectre_guard v7, v10, v18  ; v10 = 0
 ;; @004c                               v21 = load.i32 little heap v20
 ;;                                     v3 -> v21
 ;; @0051                               v23 = iconst.i64 0x0010_0003
 ;; @0051                               v24 = uadd_overflow_trap v5, v23, heap_oob  ; v23 = 0x0010_0003
 ;; @0051                               v26 = icmp ugt v24, v6
-;;                                     v34 = iconst.i64 0x000f_ffff
-;; @0051                               v29 = iadd v9, v34  ; v34 = 0x000f_ffff
+;;                                     v40 = iconst.i64 0x000f_ffff
+;; @0051                               v29 = iadd v9, v40  ; v40 = 0x000f_ffff
 ;; @0051                               v31 = select_spectre_guard v26, v10, v29  ; v10 = 0
 ;; @0051                               v32 = load.i32 little heap v31
 ;;                                     v4 -> v32
@@ -95,6 +101,12 @@
 ;;     gv2 = load.i64 notrap aligned gv0
 ;;
 ;;                                 block0(v0: i32, v1: i32, v2: i32, v3: i32, v4: i64):
+;;                                     v30 -> v4
+;;                                     v31 -> v4
+;;                                     v32 -> v4
+;;                                     v33 -> v4
+;;                                     v35 -> v4
+;;                                     v36 -> v4
 ;; @005d                               v6 = load.i64 notrap aligned v4+8
 ;; @005d                               v8 = load.i64 notrap aligned v4
 ;; @005d                               v5 = uextend.i64 v0
@@ -103,15 +115,15 @@
 ;; @005d                               v9 = iadd v8, v5
 ;; @005d                               v11 = select_spectre_guard v7, v10, v9  ; v10 = 0
 ;; @005d                               store little heap v1, v11
-;;                                     v30 = iconst.i64 4
-;; @0064                               v17 = iadd v9, v30  ; v30 = 4
+;;                                     v34 = iconst.i64 4
+;; @0064                               v17 = iadd v9, v34  ; v34 = 4
 ;; @0064                               v19 = select_spectre_guard v7, v10, v17  ; v10 = 0
 ;; @0064                               store little heap v2, v19
 ;; @006b                               v21 = iconst.i64 0x0010_0003
 ;; @006b                               v22 = uadd_overflow_trap v5, v21, heap_oob  ; v21 = 0x0010_0003
 ;; @006b                               v24 = icmp ugt v22, v6
-;;                                     v31 = iconst.i64 0x000f_ffff
-;; @006b                               v27 = iadd v9, v31  ; v31 = 0x000f_ffff
+;;                                     v37 = iconst.i64 0x000f_ffff
+;; @006b                               v27 = iadd v9, v37  ; v37 = 0x000f_ffff
 ;; @006b                               v29 = select_spectre_guard v24, v10, v27  ; v10 = 0
 ;; @006b                               store little heap v3, v29
 ;; @0070                               jump block1
diff --git a/cranelift/filetests/src/test_wasm/config.rs b/cranelift/filetests/src/test_wasm/config.rs
index ab85af333..eb9b6f60e 100644
--- a/cranelift/filetests/src/test_wasm/config.rs
+++ b/cranelift/filetests/src/test_wasm/config.rs
@@ -113,6 +113,10 @@ impl TestGlobal {
         if self.vmctx {
             ir::GlobalValueData::VMContext
         } else if let Some(load) = &self.load {
+            let mut flags = ir::MemFlags::trusted();
+            if load.readonly {
+                flags.set_readonly();
+            }
             ir::GlobalValueData::Load {
                 base: name_to_ir_global[&load.base],
                 offset: i32::try_from(load.offset).unwrap().into(),
@@ -121,7 +125,7 @@ impl TestGlobal {
                     "i64" => ir::types::I64,
                     other => panic!("test globals cannot be of type '{other}'"),
                 },
-                readonly: load.readonly,
+                flags,
             }
         } else {
             unreachable!()
@@ -178,6 +182,7 @@ impl TestHeap {
                 "i64" => ir::types::I64,
                 other => panic!("heap indices may only be i32 or i64, found '{other}'"),
             },
+            memory_type: None,
         }
     }
 
diff --git a/cranelift/filetests/src/test_wasm/env.rs b/cranelift/filetests/src/test_wasm/env.rs
index 89c7ad211..efd21a5b8 100644
--- a/cranelift/filetests/src/test_wasm/env.rs
+++ b/cranelift/filetests/src/test_wasm/env.rs
@@ -20,6 +20,7 @@ pub struct ModuleEnv {
     pub inner: DummyEnvironment,
     pub config: TestConfig,
     pub heap_access_spectre_mitigation: bool,
+    pub proof_carrying_code: bool,
 }
 
 impl ModuleEnv {
@@ -31,6 +32,7 @@ impl ModuleEnv {
             heap_access_spectre_mitigation: target_isa
                 .flags()
                 .enable_heap_access_spectre_mitigation(),
+            proof_carrying_code: target_isa.flags().enable_pcc(),
         }
     }
 }
@@ -51,6 +53,7 @@ impl<'data> ModuleEnvironment<'data> for ModuleEnv {
                 self.inner.expected_reachability.clone(),
                 self.config.clone(),
                 self.heap_access_spectre_mitigation,
+                self.proof_carrying_code,
             );
             let func_index = FuncIndex::new(
                 self.inner.get_num_func_imports() + self.inner.info.function_bodies.len(),
@@ -244,6 +247,7 @@ pub struct FuncEnv<'a> {
     pub name_to_ir_global: BTreeMap<String, ir::GlobalValue>,
     pub next_heap: usize,
     pub heap_access_spectre_mitigation: bool,
+    pub proof_carrying_code: bool,
 }
 
 impl<'a> FuncEnv<'a> {
@@ -252,6 +256,7 @@ impl<'a> FuncEnv<'a> {
         expected_reachability: Option<cranelift_wasm::ExpectedReachability>,
         config: TestConfig,
         heap_access_spectre_mitigation: bool,
+        proof_carrying_code: bool,
     ) -> Self {
         let inner = cranelift_wasm::DummyFuncEnvironment::new(mod_info, expected_reachability);
         Self {
@@ -260,6 +265,7 @@ impl<'a> FuncEnv<'a> {
             name_to_ir_global: Default::default(),
             next_heap: 0,
             heap_access_spectre_mitigation,
+            proof_carrying_code,
         }
     }
 }
@@ -278,6 +284,10 @@ impl<'a> TargetEnvironment for FuncEnv<'a> {
     fn heap_access_spectre_mitigation(&self) -> bool {
         self.heap_access_spectre_mitigation
     }
+
+    fn proof_carrying_code(&self) -> bool {
+        self.proof_carrying_code
+    }
 }
 
 impl<'a> FuncEnvironment for FuncEnv<'a> {