Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

PVS Bug 1072


Synopsis:        Soundness bug (missing typechecking condition)
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Fri May 20 13:50:00 -0700 2011
Originator:      Victor Luchangco
Release:         PVS 5.0
Organization:    oracle.com
Environment: 
 System:          
 Architecture: 

Description: 
  
  --Apple-Mail-15--947890132
  Content-Transfer-Encoding: quoted-printable
  Content-Type: text/plain;
  	charset=us-ascii
  
  Hi,
  
  I'm attaching a PVS theory that illustrates a soundness bug in the =
  prover.  (I'm using the CMU Lisp version--the requested system data is =
  in comments at the top of the file, with the machine names removed.)  =
  The problem is that a necessary typechecking condition is not generated =
  for the lemmas "falseStatement" and "falseStatement2".  To make sure I =
  wasn't just misinterpreting some subtle nuace due to conversions, I used =
  these to prove "odd?(2)".
  
  Probably related to this, I tried to prove odd?(2) using just =
  falseStatement, but I couldn't do so, and in one proof, I consistently =
  got PVS into an error state.  I'm attaching the proof file so that you =
  can see both the proofs that I used to derive the false lemmas and the =
  proof that consistently broke.
  
  - Victor
  
  PS. This theory is seriously stripped down from a refinement proof we =
  are doing to prove the correctness of some concurrent algorithms (for =
  transactional memory).  We'd like to publish this research when we are =
  done with the proof (we hope soon), and it would obviously be much nicer =
  if we could do so without this problem.
  
  
  
  --Apple-Mail-15--947890132
  Content-Disposition: attachment;
  	filename=BugTest.pvs
  Content-Type: application/octet-stream;
  	name="BugTest.pvs"
  Content-Transfer-Encoding: 7bit
  
  % PVS Version 4.2 - CMU Common Lisp 19d (19D) - CMU Common Lisp 19d (19D)
  % GNU Emacs 21.4.1 (x86_64-redhat-linux-gnu, X toolkit, Xaw3d scroll bars) of
  2008-03-13 on <machinename>
  % Linux <machinename> 2.6.18-194.el5 #1 SMP Mon Mar 29 22:10:29 EDT 2010 x86_
 64 x86_64 x86_64 GNU/Linux
  
  BugTest: THEORY
  BEGIN
  
  Lifted: DATATYPE
  BEGIN
    raised(base: nat): raised?
    unraised: unraised?
  END Lifted
  CONVERSION base::[(raised?) -> nat]
  
  p: VAR [# first: nat, second: Lifted #]
  
  f(x: Lifted): nat = IF raised?(x) THEN 2 ELSE 1 ENDIF 
  
  falseStatement: LEMMA 
    NOT odd?(p`second) IMPLIES f(p`second) = 2
  
  falseStatement2: LEMMA 
    odd?(p`second) IMPLIES f(p`second) = 2
  
  contradiction: LEMMA
    odd?(2)
  
  END BugTest
  
  --Apple-Mail-15--947890132
  Content-Disposition: attachment;
  	filename=BugTest.prf
  Content-Type: application/octet-stream;
  	name="BugTest.prf"
  Content-Transfer-Encoding: 7bit
  
  (|BugTest|
   (|falseStatement| 0
    (|falseStatement-1| NIL 3514898041 3514898415
     ("" (SKOSIMP)
      (("" (ASSERT) (("" (EXPAND "f") (("" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)
     UNCHECKED ((|f| CONST-DECL "nat" |BugTest| NIL)) 1 0 T SHOSTAK))
   (|falseStatement2| 0
    (|falseStatement2-1| NIL 3514914852 3514914865
     ("" (SKOSIMP)
      (("" (ASSERT) (("" (EXPAND "f") (("" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)
     PROVED ((|f| CONST-DECL "nat" |BugTest| NIL)) 1285 1 T SHOSTAK))
   (|contradiction| 0
    (|contradiction-2| "" 3514914960 3514914960
     ("" (CASE "2 = f(unraised)")
      (("1" (REPLACE -1) (("1" (EXPAND "f") (("1" (PROPAX) NIL NIL)) NIL)) NIL)
       ("2" (LEMMA "falseStatement")
        (("2" (LEMMA "falseStatement2")
          (("2" (ASSERT)
            (("2" (INST - "(# first := 0, second := unraised #)")
              (("2" (INST - "(# first := 0, second := unraised #)")
                (("2" (ASSERT) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL)
     PROVED NIL 7011 3 T SHOSTAK)
    (|contradiction-1| NIL 3514898432 3514914555
     ("" (CASE "2 = f(unraised)")
      (("1" (REPLACE -1) (("1" (EXPAND "f") (("1" (PROPAX) NIL NIL)) NIL)) NIL)
       ("2" (LEMMA "falseStatement")
        (("2"
          (COMMENT
           "If I instantiate first and then assert, the prover gets an error.")
          (("2" (ASSERT)
            (("2" (INST - "(# first := 0, second := unraised #)")
              (("2" (PROP) (("1" (ASSERT) NIL NIL) ("2" (POSTPONE) NIL NIL))
                NIL))
              NIL))
            ";;; If I instantiate first and then assert, the prover gets an err
 or."))
          NIL))
        NIL))
      NIL)
     PROVED
     ((|falseStatement| FORMULA-DECL NIL |BugTest| NIL)
      (|falseStatement2| FORMULA-DECL NIL |BugTest| NIL)
      (|unraised| ADT-CONSTRUCTOR-DECL "(unraised?)" |BugTest| NIL)
      (|unraised?| ADT-RECOGNIZER-DECL "[Lifted -> boolean]" |BugTest| NIL)
      (|f| CONST-DECL "nat" |BugTest| NIL)
      (|nat| NONEMPTY-TYPE-EQ-DECL NIL |naturalnumbers| NIL)
      (>= CONST-DECL "bool" |reals| NIL)
      (|bool| NONEMPTY-TYPE-EQ-DECL NIL |booleans| NIL)
      (|int| NONEMPTY-TYPE-EQ-DECL NIL |integers| NIL)
      (|integer_pred| CONST-DECL "[rational -> boolean]" |integers| NIL)
      (|rational| NONEMPTY-TYPE-FROM-DECL NIL |rationals| NIL)
      (|rational_pred| CONST-DECL "[real -> boolean]" |rationals| NIL)
      (|real| NONEMPTY-TYPE-FROM-DECL NIL |reals| NIL)
      (|real_pred| CONST-DECL "[number_field -> boolean]" |reals| NIL)
      (|number_field| NONEMPTY-TYPE-FROM-DECL NIL |number_fields| NIL)
      (|number_field_pred| CONST-DECL "[number -> boolean]" |number_fields| NIL
 )
      (|Lifted| TYPE-DECL NIL |BugTest| NIL)
      (= CONST-DECL "[T, T -> boolean]" |equalities| NIL)
      (|boolean| NONEMPTY-TYPE-DECL NIL |booleans| NIL)
      (|number| NONEMPTY-TYPE-DECL NIL |numbers| NIL))
     60785 105 T SHOSTAK)))
  
  
  --Apple-Mail-15--947890132--

How-To-Repeat: 

Fix: 
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools