Add in-place variants for wmpn_[lr]shift

examples/multiprecision/logical.mlw

@@ -141,8 +141,7 @@ module Logical
       invariant { 0 <= !i < sz }
       invariant { radix * value_sub (pelts r) (r.offset + 1 + !i) (r.offset + sz)
                   + (power radix (sz - !i)) * retval + !high
-                = value !xp (sz - !i)
-                  * (power 2 (cnt)) }
+                = value !xp (sz - !i) * (power 2 (cnt)) }
       invariant { (!rp).offset = r.offset + !i }
       invariant { (!xp).offset = x.offset + !i }
       invariant { plength !rp = plength r }
@@ -341,4 +340,186 @@ module Logical
            };
     retval
 
+  let wmpn_lshift_in_place (x:t) (sz:int32) (cnt:limb) : limb
+    requires { 0 < cnt < Limb.length }
+    requires { valid x sz }
+    requires { 0 < sz }
+    ensures  { value x sz + (power radix sz) * result =
+               value (old x) sz * power 2 cnt }
+  =
+    label Start in
+    let msb = Int32.(-) sz 1 in
+    let xp = ref (C.incr x msb) in
+    let ghost ox = { x } in
+    let ghost oxp = ref (C.incr ox msb) in
+    let high = ref (Limb.of_int 0) in
+    let low = ref (C.get !xp) in
+    let i = ref msb in
+    let l, retval = lsld_ext !low cnt in
+    high := l;
+    let ghost c = power 2 (l2i cnt) in
+    while (Int32.(>) !i 0) do
+      variant   { p2i !i }
+      invariant { 0 <= !i < sz }
+      invariant { radix * value_sub (pelts x) (x.offset + !i + 1) (x.offset + sz)
+                    + (power radix (sz - !i)) * retval + !high
+                  =  value !oxp (sz - !i) * c }
+      invariant { (!xp).offset = x.offset + !i }
+      invariant { (!oxp).offset = x.offset + !i }
+      invariant { plength !oxp = plength x }
+      invariant { !oxp.min = x.min }
+      invariant { !oxp.max = x.max }
+      invariant { pelts !oxp = pelts ox }
+      invariant { plength !xp = plength x }
+      invariant { !xp.min = x.min }
+      invariant { !xp.max = x.max }
+      invariant { pelts !xp = pelts x }
+      invariant { !high <= radix - c }
+      invariant { forall j. 0 <= j <= !i ->
+                  (pelts x)[offset x + j] = (pelts ox)[offset x + j] }
+      label StartLoop in
+      xp.contents <- C.incr !xp (-1);
+      oxp.contents <- C.incr !oxp (-1);
+      low := C.get !xp;
+      let ghost olow = C.get !oxp in
+      assert { olow = !low
+               by pelts !oxp = pelts ox
+               so offset !oxp = offset x + (!i-1) = offset !xp };
+      let l, h = lsld_ext !low cnt in
+      assert { !high + h < radix };
+      let ghost v = Limb.(+) !high h in
+      value_sub_update_no_change (pelts x) (x.offset + p2i !i)
+                                           (x.offset + 1 + p2i !i)
+                                           (x.offset + p2i sz) v;
+      value_sub_update_no_change (pelts x) (x.offset + p2i !i)
+                                            x.offset (x.offset + p2i !i) v;
+      C.set_ofs !xp 1 (Limb.(+) !high h);
+      assert { value_sub (pelts x) (x.offset + !i + 1) (x.offset + sz)
+             = (value_sub (pelts x) (x.offset + !i + 1) (x.offset + sz)
+                at StartLoop) };
+      assert { (pelts x)[x.offset + !i] = !high + h };
+      high := l;
+      value_sub_head (pelts x) (x.offset + int32'int !i) (x.offset + int32'int sz);
+      value_sub_head (pelts !oxp) (x.offset + int32'int !i - 1) (x.offset + int32'int sz);
+      (* nonlinear part *)
+      assert { radix * value_sub (pelts x) (x.offset + !i) (x.offset + sz) =
+               radix * (!high at StartLoop) + radix * h
+               + (power radix 2) * value_sub (pelts x) (x.offset + !i + 1)
+                                           (x.offset + sz) };
+      assert { value !oxp (sz - !i + 1) * c
+               = radix * (value (!oxp at StartLoop) (sz - !i) * c) + !low * c
+               by value !oxp (sz - !i + 1) * c
+                  = value_sub (pelts !oxp) (x.offset + !i - 1) (x.offset + sz) * c
+                  = !low * c + radix * value_sub (pelts !oxp) (x.offset + !i) (x.offset + sz) * c
+                  = !low * c + radix * value (!oxp at StartLoop) (sz - !i) * c };
+      assert { !high + radix * h = !low * c };
+      (* proof by reflection *)
+      assert { radix * value_sub (pelts x) (x.offset + !i) (x.offset + sz)
+                 + (power radix (sz - (!i - 1))) * retval + !high
+               = value !oxp (sz - !i + 1) * c };
+      i := Int32.(-) !i 1;
+      assert { forall j. 0 <= j <= !i ->
+                  (pelts x)[offset x + j] = (pelts ox)[offset x + j]
+               by (pelts x)[offset x + j] = (pelts x at StartLoop)[offset x + j]
+                  = (pelts ox)[offset x + j] }
+    done;
+    assert { !high + radix * value_sub (pelts x) (x.offset + 1) (x.offset + sz)
+                   + (power radix sz) * retval
+                 = value (old x) sz * (power 2 cnt) };
+    value_sub_update_no_change (pelts x) x.offset (x.offset+1)
+                               (x.offset + p2i sz) !high;
+    C.set x !high;
+    value_sub_head (pelts x) x.offset (x.offset + int32'int sz);
+    assert { value x sz
+             = !high
+               + radix * value_sub (pelts x) (x.offset + 1) (x.offset + sz) };
+    retval
+
+  let wmpn_rshift_in_place (x:t) (sz:int32) (cnt:limb) : limb
+    requires { valid x sz }
+    requires { 0 < cnt < Limb.length }
+    requires { 0 < sz }
+    ensures  { result + radix * value x sz
+               = value (old x) sz * (power 2 (Limb.length - cnt)) }
+  =
+    let tnc = Limb.(-) (Limb.of_int Limb.length) cnt in
+    let msb = Int32.(-) sz 1 in
+    let xp = ref (C.incr x 0) in
+    let ghost ox = { x } in
+    let ghost oxp = ref (C.incr ox 0) in
+    let high = ref (C.get !xp) in
+    let retval, h = lsld_ext !high tnc in
+    let low = ref h in
+    let i = ref 0 in
+    let ghost c = power 2 (l2i tnc) in
+    while (Int32.(<) !i msb) do
+      variant { sz - !i }
+      invariant { 0 <= !i <= msb }
+      invariant { retval + radix * (value x !i + (power radix !i) * !low)
+                  = value ox (!i+1) * c }
+      invariant { (!xp).offset = x.offset + !i }
+      invariant { (!oxp).offset = x.offset + !i }
+      invariant { plength !oxp = plength x }
+      invariant { !oxp.min = x.min }
+      invariant { !oxp.max = x.max }
+      invariant { pelts !oxp = pelts ox }
+      invariant { plength !xp = plength x }
+      invariant { !xp.min = x.min }
+      invariant { !xp.max = x.max }
+      invariant { pelts !xp = pelts x }
+      invariant { !low < c }
+      invariant { forall j. !i <= j < sz ->
+                  (pelts x)[x.offset + j] = (pelts ox)[x.offset + j] }
+      label StartLoop in
+      xp.contents <- C.incr !xp 1;
+      oxp.contents <- C.incr !oxp 1;
+      high := C.get !xp;
+      let ghost ohigh = C.get !oxp in
+      assert { ohigh = !high
+               by pelts !oxp = pelts ox
+               so offset !oxp = offset x + (!i+1) = offset !xp
+               so ohigh = (pelts ox)[x.offset + (!i + 1)]
+                        = (pelts x)[x.offset + (!i + 1)] = !high };
+      let l, h = lsld_ext !high tnc in
+      assert { !low + l < radix };
+      let ghost v = Limb.(+) !low l in
+      value_sub_shift_no_change (pelts x) (x.offset) (p2i !i) (p2i !i) v;
+      value_sub_update_no_change (pelts x) (x.offset + p2i !i)
+                                 (x.offset + 1 + p2i !i) (x.offset + p2i sz) v;
+      C.set_ofs !xp (-1) (Limb.(+) !low l);
+      assert { value x !i = value (x at StartLoop) !i };
+      value_tail x !i;
+      value_tail ox (!i+1);
+      assert { (pelts x)[x.offset + !i] = !low + l };
+      low := h;
+      assert { value ox (!i+2) * c = value ox (!i+1) * c
+               + power radix (!i+1) * l + power radix (!i+2) * h
+               by (pelts ox)[offset ox + !i + 1] = !high
+               so value ox (!i+2) * c =
+                  (value ox (!i+1) + power radix (!i+1) * !high) * c
+               so !high * c = l + radix * h };
+      (* nonlinear part *)
+      assert { retval + radix * (value x (!i+1) + power radix (!i+1) * !low)
+               = value ox (!i+2) * c };
+      i := Int32.(+) !i 1;
+      assert { forall j. !i <= j < sz ->
+                  (pelts x)[offset x + j] = (pelts ox)[offset x + j]
+               by (pelts x)[offset x + j] = (pelts x at StartLoop)[offset x + j]
+                  = (pelts ox)[offset x + j] }
+    done;
+    label EndLoop in
+    assert { retval + radix * (value x msb + (power radix msb) * !low)
+             = value ox sz * c };
+    value_sub_tail (pelts x) x.offset (x.offset + p2i msb);
+    assert { (!xp).offset = x.offset + msb };
+    value_sub_shift_no_change (pelts x) x.offset (x.offset + p2i msb)
+                                        (x.offset + p2i msb) !low;
+    C.set_ofs x msb !low;
+    value_tail x msb;
+    assert { value x sz = value (x at EndLoop) msb + (power radix msb) * !low };
+    retval
+                                        
+             
+   
+      
 end