--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on November 2014 ---
Hi, I looked into one of the unproved VCs ("secp256k1_fe_mul_inner_assert_rte_unsigned_overflow_38" attached), and I think that it is not valid. The VC is of the form: goal overflow_38: "some context" -> x_9 <= 67108863 -> x_10 <= 1073741823 -> x_9 * x_10 <= 4294967295 So, you are trying to show that "x_9 * x_10 <= 4294967295" always holds under the given context (i.e. for every possible values for x_9 and x_10). But this is not true when taking, for instance, x_9 = 67108863 and x_10 = 1073741823. Mohamed. -- Senior R&D Engineer, OCamlPro Research Associate, VALS team, LRI. http://www.iguer.info Le 04/11/2014 00:14, Gregory Maxwell a ?crit : > Greetings, I haven't used frama-c in some time, it's changed quite a > bit (and I've likely forgotten even more...) and I'm having a hard > time making progress with it at all this time around. > > I'm working on libsecp256k1 a free software cryptographic signature > library which will be used by the reference Bitcoin software; > verifying that optimized implementations are exactly correct is > critical for this application > > I'm trying to prove some simple theorems about some inner kernels used > for field arithmetic. > > To start with, I need to first prove that the code is overflow free, > under assumptions. (I don't just need to do this to make WP happy, its > required for correctness of the code. > > Here is a reduced testcase that I'm trying: > > $ cat a.c > #include <stdint.h> > /*@ requires \valid(a + (0..9)); > requires \valid(b + (0..9)); > requires (a[0] < 1073741824); > requires (a[1] < 1073741824); > requires (a[2] < 1073741824); > requires (a[3] < 1073741824); > requires (a[4] < 1073741824); > requires (a[5] < 1073741824); > requires (a[6] < 1073741824); > requires (a[7] < 1073741824); > requires (a[8] < 1073741824); > requires (a[9] < 67108864); > requires (b[0] < 1073741824); > requires (b[1] < 1073741824); > requires (b[2] < 1073741824); > requires (b[3] < 1073741824); > requires (b[4] < 1073741824); > requires (b[5] < 1073741824); > requires (b[6] < 1073741824); > requires (b[7] < 1073741824); > requires (b[8] < 1073741824); > requires (b[9] < 67108864); > */ > void static inline secp256k1_fe_mul_inner(const uint32_t *a, const > uint32_t *b, uint32_t *r) { > uint64_t d; > d = (uint64_t)a[0] * b[9] > + (uint64_t)a[1] * b[8] > + (uint64_t)a[2] * b[7] > + (uint64_t)a[3] * b[6] > + (uint64_t)a[4] * b[5] > + (uint64_t)a[5] * b[4] > + (uint64_t)a[6] * b[3] > + (uint64_t)a[7] * b[2] > + (uint64_t)a[8] * b[1] > + (uint64_t)a[9] * b[0]; > } > > I invoke frama-c with: > > frama-c -main secp256k1_fe_mul_inner -lib-entry -wp -wp-timeout 300 > -wp-par 1 -wp-rte a.c > > And get some successful proof for memory access, followed by alt-ergo > returning unknown on the overflow checks: > [...] > [wp] [Alt-Ergo] Goal > typed_secp256k1_fe_mul_inner_assert_rte_mem_access_20 : Valid > (Qed:1ms) (93ms) (74) > [wp] [Alt-Ergo] Goal > typed_secp256k1_fe_mul_inner_assert_rte_unsigned_overflow : Unknown > (Qed:4ms) (4s) > [wp] [Alt-Ergo] Goal > typed_secp256k1_fe_mul_inner_assert_rte_unsigned_overflow_2 : Unknown > (Qed:5ms) (4s) > > This is obviously free of overflows, since 1073741824*1073741824*8 + > 1073741824*67108864*2 < 2^64 > > (but the non-reduced code, is less trivial > http://0bin.net/paste/tTR7910ESfwij7Ib#pZwnZkivigEp+73f4D4yWQpXMaEWCmVFTb4XxE6vRUN > ... which is why I'm starting with just proving overflows since the > hand verifiable correctness proof in the comments assumes no > overflow). > > I'm using alt-ergo 0.95.1 and frama-c Neon-20140301 > > Any suggestions? > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -------------- next part -------------- (**************************************************************************) (* *) (* The Why3 Verification Platform / The Why3 Development Team *) (* Copyright 2010-2013 -- INRIA - CNRS - Paris-Sud University *) (* *) (* This software is distributed under the terms of the GNU Lesser *) (* General Public License version 2.1, with the special exception *) (* on linking described in file LICENSE. *) (* *) (* File modified by CEA (Commissariat ? l'?nergie atomique et aux *) (* ?nergies alternatives). *) (* *) (**************************************************************************) (* this is a prelude for Alt-Ergo*) (* this is a prelude for Alt-Ergo integer arithmetic *) (** The theory BuiltIn_ must be appended to this file*) (** The theory Bool_ must be appended to this file*) (**************************************************************************) (* *) (* The Why3 Verification Platform / The Why3 Development Team *) (* Copyright 2010-2013 -- INRIA - CNRS - Paris-Sud University *) (* *) (* This software is distributed under the terms of the GNU Lesser *) (* General Public License version 2.1, with the special exception *) (* on linking described in file LICENSE. *) (* *) (* File modified by CEA (Commissariat ? l'?nergie atomique et aux *) (* ?nergies alternatives). *) (* *) (**************************************************************************) (* this is a prelude for Alt-Ergo*) (** The theory BuiltIn_ must be appended to this file*) (** The theory Bool_ must be appended to this file*) (** The theory int_Int_ must be appended to this file*) logic abs_int : int -> int axiom abs_def : (forall x:int. ((0 <= x) -> (abs_int(x) = x))) axiom abs_def1 : (forall x:int. ((not (0 <= x)) -> (abs_int(x) = (-x)))) axiom Abs_le : (forall x:int. forall y:int. ((abs_int(x) <= y) -> ((-y) <= x))) axiom Abs_le1 : (forall x:int. forall y:int. ((abs_int(x) <= y) -> (x <= y))) axiom Abs_le2 : (forall x:int. forall y:int. ((((-y) <= x) and (x <= y)) -> (abs_int(x) <= y))) axiom Abs_pos : (forall x:int. (0 <= abs_int(x))) (**************************************************************************) (* *) (* The Why3 Verification Platform / The Why3 Development Team *) (* Copyright 2010-2013 -- INRIA - CNRS - Paris-Sud University *) (* *) (* This software is distributed under the terms of the GNU Lesser *) (* General Public License version 2.1, with the special exception *) (* on linking described in file LICENSE. *) (* *) (* File modified by CEA (Commissariat ? l'?nergie atomique et aux *) (* ?nergies alternatives). *) (* *) (**************************************************************************) (* this is a prelude for Alt-Ergo*) logic safe_comp_div: int, int -> int axiom safe_comp_div_def: forall x, y:int. x >= 0 and y > 0 -> safe_comp_div(x,y) = x / y logic safe_comp_mod: int, int -> int axiom safe_comp_mod_def: forall x, y:int. x >= 0 and y > 0 -> safe_comp_mod(x,y) = x % y (** The theory BuiltIn_ must be appended to this file*) (** The theory Bool_ must be appended to this file*) (** The theory int_Int_ must be appended to this file*) (** The theory int_Abs_ must be appended to this file*) axiom Div_bound : (forall x:int. forall y:int. (((0 <= x) and (0 < y)) -> (0 <= safe_comp_div(x,y)))) axiom Div_bound1 : (forall x:int. forall y:int. (((0 <= x) and (0 < y)) -> (safe_comp_div(x,y) <= x))) axiom Div_1 : (forall x:int. (safe_comp_div(x,1) = x)) axiom Mod_1 : (forall x:int. (safe_comp_mod(x,1) = 0)) axiom Div_inf : (forall x:int. forall y:int. (((0 <= x) and (x < y)) -> (safe_comp_div(x,y) = 0))) axiom Mod_inf : (forall x:int. forall y:int. (((0 <= x) and (x < y)) -> (safe_comp_mod(x,y) = x))) axiom Div_mult : (forall x:int. forall y:int. forall z:int [safe_comp_div(((x * y) + z),x)]. (((0 < x) and ((0 <= y) and (0 <= z))) -> (safe_comp_div(((x * y) + z),x) = (y + safe_comp_div(z,x))))) axiom Mod_mult : (forall x:int. forall y:int. forall z:int [safe_comp_mod(((x * y) + z),x)]. (((0 < x) and ((0 <= y) and (0 <= z))) -> (safe_comp_mod(((x * y) + z),x) = safe_comp_mod(z,x)))) (**************************************************************************) (* *) (* The Why3 Verification Platform / The Why3 Development Team *) (* Copyright 2010-2013 -- INRIA - CNRS - Paris-Sud University *) (* *) (* This software is distributed under the terms of the GNU Lesser *) (* General Public License version 2.1, with the special exception *) (* on linking described in file LICENSE. *) (* *) (* File modified by CEA (Commissariat ? l'?nergie atomique et aux *) (* ?nergies alternatives). *) (* *) (**************************************************************************) (* this is a prelude for Alt-Ergo*) (* this is a prelude for Alt-Ergo real arithmetic *) (** The theory BuiltIn_ must be appended to this file*) (** The theory Bool_ must be appended to this file*) axiom add_div : (forall x:real. forall y:real. forall z:real. ((not (z = 0.0)) -> (((x + y) / z) = ((x / z) + (y / z))))) axiom sub_div : (forall x:real. forall y:real. forall z:real. ((not (z = 0.0)) -> (((x - y) / z) = ((x / z) - (y / z))))) axiom neg_div : (forall x:real. forall y:real. ((not (y = 0.0)) -> (((-x) / y) = (-(x / y))))) axiom assoc_mul_div : (forall x:real. forall y:real. forall z:real. ((not (z = 0.0)) -> (((x * y) / z) = (x * (y / z))))) axiom assoc_div_mul : (forall x:real. forall y:real. forall z:real. (((not (y = 0.0)) and (not (z = 0.0))) -> (((x / y) / z) = (x / (y * z))))) axiom assoc_div_div : (forall x:real. forall y:real. forall z:real. (((not (y = 0.0)) and (not (z = 0.0))) -> ((x / (y / z)) = ((x * z) / y)))) (**************************************************************************) (* *) (* The Why3 Verification Platform / The Why3 Development Team *) (* Copyright 2010-2013 -- INRIA - CNRS - Paris-Sud University *) (* *) (* This software is distributed under the terms of the GNU Lesser *) (* General Public License version 2.1, with the special exception *) (* on linking described in file LICENSE. *) (* *) (* File modified by CEA (Commissariat ? l'?nergie atomique et aux *) (* ?nergies alternatives). *) (* *) (**************************************************************************) (* this is a prelude for Alt-Ergo*) (** The theory BuiltIn_ must be appended to this file*) (** The theory Bool_ must be appended to this file*) (** The theory real_Real_ must be appended to this file*) (**************************************************************************) (* *) (* The Why3 Verification Platform / The Why3 Development Team *) (* Copyright 2010-2013 -- INRIA - CNRS - Paris-Sud University *) (* *) (* This software is distributed under the terms of the GNU Lesser *) (* General Public License version 2.1, with the special exception *) (* on linking described in file LICENSE. *) (* *) (* File modified by CEA (Commissariat ? l'?nergie atomique et aux *) (* ?nergies alternatives). *) (* *) (**************************************************************************) (* this is a prelude for Alt-Ergo*) (** The theory BuiltIn_ must be appended to this file*) (** The theory Bool_ must be appended to this file*) (** The theory int_Int_ must be appended to this file*) (** The theory real_Real_ must be appended to this file*) logic from_int : int -> real axiom Zero : (from_int(0) = 0.0) axiom One : (from_int(1) = 1.0) axiom Add : (forall x:int. forall y:int. (from_int((x + y)) = (from_int(x) + from_int(y)))) axiom Sub : (forall x:int. forall y:int. (from_int((x - y)) = (from_int(x) - from_int(y)))) axiom Mul : (forall x:int. forall y:int. (from_int((x * y)) = (from_int(x) * from_int(y)))) axiom Neg : (forall x:int. (from_int((-x)) = (-from_int(x)))) (**************************************************************************) (* *) (* This file is part of WP plug-in of Frama-C. *) (* *) (* Copyright (C) 2007-2014 *) (* CEA (Commissariat a l'energie atomique et aux energies *) (* alternatives) *) (* *) (* you can redistribute it and/or modify it under the terms of the GNU *) (* Lesser General Public License as published by the Free Software *) (* Foundation, version 2.1. *) (* *) (* It is distributed in the hope that it will be useful, *) (* but WITHOUT ANY WARRANTY; without even the implied warranty of *) (* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) (* GNU Lesser General Public License for more details. *) (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) (* *) (**************************************************************************) (* this is a prelude for Alt-Ergo*) (** The theory BuiltIn_ must be appended to this file*) (** The theory Bool_ must be appended to this file*) (** The theory bool_Bool_ must be appended to this file*) (** The theory int_Int_ must be appended to this file*) (** The theory int_Abs_ must be appended to this file*) (** The theory int_ComputerDivision_ must be appended to this file*) (** The theory real_Real_ must be appended to this file*) (** The theory real_RealInfix_ must be appended to this file*) (** The theory real_FromInt_ must be appended to this file*) logic ite : bool, 'a, 'a -> 'a axiom ite1 : (forall p:bool. forall x:'a. forall y:'a [ite(p, x, y)]. (((p = true) and (ite(p, x, y) = x)) or ((p = false) and (ite(p, x, y) = y)))) logic eqb : 'a, 'a -> bool axiom eqb1 : (forall x:'a. forall y:'a. ((eqb(x, y) = true) -> (x = y))) axiom eqb2 : (forall x:'a. forall y:'a. ((x = y) -> (eqb(x, y) = true))) logic neqb : 'a, 'a -> bool axiom neqb1 : (forall x:'a. forall y:'a. ((neqb(x, y) = true) -> (not (x = y)))) axiom neqb2 : (forall x:'a. forall y:'a. ((not (x = y)) -> (neqb(x, y) = true))) logic zlt : int, int -> bool logic zleq : int, int -> bool axiom zlt1 : (forall x:int. forall y:int. ((zlt(x, y) = true) -> (x < y))) axiom zlt2 : (forall x:int. forall y:int. ((x < y) -> (zlt(x, y) = true))) axiom zleq1 : (forall x:int. forall y:int. ((zleq(x, y) = true) -> (x <= y))) axiom zleq2 : (forall x:int. forall y:int. ((x <= y) -> (zleq(x, y) = true))) logic rlt : real, real -> bool logic rleq : real, real -> bool axiom rlt1 : (forall x:real. forall y:real. ((rlt(x, y) = true) -> (x < y))) axiom rlt2 : (forall x:real. forall y:real. ((x < y) -> (rlt(x, y) = true))) axiom rleq1 : (forall x:real. forall y:real. ((rleq(x, y) = true) -> (x <= y))) axiom rleq2 : (forall x:real. forall y:real. ((x <= y) -> (rleq(x, y) = true))) logic truncate : real -> int function real_of_int(x: int) : real = from_int(x) axiom truncate_of_int : (forall x:int. (truncate(real_of_int(x)) = x)) axiom c_euclidian : (forall n:int. forall d:int [safe_comp_div(n,d), safe_comp_mod(n,d)]. ((not (d = 0)) -> (n = ((safe_comp_div(n,d) * d) + safe_comp_mod(n,d))))) axiom cdiv_cases : (forall n:int. forall d:int [safe_comp_div(n,d)]. ((0 <= n) -> ((0 < d) -> (safe_comp_div(n,d) = (n / d))))) axiom cdiv_cases1 : (forall n:int. forall d:int [safe_comp_div(n,d)]. ((n <= 0) -> ((0 < d) -> (safe_comp_div(n,d) = (-((-n) / d)))))) axiom cdiv_cases2 : (forall n:int. forall d:int [safe_comp_div(n,d)]. ((0 <= n) -> ((d < 0) -> (safe_comp_div(n,d) = (-(n / (-d))))))) axiom cdiv_cases3 : (forall n:int. forall d:int [safe_comp_div(n,d)]. ((n <= 0) -> ((d < 0) -> (safe_comp_div(n,d) = ((-n) / (-d)))))) axiom cmod_cases : (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((0 < d) -> (safe_comp_mod(n,d) = (n % d))))) axiom cmod_cases1 : (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((0 < d) -> (safe_comp_mod(n,d) = (-((-n) % d)))))) axiom cmod_cases2 : (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((d < 0) -> (safe_comp_mod(n,d) = (n % (-d)))))) axiom cmod_cases3 : (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((d < 0) -> (safe_comp_mod(n,d) = (-((-n) % (-d))))))) axiom cmod_remainder : (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((0 < d) -> (0 <= safe_comp_mod(n,d))))) axiom cmod_remainder1 : (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((0 < d) -> (safe_comp_mod(n,d) < d)))) axiom cmod_remainder2 : (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((0 < d) -> ((-d) < safe_comp_mod(n,d))))) axiom cmod_remainder3 : (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((0 < d) -> (safe_comp_mod(n,d) <= 0)))) axiom cmod_remainder4 : (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((d < 0) -> (0 <= safe_comp_mod(n,d))))) axiom cmod_remainder5 : (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((0 <= n) -> ((d < 0) -> (safe_comp_mod(n,d) < (-d))))) axiom cmod_remainder6 : (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((d < 0) -> (d < safe_comp_mod(n,d))))) axiom cmod_remainder7 : (forall n:int. forall d:int [safe_comp_mod(n,d)]. ((n <= 0) -> ((d < 0) -> (safe_comp_mod(n,d) <= 0)))) axiom cdiv_neutral : (forall a:int [safe_comp_div(a,1)]. (safe_comp_div(a,1) = a)) axiom cdiv_inv : (forall a:int [safe_comp_div(a,a)]. ((not (a = 0)) -> (safe_comp_div(a,a) = 1))) (**************************************************************************) (* *) (* This file is part of WP plug-in of Frama-C. *) (* *) (* Copyright (C) 2007-2014 *) (* CEA (Commissariat a l'energie atomique et aux energies *) (* alternatives) *) (* *) (* you can redistribute it and/or modify it under the terms of the GNU *) (* Lesser General Public License as published by the Free Software *) (* Foundation, version 2.1. *) (* *) (* It is distributed in the hope that it will be useful, *) (* but WITHOUT ANY WARRANTY; without even the implied warranty of *) (* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) (* GNU Lesser General Public License for more details. *) (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) (* *) (**************************************************************************) (* this is a prelude for Alt-Ergo*) (** The theory BuiltIn_ must be appended to this file*) (** The theory Bool_ must be appended to this file*) (** The theory bool_Bool_ must be appended to this file*) (** The theory int_Int_ must be appended to this file*) (** The theory map_Map_ must be appended to this file*) type addr = { base : int; offset : int } logic addr_le : addr, addr -> prop logic addr_lt : addr, addr -> prop logic addr_le_bool : addr, addr -> bool logic addr_lt_bool : addr, addr -> bool axiom addr_le_def : (forall p:addr. forall q:addr [addr_le(p, q)]. (((p).base = (q).base) -> (addr_le(p, q) -> ((p).offset <= (q).offset)))) axiom addr_le_def1 : (forall p:addr. forall q:addr [addr_le(p, q)]. (((p).base = (q).base) -> (((p).offset <= (q).offset) -> addr_le(p, q)))) axiom addr_lt_def : (forall p:addr. forall q:addr [addr_lt(p, q)]. (((p).base = (q).base) -> (addr_lt(p, q) -> ((p).offset < (q).offset)))) axiom addr_lt_def1 : (forall p:addr. forall q:addr [addr_lt(p, q)]. (((p).base = (q).base) -> (((p).offset < (q).offset) -> addr_lt(p, q)))) axiom addr_le_bool_def : (forall p:addr. forall q:addr [addr_le_bool(p, q)]. (addr_le(p, q) -> (addr_le_bool(p, q) = true))) axiom addr_le_bool_def1 : (forall p:addr. forall q:addr [addr_le_bool(p, q)]. ((addr_le_bool(p, q) = true) -> addr_le(p, q))) axiom addr_lt_bool_def : (forall p:addr. forall q:addr [addr_lt_bool(p, q)]. (addr_lt(p, q) -> (addr_lt_bool(p, q) = true))) axiom addr_lt_bool_def1 : (forall p:addr. forall q:addr [addr_lt_bool(p, q)]. ((addr_lt_bool(p, q) = true) -> addr_lt(p, q))) function null() : addr = { base = 0; offset = 0 } function global(b: int) : addr = { base = b; offset = 0 } function shift(p: addr, k: int) : addr = { base = (p).base; offset = ((p).offset + k) } predicate included(p: addr, a: int, q: addr, b: int) = ((0 < a) -> ((0 <= b) and (((p).base = (q).base) and (((q).offset <= (p).offset) and (((p).offset + a) <= ((q).offset + b)))))) predicate separated(p: addr, a: int, q: addr, b: int) = ((a <= 0) or ((b <= 0) or ((not ((p).base = (q).base)) or ((((q).offset + b) <= (p).offset) or (((p).offset + a) <= (q).offset))))) predicate eqmem(m1: (addr,'a) farray, m2: (addr,'a) farray, p: addr, a1: int) = (forall q:addr [(m1[p])| (m2[q])]. (included(q, 1, p, a1) -> ((m1[q]) = (m2[q])))) predicate havoc(m1: (addr,'a) farray, m2: (addr,'a) farray, p: addr, a1: int) = (forall q:addr [(m1[p])| (m2[q])]. (separated(q, 1, p, a1) -> ((m1[q]) = (m2[q])))) predicate valid_rd(m: (int,int) farray, p: addr, n: int) = ((0 < n) -> ((0 <= (p).offset) and (((p).offset + n) <= (m[(p).base])))) predicate valid_rw(m: (int,int) farray, p: addr, n: int) = ((0 < n) -> ((0 < (p).base) and ((0 <= (p).offset) and (((p).offset + n) <= (m[(p).base]))))) axiom valid_rw_rd : (forall m:(int,int) farray. (forall p:addr. (forall n:int. (valid_rw(m, p, n) -> valid_rd(m, p, n))))) axiom valid_string : (forall m:(int,int) farray. (forall p:addr. (((p).base < 0) -> (((0 <= (p).offset) and ((p).offset < (m[(p).base]))) -> valid_rd(m, p, 1))))) axiom valid_string1 : (forall m:(int,int) farray. (forall p:addr. (((p).base < 0) -> (((0 <= (p).offset) and ((p).offset < (m[(p).base]))) -> (not valid_rw(m, p, 1)))))) axiom separated_1 : (forall p:addr. forall q:addr. (forall a:int. forall b:int. forall i:int. forall j:int [separated(p, a, q, b), { base = (p).base; offset = i }, { base = (q).base; offset = j }]. (separated(p, a, q, b) -> ((((p).offset <= i) and (i < ((p).offset + a))) -> ((((q).offset <= j) and (j < ((q).offset + b))) -> (not ({ base = (p).base; offset = i } = { base = (q).base; offset = j }))))))) logic region : int -> int logic linked : (int,int) farray -> prop logic sconst : (addr,int) farray -> prop predicate framed(m: (addr,addr) farray) = (forall p:addr [(m[p])]. (region(((m[p])).base) <= 0)) axiom separated_included : (forall p:addr. forall q:addr. (forall a:int. forall b:int [separated(p, a, q, b), included(p, a, q, b)]. ((0 < a) -> ((0 < b) -> (separated(p, a, q, b) -> (not included(p, a, q, b))))))) axiom included_trans : (forall p:addr. forall q:addr. forall r:addr. (forall a:int. forall b:int. forall c:int [included(p, a, q, b), included(q, b, r, c)]. (included(p, a, q, b) -> (included(q, b, r, c) -> included(p, a, r, c))))) axiom separated_trans : (forall p:addr. forall q:addr. forall r:addr. (forall a:int. forall b:int. forall c:int [included(p, a, q, b), separated(q, b, r, c)]. (included(p, a, q, b) -> (separated(q, b, r, c) -> separated(p, a, r, c))))) axiom separated_sym : (forall p:addr. forall q:addr. (forall a:int. forall b:int [separated(p, a, q, b)]. (separated(p, a, q, b) -> separated(q, b, p, a)))) axiom separated_sym1 : (forall p:addr. forall q:addr. (forall a:int. forall b:int [separated(p, a, q, b)]. (separated(q, b, p, a) -> separated(p, a, q, b)))) axiom eqmem_included : (forall m1:(addr,'a) farray. forall m2:(addr,'a) farray. (forall p:addr. forall q:addr. (forall a1:int. forall b:int [eqmem(m1, m2, p, a1), eqmem(m1, m2, q, b)]. (included(p, a1, q, b) -> (eqmem(m1, m2, q, b) -> eqmem(m1, m2, p, a1)))))) axiom eqmem_sym : (forall m1:(addr,'a) farray. forall m2:(addr,'a) farray. (forall p:addr. (forall a1:int. (eqmem(m1, m2, p, a1) -> eqmem(m2, m1, p, a1))))) axiom havoc_sym : (forall m1:(addr,'a) farray. forall m2:(addr,'a) farray. (forall p:addr. (forall a1:int. (havoc(m1, m2, p, a1) -> havoc(m2, m1, p, a1))))) logic cast : addr -> int axiom cast_injective : (forall p:addr. forall q:addr [cast(p), cast(q)]. ((cast(p) = cast(q)) -> (p = q))) logic hardware : int -> int axiom hardnull : (hardware(0) = 0) (**************************************************************************) (* *) (* This file is part of WP plug-in of Frama-C. *) (* *) (* Copyright (C) 2007-2014 *) (* CEA (Commissariat a l'energie atomique et aux energies *) (* alternatives) *) (* *) (* you can redistribute it and/or modify it under the terms of the GNU *) (* Lesser General Public License as published by the Free Software *) (* Foundation, version 2.1. *) (* *) (* It is distributed in the hope that it will be useful, *) (* but WITHOUT ANY WARRANTY; without even the implied warranty of *) (* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) (* GNU Lesser General Public License for more details. *) (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) (* *) (**************************************************************************) (* this is a prelude for Alt-Ergo*) (** The theory BuiltIn_ must be appended to this file*) (** The theory Bool_ must be appended to this file*) (** The theory bool_Bool_ must be appended to this file*) (** The theory int_Int_ must be appended to this file*) logic is_uint8 : int -> prop axiom is_uint8_def : (forall x:int [is_uint8(x)]. (is_uint8(x) -> (0 <= x))) axiom is_uint8_def1 : (forall x:int [is_uint8(x)]. (is_uint8(x) -> (x < 256))) axiom is_uint8_def2 : (forall x:int [is_uint8(x)]. (((0 <= x) and (x < 256)) -> is_uint8(x))) logic is_sint8 : int -> prop axiom is_sint8_def : (forall x:int [is_sint8(x)]. (is_sint8(x) -> ((-128) <= x))) axiom is_sint8_def1 : (forall x:int [is_sint8(x)]. (is_sint8(x) -> (x < 128))) axiom is_sint8_def2 : (forall x:int [is_sint8(x)]. ((((-128) <= x) and (x < 128)) -> is_sint8(x))) logic is_uint16 : int -> prop axiom is_uint16_def : (forall x:int [is_uint16(x)]. (is_uint16(x) -> (0 <= x))) axiom is_uint16_def1 : (forall x:int [is_uint16(x)]. (is_uint16(x) -> (x < 65536))) axiom is_uint16_def2 : (forall x:int [is_uint16(x)]. (((0 <= x) and (x < 65536)) -> is_uint16(x))) predicate is_sint16(x: int) = (((-32768) <= x) and (x < 32768)) logic is_uint32 : int -> prop axiom is_uint32_def : (forall x:int [is_uint32(x)]. (is_uint32(x) -> (0 <= x))) axiom is_uint32_def1 : (forall x:int [is_uint32(x)]. (is_uint32(x) -> (x < 4294967296))) axiom is_uint32_def2 : (forall x:int [is_uint32(x)]. (((0 <= x) and (x < 4294967296)) -> is_uint32(x))) logic is_sint32 : int -> prop axiom is_sint32_def : (forall x:int [is_sint32(x)]. (is_sint32(x) -> ((-2147483648) <= x))) axiom is_sint32_def1 : (forall x:int [is_sint32(x)]. (is_sint32(x) -> (x < 2147483648))) axiom is_sint32_def2 : (forall x:int [is_sint32(x)]. ((((-2147483648) <= x) and (x < 2147483648)) -> is_sint32(x))) logic is_uint64 : int -> prop axiom is_uint64_def : (forall x:int [is_uint64(x)]. (is_uint64(x) -> (0 <= x))) axiom is_uint64_def1 : (forall x:int [is_uint64(x)]. (is_uint64(x) -> (x < 18446744073709551616))) axiom is_uint64_def2 : (forall x:int [is_uint64(x)]. (((0 <= x) and (x < 18446744073709551616)) -> is_uint64(x))) logic is_sint64 : int -> prop axiom is_sint64_def : (forall x:int [is_sint64(x)]. (is_sint64(x) -> ((-9223372036854775808) <= x))) axiom is_sint64_def1 : (forall x:int [is_sint64(x)]. (is_sint64(x) -> (x < 9223372036854775808))) axiom is_sint64_def2 : (forall x:int [is_sint64(x)]. ((((-9223372036854775808) <= x) and (x < 9223372036854775808)) -> is_sint64(x))) logic to_uint8 : int -> int logic to_sint8 : int -> int logic to_uint16 : int -> int logic to_sint16 : int -> int logic to_uint32 : int -> int logic to_sint32 : int -> int logic to_uint64 : int -> int logic to_sint64 : int -> int axiom is_to_uint8 : (forall x:int [is_uint8(to_uint8(x))]. is_uint8(to_uint8(x))) axiom is_to_sint8 : (forall x:int [is_sint8(to_sint8(x))]. is_sint8(to_sint8(x))) axiom is_to_uint16 : (forall x:int [is_uint16(to_uint16(x))]. is_uint16(to_uint16(x))) axiom is_to_sint16 : (forall x:int [is_sint16(to_sint16(x))]. is_sint16(to_sint16(x))) axiom is_to_uint32 : (forall x:int [is_uint32(to_uint32(x))]. is_uint32(to_uint32(x))) axiom is_to_sint32 : (forall x:int [is_sint32(to_sint32(x))]. is_sint32(to_sint32(x))) axiom is_to_uint64 : (forall x:int [is_uint64(to_uint64(x))]. is_uint64(to_uint64(x))) axiom is_to_sint64 : (forall x:int [is_sint64(to_sint64(x))]. is_sint64(to_sint64(x))) axiom id_uint8 : (forall x:int [to_uint8(x)]. (((0 <= x) and (x < 256)) -> (to_uint8(x) = x))) axiom id_sint8 : (forall x:int [to_sint8(x)]. ((((-128) <= x) and (x < 128)) -> (to_sint8(x) = x))) axiom id_uint16 : (forall x:int [to_uint16(x)]. (((0 <= x) and (x < 65536)) -> (to_uint16(x) = x))) axiom id_sint16 : (forall x:int [to_sint16(x)]. ((((-32768) <= x) and (x < 32768)) -> (to_sint16(x) = x))) axiom id_uint32 : (forall x:int [to_uint32(x)]. (((0 <= x) and (x < 4294967296)) -> (to_uint32(x) = x))) axiom id_sint32 : (forall x:int [to_sint32(x)]. ((((-2147483648) <= x) and (x < 2147483648)) -> (to_sint32(x) = x))) axiom id_uint64 : (forall x:int [to_uint64(x)]. (((0 <= x) and (x < 18446744073709551616)) -> (to_uint64(x) = x))) axiom id_sint64 : (forall x:int [to_sint64(x)]. ((((-9223372036854775808) <= x) and (x < 9223372036854775808)) -> (to_sint64(x) = x))) logic lnot : int -> int logic ac land : int, int -> int logic ac lxor : int, int -> int logic ac lor : int, int -> int logic lsl : int, int -> int logic lsr : int, int -> int logic bit_testb : int, int -> bool logic bit_test : int, int -> prop (* ---------------------------------------------------------- *) (* --- Assertion 'rte,unsigned_overflow' (file a.c, line 37) --- *) (* ---------------------------------------------------------- *) goal secp256k1_fe_mul_inner_assert_rte_unsigned_overflow_38: forall Malloc_0 : int farray. forall Mint_0 : (addr,int) farray. forall a_0,b_0 : addr. let a_1 = shift(a_0, 0) : addr in let x_0 = Mint_0[a_1] : int in let x_1 = Mint_0[shift(a_0, 1)] : int in let x_2 = Mint_0[shift(a_0, 2)] : int in let x_3 = Mint_0[shift(a_0, 3)] : int in let x_4 = Mint_0[shift(a_0, 4)] : int in let x_5 = Mint_0[shift(a_0, 5)] : int in let x_6 = Mint_0[shift(a_0, 6)] : int in let x_7 = Mint_0[shift(a_0, 7)] : int in let x_8 = Mint_0[shift(a_0, 8)] : int in let x_9 = Mint_0[shift(a_0, 9)] : int in let a_2 = shift(b_0, 0) : addr in let x_10 = Mint_0[a_2] : int in let x_11 = Mint_0[shift(b_0, 1)] : int in let x_12 = Mint_0[shift(b_0, 2)] : int in let x_13 = Mint_0[shift(b_0, 3)] : int in let x_14 = Mint_0[shift(b_0, 4)] : int in let x_15 = Mint_0[shift(b_0, 5)] : int in let x_16 = Mint_0[shift(b_0, 6)] : int in let x_17 = Mint_0[shift(b_0, 7)] : int in let x_18 = Mint_0[shift(b_0, 8)] : int in let x_19 = Mint_0[shift(b_0, 9)] : int in linked(Malloc_0) -> (x_0 <= 1073741823) -> (x_1 <= 1073741823) -> (x_2 <= 1073741823) -> (x_3 <= 1073741823) -> (x_4 <= 1073741823) -> (x_5 <= 1073741823) -> (x_6 <= 1073741823) -> (x_7 <= 1073741823) -> (x_8 <= 1073741823) -> (x_9 <= 67108863) -> (x_10 <= 1073741823) -> (x_11 <= 1073741823) -> (x_12 <= 1073741823) -> (x_13 <= 1073741823) -> (x_14 <= 1073741823) -> (x_15 <= 1073741823) -> (x_16 <= 1073741823) -> (x_17 <= 1073741823) -> (x_18 <= 1073741823) -> (x_19 <= 67108863) -> is_uint32(x_0) -> is_uint32(x_1) -> is_uint32(x_2) -> is_uint32(x_3) -> is_uint32(x_4) -> is_uint32(x_5) -> is_uint32(x_6) -> is_uint32(x_7) -> is_uint32(x_8) -> is_uint32(x_9) -> is_uint32(x_10) -> is_uint32(x_11) -> is_uint32(x_12) -> is_uint32(x_13) -> is_uint32(x_14) -> is_uint32(x_15) -> is_uint32(x_16) -> is_uint32(x_17) -> is_uint32(x_18) -> is_uint32(x_19) -> valid_rw(Malloc_0, a_1, 10) -> valid_rw(Malloc_0, a_2, 10) -> ((x_9 * x_10) <= 4294967295)