RSAVerify — Computable L1 Pipeline for Reflection-Based Verification

Computable pipeline that mirrors the ℝ L0→S1→L1 computation in RSAConfig. Used by native_decide to verify RSA predictions.

The pipeline tracks lower and upper bounds as separate ℚ values, avoiding Finset.toList (which is noncomputable). All summation uses Finset.sum over ℚ, which is computable.

For beliefBased (α ∈ ℕ), bounds are exact: lo = hi throughout. For patterns with exp/log, bounds have width from Padé approximation.

structure RSA.Verify.Bounds : Type

Lower and upper bounds for a nonneg real value. No validity proof (lo ≤ hi) — this is enforced by construction and verified in the soundness theorem.

• lo : ℚ
• hi : ℚ

def RSA.Verify.instReprBounds.repr : Bounds → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance RSA.Verify.instReprBounds : Repr Bounds

Equations

• RSA.Verify.instReprBounds = { reprPrec := RSA.Verify.instReprBounds.repr }

def RSA.Verify.instDecidableEqBounds.decEq (x✝ x✝¹ : Bounds) : Decidable (x✝ = x✝¹)

Equations

• RSA.Verify.instDecidableEqBounds.decEq { lo := a, hi := a_1 } { lo := b, hi := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

instance RSA.Verify.instDecidableEqBounds : DecidableEq Bounds

Equations

• RSA.Verify.instDecidableEqBounds = RSA.Verify.instDecidableEqBounds.decEq

instance RSA.Verify.instInhabitedBounds : Inhabited Bounds

Equations

• RSA.Verify.instInhabitedBounds = { default := { lo := 0, hi := 0 } }

def RSA.Verify.Bounds.exact (q : ℚ) : Bounds

Equations

• RSA.Verify.Bounds.exact q = { lo := q, hi := q }

def RSA.Verify.Bounds.zero : Bounds

Equations

• RSA.Verify.Bounds.zero = { lo := 0, hi := 0 }

def RSA.Verify.Bounds.add (a b : Bounds) : Bounds

Equations

• a.add b = { lo := a.lo + b.lo, hi := a.hi + b.hi }

def RSA.Verify.Bounds.sub (a b : Bounds) : Bounds

Interval subtraction: [a.lo - b.hi, a.hi - b.lo].

Equations

• a.sub b = { lo := a.lo - b.hi, hi := a.hi - b.lo }

def RSA.Verify.Bounds.scaleNonneg (q : ℚ) (b : Bounds) : Bounds

Multiply nonneg bounds by a nonneg scalar.

Equations

• RSA.Verify.Bounds.scaleNonneg q b = { lo := q * b.lo, hi := q * b.hi }

def RSA.Verify.Bounds.mul (a b : Bounds) : Bounds

Multiply two bounds (4-corner for general, nonneg shortcut when possible).

Equations

• One or more equations did not get rendered due to their size.

def RSA.Verify.Bounds.divPos (a b : Bounds) : Bounds

Divide nonneg numerator by positive denominator.

Equations

• One or more equations did not get rendered due to their size.

def RSA.Verify.expBounds (q : ℚ) : Bounds

Bounds for exp(q) via Padé approximation.

Equations

• RSA.Verify.expBounds q = { lo := (Linglib.Interval.expPoint q).lo, hi := (Linglib.Interval.expPoint q).hi }

def RSA.Verify.expIntervalBounds (b : Bounds) : Bounds

Bounds for exp over an interval [lo, hi]. Uses monotonicity: exp(lo) ≤ exp(x) ≤ exp(hi).

Equations

• RSA.Verify.expIntervalBounds b = { lo := (Linglib.Interval.expPoint b.lo).lo, hi := (Linglib.Interval.expPoint b.hi).hi }

def RSA.Verify.powBounds (p α : ℚ) : Bounds

Bounds for p^α where p ≥ 0. Exact when α is a natural number (α.den = 1), interval via exp(α·log(p)) otherwise.

Equations

• One or more equations did not get rendered due to their size.

def RSA.Verify.computeL0Rat {U : Type u_1} {W : Type u_2} {L : Type u_3} [Fintype W] (meaning : L → U → W → ℚ) (l : L) (u : U) (w : W) : ℚ

Compute L0 policy as exact ℚ: meaning(l,u,w) / Σ_w' meaning(l,u,w'). Returns 0 if total is 0 (no world has nonzero meaning).

