Boundedness of Fencode

[JasonGross]

Suppose I have that forall i, 0 < wt (S i) / wt i <= wt 1, and wt 0 = 1 (and also forall i, 0 < wt i). I want

forall v,
  Tuple.map (fun x => (Z.max 0 x) mod (wt 1)) (Positional.Fencode wt v)
  = Positional.Fencode wt v

@jadephilipoom Can you add a proof of this, or something closely related, or tell me how to prove it?

[andres-erbsen]

I confused about how this wt 1 got in there. What is the higher-level goal for which you need this?

[JasonGross]

The higher-level goal is forall v, decode b (Interp (encode b v) tt) = v or

  Positional.Fdecode (wt curve)
    (Tuple.map interpToZ
       (flat_interp_tuple
          (interpf interp_op
             (SmartPairf
                (flat_interp_untuple
                   (Tuple.map (fun v0 : Z => Op (OpConst v0) ()%expr)
                      (Positional.Fencode (wt curve) v))))))) = v

I have that wt i := 2^Qceiling((Z.log2_up m/sz)*i), so wt 1 is how I chose to access 2^Qceiling((Z.log2_up m/sz)) in a generic way.

[andres-erbsen]

Do we still need this?

[JasonGross]

This would still be nice to have; I expect that either we will need to prove this, or it'll show up as a side-condition of the redesigned mostly-in-gallina synthesis pipeline.

[JasonGross]

Yes, I still need this. I'm currently admitting

forall (sz : nat) (wt : nat -> Z) (m : positive) (v : F m),
  (forall i : nat, wt i <> 0) ->
  (forall i : nat, 0 <= wt i) ->
  (forall i : nat, wt (S i) / wt i <= wt 1%nat) ->
  @Tuple.map sz Z Z (fun x : Z => Z.max 0 x mod wt 1%nat)
    (@Positional.Fencode wt sz m (@modulo_cps) (@div_cps) v) =
  @Positional.Fencode wt sz m (@modulo_cps) (@div_cps) v

I think the primary place it shows up is in proving that we can use encoded word things to form a correct ring.

[JasonGross]

Hmmm, I also need a proof that encode is bounded by the tight bounds....

[JasonGross]

I think what I need is this:

  forall (wt : nat -> Z) (sz : nat) (m : positive),
  sz <> 0%nat
->
  (forall i : nat, wt i <> 0)
->
  (forall i : nat, 0 <= wt i)
->
  @Tuple.fieldwise nat Z sz
    (fun (x : nat) (y : Z) => 0 <= y < 2 ^ Z.log2 (wt (S x) / wt x))
    (@Tuple.from_list nat sz (seq 0 sz) (seq_length sz 0))
    (@Positional.encode wt (@modulo_cps) (@div_cps) sz (Z.pos m - 1))
->
  @Positional.eval wt sz
    (@Positional.encode wt (@modulo_cps) (@div_cps) sz (Z.pos m - 1)) = Z.pos m - 1
->
  forall v : F m,
  @Tuple.fieldwise nat Z sz
    (fun (x : nat) (y : Z) => 0 <= y < 2 ^ Z.log2 (wt (S x) / wt x))
    (@Tuple.from_list nat sz (seq 0 sz) (seq_length sz 0))
    (@Positional.Fencode wt sz m (@modulo_cps) (@div_cps) v)

I'm not 100% sure that the two preconditions on m will hold, but I hope I can let you know soon. In any case, @jadephilipoom, is this a thing you could prove?

[jadephilipoom]

Probably. I'll work on it today.

Basically, you want to use bounds on Positional.encode to prove bounds on Positional.Fencode? The point I don't understand is why this isn't trivial.

[JasonGross]

No, I (hopefully) have fieldwise bounds on Positional.encode (Z.pos m - 1). From this, I want fieldwise bounds on Positional.Fencode (m:=m) v for all v (i.e., for Positional.encode v for all 0 <= v < m). Possibly more generally, it might be nice to have a thing that says under what conditions Positional.Fencode v is fieldwise bounded in a nice way for all v.