Skip to content
Browse files

adding a test case, recording in, removing the lextop axiom

  • Loading branch information
nikswamy committed Feb 6, 2020
1 parent cb62da5 commit e4296312a87b94c3cbcd683a56555a8e30b7cbde
Showing with 76 additions and 16 deletions.
  1. +10 −0
  2. +58 −0 examples/bug-reports/BugLexTop.fst
  3. +1 −1 examples/bug-reports/Makefile
  4. +7 −15 src/smtencoding/FStar.SMTEncoding.Encode.fs
@@ -48,6 +48,16 @@ Guidelines for the changelog:

The workaround is an explicit annotation (see comments in the commit above).

* An unsoundness was discovered and fixed in the treatment of
lexicographic tuples. In particular, we used to allow relating lex
tuples of different arity, notably, we had `LexCons _ _ << LexTop`.
This was intended for the convenience of writing mutual recursive
functions with decreases clauses using lex tuples of different arities.
However, this convenience was seldom used and it actually lead to
an unsoundness: See examples/bug-reports/BugLexTop.fst. This
variable arity lexicographic tuple ordering is no longer supported.

## Libraries

* Two core axioms were discovered by Aseem Rastogi to be formulated
@@ -0,0 +1,58 @@
module BugLexTop
This is a bug report due to Son Ho,
Also, with contributions from Jay Bosamiya for the proof of False.
It was fixed in 92e50f9b5ba34afe97b2cc09ba66dfa090438825
val n_lexcons : nat -> lex_t
let rec n_lexcons n =
if n = 0 then LexTop else LexCons LexTop (n_lexcons (n-1))

/// Previously, this used to go through, because we had `LexCons _ _ << LexTop`
[@(expect_failure [19])]
let rec decrease_lexcons (n:nat)
: Lemma (n_lexcons (n+1) << n_lexcons n)
= if n = 0 then () else decrease_lexcons (n-1)

/// Letting it go through quickly leads to a proof of false, as shown below
/// by Son and Jay
val decrease_lexcons_bad : n:nat -> Lemma (n_lexcons (n+1) << n_lexcons n)

val infinite_fun : n:nat -> x:lex_t{x==n_lexcons n} -> Tot False (decreases x)
let rec infinite_fun n x =
decrease_lexcons_bad n;
infinite_fun (n+1) (n_lexcons (n+1))

/// You can no longer meaningfully relate lex tuples of different length
[@(expect_failure [19])]
let rec f (x:nat) (y:nat)
: Tot nat
(decreases (LexCons x LexTop))
= if y > 0
then g x (y - 1)
else if x > 0
then f (x - 1) y
else x
and g (x:nat) (y:nat)
: Tot nat
(decreases (LexCons x (LexCons y LexTop)))
= if x = 0 then 0
else f (x - 1) (x + 1)

/// You must "pad" out the lex tuples to the same length to relate
/// them by <<
let rec h (x:nat) (y:nat)
: Tot nat
(decreases (LexCons x (LexCons y LexTop)))
= if y > 0
then i x (y - 1)
else if x > 0
then h (x - 1) y
else x
and i (x:nat) (y:nat)
: Tot nat
(decreases (LexCons x (LexCons y LexTop)))
= if x = 0 then 0
else h (x - 1) (x + 1)
@@ -37,7 +37,7 @@ SHOULD_VERIFY_CLOSED=bug022.fst bug024.fst bug025.fst bug026.fst bug026b.fst bug
Bug1730b.fst Bug1612.fst Bug1614a.fst Bug1614b.fst Bug1614c.fst Bug1614d.fst Bug1614e.fst Bug1750.fst Bug1750.Aux.fst \
Bug1622.fst bug1540.fst Bug1784.fst Bug1802.fst Bug1055.fst Bug1818.fst Bug1640.fst Bug1243.fst Bug1841.fst \
Bug1847.fst Bug1855.fst Bug1812.fst Bug1840.fst Bug1866.fst Bug811.fst Bug841.fst Bug1060.fst Bug1070.fst \
Bug1130.fst Bug1170.fst Bug1191.fst Bug1799.fst Bug1900.fst Bug1908.fst Bug1913.fst
Bug1130.fst Bug1170.fst Bug1191.fst Bug1799.fst Bug1900.fst Bug1908.fst Bug1913.fst BugLexTop.fst

SHOULD_VERIFY_INTERFACE_CLOSED=bug771.fsti bug771b.fsti
@@ -1468,28 +1468,20 @@ and encode_sigelt' (env:env_t) (se:sigelt) : (decls_t * env_t) =
("data_elim_" ^ ddconstrsym)) in
let subterm_ordering =
let lex_t = mkFreeV <| mk_fv (text_of_lid Const.lex_t_lid, Term_sort) in
if lid_equals d Const.lextop_lid
&& false
then let x = mk_fv (varops.fresh env.current_module_name "x", Term_sort) in
let xtm = mkFreeV x in
Util.mkAssume(mkForall (Ident.range_of_lid d)
([[mk_Precedes lex_t lex_t xtm dapp]],
mkImp(mk_tester "LexCons" xtm, mk_Precedes lex_t lex_t xtm dapp)),
Some "lextop is top",
(varops.mk_unique "lextop"))
else (* subterm ordering *)
let prec =
(* subterm ordering *)
let prec =
|> List.mapi (fun i v ->
(* it's a parameter, so it's inaccessible and no need for a sub-term ordering on it *)
if i < n_tps
then []
else [mk_Precedes lex_t lex_t (mkFreeV v) dapp])
|> List.flatten
Util.mkAssume(mkForall (Ident.range_of_lid d)
([[ty_pred]], add_fuel (mk_fv (fuel_var, Fuel_sort)) (vars@arg_binders), mkImp(ty_pred, mk_and_l prec)),
Util.mkAssume(mkForall (Ident.range_of_lid d)
add_fuel (mk_fv (fuel_var, Fuel_sort)) (vars@arg_binders),
mkImp(ty_pred, mk_and_l prec)),
Some "subterm ordering",

0 comments on commit e429631

Please sign in to comment.
You can’t perform that action at this time.