Equations

• RSA.Verify.computeL0Rat meaning l u w = if Finset.univ.sum (meaning l u) = 0 then 0 else meaning l u w / Finset.univ.sum (meaning l u)

def RSA.Verify.computeS1ScoreBounds {U : Type u_1} {W : Type u_2} {L : Type u_3} [Fintype W] [DecidableEq W] [DecidableEq L] (spec : S1ScoreSpec U W L) (meaning : L → U → W → ℚ) (α : ℚ) (l : L) (w : W) (u : U) (qudProj : Option (W → L → ℕ) := none) : Bounds

Compute S1 score bounds, dispatching on the scoring specification.

For beliefBased: exact (lo = hi = L0^α). For beliefAction: algebraic rewrite exp(α·(log x - c)) = x^α · exp(-α·c), exact base + Padé discount. For actionBased: Padé exp directly. For beliefWeighted: full interval pipeline.

The qudProj parameter applies QUD projection to L0 before scoring: when some project, L0(w|u) becomes Σ_{w'∼w} L0(w'|u).

Equations

• One or more equations did not get rendered due to their size.
• RSA.Verify.computeS1ScoreBounds RSA.S1ScoreSpec.beliefBased meaning α l w u = RSA.Verify.powBounds (RSA.Verify.computeL0Rat meaning l u w) α
• RSA.Verify.computeS1ScoreBounds RSA.S1ScoreSpec.beliefBased meaning α l w u (some project) = RSA.Verify.powBounds ({w' : W | project w' l = project w l}.sum (RSA.Verify.computeL0Rat meaning l u)) α
• RSA.Verify.computeS1ScoreBounds (RSA.S1ScoreSpec.actionBased cost) meaning α l w u = RSA.Verify.expBounds (α * (RSA.Verify.computeL0Rat meaning l u w - cost u))

def RSA.Verify.computeS1PolicyBounds {U : Type u_1} {W : Type u_2} {L : Type u_3} [Fintype U] [Fintype W] [DecidableEq U] [DecidableEq W] [DecidableEq L] (spec : S1ScoreSpec U W L) (meaning : L → U → W → ℚ) (α : ℚ) (l : L) (w : W) (u : U) (qudProj : Option (W → L → ℕ) := none) : Bounds

Compute S1 policy bounds: score(u) / Σ_{u'} score(u'). Uses Finset.sum for totals (computable over ℚ).

Equations

• One or more equations did not get rendered due to their size.

def RSA.Verify.computeL1ScoreBounds {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] [DecidableEq U] [DecidableEq W] (d : RSAConfigData U W) (u : U) (w : W) : Bounds

Compute L1 unnormalized score bounds: L1_score(u,w) = worldPrior(w) · Σ_l latentPrior(w,l) · S1_policy(l,w,u).

Uses Finset.sum over latent variables (computable over ℚ).

Equations

• One or more equations did not get rendered due to their size.

Reduction 1: Zero-term pruning

For belief-gated specs (beliefBased, beliefAction, weightedBeliefAction, combinedUtility with logActive), S1_score(l,w,u) = 0 when meaning(l,u,w) = 0. The latent state's contribution to L1 is 0 · latentPrior = 0, so we skip the expensive S1 policy computation entirely.

For Nouwen2024 with 100 latent states, ~76% are pruned per (u,w) pair.

def RSA.Verify.canPruneLatent {U : Type u_1} {W : Type u_2} {L : Type u_3} [Fintype W] (spec : S1ScoreSpec U W L) (meaning : L → U → W → ℚ) (l : L) (u : U) (w : W) (qudProj : Option (W → L → ℕ)) : Bool

Check if a latent state contributes zero to L1 score for a given (u, w). Sound when qudProj = none: meaning = 0 ⟹ L0 = 0 ⟹ S1_score = 0 for belief-gated specs.

