Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

gcd.mlw 3.15 KB
Newer Older
1 2 3 4

(* Greatest common divisor, using the Euclidean algorithm *)

module EuclideanAlgorithm
5

6
  use import mach.int.Int
7
  use import number.Gcd
8

9
  let rec euclid (u v: int) : int
10
    variant  { v }
11
    requires { u >= 0 /\ v >= 0 }
12 13 14
    ensures  { result = gcd u v }
  =
    if v = 0 then
15 16
      u
    else
17
      euclid v (u % v)
18

19
end
20 21 22

module EuclideanAlgorithmIterative

23
  use import mach.int.Int
24 25 26
  use import ref.Ref
  use import number.Gcd

27
  let euclid (u0 v0: int) : int
28 29 30 31 32 33 34 35 36 37
    requires { u0 >= 0 /\ v0 >= 0 }
    ensures  { result = gcd u0 v0 }
  =
    let u = ref u0 in
    let v = ref v0 in
    while !v <> 0 do
      invariant { !u >= 0 /\ !v >= 0 }
      invariant { gcd !u !v = gcd u0 v0 }
      variant   { !v }
      let tmp = !v in
38
      v := !u % !v;
39 40 41 42 43
      u := tmp
    done;
    !u

end
44 45 46

module BinaryGcd

47
  use import mach.int.Int
48 49 50 51 52 53 54 55
  use import int.Lex2
  use import number.Parity
  use import number.Gcd

  lemma even1: forall n: int. 0 <= n -> even n <-> n = 2 * div n 2
  lemma odd1: forall n: int. 0 <= n -> not (even n) <-> n = 2 * div n 2 + 1
  lemma div_nonneg: forall n: int. 0 <= n -> 0 <= div n 2

56 57
  use number.Coprime

58 59 60 61 62 63 64 65
  lemma gcd_even_even: forall u v: int. 0 <= v -> 0 <= u ->
    gcd (2 * u) (2 * v) = 2 * gcd u v
  lemma gcd_even_odd: forall u v: int. 0 <= v -> 0 <= u ->
    gcd (2 * u) (2 * v + 1) = gcd u (2 * v + 1)
  lemma gcd_even_odd2: forall u v: int. 0 <= v -> 0 <= u ->
    even u -> odd v -> gcd u v = gcd (div u 2) v
  lemma odd_odd_div2: forall u v: int. 0 <= v -> 0 <= u ->
    div ((2*u+1) - (2*v+1)) 2 = u - v
66 67 68 69 70 71 72

  let lemma gcd_odd_odd (u v: int)
    requires { 0 <= v <= u }
    ensures { gcd (2 * u + 1) (2 * v + 1) = gcd (u - v) (2 * v + 1) }
  = assert { gcd (2 * u + 1) (2 * v + 1) =
             gcd ((2*u+1) - 1*(2*v+1)) (2 * v + 1) }

73
  lemma gcd_odd_odd2: forall u v: int. 0 <= v <= u ->
74 75 76 77 78 79 80 81 82
    odd u -> odd v -> gcd u v = gcd (div (u - v) 2) v

  let rec binary_gcd (u v: int) : int
    variant  { (v, u) with lex }
    requires { u >= 0 /\ v >= 0 }
    ensures  { result = gcd u v }
  =
    if v > u then binary_gcd v u else
    if v = 0 then u else
83 84 85 86 87 88
    if mod u 2 = 0 then
      if mod u 2 = 0 then 2 * binary_gcd (u / 2) (v / 2)
                     else binary_gcd (u / 2) v
      else
      if mod u 2 = 0 then binary_gcd u (v / 2)
                     else binary_gcd ((u - v) / 2) v
89 90

end
91

92 93 94
(** With machine integers.
    Note that we assume parameters u, v to be nonnegative.
    Otherwise, for u = v = min_int, the gcd could not be represented. *)
95

96
(* does not work with extraction driver ocaml64
97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112
module EuclideanAlgorithm31

  use import mach.int.Int31
  use import number.Gcd

  let rec euclid (u v: int31) : int31
    variant  { to_int v }
    requires { to_int u >= 0 /\ to_int v >= 0 }
    ensures  { to_int result = gcd (to_int u) (to_int v) }
  =
    if Int31.eq v (of_int 0) then
      u
    else
      euclid v (u % v)

end
113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130
*)

module EuclideanAlgorithm63

  use import mach.int.Int63
  use import number.Gcd

  let rec euclid (u v: int63) : int63
    variant  { to_int v }
    requires { to_int u >= 0 /\ to_int v >= 0 }
    ensures  { to_int result = gcd (to_int u) (to_int v) }
  =
    if Int63.eq v (of_int 0) then
      u
    else
      euclid v (u % v)

end