diff --git a/changelog.d/wpfacts-array-rep-fields.md b/changelog.d/wpfacts-array-rep-fields.md
new file mode 100644
index 00000000000..22ca28320fa
--- /dev/null
+++ b/changelog.d/wpfacts-array-rep-fields.md
@@ -0,0 +1 @@
+Performance: an array held in a class field reads under its whole-program array representation. A field that, on every object of its class, holds only plain program Arrays for the object's whole life (`FieldFacts::rep`: definite, a data field, the class neither escaped nor reshaped by `delete` or `setPrototypeOf`) makes a read of it a value of representation `Arr`, the join over the receiver's classes, so `this.f[i]` takes the element read tier that locals and module constants already take: no pointer-band test, no type test, the capacity as the bound, the slot addressed right behind the header. A method that is exactly `return this.f[k] ?? L` and is called with a key the facts prove inside the dense floor of every Array the field can hold (`this.at(move & 127)` on a board born `new Array(128).fill(0)`) reads a present element: the call is the field load, the forwarding test when the storage can grow, and the slot load, with no bound, no hole test and, for Number elements, no `??`. A call whose key can leave the floor keeps the bound, the hole test and the `??`. `PERRY_FACTS_ARRAY_FIELDS=0` turns both off; `PERRY_VERIFY_FACTS=1` re-tests the field's claim where the field is read and the call's claim where the slot is loaded, and `PERRY_FACTS_SABOTAGE=arrfield` and `arrb1` are the negative controls. `PERRY_FACTS_DUMP` prints each such call with its key interval, the representation it reads from and the in-floor verdict.
diff --git a/crates/perry-codegen/src/codegen/program_facts_view.rs b/crates/perry-codegen/src/codegen/program_facts_view.rs
index 243230d9239..1220297b6ab 100644
--- a/crates/perry-codegen/src/codegen/program_facts_view.rs
+++ b/crates/perry-codegen/src/codegen/program_facts_view.rs
@@ -88,6 +88,11 @@ pub struct FactsField {
     /// or when interpreted code can run.
     pub classes: Vec<u32>,
     pub nullable: bool,
+    /// The field's representation (wpfacts `FieldFacts::rep`, DESIGN-p4l1
+    /// §3): `Arr` when the field, on every object of the class, holds only
+    /// plain program Arrays for the object's whole life. A read of the
+    /// field is a value of this representation (`FieldProof::array`).
+    pub rep: FactsRep,
 }
 
 /// A plain compiled body of this module that a binding or a field holds
@@ -222,6 +227,23 @@ pub enum FactsEnc {
     I32,
 }
 