Equations

• RSA.Verify.canPruneLatent RSA.S1ScoreSpec.beliefBased meaning l u w qudProj = if qudProj.isSome = true then false else if meaning l u w = 0 then true else false
• RSA.Verify.canPruneLatent (RSA.S1ScoreSpec.beliefAction cost) meaning l u w qudProj = if qudProj.isSome = true then false else if meaning l u w = 0 then true else false
• RSA.Verify.canPruneLatent (RSA.S1ScoreSpec.weightedBeliefAction infWeight bonus) meaning l u w qudProj = if qudProj.isSome = true then false else if meaning l u w = 0 then true else false
• RSA.Verify.canPruneLatent (RSA.S1ScoreSpec.combinedUtility terms logActive) meaning l u w qudProj = if qudProj.isSome = true then false else if meaning l u w = 0 then logActive l else false
• RSA.Verify.canPruneLatent (RSA.S1ScoreSpec.actionBased cost) meaning l u w qudProj = if qudProj.isSome = true then false else if meaning l u w = 0 then false else false
• RSA.Verify.canPruneLatent (RSA.S1ScoreSpec.beliefWeighted belief quality) meaning l u w qudProj = if qudProj.isSome = true then false else if meaning l u w = 0 then false else false

Reduction 2: Shared exp-cost bounds

For beliefAction, S1_score(l,w,u) = L0^α · exp(-α·cost(u)). The exp factor depends only on (α, cost(u)), not on (l, w). Precompute it once per utterance and reuse across all latent states.

Saves O(|L| × |W|) redundant Padé evaluations → O(|U|) total.

def RSA.Verify.precomputeExpCost {U : Type u_1} {W : Type u_2} {L : Type u_3} [Fintype U] (spec : S1ScoreSpec U W L) (α : ℚ) : U → Bounds

Precompute exp(-α · cost(u)) bounds for each utterance.

Equations

• RSA.Verify.precomputeExpCost (RSA.S1ScoreSpec.beliefAction cost) α = fun (u : U) => RSA.Verify.expBounds (-(α * cost u))
• RSA.Verify.precomputeExpCost spec α = fun (x : U) => RSA.Verify.Bounds.exact 1

def RSA.Verify.computeS1ScoreBoundsCached {U : Type u_1} {W : Type u_2} {L : Type u_3} [Fintype W] [DecidableEq W] [DecidableEq L] (spec : S1ScoreSpec U W L) (meaning : L → U → W → ℚ) (α : ℚ) (l : L) (w : W) (u : U) (kCache : U → Bounds) (qudProj : Option (W → L → ℕ) := none) : Bounds

Compute S1 score bounds using precomputed exp-cost bounds.

Equations

• One or more equations did not get rendered due to their size.
• RSA.Verify.computeS1ScoreBoundsCached RSA.S1ScoreSpec.beliefBased meaning α l w u kCache = RSA.Verify.powBounds (RSA.Verify.computeL0Rat meaning l u w) α
• RSA.Verify.computeS1ScoreBoundsCached spec meaning α l w u kCache qudProj = RSA.Verify.computeS1ScoreBounds spec meaning α l w u qudProj

def RSA.Verify.computeS1PolicyBoundsCached {U : Type u_1} {W : Type u_2} {L : Type u_3} [Fintype U] [Fintype W] [DecidableEq U] [DecidableEq W] [DecidableEq L] (spec : S1ScoreSpec U W L) (meaning : L → U → W → ℚ) (α : ℚ) (l : L) (w : W) (u : U) (kCache : U → Bounds) (qudProj : Option (W → L → ℕ) := none) : Bounds

Compute S1 policy bounds with shared exp-cost cache.

Equations

• One or more equations did not get rendered due to their size.

Reduction 3: Same-utterance K(u) cancellation

For same-utterance L1 comparisons (L1 u w₁ > L1 u w₂), K(u) = exp(-α·c(u)) appears as a common positive factor in both L1 scores:

L1_score(u,w) = K(u) · worldPrior(w) · Σ_l lp(w,l) · L0^α / D(l,w)

