Refinement subtypes being discarded

[amosr]

Hi,
I came across a bug which allowed me to use integer division in a context that required a function of type int -> int -> int. This should be a type error because the rhs of the division is not nonzero.

I've tried to minimise it, so the concepts might not make much sense, but I think they're required to make a complex result type that eventually normalises to int -> int -> int. The last four lines show the inconsistency. The unminimised version is here: https://github.com/songlarknet/pipit/blob/submit/ecoop24/src/Pipit.Prim.Vanilla.fst

module Test.Div

type funty (valty: Type) =
 | FTVal: t: valty -> funty valty
 | FTFun: t: valty -> rest: funty valty -> funty valty

let rec funty_sem (#ty: Type) (ty_sem: ty -> eqtype) (ft: funty ty) =
  match ft with
  | FTVal t -> ty_sem t
  | FTFun t r -> (ty_sem t -> funty_sem ty_sem r)

type valtype =
 | TInt:  valtype

let ty_sem (t: valtype): eqtype = match t with
 | TInt  -> int

type prim_arith =
 | P'A'Div

let prim_arith_ty (p: prim_arith) (at: valtype): funty valtype = match p with
 | P'A'Div -> FTFun at (FTFun at (FTVal at))

let prim_arith_sem (p: prim_arith): funty_sem ty_sem (prim_arith_ty p TInt) =
  fun x y -> x / y

let div_is_int_to_int: int -> int -> int =
  prim_arith_sem P'A'Div

[TWal]

Further minimized to

let prim_arith_ty (p: unit): Type0 =
  let () = p in
  int -> int -> int

let prim_arith_sem (p: unit): (prim_arith_ty p) =
  fun x y -> x / y

let div_is_int_to_int: int -> int -> int =
  prim_arith_sem ()

[mtzguido]

Yikes. Looks like the typing is going to SMT and it is accepting it:
Query:

; Encoding query formula : forall (p: Prims.unit).
;   (*  - Subtyping check failed
;   - Expected type
;       let () = p in
;       _: Prims.int -> _: Prims.int -> Prims.int
;     got type x: Prims.int -> y: Prims.nonzero -> Prims.int
; *)
;   Prims.has_type (fun x y -> x / y)
;     (let () = p in
;       _: Prims.int -> _: Prims.int -> Prims.int)


; Context: While encoding a query
; While typechecking the top-level declaration `let prim_arith_sem`

(push)

; <fuel='2' ifuel='1'>

;;; Fact-ids: 
(assert (! (= MaxFuel
(SFuel (SFuel ZFuel)))
:named @MaxFuel_assumption))
;;; Fact-ids: 
(assert (! (= MaxIFuel
(SFuel ZFuel))
:named @MaxIFuel_assumption))
;;;;;;;;;;;;;;;;query
;;; Fact-ids: 
(assert (! (not (forall ((@x0 Term))
 (! (implies (HasType @x0
Prims.unit)

;; def=Yikes.fst(9,13-9,18); use=Yikes.fst(9,13-9,18)
(or label_1
(HasType Tm_abs_08309fc2bd63a3fd5b9632055d528dbf
(let ((@lb1 @x0))
(ite (= @lb1
Tm_unit)
Tm_arrow_47fc285d7b44e13bcb7e420cbfc55623
Tm_unit))))
)
 
;;no pats
:qid @query)))
:named @query))

Definition of the abstraction, no typing for the arguments?

(declare-fun Tm_abs_08309fc2bd63a3fd5b9632055d528dbf () Term)
;;;;;;;;;;;;;;;;typing_Tm_abs_08309fc2bd63a3fd5b9632055d528dbf
;;; Fact-ids: 
(assert (! (HasType Tm_abs_08309fc2bd63a3fd5b9632055d528dbf
Tm_arrow_caf54773c365d5c2d3fce97c5e20c51a)
:named typing_Tm_abs_08309fc2bd63a3fd5b9632055d528dbf))
;;;;;;;;;;;;;;;;interpretation_Tm_abs_08309fc2bd63a3fd5b9632055d528dbf
;;; Fact-ids: 
(assert (! 
;; def=Yikes.fst(9,13-9,18); use=Yikes.fst(9,13-9,18)
(forall ((@x0 Term) (@x1 Term))
 (! (= (ApplyTT (ApplyTT Tm_abs_08309fc2bd63a3fd5b9632055d528dbf
@x0)
@x1)
(Prims.op_Division @x0
@x1))
 

:pattern ((ApplyTT (ApplyTT Tm_abs_08309fc2bd63a3fd5b9632055d528dbf
@x0)
@x1))
:qid interpretation_Tm_abs_08309fc2bd63a3fd5b9632055d528dbf))

:named interpretation_Tm_abs_08309fc2bd63a3fd5b9632055d528dbf))

[nikswamy]

Thanks for the report! This is ugly, sorry.

Here's what's going on.

• This issue is confined to the use of primitive operations that have refinements on their domains, i.e., Prims.op_Division and Prims.op_Modulus. We encode them incorrectly to the SMT solver as just abbreviations for the underlying SMT theory operators div and mod. This allows the SMT solver to incorrectly derive that, say, exists u. x / 0 = BoxInt u and then derive that HasType (x / 0) Prims.int, which is clearly wrong.

• Note, if you try these examples with some non-primitive function with a refined domain then F* correctly rejects it, e.g., this fails

assume
val my_division (i:int) (p:nonzero) : j:int { j = i / p }

let prim_arith_ty (p: unit): Type0 =
  let () = p in
  int -> int -> int

let prim_arith_sem (p: unit): (prim_arith_ty p) =
  fun x y -> my_division x y

• I'm working on a patch on the SMT encoding for these primitive operations, adding a precondition to the domain. Will report back here on the fallout

[amosr]

That was an impressively quick diagnosis and fix! Thanks

[TWal]

There is still something weird happening:

//let f (x:int) (y:nonzero): int = x / y
let g (x:int) (y:nonzero): int = x + y

let prim_arith_ty (p: unit): Type0 =
  let () = p in
  int -> int -> int

let prim_arith_sem (p: unit): (prim_arith_ty p) =
  fun x y -> g x y

let div_is_int_to_int: int -> int -> int =
  prim_arith_sem ()

Although the code with f doesn't typecheck anymore (hence we now can't divide by 0), the code with g does typecheck.
This shouldn't be possible since we shouldn't be able to call f with y == 0, right?

[mtzguido]

Ouch, changing x + y to x + 1/y also typechecks...