+impl FactsArrRep {
+    /// The join (says less) of two array reps, wpfacts `ArrRep::join`.
+    pub fn join(a: FactsArrRep, b: FactsArrRep) -> FactsArrRep {
+        use FactsElemRep::{Boxed, F64, I32};
+        FactsArrRep {
+            elem: match (a.elem, b.elem) {
+                (Boxed, _) | (_, Boxed) => Boxed,
+                (F64, _) | (_, F64) => F64,
+                (I32, I32) => I32,
+            },
+            floor: a.floor.min(b.floor),
+            dense: a.dense && b.dense,
+            fixed: a.fixed && b.fixed,
+        }
+    }
+}
+
 impl FactsRep {
     /// The slot encoding: an `Arr` slot holds the Boxed word.
     pub fn encoding(self) -> FactsEnc {
@@ -463,6 +485,11 @@ pub struct FactsFieldReadCall {
     /// The method body's `IndexGet::element_offset` and `this.f` offset.
     pub element_offset: u32,
     pub field_offset: u32,
+    /// `Some(floor)`: this call's index is an integer in `[0, floor)`, and
+    /// every Array the method's read may read from has at least `floor`
+    /// elements with no hole below it (wpfacts `FieldReadCall::in_floor`,
+    /// DESIGN-p4l1 §2.8): the slot is a present own element.
+    pub in_floor: Option<u32>,
 }
 
 #[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
diff --git a/crates/perry-codegen/src/expr/family_guard_tests.rs b/crates/perry-codegen/src/expr/family_guard_tests.rs
index 4f9037d9c5f..f887c95603c 100644
--- a/crates/perry-codegen/src/expr/family_guard_tests.rs
+++ b/crates/perry-codegen/src/expr/family_guard_tests.rs
@@ -90,6 +90,7 @@ fn tm1_facts(m: &Module) -> crate::codegen::ProgramFactsView {
         fns: Vec::new(),
         classes: Vec::new(),
         nullable: false,
+        rep: crate::codegen::FactsRep::Boxed,
     };
     let mut elision = ElisionFacts::default();
     elision.locals.insert(
diff --git a/crates/perry-codegen/src/expr/index_get.rs b/crates/perry-codegen/src/expr/index_get.rs
index 245188eea98..f7c5ab56425 100644
--- a/crates/perry-codegen/src/expr/index_get.rs
+++ b/crates/perry-codegen/src/expr/index_get.rs
@@ -40,7 +40,7 @@ use super::{
     TypedFeedbackContract, TypedFeedbackKind,
 };
 
-mod array_rep;
+pub(crate) mod array_rep;
 mod foreign_counter;
 pub(crate) mod descriptor_read;
 pub(crate) mod elem_floor;
diff --git a/crates/perry-codegen/src/expr/index_get/array_rep.rs b/crates/perry-codegen/src/expr/index_get/array_rep.rs
index 2411e015cf6..0c61f872a47 100644
--- a/crates/perry-codegen/src/expr/index_get/array_rep.rs
+++ b/crates/perry-codegen/src/expr/index_get/array_rep.rs
@@ -79,12 +79,23 @@ pub(crate) fn witness(ctx: &mut FnCtx<'_>, expr: &Expr) -> Result<()> {
     } else {
         None
     };
-    emit(ctx, &recv, key.as_deref(), r, *id);
+    emit(ctx, &recv, key.as_deref(), r, &format!("local {id}"));
     Ok(())
 }
 
+/// Check mode at a field read the facts give `Arr(r)` (DESIGN-p4l1 §5.1,
+/// PR-C3): the claim on the word `value` the read loaded. `what` names the
+/// field for the report.
+pub(crate) fn witness_value(ctx: &mut FnCtx<'_>, value: &str, r: FactsArrRep, what: &str) {
+    crate::verify_facts::covered(
+        crate::verify_facts::Fact::ArrayRep,
+        || serde_json::json!({ "field": what, "floor": r.floor }),
+    );
+    emit(ctx, value, None, r, what);
+}
+
 /// The tests of `witness` on the lowered receiver `recv` and key `key`.
-fn emit(ctx: &mut FnCtx<'_>, recv: &str, key: Option<&str>, r: FactsArrRep, id: u32) {
+fn emit(ctx: &mut FnCtx<'_>, recv: &str, key: Option<&str>, r: FactsArrRep, what: &str) {
     let miss = ctx.new_block("arr_rep.verify_miss");
     let next = ctx.new_block("arr_rep.admitted");
     let (miss_l, next_l) = (ctx.block_label(miss), ctx.block_label(next));
@@ -121,7 +132,7 @@ fn emit(ctx: &mut FnCtx<'_>, recv: &str, key: Option<&str>, r: FactsArrRep, id:
     let extent = ctx.block().and(I1, &long, &backed);
     let Some(key) = key else {
         ctx.block().cond_br(&extent, &next_l, &miss_l);
-        finish(ctx, miss, next, recv, r, id);
+        finish(ctx, miss, next, recv, r, what);
         return;
     };
     branch(ctx, &extent, "arr_rep.key", &miss_l);
@@ -154,7 +165,7 @@ fn emit(ctx: &mut FnCtx<'_>, recv: &str, key: Option<&str>, r: FactsArrRep, id:
     let present = ctx.block().xor(I1, &hole, "true");
     branch(ctx, &present, "arr_rep.elem_kind", &next_l);
     elem_test(ctx, &raw, r.elem, &next_l, &miss_l);
-    finish(ctx, miss, next, recv, r, id);
+    finish(ctx, miss, next, recv, r, what);
 }
 
 /// Check mode at the rep-keyed tier: what the read `recv[idx]` (`idx` an
@@ -169,7 +180,7 @@ pub(super) fn witness_read(
     let r = read.rep;
     crate::verify_facts::covered(
         crate::verify_facts::Fact::ArrayRep,
-        || serde_json::json!({ "local": read.local, "floor": r.floor, "read": true }),
+        || serde_json::json!({ "receiver": read.receiver.label(), "floor": r.floor, "read": true }),
     );
     let miss = ctx.new_block("arep.verify_miss");
     let next = ctx.new_block("arep.admitted");
@@ -215,7 +226,8 @@ pub(super) fn witness_read(
     let extent = ctx.block().and(I1, &long, &backed);
     branch(ctx, &extent, "arep.verify_key", &miss_l);
     if read.in_floor {
-        let below = ctx.block().icmp_ult(I32, idx, &floor);
+        // The floor the key was proven below (a field read call's own).
+        let below = ctx.block().icmp_ult(I32, idx, &read.key_floor.to_string());
         branch(ctx, &below, "arep.verify_stored", &miss_l);
     }
     // The slot, when the store holds it.
@@ -247,7 +259,7 @@ pub(super) fn witness_read(
         r.elem
     };
     elem_test(ctx, &raw, elem, &next_l, &miss_l);
-    finish(ctx, miss, next, recv, r, read.local);
+    finish(ctx, miss, next, recv, r, &read.receiver.label());
 }
 
 /// The element kind test of a present slot `raw`: none for Boxed, a plain
@@ -287,12 +299,12 @@ fn branch(ctx: &mut FnCtx<'_>, cond: &str, name: &str, other: &str) {
 }
 
 /// The miss block's report, then `next` is current.
-fn finish(ctx: &mut FnCtx<'_>, miss: usize, next: usize, recv: &str, r: FactsArrRep, id: u32) {
+fn finish(ctx: &mut FnCtx<'_>, miss: usize, next: usize, recv: &str, r: FactsArrRep, what: &str) {
     ctx.current_block = miss;
     let site = crate::verify_facts::site_arg(
         ctx,
         &format!(
-            "array rep of local {id}: elem {:?}, floor {}, dense {}, fixed {}",
+            "array rep of {what}: elem {:?}, floor {}, dense {}, fixed {}",
             r.elem, r.floor, r.dense, r.fixed
         ),
         crate::verify_facts::Fact::ArrayRep,
diff --git a/crates/perry-codegen/src/expr/index_get/proven_array.rs b/crates/perry-codegen/src/expr/index_get/proven_array.rs
index e0a1d7fd429..dbcfa5f96bc 100644
--- a/crates/perry-codegen/src/expr/index_get/proven_array.rs
+++ b/crates/perry-codegen/src/expr/index_get/proven_array.rs
@@ -1,8 +1,10 @@
 //! Element reads whose receiver wpfacts proves (representation RFC §10.7,
 //! phase P4).
 //!
-//! **The rep-keyed tier** (DESIGN-p4l1 §4.2, PR-C2; `RepRead`). A local,
-//! parameter or module const the facts give `FactsRep::Arr(r)` holds only
+//! **The rep-keyed tier** (DESIGN-p4l1 §4.2, PR-C2 and PR-C3; `RepRead`).
+//! A local, parameter or module const the facts give `FactsRep::Arr(r)`,
+//! and a field read whose every class holds `Arr` in the field
+//! (`wpfacts_access::field_array`, `r` their join), holds only
 //! plain program Arrays: each is a `GC_TYPE_ARRAY` for its whole life, with
 //! no element descriptor and no deleted element (no hard marker), `length`
 //! and `capacity` of at least `r.floor`, no hole below the floor when
@@ -33,9 +35,14 @@
 //! (REVIEW-p4l1 R6). `PERRY_FACTS_ARRAY_TIER=0` turns the tier off: every
 //! read keeps the tier it had.
 //!
+//! A field read call (b1, `lower_call::field_read_call`) whose own index
+//! is in the floor (wpfacts `FieldReadCall::in_floor`) reads here too
+//! (`lower_in_floor`): the method body's read joins every caller's key,
+//! the call has its own.
+//!
 //! **The fixed-storage read** (wpfacts `ModuleBindings::element_reads`,
 //! `FactsElementRead`), for a receiver the tier above does not name (a
-//! field read, a temporary).
+//! temporary, a field the facts do not give `Arr`).
 //!
 //! Every receiver of such a read is a program Array that keeps its birth
 //! length for the whole program: no store, builtin, `defineProperty` or
@@ -76,12 +83,32 @@ pub(super) enum Proven {
 #[derive(Clone, Copy, Debug, PartialEq, Eq)]
 pub(crate) struct RepRead {
     pub(crate) rep: FactsArrRep,
-    /// The key is an integer in `[0, rep.floor)` at every copy of the read.
+    /// The key is an integer in `[0, key_floor)` at every copy of the read.
     pub(crate) in_floor: bool,
+    /// The floor the key is below: `rep.floor`, or a field read call's own
+    /// (every Array that call can read has at least as many elements).
+    pub(crate) key_floor: u32,
     /// The read's value is a proven Number: a plain double.
     pub(crate) number: bool,
-    /// The receiver local, for the check-mode report.
-    pub(crate) local: u32,
+    /// The receiver, for the check-mode report.
+    pub(crate) receiver: Receiver,
+}
+
+/// The receiver expression of a rep-keyed read.
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub(crate) enum Receiver {
+    Local(u32),
+    /// A field read (`FieldProof::array`).
+    Field,
+}
+
+impl Receiver {
+    pub(crate) fn label(self) -> String {
+        match self {
+            Receiver::Local(id) => format!("local {id}"),
+            Receiver::Field => "a field read".to_string(),
+        }
+    }
 }
 
 impl RepRead {
@@ -114,19 +141,7 @@ pub(crate) fn rep_read(ctx: &FnCtx<'_>, object: &Expr, element_offset: u32) -> O
     if !tier_enabled() || typed_feedback_emission_enabled() {
         return None;
     }
-    let Expr::LocalGet(id) = object else {
-        return None;
-    };
-    // A local the codegen keeps in scalar slots holds no array word (R6).
-    if ctx.scalar_replaced_arrays.contains_key(id)
-        || ctx.array_row_aliases.contains_key(id)
-        || ctx.scalar_replaced.contains_key(id)
-    {
-        return None;
-    }
-    let FactsRep::Arr(rep) = crate::codegen::facts_rep::local(ctx, *id)? else {
-        return None;
-    };
+    let (rep, receiver) = receiver_rep(ctx, object)?;
     let in_floor = element_offset != 0
         && ctx
             .wpfacts
@@ -138,11 +153,78 @@ pub(crate) fn rep_read(ctx: &FnCtx<'_>, object: &Expr, element_offset: u32) -> O
     Some(RepRead {
         rep,
         in_floor,
+        key_floor: rep.floor,
         number,
-        local: *id,
+        receiver,
     })
 }
 
+/// THE query for a receiver expression's `Arr` representation
+/// (DESIGN-p4l1 §4.2): a local, parameter or module const
+/// (`BindingFacts::rep`), or a field read (`FieldProof::array`).
+fn receiver_rep(ctx: &FnCtx<'_>, object: &Expr) -> Option<(FactsArrRep, Receiver)> {
+    match object {
+        Expr::LocalGet(id) => {
+            // A local the codegen keeps in scalar slots holds no array
+            // word (R6).
+            if ctx.scalar_replaced_arrays.contains_key(id)
+                || ctx.array_row_aliases.contains_key(id)
+                || ctx.scalar_replaced.contains_key(id)
+            {
+                return None;
+            }
+            let FactsRep::Arr(rep) = crate::codegen::facts_rep::local(ctx, *id)? else {
+                return None;
+            };
+            Some((rep, Receiver::Local(*id)))
+        }
+        Expr::PropertyGet {
+            object: holder,
+            property,
+            ..
+        } => {
+            if !crate::codegen::facts_rep::enabled() || ctx.wpfacts_off {
+                return None;
+            }
+            let rep = crate::expr::wpfacts_access::field_array(ctx, holder, property)?;
+            Some((rep, Receiver::Field))
+        }
+        _ => None,
+    }
+}
+
+/// The read of a field read call whose own index is in the floor
+/// (`lower_call::field_read_call`), when the tier takes it: the receiver
+/// expression's representation, dense, with a floor.
+pub(crate) fn in_floor_rep(ctx: &FnCtx<'_>, object: &Expr) -> Option<FactsArrRep> {
+    if !tier_enabled() || typed_feedback_emission_enabled() || ctx.wpfacts_off {
+        return None;
+    }
+    let (rep, _) = receiver_rep(ctx, object)?;
+    (rep.dense && rep.floor > 0).then_some(rep)
+}
+
+/// Read `arr_box[idx_i32]` for a field read call whose index is an integer
+/// in `[0, key_floor)` (`in_floor_rep` gave `rep`): a present own element,
+/// so the load has no bound and no hole test, and the value is of
+/// `rep.elem`.
+pub(crate) fn lower_in_floor(
+    ctx: &mut FnCtx<'_>,
+    arr_box: &str,
+    idx_i32: &str,
+    rep: FactsArrRep,
+    key_floor: u32,
+) -> String {
+    let read = RepRead {
+        rep,
+        in_floor: true,
+        key_floor,
+        number: rep.elem != crate::codegen::FactsElemRep::Boxed,
+        receiver: Receiver::Field,
+    };
+    lower_rep(ctx, arr_box, idx_i32, read, false)
+}
+
 /// `e` is an element read the tier loads below a dense floor and whose
 /// value is a proven Number: a present own element, never `undefined` or
 /// `null`, so `e ?? d` is `e`.
@@ -223,7 +305,7 @@ fn lower_rep(
     crate::expr::store_census::bump(ctx, crate::expr::store_census::ELEM_READ_OTHER_TIER);
     crate::verify_facts::consumed(
         crate::verify_facts::Fact::ArrayRep,
-        || serde_json::json!({ "local": read.local, "floor": r.floor, "in_floor": read.in_floor }),
+        || serde_json::json!({ "receiver": read.receiver.label(), "floor": r.floor, "in_floor": read.in_floor }),
     );
     crate::facts_consumed::used();
     if crate::verify_facts::enabled() {
diff --git a/crates/perry-codegen/src/expr/index_get/proven_array_tests.rs b/crates/perry-codegen/src/expr/index_get/proven_array_tests.rs
index feda03b0613..840396cb42d 100644
--- a/crates/perry-codegen/src/expr/index_get/proven_array_tests.rs
+++ b/crates/perry-codegen/src/expr/index_get/proven_array_tests.rs
@@ -322,3 +322,204 @@ fn a_scalar_replaced_literal_never_takes_the_tier() {
     // header; the read stays the scalar slots' own.
     assert_eq!(with, ir(false), "the rep changes nothing\n{f}");
 }
+
+// ---- PR-C3: a field read as the receiver, and the in-floor field read call ----
+
+const FIELD_SRC: &str = "export class Board {\n\
+  board: number[] = [];\n\
+  at(sq: number): number { return this.board[sq] ?? 0; }\n\
+  inFloor(): number { return this.at(5); }\n\
+  outside(): number { return this.at(200); }\n\
+  direct(m: number): number { return this.board[m & 127]; }\n\
+}\n";
+
+/// A growable board: dense below 128, storage that may move.
+const GROWABLE: FactsArrRep = FactsArrRep {
+    elem: FactsElemRep::F64,
+    floor: 128,
+    dense: true,
+    fixed: false,
+};
+
+/// IR of `FIELD_SRC` with `this` a `Board` in every method, `board` of
+/// representation `rep`, both `this.at(...)` calls field read calls, and
+/// `inFloor`'s call in the floor when `in_floor`.
+fn field_ir(rep: FactsRep, in_floor: bool) -> String {
+    use crate::codegen::{FactsClass, FactsField, FactsFieldReadCall, FactsRecv};
+    let m = lower(FIELD_SRC);
+    let class = m.classes.iter().find(|c| c.name == "Board").expect("Board");
+    let mut elision = ElisionFacts::default();
+    for f in &class.methods {
+        elision.this_of.insert(
+            f.id,
+            FactsRecv {
+                class_ids: vec![class.id],
+                nullable: false,
+                checked: false,
+            },
+        );
+    }
+    elision.classes.insert(
+        class.id,
+        FactsClass {
+            display: class.name.clone(),
+            fixed_layout: true,
+            fields: vec![FactsField {
+                key: "board".into(),
+                slot: 0,
+                readonly: true,
+                kind_mask: 0x80,
+                ta_stable: false,
+                ta_kind: None,
+                declared: false,
+                reserved: false,
+                fns: Vec::new(),
+                classes: Vec::new(),
+                nullable: false,
+                rep,
+            }],
+        },
+    );
+    // SWC offsets are 1-based.
+    let at = |text: &str| FIELD_SRC.find(text).expect(text) as u32 + 1;
+    let read = FactsFieldReadCall {
+        field: "board".into(),
+        index_arg: 0,
+        default: Some(0f64.to_bits()),
+        element_offset: at("this.board[sq]"),
+        field_offset: at("this.board[sq]"),
+        in_floor: None,
+    };
+    let inside = at("this.at(5)");
+    let outside = at("this.at(200)");
+    elision.field_read_calls.insert(
+        inside,
+        FactsFieldReadCall {
+            in_floor: in_floor.then_some(128),
+            ..read.clone()
+        },
+    );
+    elision.field_read_calls.insert(outside, read);
+    elision.call_arg_ranges.insert(inside, vec![Some((5, 5))]);
+    elision
+        .call_arg_ranges
+        .insert(outside, vec![Some((200, 200))]);
+    // The body's own read joins every caller's key; the direct read has
+    // its own.
+    elision.element_keys.insert(at("this.board[sq]"), (5, 200));
+    elision
+        .element_keys
+        .insert(at("this.board[m & 127]"), (0, 127));
+    let opts = CompileOptions {
+        emit_ir_only: true,
+        program_layouts: Arc::new(crate::layout_families::compute(
+            [("pa.ts", &m)],
+            true,
+            &Default::default(),
+        )),
+        program_facts: ProgramFactsView {
+            elision: Arc::new(elision),
+            ..Default::default()
+        },
+        ..Default::default()
+    };
+    String::from_utf8(compile_module(&m, opts).expect("fixture compiles")).expect("UTF-8 IR")
+}
+
+/// The capacity bound of a read outside the floor.
+fn capacity_bound(ir: &str) -> bool {
+    ir.contains("arep.inside")
+}
+
+#[test]
+fn an_in_floor_field_read_call_is_the_field_load_and_the_slot_load() {
+    let ir = field_ir(FactsRep::Arr(GROWABLE), true);
+    let f = body(&ir, "inFloor").join("\n");
+    assert!(!f.contains(".guard.prefix"), "no guarded tier\n{f}");
+    assert!(!capacity_bound(&f), "no bound\n{f}");
+    assert!(!f.contains("arep.own"), "no hole test\n{f}");
+    assert!(!f.contains("arep.number"), "no number test\n{f}");
+    // Growable storage: exactly the forwarding test stays, with its cold
+    // read.
+    assert!(forwarding_test(&f), "{f}");
+    assert_eq!(
+        f.lines().filter(|l| l.starts_with("arep.live")).count(),
+        1,
+        "{f}"
+    );
+    assert!(
+        f.lines()
+            .any(|l| l.contains("add i64") && l.trim_end().ends_with(", 24")),
+        "front-offset address\n{f}"
+    );
+    // Fixed storage: one load, no test and no cold arm.
+    let ir = field_ir(FactsRep::Arr(BOARD), true);
+    let f = body(&ir, "inFloor").join("\n");
+    assert!(!f.contains("arep."), "{f}");
+    assert!(!f.contains("perry_array_read_cold_shared"), "{f}");
+    assert!(!forwarding_test(&f), "{f}");
+}
+
+#[test]
+fn a_field_read_call_outside_the_floor_keeps_its_bound_and_its_default() {
+    let ir = field_ir(FactsRep::Arr(GROWABLE), true);
+    let f = body(&ir, "outside").join("\n");
+    assert!(
+        !f.contains(".guard.prefix"),
+        "the tier, not the guards\n{f}"
+    );
+    assert!(capacity_bound(&f), "the capacity bound\n{f}");
+    assert!(forwarding_test(&f), "{f}");
+    assert!(f.contains("perry_array_read_cold_shared"), "{f}");
+    // Without the call's own floor, the in-floor call is the same read.
+    let ir = field_ir(FactsRep::Arr(GROWABLE), false);
+    let f = body(&ir, "inFloor").join("\n");
+    assert!(capacity_bound(&f), "{f}");
+}
+
+#[test]
+fn a_direct_read_of_an_arr_field_takes_the_tier() {
+    let ir = field_ir(FactsRep::Arr(GROWABLE), false);
+    let f = body(&ir, "direct").join("\n");
+    assert!(!f.contains(".guard.prefix"), "no guarded tier\n{f}");
+    assert!(forwarding_test(&f), "{f}");
+    assert!(!capacity_bound(&f), "in the floor by its own key\n{f}");
+}
+
+#[test]
+fn a_boxed_field_keeps_every_read_as_it_was() {
+    let boxed = field_ir(FactsRep::Boxed, true);
+    assert!(!boxed.contains("arep."), "{boxed}");
+    // The call's floor alone changes nothing: the field read is not `Arr`.
+    assert_eq!(boxed, field_ir(FactsRep::Boxed, false));
+}
+
+#[test]
+fn the_array_rep_join_says_what_both_say() {
+    let a = FactsArrRep {
+        elem: FactsElemRep::I32,
+        floor: 128,
+        dense: true,
+        fixed: true,
+    };
+    let b = FactsArrRep {
+        elem: FactsElemRep::F64,
+        floor: 8,
+        dense: true,
+        fixed: false,
+    };
+    let j = FactsArrRep::join(a, b);
+    assert_eq!(
+        (j.elem, j.floor, j.dense, j.fixed),
+        (FactsElemRep::F64, 8, true, false)
+    );
+    assert_eq!(FactsArrRep::join(a, b), FactsArrRep::join(b, a));
+    assert_eq!(FactsArrRep::join(a, a), a);
+    let holey = FactsArrRep {
+        dense: false,
+        elem: FactsElemRep::Boxed,
+        ..a
+    };
+    let j = FactsArrRep::join(a, holey);
+    assert_eq!((j.elem, j.dense), (FactsElemRep::Boxed, false));
+}
diff --git a/crates/perry-codegen/src/expr/wpfacts_access.rs b/crates/perry-codegen/src/expr/wpfacts_access.rs
index 275e32d1709..9dabf1136fc 100644
--- a/crates/perry-codegen/src/expr/wpfacts_access.rs
+++ b/crates/perry-codegen/src/expr/wpfacts_access.rs
@@ -108,6 +108,12 @@ pub(crate) struct FieldProof {
     /// once stored, so the load is followed by the hole compare, whose miss
     /// is the site's complete generic operation.
     pub maybe_absent: bool,
+    /// The read is a value of representation `Arr` (DESIGN-p4l1 §3.2): the
+    /// join, over the class set, of what the field holds
+    /// (`FactsField::rep`). `None` when some class's field may hold
+    /// anything but plain program Arrays, and for a guarded or possibly
+    /// absent read, whose value may come from elsewhere.
+    pub array: Option<crate::codegen::FactsArrRep>,
 }
 
 impl FieldProof {
@@ -227,6 +233,49 @@ fn receiver(ctx: &FnCtx<'_>, object: &Expr) -> Option<(crate::codegen::FactsRecv
     }
 }
 
+/// The join of the field `property`'s representation over the classes
+/// `class_ids`, when it is `Arr` in each (`FieldProof::array`).
+fn class_set_array(
+    ctx: &FnCtx<'_>,
+    class_ids: &[u32],
+    property: &str,
+) -> Option<crate::codegen::FactsArrRep> {
+    use crate::codegen::{FactsArrRep, FactsRep};
+    let mut out: Option<FactsArrRep> = None;
+    for &cid in class_ids {
+        let f = ctx.wpfacts.field(cid, property)?;
+        let FactsRep::Arr(r) = f.rep else {
+            return None;
+        };
+        if f.declared || f.reserved {
+            return None;
+        }
+        out = Some(out.map_or(r, |o| FactsArrRep::join(o, r)));
+    }
+    out
+}
+
+/// The representation of the value `object.property` reads, when the facts
+/// give it `Arr` (DESIGN-p4l1 §3.2, §4.2): `object` is an unchecked proven
+/// receiver, no interpreted code can run, and in every class it may be the
+/// field holds only plain program Arrays for the object's whole life. It
+/// is `FieldProof::array` without the proof's slot: the field's value is
+/// the same whichever way the read is lowered.
+pub(crate) fn field_array(
+    ctx: &FnCtx<'_>,
+    object: &Expr,
+    property: &str,
+) -> Option<crate::codegen::FactsArrRep> {
+    if property.starts_with('#') || ctx.wpfacts.interp_guard {
+        return None;
+    }
+    let (r, _) = receiver(ctx, object)?;
+    if r.checked {
+        return None;
+    }
+    class_set_array(ctx, &r.class_ids, property)
+}
+
 /// FVA: the class ids the facts prove a call's receiver to be one of (an
 /// unchecked binding, no interpreted code), and whether it may also be
 /// null or undefined (then the site keeps that receiver test, as a read
@@ -571,6 +620,11 @@ pub(crate) fn prove(
         checked,
         interp_guard,
         maybe_absent,
+        array: if guarded || maybe_absent {
+            None
+        } else {
+            class_set_array(ctx, &recv.class_ids, property)
+        },
     };
     crate::verify_facts::field_consumed(&proof, property);
     Some(proof)
@@ -909,6 +963,15 @@ pub(crate) fn try_lower_get(
         let field_ptr = emit_proof_slot_ptr(ctx, &recv_box, &p);
         let val = ctx.block().load(DOUBLE, &field_ptr);
         emit_witness(ctx, &recv_box, &val, property, &p, 0, site);
+        if let Some(r) = p.array.filter(|_| crate::verify_facts::enabled()) {
+            // Check mode: the field's `Arr` claim, on the word just read.
+            super::index_get::array_rep::witness_value(
+                ctx,
+                &val,
+                r,
+                &format!("field {property} of {}", p.binding),
+            );
+        }
         // A Number has one encoding in every JS value (the raw double), so
         // a read the facts prove is a Number is the loaded word: no tag
         // test, no select, no branch.
diff --git a/crates/perry-codegen/src/lower_call/field_read_call.rs b/crates/perry-codegen/src/lower_call/field_read_call.rs
index 9f6df8a96ad..8a2a972526b 100644
--- a/crates/perry-codegen/src/lower_call/field_read_call.rs
+++ b/crates/perry-codegen/src/lower_call/field_read_call.rs
@@ -9,9 +9,20 @@
 //! are inert and reach no ender, so evaluating the index argument inside the
 //! read (and dropping the others) is the call's evaluation exactly.
 //!
+//! **In the floor (DESIGN-p4l1 §2.8, §4.2; PR-C3).** The body's read joins
+//! every caller's key, so its own facts keep the bound, the hole test and
+//! the `??`. A call whose own index the facts prove inside the floor of
+//! every Array the field can hold (`FactsFieldReadCall::in_floor`) reads a
+//! present own element: when the field read is a value of representation
+//! `Arr` (`proven_array::in_floor_rep`), the call is the field load and the
+//! slot load of the rep-keyed tier, and with Number elements the value is
+//! never nullish, so `?? L` is the value.
+//!
 //! Check mode (`PERRY_VERIFY_FACTS=1`): the real call runs beside the read,
 //! and the two values must be the same bits. A miss reports the false
-//! proof and exits 86.
+//! proof and exits 86. An in-floor read is also tested where it loads
+//! (`array_rep::witness_read`: the key is below the call's floor, the slot
+//! is no hole and holds an element of the proven kind).
 
 use anyhow::Result;
 use perry_hir::{Expr, LogicalOp};
@@ -104,13 +115,52 @@ pub(crate) fn try_lower(
         || serde_json::json!({ "call": site }),
     );
     crate::facts_consumed::used();
-    let value = crate::expr::lower_expr(ctx, &read)?;
+    let value = match in_floor(ctx, site, &read) {
+        Some((object, index, rep, floor)) => {
+            // The index is inert and reaches no ender (the accessor), so no
+            // collection runs between it and the field load.
+            let idx = crate::expr::lower_expr_as_i32(ctx, index)?;
+            let arr = crate::expr::lower_expr(ctx, object)?;
+            crate::expr::index_get::proven_array::lower_in_floor(ctx, &arr, &idx, rep, floor)
+        }
+        None => crate::expr::lower_expr(ctx, &read)?,
+    };
     if crate::verify_facts::enabled() {
         witness(ctx, callee, args, &value, site)?;
     }
     Ok(Some(value))
 }
 
+/// The in-floor form of the proven read `read` of the call at `site`
+/// (module docs): its field read, its index, the field read's
+/// representation and the floor the call's index is below. `None` keeps the
+/// read as written: the call is not in the floor, the field read is not
+/// `Arr`, or a `?? L` is over elements that are not all Numbers (a stored
+/// `null` or `undefined` is a present element).
+fn in_floor<'e>(
+    ctx: &FnCtx<'_>,
+    site: u32,
+    read: &'e Expr,
+) -> Option<(&'e Expr, &'e Expr, crate::codegen::FactsArrRep, u32)> {
+    let floor = ctx.wpfacts.field_read_calls.get(&site)?.in_floor?;
+    let (element, coalesced) = match read {
+        Expr::Logical {
+            op: LogicalOp::Coalesce,
+            left,
+            ..
+        } => (left.as_ref(), true),
+        e => (e, false),
+    };
+    let Expr::IndexGet { object, index, .. } = element else {
+        return None;
+    };
+    let rep = crate::expr::index_get::proven_array::in_floor_rep(ctx, object)?;
+    if coalesced && rep.elem == crate::codegen::FactsElemRep::Boxed {
+        return None;
+    }
+    Some((object, index, rep, floor))
+}
+
 /// Check mode: the real call's value equals the read's.
 fn witness(
     ctx: &mut FnCtx<'_>,
diff --git a/crates/perry-codegen/src/type_analysis/numeric/number_result_tests.rs b/crates/perry-codegen/src/type_analysis/numeric/number_result_tests.rs
index cf6034db594..69f2b3330a6 100644
--- a/crates/perry-codegen/src/type_analysis/numeric/number_result_tests.rs
+++ b/crates/perry-codegen/src/type_analysis/numeric/number_result_tests.rs
@@ -41,6 +41,7 @@ fn body(with_facts: bool, checked: bool, interp: bool, kind: u16) -> String {
                     declared: false,
                     reserved: false,
                     fns: Vec::new(),
+                    rep: crate::codegen::FactsRep::Boxed,
                 }],
             },
         );
diff --git a/crates/perry-wpfacts/src/bindings.rs b/crates/perry-wpfacts/src/bindings.rs
index 224820127e2..f50ec3e7068 100644
--- a/crates/perry-wpfacts/src/bindings.rs
+++ b/crates/perry-wpfacts/src/bindings.rs
@@ -617,13 +617,20 @@ fn facts_of(g: &Gen, n: u32) -> BindingFacts {
 /// value proves nothing. The rep is the join over the tokens of each one's
 /// own (`tok_arr_rep`). `None` with `Model::array_reps` off.
 pub(crate) fn arr_rep(m: &Model, nodes: &[NodeId]) -> Option<ArrRep> {
+    arr_rep_beside(m, nodes, 0)
+}
+
+/// `arr_rep` of `nodes` with the primitives `ignored` left out of account:
+/// 0 everywhere but under the negative control `arrfield`
+/// (`Model::arr_field_sabotage`).
+pub(crate) fn arr_rep_beside(m: &Model, nodes: &[NodeId], ignored: u16) -> Option<ArrRep> {
     if !m.array_reps {
         return None;
     }
     let mut out: Option<ArrRep> = None;
     for &n in nodes {
         let node = &m.nodes[n as usize];
-        if node.prim != 0 {
+        if node.prim & !ignored != 0 {
             return None;
         }
         for t in node.pts.to_sorted() {
diff --git a/crates/perry-wpfacts/src/derive.rs b/crates/perry-wpfacts/src/derive.rs
index 688555b0292..2b4fd8f6634 100644
--- a/crates/perry-wpfacts/src/derive.rs
+++ b/crates/perry-wpfacts/src/derive.rs
@@ -113,8 +113,9 @@ pub struct FieldFacts {
     /// (`bindings::arr_rep`) when it is definite, a data field, and the
     /// template is neither escaped nor hard (a `delete` or a
     /// `setPrototypeOf` on an instance can make the read `undefined`
-    /// without the field node holding it); Boxed otherwise. No consumer
-    /// yet (PR-C3 reads it).
+    /// without the field node holding it); Boxed otherwise, and with
+    /// `PERRY_FACTS_ARRAY_FIELDS=0`. A read of the field is a value of this
+    /// representation (PR-C3: codegen's `FieldProof::array`).
     pub rep: crate::bindings::Rep,
 }
 
@@ -899,14 +900,21 @@ fn template_facts(
         } else {
             Vec::new()
         };
-        let rep = if definite && !is_accessor && escape.is_none() && hard.is_none() {
+        let whole_life =
+            m.array_fields && definite && !is_accessor && escape.is_none() && hard.is_none();
+        let rep = if whole_life {
             // The field nodes of the tokens that have one, as `field_kind`
             // reads them.
             let nodes: Vec<NodeId> = ts
                 .iter()
                 .filter_map(|t| m.fields.get(&(*t, a)).copied())
                 .collect();
-            crate::bindings::arr_rep(m, &nodes)
+            let ignored = if m.arr_field_sabotage {
+                prim::NULL | prim::UNDEF
+            } else {
+                0
+            };
+            crate::bindings::arr_rep_beside(m, &nodes, ignored)
                 .map_or(crate::bindings::Rep::Boxed, crate::bindings::Rep::Arr)
         } else {
             crate::bindings::Rep::Boxed
diff --git a/crates/perry-wpfacts/src/dump.rs b/crates/perry-wpfacts/src/dump.rs
index c00e61d7856..2c694fa1f66 100644
--- a/crates/perry-wpfacts/src/dump.rs
+++ b/crates/perry-wpfacts/src/dump.rs
@@ -137,6 +137,27 @@ pub fn dump_text(pf: &ProgramFacts) -> String {
             }
         }
     }
+    // DESIGN-p4l1 §5.6: each field read call (b1), its key's interval at
+    // the call, what the read reads from, and the in-floor verdict.
+    for (mi, bindings) in pf.bindings.iter().enumerate() {
+        for (offset, c) in &bindings.field_read_calls {
+            let key = bindings
+                .call_arg_ranges
+                .binary_search_by_key(offset, |(o, _)| *o)
+                .ok()
+                .and_then(|at| bindings.call_arg_ranges[at].1.get(c.index_arg as usize))
+                .copied()
+                .flatten()
+                .map_or("top".to_string(), |(lo, hi)| format!("[{lo},{hi}]"));
+            let rep = c
+                .array
+                .map_or("boxed".to_string(), |r| crate::bindings::Rep::Arr(r).name());
+            out.push_str(&format!(
+                "# field_read_call module={mi} call={offset} field={} key={key} rep={rep} in_floor={}\n",
+                c.field, c.in_floor as u8
+            ));
+        }
+    }
     // N6: each module binding the facts give one Number.
     for (mi, bindings) in pf.bindings.iter().enumerate() {
         for (id, value) in &bindings.const_numbers {
diff --git a/crates/perry-wpfacts/src/field_read_calls.rs b/crates/perry-wpfacts/src/field_read_calls.rs
index 56890f7714b..6124d9c5cdc 100644
--- a/crates/perry-wpfacts/src/field_read_calls.rs
+++ b/crates/perry-wpfacts/src/field_read_calls.rs
@@ -25,8 +25,17 @@
 //! The caller's receivers flow into F's `this` (1), so they are a subset of
 //! every set F's facts were joined over (4, 5b, 5d): the facts hold for
 //! every value the caller can pass.
+//!
+//! **In the floor (DESIGN-p4l1 §2.8, §3; PR-C3).** `FieldReadCall::array` is
+//! the representation of everything F's element read may read from
+//! (`bindings::arr_rep` over every copy of its receiver), and `in_floor`
+//! says this call's own argument `k` is an integer in `[0, array.floor)` of
+//! arrays that are dense below it. The slot is then a present own element
+//! at every such call, whatever keys F's other callers pass: the body's
+//! read joins them all and keeps its `undefined`, the call does not.
+//! `PERRY_FACTS_ARRAY_FIELDS=0` exports neither.
 
-use crate::bindings::{owner_metadata_written, ModuleBindings};
+use crate::bindings::{arr_rep, owner_metadata_written, ArrRep, ModuleBindings};
 use crate::derive::{SiteFacts, Verdict};
 use crate::gen::Gen;
 use crate::model::{TokKind, TOP};
@@ -69,6 +78,12 @@ pub struct FieldReadCall {
     pub element_offset: u32,
     /// F's `this.f` read's byte offset.
     pub field_offset: u32,
+    /// What F's element read reads from, when that is only plain program
+    /// Arrays (module docs).
+    pub array: Option<ArrRep>,
+    /// This call's index is an integer in `[0, array.floor)` and the arrays
+    /// are dense below the floor: the slot is a present own element.
+    pub in_floor: bool,
 }
 
 type Shape = (String, usize, Option<FieldReadDefault>, u32, u32);
@@ -145,13 +160,16 @@ fn method(m: &perry_hir::Module, func_id: u32) -> Option<&perry_hir::Function> {
 /// Fill `ModuleBindings::field_read_calls` (module docs). `interpreted`:
 /// interpreted code can run (`ProgramFacts::interp_guard`). `sabotage`: the
 /// negative control `PERRY_FACTS_SABOTAGE=fieldreadcall` drops conditions
-/// 1, 4 and 5 (the shape and argument count still hold).
+/// 1, 4 and 5 (the shape and argument count still hold). `floor_sabotage`:
+/// the negative control `PERRY_FACTS_SABOTAGE=arrb1` claims `in_floor` for
+/// every call into a dense floor, whatever its key.
 pub(crate) fn collect(
     g: &Gen<'_>,
     sites: &[SiteFacts],
     bindings: &mut [ModuleBindings],
     interpreted: bool,
     sabotage: bool,
+    floor_sabotage: bool,
 ) {
     let m = &g.m;
     // 5c.
@@ -196,6 +214,31 @@ pub(crate) fn collect(
                         })
             })
     };
+    // A summarized body's receiver node has one copy per instance
+    // (`Inst::fresh`), as `element_keys` reads a key's.
+    let mut inst_copies: std::collections::HashMap<crate::model::NodeId, Vec<_>> =
+        Default::default();
+    if m.array_fields {
+        for inst in 0..m.sum.insts.len() as u32 {
+            m.inst_copies(inst, |orig, copy| {
+                inst_copies.entry(orig).or_default().push(copy)
+            });
+        }
+    }
+    // What F's element read reads from: every copy of its receiver.
+    let array_of = |mi: u32, offset: u32| -> Option<ArrRep> {
+        if !m.array_fields {
+            return None;
+        }
+        let mut nodes = Vec::new();
+        for e in &g.element_sites {
+            if e.module == mi && e.byte_offset == offset && e.op == crate::derive::ElementOp::Read {
+                nodes.push(e.recv);
+                nodes.extend(inst_copies.get(&e.recv).into_iter().flatten().copied());
+            }
+        }
+        arr_rep(m, &nodes)
+    };
     for s in sites {
         let one_body = s.target_fns.len() == 1 || sabotage && !s.target_fns.is_empty();
         if !s.is_call || !one_body {
@@ -233,6 +276,16 @@ pub(crate) fn collect(
         {
             continue;
         }
+        let array = array_of(fm, element_offset);
+        let in_floor = array.is_some_and(|r| {
+            r.dense
+                && (floor_sabotage
+                    || args
+                        .get(k)
+                        .copied()
+                        .flatten()
+                        .is_some_and(|(lo, hi)| lo >= 0 && hi < i64::from(r.floor)))
+        });
         bindings[s.module as usize].field_read_calls.push((
             s.byte_offset,
             FieldReadCall {
@@ -241,6 +294,8 @@ pub(crate) fn collect(
                 default,
                 element_offset,
                 field_offset,
+                array,
+                in_floor,
             },
         ));
     }
diff --git a/crates/perry-wpfacts/src/lib.rs b/crates/perry-wpfacts/src/lib.rs
index effd78c8f4a..df839dc2c68 100644
--- a/crates/perry-wpfacts/src/lib.rs
+++ b/crates/perry-wpfacts/src/lib.rs
@@ -87,6 +87,9 @@ pub struct FactsConfig {
     /// No plain Array births, fused-fill birth or `Rep::Arr`
     /// (`PERRY_FACTS_ARRAY_REPS=0`, DESIGN-p4l1 PR-B).
     pub no_array_reps: bool,
+    /// No `Rep::Arr` for a field and no in-floor field read call
+    /// (`PERRY_FACTS_ARRAY_FIELDS=0`, DESIGN-p4l1 PR-C3).
+    pub no_array_fields: bool,
     /// An element read's past-the-end `undefined` is unconditional again
     /// (`PERRY_FACTS_ELEM_UNDEF=0`, PR-C1: `Cons::ElemUndef`).
     pub no_elem_undef: bool,
@@ -483,6 +486,8 @@ fn generate<'a>(
     g.m.arr_elem_sabotage = cfg.sabotage.as_deref() == Some("arrelem");
     g.m.arr_lazy_sabotage = cfg.sabotage.as_deref() == Some("arrlazy");
     g.m.arr_front_sabotage = cfg.sabotage.as_deref() == Some("arrfront");
+    g.m.array_fields = !cfg.no_array_fields;
+    g.m.arr_field_sabotage = cfg.sabotage.as_deref() == Some("arrfield");
     g.int_ranges = !cfg.no_int_ranges;
     g.arr_lengths = g.int_ranges && !cfg.no_array_lengths;
     g.guard_ranges = g.int_ranges && !cfg.no_guard_ranges;
@@ -907,6 +912,7 @@ fn compute_act<'a>(
             &mut bindings,
             interp_guard.is_some(),
             cfg.sabotage.as_deref() == Some("fieldreadcall"),
+            cfg.sabotage.as_deref() == Some("arrb1"),
         );
     }
     if canonical_numbers::enabled() {
diff --git a/crates/perry-wpfacts/src/model.rs b/crates/perry-wpfacts/src/model.rs
index d2c65faccb3..ff608963fd4 100644
--- a/crates/perry-wpfacts/src/model.rs
+++ b/crates/perry-wpfacts/src/model.rs
@@ -1324,6 +1324,14 @@ pub struct Model {
     /// allocation) keeps its floor, a wrong claim the element tier's
     /// front-offset witness must catch.
     pub arr_front_sabotage: bool,
+    /// PR-C3 (DESIGN-p4l1 §3): a field's `Rep::Arr` (`FieldFacts::rep`) and
+    /// a field read call's floor (`FieldReadCall::in_floor`);
+    /// `PERRY_FACTS_ARRAY_FIELDS=0` turns them off.
+    pub array_fields: bool,
+    /// Negative control (`PERRY_FACTS_SABOTAGE=arrfield`): a field's
+    /// representation ignores the `null` and `undefined` it also holds, a
+    /// wrong claim the witness at the field read must catch.
+    pub arr_field_sabotage: bool,
     pub max_work: u64,
     pub max_nodes: usize,
     pub atoms: Vec<String>,
diff --git a/crates/perry-wpfacts/src/tests/array_reps.rs b/crates/perry-wpfacts/src/tests/array_reps.rs
index 08a89d3ba85..9f4bbee3e36 100644
--- a/crates/perry-wpfacts/src/tests/array_reps.rs
+++ b/crates/perry-wpfacts/src/tests/array_reps.rs
@@ -490,3 +490,195 @@ fn a_redefined_or_deleted_element_gives_no_array_rep() {
         assert_eq!(rep(&src, "K"), Rep::Boxed, "{stmt}");
     }
 }
+
+// ---- PR-C3 (DESIGN-p4l1 §3, §2.8): the field's rep and the in-floor call ----
+
+/// The chess shape: a board born dense with 128 elements, stored into at
+/// keys that leave it, and read behind `at` by calls with their own keys.
+const FIELD_BOARD: &str = r#"
+class Chess {
+  board: number[] = new Array(128).fill(0);
+  ep: number = -1;
+  at(square: number): number { return this.board[square] ?? 0; }
+  set(square: number, piece: number): void { this.board[square] = piece; }
+  ranks(): number {
+    let s = 0;
+    for (let r = 7; r >= 0; r--) s += this.at(r * 16);
+    return s;
+  }
+  masked(move: number): number { return this.at(move & 127); }
+  capture(move: number): number { return this.at((move & 127) - 16); }
+  past(): number { return this.at(this.ep + 16); }
+}
+const c = new Chess();
+for (let i = -16; i < 144; i++) c.set(i, i & 7);
+c.ep = process.argv.length > 100 ? 40 : 20;
+let t = 0;
+for (let i = 0; i < 1000; i++) t += c.masked(i) + c.capture(i);
+console.log(c.ranks(), t, c.past());
+"#;
+
+/// The field read calls of `src` by the source text of their call.
+fn b1(src: &str, cfg: FactsConfig) -> Vec<(String, crate::FieldReadCall)> {
+    let pf = facts_with(src, cfg);
+    pf.bindings
+        .iter()
+        .flat_map(|b| b.field_read_calls.iter())
+        .map(|(offset, c)| {
+            // Offsets are 1-based.
+            let rest = &src[*offset as usize - 1..];
+            let end = rest.find(')').map_or(rest.len(), |e| e + 1);
+            (rest[..end].to_string(), c.clone())
+        })
+        .collect()
+}
+
+#[test]
+fn a_stored_into_board_field_keeps_its_dense_floor() {
+    let pf = facts(FIELD_BOARD);
+    let f = field(tmpl(&pf, "Chess"), "board");
+    // Growable: a store key reaches past the birth length.
+    assert!(
+        matches!(f.rep, Rep::Arr(a) if a.floor == 128 && a.dense && !a.fixed && a.elem != ElemRep::Boxed),
+        "{:?}",
+        f.rep
+    );
+}
+
+#[test]
+fn a_field_read_call_is_in_the_floor_by_its_own_key() {
+    let calls = b1(FIELD_BOARD, FactsConfig::default());
+    let of = |text: &str| {
+        calls
+            .iter()
+            .find(|(t, _)| t.starts_with(text))
+            .unwrap_or_else(|| panic!("no call {text}: {calls:?}"))
+            .1
+            .clone()
+    };
+    // Every call reads from the same arrays.
+    for (_, c) in &calls {
+        assert!(
+            matches!(c.array, Some(a) if a.floor == 128 && a.dense),
+            "{c:?}"
+        );
+    }
+    assert!(of("this.at(r * 16)").in_floor);
+    assert!(of("this.at(move & 127)").in_floor);
+    // `[-16, 111]` leaves the floor below; `[15, 56]` is inside.
+    assert!(!of("this.at((move & 127)").in_floor);
+    assert!(of("this.at(this.ep + 16").in_floor);
+}
+
+#[test]
+fn a_key_past_the_floor_is_not_in_it_unless_sabotaged() {
+    let src = FIELD_BOARD.replace("this.at(this.ep + 16)", "this.at(this.ep + 100)");
+    let past = |cfg| {
+        b1(&src, cfg)
+            .into_iter()
+            .find(|(t, _)| t.starts_with("this.at(this.ep + 100"))
+            .expect("the call is a field read")
+            .1
+            .in_floor
+    };
+    assert!(!past(FactsConfig::default()));
+    assert!(past(FactsConfig {
+        sabotage: Some("arrb1".into()),
+        ..Default::default()
+    }));
+}
+
+#[test]
+fn the_fields_switch_off_gives_no_field_rep_and_no_floor() {
+    let off = || FactsConfig {
+        no_array_fields: true,
+        ..Default::default()
+    };
+    let pf = facts_with(FIELD_BOARD, off());
+    assert_eq!(field(tmpl(&pf, "Chess"), "board").rep, Rep::Boxed);
+    let calls = b1(FIELD_BOARD, off());
+    assert!(!calls.is_empty());
+    for (_, c) in &calls {
+        assert!(c.array.is_none() && !c.in_floor, "{c:?}");
+    }
+    // A local keeps its rep: the switch is the field's.
+    let pf = facts_with("const K = [1, 2, 3];\nconsole.log(K[1]);", off());
+    assert!(pf
+        .bindings
+        .iter()
+        .flat_map(|b| b.locals.iter())
+        .any(|(_, b)| matches!(b.rep, Rep::Arr(_))));
+}
+
+#[test]
+fn a_call_into_a_holey_or_undefined_holding_field_is_not_in_the_floor() {
+    // No fused fill: holes below the length.
+    let holey = FIELD_BOARD.replace("new Array(128).fill(0)", "new Array(128)");
+    for (_, c) in b1(&holey, FactsConfig::default()) {
+        assert!(!c.in_floor, "{c:?}");
+    }
+    // A `delete` of an element makes the array hard: no rep at all.
+    let deleted = FIELD_BOARD.replace("c.ep = ", "delete c.board[3];\nc.ep = ");
+    for (_, c) in b1(&deleted, FactsConfig::default()) {
+        assert!(c.array.is_none() && !c.in_floor, "{c:?}");
+    }
+    // A length store takes the floor away.
+    let cut = FIELD_BOARD.replace("c.ep = ", "c.board.length = 4;\nc.ep = ");
+    for (_, c) in b1(&cut, FactsConfig::default()) {
+        assert!(!c.in_floor, "{c:?}");
+    }
+    // A stored `undefined` is a present element: the call stays in the
+    // floor, and the elements are Boxed (the `??` stays in codegen).
+    let undef = FIELD_BOARD.replace("c.ep = ", "(c.board as any)[5] = undefined;\nc.ep = ");
+    let calls = b1(&undef, FactsConfig::default());
+    assert!(calls.iter().any(|(_, c)| c.in_floor));
+    for (_, c) in &calls {
+        assert!(
+            matches!(c.array, Some(a) if a.elem == ElemRep::Boxed),
+            "{c:?}"
+        );
+    }
+}
+
+#[test]
+fn the_arrfield_control_ignores_a_null_in_the_field() {
+    let src = r#"class B {
+  items: number[] | null = null;
+  fill(): void { this.items = [1, 2, 3, 4]; }
+}
+const b = new B();
+b.fill();
+console.log(b.items);"#;
+    assert_eq!(field(tmpl(&facts(src), "B"), "items").rep, Rep::Boxed);
+    let pf = facts_with(
+        src,
+        FactsConfig {
+            sabotage: Some("arrfield".into()),
+            ..Default::default()
+        },
+    );
+    assert!(matches!(field(tmpl(&pf, "B"), "items").rep, Rep::Arr(_)));
+}
+
+#[test]
+fn the_dump_prints_each_field_read_call_with_its_key_and_verdict() {
+    let pf = facts(FIELD_BOARD);
+    let dump = pf.dump_text();
+    let lines: Vec<&str> = dump
+        .lines()
+        .filter(|l| l.starts_with("# field_read_call "))
+        .collect();
+    assert!(
+        lines
+            .iter()
+            .any(|l| l.contains("key=[0,127]") && l.ends_with("in_floor=1")),
+        "{lines:#?}"
+    );
+    assert!(
+        lines
+            .iter()
+            .any(|l| l.contains("key=[-16,111]") && l.ends_with("in_floor=0")),
+        "{lines:#?}"
+    );
+    assert!(lines.iter().all(|l| l.contains("rep=arr<")), "{lines:#?}");
+}
diff --git a/crates/perry/src/commands/compile/compile_env.rs b/crates/perry/src/commands/compile/compile_env.rs
index 35cfc2f1aaf..dd784b9a12c 100644
--- a/crates/perry/src/commands/compile/compile_env.rs
+++ b/crates/perry/src/commands/compile/compile_env.rs
@@ -65,6 +65,7 @@ pub(super) const COMPILE_ENV_VARS: &[&str] = &[
     "PERRY_FACTS_INT32_LOCALS",
     "PERRY_FACTS_INT_RANGES",
     "PERRY_FACTS_INT_DEMAND",
+    "PERRY_FACTS_ARRAY_FIELDS",
     "PERRY_FACTS_ARRAY_FLOOR",
     "PERRY_FACTS_ARRAY_REPS",
     "PERRY_FACTS_ARRAY_TIER",
diff --git a/crates/perry/src/commands/compile/compile_env/tests.rs b/crates/perry/src/commands/compile/compile_env/tests.rs
index e91586730aa..ee554d4f850 100644
--- a/crates/perry/src/commands/compile/compile_env/tests.rs
+++ b/crates/perry/src/commands/compile/compile_env/tests.rs
@@ -323,6 +323,7 @@ fn codegen_env_vars_are_build_cache_inputs() {
 #[test]
 fn array_fact_switches_are_cache_inputs() {
     for name in [
+        "PERRY_FACTS_ARRAY_FIELDS",
         "PERRY_FACTS_ARRAY_FLOOR",
         "PERRY_FACTS_ARRAY_LENGTHS",
         "PERRY_FACTS_ARRAY_REPS",
diff --git a/crates/perry/src/commands/compile/program_facts.rs b/crates/perry/src/commands/compile/program_facts.rs
index 594501be598..e6e253f60f9 100644
--- a/crates/perry/src/commands/compile/program_facts.rs
+++ b/crates/perry/src/commands/compile/program_facts.rs
@@ -147,6 +147,10 @@ pub(crate) fn run(
             std::env::var("PERRY_FACTS_ARRAY_REPS").as_deref(),
             Ok("0") | Ok("off") | Ok("false")
         ),
+        no_array_fields: matches!(
+            std::env::var("PERRY_FACTS_ARRAY_FIELDS").as_deref(),
+            Ok("0") | Ok("off") | Ok("false")
+        ),
         no_elem_undef: matches!(
             std::env::var("PERRY_FACTS_ELEM_UNDEF").as_deref(),
             Ok("0") | Ok("off") | Ok("false")
@@ -587,6 +591,7 @@ fn elision_for(pf: &perry_wpfacts::ProgramFacts, path: &str) -> perry_codegen::E
                     default,
                     element_offset: c.element_offset,
                     field_offset: c.field_offset,
+                    in_floor: c.array.filter(|_| c.in_floor).map(|r| r.floor),
                 },
             );
         }
@@ -713,6 +718,7 @@ fn elision_for(pf: &perry_wpfacts::ProgramFacts, path: &str) -> perry_codegen::E
                     ta_kind: f.ta_kind,
                     declared: f.declared,
                     reserved: f.reserved,
+                    rep: facts_rep(f.rep),
                 })
             })
             .collect();
@@ -886,6 +892,10 @@ pub(crate) fn activation(
             std::env::var("PERRY_FACTS_ARRAY_REPS").as_deref(),
             Ok("0") | Ok("off") | Ok("false")
         ),
+        no_array_fields: matches!(
+            std::env::var("PERRY_FACTS_ARRAY_FIELDS").as_deref(),
+            Ok("0") | Ok("off") | Ok("false")
+        ),
         no_elem_undef: matches!(
             std::env::var("PERRY_FACTS_ELEM_UNDEF").as_deref(),
             Ok("0") | Ok("off") | Ok("false")
diff --git a/scripts/test-verify-facts-s0.py b/scripts/test-verify-facts-s0.py
index 4d3e1974dba..c925fbb5ad0 100644
--- a/scripts/test-verify-facts-s0.py
+++ b/scripts/test-verify-facts-s0.py
@@ -117,6 +117,8 @@ def oracle(source, *argv):
         ("array-elem-negative", "arrelem", "array rep"),
         ("array-lazy-negative", "arrlazy", "array rep"),
         ("array-front-negative", "arrfront", "array rep"),
+        ("array-field-negative", "arrfield", "array rep"),
+        ("array-b1-negative", "arrb1", "array rep"),
         ("number-call-negative", "numbercall", "numeric result"),
         ("field-read-call-negative", "fieldreadcall", "field read call"),
         ("array-undef-negative", "arrundef", "element floor"),
diff --git a/scripts/verify_facts_s0/array-b1-negative.ts b/scripts/verify_facts_s0/array-b1-negative.ts
new file mode 100644
index 00000000000..c0324542439
--- /dev/null
+++ b/scripts/verify_facts_s0/array-b1-negative.ts
@@ -0,0 +1,21 @@
+// `at` is a field element read, and `board` is born dense with 16
+// elements. `probe` calls it with keys that leave the floor (`ep - 16` is
+// negative, `ep + 16` is past the end), whose value is the `?? 0`.
+// Under PERRY_FACTS_SABOTAGE=arrb1 the facts claim every such call's key
+// is in the floor, so the call loads the slot with no bound. The element
+// tier's witness must report the false proof at the key.
+class Board {
+  board: number[] = new Array(16).fill(1);
+  ep: number = process.argv.length > 100 ? 5 : 3;
+  at(sq: number): number {
+    return this.board[sq] ?? 0;
+  }
+  probe(): number {
+    const ep = this.ep;
+    return this.at(ep) * 100 + this.at(ep - 16) * 10 + this.at(ep + 16);
+  }
+}
+const b = new Board();
+let s = 0;
+for (let i = 0; i < 3; i++) s += b.probe();
+console.log(s);
diff --git a/scripts/verify_facts_s0/array-field-negative.ts b/scripts/verify_facts_s0/array-field-negative.ts
new file mode 100644
index 00000000000..e391fcae79a
--- /dev/null
+++ b/scripts/verify_facts_s0/array-field-negative.ts
@@ -0,0 +1,21 @@
+// `Bag.items` holds an Array or `null`. Under PERRY_FACTS_SABOTAGE=arrfield
+// the facts leave the `null` out of the field's representation, so a read
+// of the field is claimed to be a plain Array. The witness at the field
+// read must report the false proof at the `null` word.
+class Bag {
+  items: number[] | null = null;
+  fill(): void {
+    this.items = [1, 2, 3, 4];
+  }
+  sum(): number {
+    const a = this.items;
+    if (a === null) return -1;
+    let s = 0;
+    for (let i = 0; i < 4; i++) s += a[i] ?? 0;
+    return s;
+  }
+}
+const full = new Bag();
+const empty = new Bag();
+if (process.argv.length < 100) full.fill();
+console.log(full.sum(), empty.sum());
diff --git a/tests/parity/language/array/test_array_reps_fields.ts b/tests/parity/language/array/test_array_reps_fields.ts
new file mode 100644
index 00000000000..62c4fee9772
--- /dev/null
+++ b/tests/parity/language/array/test_array_reps_fields.ts
@@ -0,0 +1,205 @@
+// Arrays held in class fields read through the array representation tier
+// (DESIGN-p4l1 §3, §4.2, PR-C3): direct `this.f[i]` reads and reads behind
+// a method (`this.at(i)` is `this.f[i] ?? 0`), inside and outside the
+// floor, with the controls that must keep the bound, the hole test and the
+// `??`. Every line is a value node prints too.
+
+class Board {
+  board: number[] = new Array(128).fill(0);
+  side: number = 1;
+  ep: number = -1;
+  at(sq: number): number {
+    return this.board[sq] ?? 0;
+  }
+  set(sq: number, piece: number): void {
+    const old = this.at(sq);
+    this.board[sq] = piece + old * 0;
+  }
+  // Every key is on the board (the facts' interval for `r * 16 + f` may
+  // still be wider than the floor: the read then keeps its bound).
+  sumRanks(): number {
+    let s = 0;
+    for (let r = 0; r < 8; r++) {
+      for (let f = 0; f < 8; f++) s += this.at(r * 16 + f) * (r + 1);
+    }
+    return s;
+  }
+  // A masked key, and a direct read of the field.
+  masked(k: number): number {
+    return this.at(k & 127) + (this.board[k & 127] ?? 50) + this.board[(k + 1) & 127];
+  }
+  // Keys that leave the floor: the `??` is the value.
+  around(sq: number): string {
+    return [this.at(sq - 16), this.at(sq + 16), this.at(sq - 200), this.at(sq + 200)].join(",");
+  }
+  ray(from: number, step: number): number {
+    let n = 0;
+    let sq = from + step;
+    while ((sq & 0x88) === 0) {
+      if (this.at(sq) !== 0) return n * 10 + this.at(sq);
+      n++;
+      sq += step;
+    }
+    return -n - 1;
+  }
+}
+
+const b = new Board();
+for (let i = 0; i < 128; i++) if ((i & 0x88) === 0) b.set(i, (i * 7) % 13 - 6);
+console.log("ranks", b.sumRanks());
+let m = 0;
+for (let i = -300; i < 300; i++) m += b.masked(i);
+console.log("masked", m);
+console.log("around", b.around(0), b.around(119), b.around(64));
+console.log("ray", b.ray(0, 1), b.ray(4, 16), b.ray(119, -17), b.ray(7, 1));
+
+// Fixture 11: the field is reassigned to an array with another floor. The
+// facts join the two; reads in the same method see whichever is there.
+class Swap {
+  cells: number[] = new Array(32).fill(1);
+  at(i: number): number {
+    return this.cells[i] ?? -1;
+  }
+  total(n: number): number {
+    let s = 0;
+    for (let i = 0; i < n; i++) s += this.at(i & 31);
+    return s;
+  }
+  shrink(): number {
+    const before = this.total(64);
+    this.cells = new Array(8).fill(2);
+    return before * 1000 + this.total(64);
+  }
+}
+const sw = new Swap();
+console.log("swap", sw.total(40), sw.shrink(), sw.at(7), sw.at(8), sw.cells.length);
+
+// K-FS3: a computed-key store names the field.
+class Named {
+  data: number[] = new Array(16).fill(3);
+  at(i: number): number {
+    return this.data[i] ?? -1;
+  }
+  replace(name: string, other: number[]): void {
+    (this as any)[name] = other;
+  }
+  sum(): number {
+    let s = 0;
+    for (let i = 0; i < 16; i++) s += this.at(i);
+    return s;
+  }
+}
+const nm = new Named();
+const firstSum = nm.sum();
+nm.replace(process.argv.length > 100 ? "other" : "data", [9, 9]);
+console.log("named", firstSum, nm.sum(), nm.at(1), nm.at(2));
+
+// Negative controls. A stored `undefined` is a present element: `??`
+// applies to it.
+class Undef {
+  v: (number | undefined)[] = new Array(8).fill(4);
+  at(i: number): number {
+    return this.v[i] ?? 77;
+  }
+  run(): string {
+    const a = this.at(1);
+    this.v[1] = undefined;
+    return [a, this.at(1), this.at(2), typeof this.v[1]].join(",");
+  }
+}
+console.log("undef", new Undef().run());
+
+// A field that also holds `null`.
+class Maybe {
+  v: number[] | null = null;
+  at(i: number): number {
+    return this.v === null ? -5 : (this.v[i] ?? -6);
+  }
+  fill(): void {
+    this.v = new Array(4).fill(8);
+  }
+}
+const mb = new Maybe();
+const beforeFill = mb.at(1);
+mb.fill();
+console.log("maybe", beforeFill, mb.at(1), mb.at(4));
+
+// Holes: no fused fill, a sparse store past the end, `delete`, a length
+// store.
+class Holes {
+  bare: number[] = new Array(8);
+  sparse: number[] = new Array(8).fill(1);
+  gone: number[] = new Array(8).fill(2);
+  cut: number[] = new Array(8).fill(3);
+  bareAt(i: number): number {
+    return this.bare[i] ?? -1;
+  }
+  sparseAt(i: number): number {
+    return this.sparse[i] ?? -2;
+  }
+  goneAt(i: number): number {
+    return this.gone[i] ?? -3;
+  }
+  cutAt(i: number): number {
+    return this.cut[i] ?? -4;
+  }
+  run(): string {
+    const out: number[] = [];
+    this.bare[2] = 5;
+    for (let i = 0; i < 4; i++) out.push(this.bareAt(i));
+    this.sparse[20] = 6;
+    out.push(this.sparseAt(7), this.sparseAt(8), this.sparseAt(20), this.sparse.length);
+    delete this.gone[3];
+    out.push(this.goneAt(2), this.goneAt(3), this.goneAt(4));
+    this.cut.length = 2;
+    out.push(this.cutAt(1), this.cutAt(2), this.cutAt(7), this.cut.length);
+    return out.join(",");
+  }
+}
+console.log("holes", new Holes().run());
+
+// A deleted field and a subclass that overrides the reader.
+class Hard {
+  v: number[] = new Array(4).fill(6);
+  at(i: number): number {
+    const a = this.v;
+    return a === undefined ? -9 : (a[i] ?? -8);
+  }
+}
+const hd = new Hard();
+const beforeDelete = hd.at(1);
+delete (hd as any).v;
+console.log("hard", beforeDelete, hd.at(1));
+
+class Base {
+  v: number[] = new Array(4).fill(1);
+  at(i: number): number {
+    return this.v[i] ?? 0;
+  }
+}
+class Derived extends Base {
+  at(i: number): number {
+    return 40 + (this.v[i] ?? 0);
+  }
+}
+const objs: Base[] = [new Base(), new Derived()];
+let poly = 0;
+for (let i = 0; i < 8; i++) poly += objs[i & 1]!.at(i & 3);
+console.log("poly", poly);
+
+// Elements that are not Numbers behind the reader.
+class Words {
+  w: string[] = new Array(4).fill("a");
+  at(i: number): string {
+    return this.w[i] ?? "none";
+  }
+  get(i: number): string {
+    return this.w[i];
+  }
+}
+const ws = new Words();
+ws.w[2] = "b";
+console.log("words", ws.at(0), ws.at(2), ws.at(4), ws.get(1), ws.get(2), ws.get(9));
+
+// A fraction, NaN and -0 as the key.
+console.log("keys", b.at(0.5), b.at(NaN), b.at(-0), b.at(127), b.at(128));
diff --git a/tests/parity/language/array/test_array_reps_fields_gc.ts b/tests/parity/language/array/test_array_reps_fields_gc.ts
new file mode 100644
index 00000000000..8b2f1e87742
--- /dev/null
+++ b/tests/parity/language/array/test_array_reps_fields_gc.ts
@@ -0,0 +1,25 @@
+// DESIGN-p4l1 §5.4 fixture 13: a loop that allocates and reads a field-held
+// array 10^5 times, so collections run between the field load and the
+// element load of other iterations. Run under PERRY_GC_MOVING_LOOP_POLLS=1
+// and a seeded PERRY_GC_STRESS as well.
+
+class Grid {
+  cells: number[] = new Array(64).fill(0);
+  log: string[] = [];
+  at(i: number): number {
+    return this.cells[i] ?? 0;
+  }
+  run(n: number): number {
+    let s = 0;
+    for (let i = 0; i < n; i++) {
+      const k = i & 63;
+      this.cells[k] = (i * 31) % 97;
+      const pair = { a: this.at(k), b: this.cells[(k + 1) & 63] ?? 0 };
+      if ((i & 1023) === 0) this.log.push("s" + pair.a);
+      s = (s + pair.a * 3 + pair.b + this.at((k * 5) & 63)) % 1000003;
+    }
+    return s;
+  }
+}
+const g = new Grid();
+console.log(g.run(100000), g.log.length, g.log[3], g.at(63), g.at(64));
diff --git a/tests/parity/language/array/test_array_reps_fields_growth.ts b/tests/parity/language/array/test_array_reps_fields_growth.ts
new file mode 100644
index 00000000000..d47ef6de0aa
--- /dev/null
+++ b/tests/parity/language/array/test_array_reps_fields_growth.ts
@@ -0,0 +1,41 @@
+// DESIGN-p4l1 §5.4 fixture 14: a loop reads `this.f[i]` and pushes to
+// `this.f`, so the storage moves while the loop runs; and an index store
+// past the capacity grows a field-held array that is read before and
+// after.
+
+class Queue {
+  items: number[] = [1, 2, 3];
+  at(i: number): number {
+    return this.items[i] ?? -1;
+  }
+  run(n: number): number {
+    let s = 0;
+    for (let i = 0; i < n; i++) {
+      s += this.items[i]! + this.at(i);
+      this.items.push(this.items[i]! * 2 + 1);
+    }
+    return s % 1000000007;
+  }
+}
+const q = new Queue();
+console.log(q.run(40) > 0, q.items.length, q.at(0), q.at(42), q.at(43), q.at(-1));
+
+class Board {
+  board: number[] = new Array(128).fill(0);
+  at(sq: number): number {
+    return this.board[sq] ?? 0;
+  }
+  sum(): number {
+    let s = 0;
+    for (let i = 0; i < 128; i++) s += this.at(i);
+    return s;
+  }
+}
+const b = new Board();
+for (let i = 0; i < 128; i++) b.board[i] = i;
+const before = b.sum();
+// One store far past the capacity: the storage is reallocated.
+b.board[5000] = 7;
+let after = 0;
+for (let r = 0; r < 100; r++) after += b.sum();
+console.log(before, after, b.at(5), b.at(127), b.at(128), b.at(5000), b.board.length);