Since K(u) > 0, it cancels. We compute L1 scores with K(u) = 1 for the target utterance's numerator (the denominator D(l,w) still uses all K values). This eliminates one interval multiplication per side, tightening bounds.

def RSA.Verify.computeS1PolicyBoundsNoK {U : Type u_1} {W : Type u_2} {L : Type u_3} [Fintype U] [Fintype W] [DecidableEq U] [DecidableEq W] [DecidableEq L] (spec : S1ScoreSpec U W L) (meaning : L → U → W → ℚ) (α : ℚ) (l : L) (w : W) (u : U) (kCache : U → Bounds) (qudProj : Option (W → L → ℕ) := none) : Bounds

S1 score with K(u) factored out: score_noK = L0^α (no exp factor). The S1 denominator still uses full scores (with K for all utterances).

Equations

• One or more equations did not get rendered due to their size.
• RSA.Verify.computeS1PolicyBoundsNoK spec meaning α l w u kCache qudProj = RSA.Verify.computeS1PolicyBoundsCached spec meaning α l w u kCache qudProj

Reduction 5: L0 normalization caching

computeL0Rat recomputes Σ_w' meaning(l,u,w') for each world w. This total depends on (l,u) but not w, so caching it saves O(|W|) additions per call. We provide a row-based L0 computation that computes the total once.

def RSA.Verify.computeL0Row {U : Type u_1} {W : Type u_2} [Fintype W] (meaning : U → W → ℚ) (u : U) : (W → ℚ) × ℚ

Compute L0 policy for all worlds at (l, u), caching the normalization total. Returns (lookup_fn, total).

Equations

• RSA.Verify.computeL0Row meaning u = if Finset.univ.sum (meaning u) = 0 then (fun (x : W) => 0, 0) else (fun (w : W) => meaning u w / Finset.univ.sum (meaning u), Finset.univ.sum (meaning u))

def RSA.Verify.computeL1ScoreBoundsOpt {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] [DecidableEq U] [DecidableEq W] (d : RSAConfigData U W) (u : U) (w : W) (cancelK : Bool := false) : Bounds

Optimized L1 score bounds with all algebraic reductions:

1. Zero-term pruning (skip latent states where meaning = 0)
2. Shared exp bounds (precompute exp(-α·cost) once per utterance)
3. K(u) cancellation (factor out common exp factor for same-u comparisons)
4. L0 total caching (shared within S1 policy computation)

Equations

• One or more equations did not get rendered due to their size.

def RSA.Verify.checkL1ScoreGt {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] [DecidableEq U] [DecidableEq W] (d : RSAConfigData U W) (u₁ : U) (w₁ : W) (u₂ : U) (w₂ : W) : Bool

Check that L1 score for (u₁,w₁) is strictly greater than for (u₂,w₂). Uses bound separation: score₂.hi < score₁.lo.

Equations

• RSA.Verify.checkL1ScoreGt d u₁ w₁ u₂ w₂ = decide ((RSA.Verify.computeL1ScoreBounds d u₂ w₂).hi < (RSA.Verify.computeL1ScoreBounds d u₁ w₁).lo)

def RSA.Verify.checkL1ScoreGtOpt {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] [DecidableEq U] [DecidableEq W] (d : RSAConfigData U W) (u₁ : U) (w₁ : W) (u₂ : U) (w₂ : W) : Bool

Optimized version of checkL1ScoreGt with algebraic reductions: zero-term pruning, shared exp bounds, K(u) cancellation.

For same-utterance comparisons (u₁ = u₂), uses K(u) cancellation for tighter bounds.

Equations

• RSA.Verify.checkL1ScoreGtOpt d u₁ w₁ u₂ w₂ = decide ((RSA.Verify.computeL1ScoreBoundsOpt d u₂ w₂ (u₁ == u₂)).hi < (RSA.Verify.computeL1ScoreBoundsOpt d u₁ w₁ (u₁ == u₂)).lo)

def RSA.Verify.checkL1ScoreNotGt {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] [DecidableEq U] [DecidableEq W] (d : RSAConfigData U W) (u₁ : U) (w₁ : W) (u₂ : U) (w₂ : W) : Bool

