Add Oracle Types by jcreedcmu · Pull Request #43480 · microsoft/TypeScript

type Today = Shell<'date "+%Y-%m-%d"'>

//
// First we build up some machinery to generate Z3 inputs.
//

// A phantom type used to express constraints about integer values
type Constr<T> = { constr: T };

// An integer value so constrained
type ConstrNum<T> = number & Constr<T>;

// Generate a Z3 assertion for constraint T
type GenAssert<T> = T extends string ? `(${T})` : 'false';

// Generate Z3 code that checks whether T implies U.
// Z3 will return 'unsat' if the implication *does* hold,
// because T && !U will be false.
type GenZ3<T, U> = `
(declare-const x Int)
(assert ${GenAssert<T>})
(assert (not ${GenAssert<U>}))
(check-sat)
`;


//
// Now we deal with calling Z3 and cleaning up the output
//

// Strip trailing newline from a string literal type
type StripNl<T extends string> = T extends `${infer S}\n` ? S : T;

// Given a string type containing an sexp expressing a z3 program,
// return 'sat' or 'unsat'
type SolverResult<Z3 extends string> =
  StripNl<Shell<`echo '${Z3}' | z3 -in`>>;


//
// Set up some conveniences for the user
//

// If T => U, yields the appropriate result type for constraint U, otherwise unknown.
type InferCond<T, U> = SolverResult<GenZ3<T, U>> extends 'unsat' ? ConstrNum<U> : unknown;

// Convert x from one constraint type to another
export function infer<T, U>(x: ConstrNum<T>): InferCond<T, U> {
  return x as any;
}

type strish = string | number;
export type Plus<T extends strish, U extends strish> = `(+ ${T} ${U})`;
export type LessEq<T extends strish> = ConstrNum<`<= x ${T}`>;

//
// Example usage
//
function test_cases(x: LessEq<5>) {

  // Error, because <= x (+ 2 3) is not intensionally the same as <= x 5!
  { const bad: LessEq<Plus<2, 3>> = x; }

  // However, we can insert an `infer' call to mediate between
  // different representations of logically equivalent constraints:
  { const good: LessEq<Plus<2, 3>> = infer(x); }

  // Error, because not sound to infer <= (+ 2 2) from <= 5!
  { const bad: LessEq<Plus<2, 2>> = infer(x); }

  // Sound, because <= 5 implies <= 6
  { const good: LessEq<Plus<2, 4>> = infer(x); }

}