Check that L1 score for (u₁,w₁) is NOT strictly greater than for (u₂,w₂). Uses: score₁.hi ≤ score₂.lo (real value ≤ upper bound ≤ lower bound ≤ real value).

Equations

• RSA.Verify.checkL1ScoreNotGt d u₁ w₁ u₂ w₂ = decide ((RSA.Verify.computeL1ScoreBounds d u₁ w₁).hi ≤ (RSA.Verify.computeL1ScoreBounds d u₂ w₂).lo)

def RSA.Verify.checkL1ScoreNotGtOpt {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] [DecidableEq U] [DecidableEq W] (d : RSAConfigData U W) (u₁ : U) (w₁ : W) (u₂ : U) (w₂ : W) : Bool

Optimized version of checkL1ScoreNotGt with algebraic reductions.

Equations

• RSA.Verify.checkL1ScoreNotGtOpt d u₁ w₁ u₂ w₂ = decide ((RSA.Verify.computeL1ScoreBoundsOpt d u₁ w₁ (u₁ == u₂)).hi ≤ (RSA.Verify.computeL1ScoreBoundsOpt d u₂ w₂ (u₁ == u₂)).lo)

def RSA.Verify.trySymbolicS1ScoreGt {U : Type u_1} {W : Type u_2} {L : Type u_3} [Fintype W] [DecidableEq W] [DecidableEq L] (spec : S1ScoreSpec U W L) (meaning : L → U → W → ℚ) (α : ℚ) (l : L) (w : W) (u₁ u₂ : U) (qudProj : Option (W → L → ℕ) := none) : Bool

Symbolic S1 score comparison: score(u₁) > score(u₂) via algebraic identity.

Reduces S1 score comparisons to exact ℚ arithmetic by exploiting the structure of each scoring spec, bypassing interval approximation entirely.

• actionBased: exp is monotone, so compare arguments directly (ℚ exact).
• beliefAction: factor as L0^α · exp(-α·c), then:
  • Equal L0: cancel L0^α → cost comparison (ℚ exact)
  • Equal cost: cancel exp → L0 comparison (ℚ exact)
  • Dominance: L0₁ ≥ L0₂ ∧ c₁ ≤ c₂ with one strict → score₁ > score₂
  • General: compare L0₁^α / L0₂^α against expBounds(α·(c₁-c₂))
• beliefBased: already exact (no exp), no shortcut needed.
• beliefWeighted: no simple shortcut, fall back to intervals.

The qudProj parameter applies QUD projection to L0 values.

Equations

• One or more equations did not get rendered due to their size.
• RSA.Verify.trySymbolicS1ScoreGt spec meaning α l w u₁ u₂ qudProj = false

def RSA.Verify.trySymbolicS1ScoreNotGt {U : Type u_1} {W : Type u_2} {L : Type u_3} [Fintype W] [DecidableEq W] [DecidableEq L] (spec : S1ScoreSpec U W L) (meaning : L → U → W → ℚ) (α : ℚ) (l : L) (w : W) (u₁ u₂ : U) (qudProj : Option (W → L → ℕ) := none) : Bool

Symbolic S1 score comparison: ¬(score(u₁) > score(u₂)).

Equations

• One or more equations did not get rendered due to their size.
• RSA.Verify.trySymbolicS1ScoreNotGt spec meaning α l w u₁ u₂ qudProj = false

def RSA.Verify.checkS1PolicyGt {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] [DecidableEq U] [DecidableEq W] (d : RSAConfigData U W) (l : d.Latent) (w : W) (u₁ u₂ : U) : Bool

Check that S1 score for (l,w,u₁) is strictly greater than for (l,w,u₂). Same (l,w) → same denominator → score ordering = policy ordering.

Tries symbolic comparison first (exact ℚ, no interval approximation), then falls back to interval bound separation.

Equations

• One or more equations did not get rendered due to their size.

def RSA.Verify.checkS1PolicyNotGt {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] [DecidableEq U] [DecidableEq W] (d : RSAConfigData U W) (l : d.Latent) (w : W) (u₁ u₂ : U) : Bool

Check that S1 score for (l,w,u₁) is NOT strictly greater than for (l,w,u₂).

Tries symbolic comparison first, then falls back to interval bounds.

Equations

• One or more equations did not get rendered due to their size.

def RSA.Verify.roundDownQ (q : ℚ) (n : ℕ) : ℚ

Round q down (toward -∞) to nearest multiple of 1/2^n. Guarantees roundDownQ q n ≤ q.

Equations

• RSA.Verify.roundDownQ q n = ↑⌊q * ↑(2 ^ n)⌋ / ↑(2 ^ n)

def RSA.Verify.roundUpQ (q : ℚ) (n : ℕ) : ℚ

Round q up (toward +∞) to nearest multiple of 1/2^n. Guarantees q ≤ roundUpQ q n.

Equations

• RSA.Verify.roundUpQ q n = ↑⌈q * ↑(2 ^ n)⌉ / ↑(2 ^ n)

def RSA.Verify.Bounds.coarsen (b : Bounds) (n : ℕ) : Bounds

Coarsen bounds to denominators of at most 2^n. Widens the interval slightly: lo rounds down, hi rounds up. This prevents denominator explosion in nested interval pipelines (e.g., logPoint on the output of divPos on S1 pipeline results).

Equations

• b.coarsen n = { lo := RSA.Verify.roundDownQ b.lo n, hi := RSA.Verify.roundUpQ b.hi n }

def RSA.Verify.logBounds (b : Bounds) : Bounds

Bounds for log(b) where b is a nonneg Bounds interval. Uses logPoint on lo/hi (monotonicity of log). Returns [log(lo), log(hi)] when lo > 0; [-1000, log(hi)] when lo ≤ 0 (as a safe fallback).

Equations

• One or more equations did not get rendered due to their size.

def RSA.Verify.computeL1NormBounds {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] [DecidableEq U] [DecidableEq W] (d : RSAConfigData U W) (u : U) : Bounds

Compute L1 normalization constant bounds: Σ_{w,l} prior(w) · prior(w,l) · S1(l,w,u).

Equations

• One or more equations did not get rendered due to their size.

def RSA.Verify.computeL1StateMarginalBounds {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] [DecidableEq U] [DecidableEq W] (d : RSAConfigData U W) (u : U) (w : W) : Bounds

Compute L1 state marginal bounds: P_L1(w|u) = L1_score(u,w) / Σ_w' L1_score(u,w'). Returns bounds for the marginal probability of state w given utterance u.

Equations

• RSA.Verify.computeL1StateMarginalBounds d u w = (RSA.Verify.computeL1ScoreBounds d u w).divPos (RSA.Verify.computeL1NormBounds d u)

def RSA.Verify.computeL1LatentMarginalBounds {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] [DecidableEq U] [DecidableEq W] (d : RSAConfigData U W) (u : U) (l : d.Latent) : Bounds

Compute L1 latent marginal bounds: P_L1(l|u) = Σ_w prior(w)·prior(w,l)·S1(l,w,u) / norm.

Equations

• One or more equations did not get rendered due to their size.

def RSA.Verify.computeS2ScoreBounds {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] [DecidableEq U] [DecidableEq W] (d : RSAConfigData U W) (spec : S2ScoreSpec U W d.Latent) (w : W) (u : U) : Bounds

Compute S2 score bounds, dispatching on S2ScoreSpec.

For utilityMaximizing: computes L1 marginals inline, evaluating S1 policies once and reusing the results for all terms.

Equations

• One or more equations did not get rendered due to their size.
• RSA.Verify.computeS2ScoreBounds d RSA.S2ScoreSpec.endorsement w u = RSA.Verify.computeL1ScoreBounds d u w

def RSA.Verify.checkS2ScoreGt {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] [DecidableEq U] [DecidableEq W] (d : RSAConfigData U W) (w : W) (u₁ u₂ : U) : Bool

Check that S2 score for (w,u₁) is strictly greater than for (w,u₂). For utilityMaximizing, compares utilities directly (exp is monotone).

Equations

• One or more equations did not get rendered due to their size.