diff --git a/third-party/java8-annotations/org/jspecify/annotations/NonNull.java b/third-party/java8-annotations/org/jspecify/annotations/NonNull.java
new file mode 100644
index 00000000000..771c769564c
--- /dev/null
+++ b/third-party/java8-annotations/org/jspecify/annotations/NonNull.java
@@ -0,0 +1,101 @@
+/*
+ * Copyright 2022 The JSpecify Authors.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package org.jspecify.annotations;
+
+import static java.lang.annotation.ElementType.TYPE_USE;
+import static java.lang.annotation.RetentionPolicy.RUNTIME;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.Retention;
+import java.lang.annotation.Target;
+
+/**
+ * Indicates that the annotated <a href="https://github.com/jspecify/jspecify/wiki/type-usages">type
+ * usage</a> (commonly a parameter type or return type) is considered to <i>exclude</i> {@code null}
+ * as a value; rarely needed within {@linkplain NullMarked null-marked} code.
+ *
+ * <p>This annotation serves two primary purposes:
+ *
+ * <ul>
+ *   <li>To mark any sporadic non-null type usages inside a scope that is not ready to be fully
+ *       {@link NullMarked} yet.
+ *   <li>To perform a <i>non-null projection</i> of a type variable, explained below.
+ * </ul>
+ *
+ * <p>For a comprehensive introduction to JSpecify, please see <a
+ * href="http://jspecify.org">jspecify.org</a>.
+ *
+ * <p><b>Warning:</b> These annotations are under development, and <b>any</b> aspect of their
+ * naming, locations, or design is subject to change until the JSpecify 1.0 release. Moreover,
+ * supporting analysis tools will be tracking the changes on varying schedules. Releasing a library
+ * using these annotations in its API is <b>strongly discouraged</b> at this time.
+ *
+ * <h2 id="projection">Non-null projection</h2>
+ *
+ * <p>In the following example, {@code MyOptional}'s type parameter {@code T} accepts only non-null
+ * type arguments, but {@code MyList}'s type parameter {@code E} will accept either a non-null or
+ * nullable type argument.
+ *
+ * <pre>{@code
+ * // All the below is null-marked code
+ *
+ * class MyOptional<T> { … }
+ *
+ * interface MyList<E extends @Nullable Object> {
+ *   // Returns the first non-null element, if such element exists.
+ *   MyOptional<E> firstNonNull() { … } // problem here!
+ * }
+ *
+ * MyList<@Nullable String> maybeNulls = …
+ * MyList<String> nonNulls = …
+ * }</pre>
+ *
+ * <p>Because {@code MyOptional} accepts only non-null type arguments, we need both {@code
+ * maybeNulls.firstNonNull()} and {@code nonNulls.firstNonNull()} to produce the same return type:
+ * {@code MyOptional!<String!>} (see <a
+ * href="https://github.com/jspecify/jspecify/wiki/notation#shorthand-notation">notation</a>).
+ * However, as specified above, they won't do that. In fact, there is a problem with the {@code
+ * firstNonNull} signature, since the type argument {@code String?} would not meet the requirements
+ * of {@code MyOptional}'s type parameter.
+ *
+ * <p>The solution is to <b>project</b> the type argument to its non-null counterpart:
+ *
+ * <pre>{@code
+ * // Returns the first non-null element, if such element exists.
+ * MyOptional<@NonNull E> firstNonNull() { … } // problem fixed!
+ * }</pre>
+ *
+ * <p>Here, {@code @NonNull E} selects the non-null form of the type argument, whether it was
+ * already non-null or not, which is just what we need in this scenario.
+ *
+ * <p>If {@code E} has a non-null upper bound, then the apparent projection {@code @NonNull E} is
+ * redundant but harmless.
+ *
+ * <p><a href="Nullable.html#projection">Nullable projection</a> serves the equivalent purpose in
+ * the opposite direction, and is far more commonly useful.
+ *
+ * <p>If a type variable has <i>all</i> its usages being projected in one direction or the other, it
+ * should be given a non-null upper bound, and any non-null projections can then be removed.
+ *
+ * <h2>Where it is not applicable</h2>
+ *
+ * <p>{@code @NonNull} is inapplicable in all the <a href="Nullable.html#applicability">same
+ * locations</a> as {@link Nullable}.
+ */
+@Documented
+@Target(TYPE_USE)
+@Retention(RUNTIME)
+public @interface NonNull {}
diff --git a/third-party/java8-annotations/org/jspecify/annotations/NullMarked.java b/third-party/java8-annotations/org/jspecify/annotations/NullMarked.java
new file mode 100644
index 00000000000..bfc987c891d
--- /dev/null
+++ b/third-party/java8-annotations/org/jspecify/annotations/NullMarked.java
@@ -0,0 +1,116 @@
+/*
+ * Copyright 2018-2020 The JSpecify Authors.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package org.jspecify.annotations;
+
+import static java.lang.annotation.ElementType.CONSTRUCTOR;
+import static java.lang.annotation.ElementType.METHOD;
+import static java.lang.annotation.ElementType.PACKAGE;
+import static java.lang.annotation.ElementType.TYPE;
+import static java.lang.annotation.RetentionPolicy.RUNTIME;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.Retention;
+import java.lang.annotation.Target;
+
+/**
+ * Indicates that the annotated element and the code transitively {@linkplain
+ * javax.lang.model.element.Element#getEnclosedElements() enclosed} within it are <b>null-marked
+ * code</b>: there, type usages are generally considered to exclude {@code null} as a value unless
+ * specified otherwise. Using this annotation avoids the need to write {@link NonNull @NonNull} many
+ * times throughout your code.
+ *
+ * <p>For a comprehensive introduction to JSpecify, please see <a
+ * href="http://jspecify.org">jspecify.org</a>.
+ *
+ * <p><b>Warning:</b> These annotations are under development, and <b>any</b> aspect of their
+ * naming, locations, or design is subject to change until the JSpecify 1.0 release. Moreover,
+ * supporting analysis tools will be tracking the changes on varying schedules. Releasing a library
+ * using these annotations in its API is <b>strongly discouraged</b> at this time.
+ *
+ * <h2 id="effects">Effects of being null-marked</h2>
+ *
+ * <p>Within null-marked code, as a <i>general</i> rule, a type usage is considered non-null (to
+ * exclude {@code null} as a value) unless explicitly annotated as {@link Nullable}. However, there
+ * are several special cases to address.
+ *
+ * <h3 id="effects-special-cases">Special cases</h3>
+ *
+ * <p>Within null-marked code:
+ *
+ * <ul>
+ *   <li>We might expect the type represented by a <b>wildcard</b> (like the {@code ?} in {@code
+ *       List<?>}) to be non-null, but it isn't necessarily. It's non-null only if it {@code
+ *       extends} a non-null type (like in {@code List<? extends String>}), or if the <i>class</i>
+ *       in use accepts only non-null type arguments (such as if {@code List} were declared as
+ *       {@code class List<E extends String>}). But if {@code List} does accept nullable type
+ *       arguments, then the wildcards seen in {@code List<?>} and {@code List<? super String>} must
+ *       include {@code null}, because they have no "upper bound". (<a
+ *       href="https://bit.ly/3ppb8ZC">Why?</a>)
+ *       <ul>
+ *         <li>Conversely, a <b>type parameter</b> is always considered to have an upper bound; when
+ *             none is given explicitly, {@code Object} is filled in by the compiler. The example
+ *             {@code class MyList<E>} is interpreted identically to {@code class MyList<E extends
+ *             Object>}: in both cases the type argument in {@code MyList<@Nullable Foo>} is
+ *             out-of-bounds, so the list elements are always non-null. (<a
+ *             href="https://bit.ly/3ppb8ZC">Why?</a>)
+ *       </ul>
+ *   <li>Otherwise, being null-marked has no consequence for any type usage where {@code @Nullable}
+ *       and {@code @NonNull} are <a href="Nullable.html#applicability"><b>not applicable</b></a>,
+ *       such as the root type of a local variable declaration.
+ *   <li>When a type variable has a nullable upper bound, such as the {@code E} in {@code class
+ *       Foo<E extends @Nullable Bar>}), an unannotated usage of this type variable is not
+ *       considered nullable, non-null, or even of "unspecified" nullness. Rather it has
+ *       <b>parametric nullness</b>. In order to support both nullable and non-null type arguments
+ *       safely, the {@code E} type itself must be handled <i>strictly</i>: as if nullable when
+ *       "read from", but as if non-null when "written to". (Contrast with {@code class Foo<E
+ *       extends Bar>}, where usages of {@code E} are simply non-null, just like usages of {@code
+ *       String} are.)
+ *   <li>By using {@link NullUnmarked}, an element within null-marked code can be excluded and made
+ *       null-unmarked, exactly as if there were no enclosing {@code @NullMarked} element at all.
+ * </ul>
+ *
+ * <h2 id="where">Where it can be used</h2>
+ *
+ * {@code @NullMarked} and {@link NullUnmarked @NullUnmarked} can be used on any package, class,
+ * method, or constructor declaration; {@code @NullMarked} can be used on a module declaration as
+ * well. Special considerations:
+ *
+ * <ul>
+ *   <li>To apply this annotation to an entire (single) <b>package</b>, create a <a
+ *       href="https://docs.oracle.com/javase/specs/jls/se19/html/jls-7.html#jls-7.4.1">{@code
+ *       package-info.java}</a> file there. This is recommended so that newly-created classes will
+ *       be null-marked by default. This annotation has no effect on "subpackages". <b>Warning</b>:
+ *       if the package does not belong to a module, be very careful: it can easily happen that
+ *       different versions of the package-info file are seen and used in different circumstances,
+ *       causing the same classes to be interpreted inconsistently. For example, a package-info file
+ *       from a {@code test} source path might hide the corresponding one from the {@code main}
+ *       source path, or generated code might be compiled without seeing a package-info file at all.
+ *   <li>Although Java permits it to be applied to a <b>record component</b> declaration (as in
+ *       {@code record Foo(@NullMarked String bar) {...}}), this annotation has no meaning when used
+ *       in that way.
+ *   <li>Applying this annotation to an instance <b>method</b> of a <i>generic</i> class is
+ *       acceptable, but is not recommended because it can lead to some confusing situations.
+ *   <li>An advantage of Java <b>modules</b> is that you can make a lot of code null-marked with
+ *       just a single annotation (before the {@code module} keyword). {@link NullUnmarked} is not
+ *       supported on modules, since it's already the default.
+ *   <li>If both {@code @NullMarked} and {@code @NullUnmarked} appear together on the same element,
+ *       <i>neither</i> one is recognized.
+ * </ul>
+ */
+@Documented
+@Target({PACKAGE, TYPE, METHOD, CONSTRUCTOR})
+@Retention(RUNTIME)
+public @interface NullMarked {}
diff --git a/third-party/java8-annotations/org/jspecify/annotations/NullUnmarked.java b/third-party/java8-annotations/org/jspecify/annotations/NullUnmarked.java
new file mode 100644
index 00000000000..36d55de6509
--- /dev/null
+++ b/third-party/java8-annotations/org/jspecify/annotations/NullUnmarked.java
@@ -0,0 +1,87 @@
+/*
+ * Copyright 2022 The JSpecify Authors.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package org.jspecify.annotations;
+
+import static java.lang.annotation.ElementType.CONSTRUCTOR;
+import static java.lang.annotation.ElementType.METHOD;
+import static java.lang.annotation.ElementType.PACKAGE;
+import static java.lang.annotation.ElementType.TYPE;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+/**
+ * Indicates that the annotated element and the code transitively {@linkplain
+ * javax.lang.model.element.Element#getEnclosedElements() enclosed} within it is <b>null-unmarked
+ * code</b>: there, type usages generally have <b>unspecified nullness</b> unless explicitly
+ * annotated otherwise.
+ *
+ * <p>This annotation's purpose is to ease migration of a large existing codebase to null-marked
+ * status. It makes it possible to "flip the default" for new code added to a class or package even
+ * before that class or package has been fully migrated. Since new code is the most important code
+ * to analyze, this is strongly recommended as a temporary measure whenever necessary. However, once
+ * a codebase has been fully migrated it would be appropriate to ban use of this annotation.
+ *
+ * <p>For a comprehensive introduction to JSpecify, please see <a
+ * href="http://jspecify.org">jspecify.org</a>.
+ *
+ * <p><b>Warning:</b> These annotations are under development, and <b>any</b> aspect of their
+ * naming, locations, or design is subject to change until the JSpecify 1.0 release. Moreover,
+ * supporting analysis tools will track with these changes on varying schedules. Releasing a library
+ * using these annotations in its API is <b>strongly discouraged</b> at this time.
+ *
+ * <h2>Null-marked and null-unmarked code</h2>
+ *
+ * <p>{@link NullMarked} and this annotation work as a pair to include and exclude sections of code
+ * from null-marked status (respectively). Specifically, code is considered null-marked if the most
+ * narrowly enclosing element annotated with either of these two annotations exists and is annotated
+ * with {@code @NullMarked}.
+ *
+ * <p>Otherwise it is considered null-unmarked. This can happen in two ways: either it is more
+ * narrowly enclosed by a {@code @NullUnmarked}-annotated element than by any
+ * {@code @NullMarked}-annotated element, or neither annotation is present on any enclosing element.
+ * No distinction is made between these cases.
+ *
+ * <p>The effects of being null-marked are described in the <a
+ * href="NullMarked.html#effects">Effects</a> section of {@code NullMarked}.
+ *
+ * <h2>Unspecified nullness</h2>
+ *
+ * <p>Within null-unmarked code, a type usage with no nullness annotation has <b>unspecified
+ * nullness</b> (<a href="https://bit.ly/3ppb8ZC">Why?</a>). This means that, while there is always
+ * <i>some</i> correct way to annotate it for nullness, that information is missing: we <i>do not
+ * know</i> whether it includes or excludes {@code null} as a value. In such a case, tools can vary
+ * widely in how strict or lenient their enforcement is, or might make it configurable.
+ *
+ * <p>For more, please see this more <a
+ * href="https://github.com/jspecify/jspecify/wiki/nullness-unspecified">comprehensive
+ * discussion</a> of unspecified nullness.
+ *
+ * <p>There is no way for an individual type usage within null-marked code to have unspecified
+ * nullness. (<a href="https://bit.ly/3ppb8ZC">Why?</a>)
+ *
+ * <h2>Where it can be used</h2>
+ *
+ * The information in the <a href="NullMarked.html#where">Where it can be used</a> section of {@code
+ * NullMarked} applies as well to this annotation.
+ */
+// TODO(kevinb9n): word the middle section better with good words
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({PACKAGE, TYPE, METHOD, CONSTRUCTOR})
+public @interface NullUnmarked {}
diff --git a/third-party/java8-annotations/org/jspecify/annotations/Nullable.java b/third-party/java8-annotations/org/jspecify/annotations/Nullable.java
new file mode 100644
index 00000000000..8d07ca3a244
--- /dev/null
+++ b/third-party/java8-annotations/org/jspecify/annotations/Nullable.java
@@ -0,0 +1,144 @@
+/*
+ * Copyright 2018-2020 The JSpecify Authors.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package org.jspecify.annotations;
+
+import static java.lang.annotation.ElementType.TYPE_USE;
+import static java.lang.annotation.RetentionPolicy.RUNTIME;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.Retention;
+import java.lang.annotation.Target;
+
+/**
+ * Indicates that the annotated <a href="https://github.com/jspecify/jspecify/wiki/type-usages">type
+ * usage</a> (commonly a parameter type or return type) is considered to include {@code null} as a
+ * value.
+ *
+ * <p>Example usages:
+ *
+ * <pre>{@code
+ * @Nullable String field;
+ *
+ * @Nullable String getField() { return field; }
+ *
+ * void setField(@Nullable String value) { field = value; }
+ *
+ * List<@Nullable String> getList() { … }
+ * }</pre>
+ *
+ * <p>For a comprehensive introduction to JSpecify, please see <a
+ * href="http://jspecify.org">jspecify.org</a>.
+ *
+ * <p><b>Warning:</b> These annotations are under development, and <b>any</b> aspect of their
+ * naming, locations, or design is subject to change until the JSpecify 1.0 release. Moreover,
+ * supporting analysis tools will be tracking the changes on varying schedules. Releasing a library
+ * using these annotations in its API is <b>strongly discouraged</b> at this time.
+ *
+ * <h2>Meaning per each kind of type usage</h2>
+ *
+ * <p>The essential meaning of this annotation is always the same: the type it annotates is
+ * considered to include {@code null} as a value. But this may affect your code a little differently
+ * based on the kind of type usage involved.
+ *
+ * <ul>
+ *   <li>On a <b>parameter type</b>: The {@code setField} method (at top) permissively accepts a
+ *       "string-or-null", meaning that it is okay to pass an actual string, or to pass {@code
+ *       null}. (This doesn't guarantee that passing {@code null} won't produce an exception at
+ *       runtime, but it should be much less likely.) This also applies to the type of a lambda
+ *       expression parameter, if that type is given explicitly (otherwise its nullness must be
+ *       inferred from context).
+ *   <li>On a <b>method return type</b>: The {@code getField} method returns a "string-or-null", so
+ *       while the caller might get a string back, it should also address the possibility of getting
+ *       {@code null} instead. (This doesn't guarantee there is any circumstance in which {@code
+ *       null} <i>will</i> actually be returned.)
+ *   <li>On a <b>field type</b>: The {@code field} field has the type "string-or-null", so at times
+ *       it might hold a string, and at times it might hold {@code null}. (Of course, every field of
+ *       a reference type <i>originally</i> holds {@code null}, but as long as the class ensures
+ *       that its uninitialized states can't be observed, it's appropriate to overlook that fact.)
+ *   <li>On a <b>type argument</b>: A type usage of "nullable string" appears <i>within</i> the
+ *       compound type {@code List<@Nullable String>}. No matter how this type is used (return type,
+ *       etc.), this means the same thing: every appearance of {@code E} in {@code List}'s member
+ *       signatures will be considered nullable. For a list, this means it may contain null
+ *       <i>elements</i>. If the list reference itself might be null as well, we can write
+ *       {@code @Nullable List<@Nullable String>}, a "nullable list of nullable strings".
+ *   <li>On the upper bound of a <b>type parameter</b>: For example, as seen in {@code class List<E
+ *       extends @Nullable Object>}. This means that a <i>type argument</i> supplied for that type
+ *       parameter is permitted to be nullable if desired: {@code List<@Nullable String>}. (A
+ *       non-null type argument, as in {@code List<String>}, is permitted either way.)
+ *   <li>On a usage of a <b>type variable</b>: A type parameter, like the {@code E} in {@code
+ *       interface List<E>}, defines a "type variable" of the same name, usable only <i>within</i>
+ *       the scope of the declaring API element. In any example using {@code String} above, a type
+ *       variable like {@code E} might appear instead. {@code @Nullable} continues to mean "or null"
+ *       as always, but notably, this works without regard to whether the type argument is
+ *       <i>already</i> nullable. For example, suppose that {@code class Foo<E extends @Nullable
+ *       Object>} has a method {@code @Nullable E eOrNull()}. Then, whether {@code foo} is of type
+ *       {@code Foo<String>} or {@code Foo<@Nullable String>}, the expression {@code foo.eOrNull()}
+ *       is nullable either way. Using {@code @Nullable E} in this way is called "nullable
+ *       projection" (<a href="NonNull.html#projection">non-null projection</a> is likewise
+ *       supported, but less commonly useful).
+ *   <li>On a <b>nested type</b>: In most examples above, in place of {@code String} we might use a
+ *       nested type such as {@code Map.Entry}. The Java syntax for annotating such a type as
+ *       nullable looks like {@code Map.@Nullable Entry}.
+ *   <li>On a <b>record component</b>: As expected, {@code @Nullable} here applies equally to the
+ *       corresponding parameter type of the canonical constructor, and to the return type of a
+ *       generated accessor method as well. If an explicit accessor method is provided for this
+ *       record component, it must still be annotated explicitly. Any non-null components should be
+ *       checked (for example using {@link java.util.Objects#requireNonNull}) in a <a
+ *       href="https://docs.oracle.com/en/java/javase/19/language/records.html">compact
+ *       constructor</a>.
+ * </ul>
+ *
+ * <h2 id="applicability">Where it is applicable</h2>
+ *
+ * <p>This annotation and {@link NonNull} are applicable to any <a
+ * href="https://github.com/jspecify/jspecify/wiki/type-usages">type usage</a> <b>except</b> the
+ * following cases, where they have no defined meaning:
+ *
+ * <ul>
+ *   <li>On any<b> intrinsically non-null type usage</b>. Some type usages are incapable of
+ *       including {@code null} by the rules of the Java language. Examples include any usage of a
+ *       primitive type, the argument to {@code instanceof}, a method return type in an annotation
+ *       interface, or the type following {@code throws} or {@code catch}. In such locations, a
+ *       nullness annotation could only be contradictory ({@code @Nullable}) or redundant
+ *       ({@code @NonNull}).
+ *   <li>On the root type of a <b>local variable</b> declaration. The nullness of a local variable
+ *       itself is not a fixed declarative property of its <i>type</i>. Rather it should be inferred
+ *       from the nullness of each expression assigned to the variable, possibly changing over time.
+ *       (<a href="https://bit.ly/3ppb8ZC">Why?</a>). Subcomponents of the type (type arguments,
+ *       array component types) are annotatable as usual.
+ *   <li>On the root type in a <b>cast expression</b>. To inform an analyzer that an expression it
+ *       sees as nullable is truly non-null, use an assertion or a method like {@link
+ *       java.util.Objects#requireNonNull}. (<a href="https://bit.ly/3ppb8ZC">Why?</a>)
+ *       Subcomponents of the type (type arguments, array component types) are annotatable as usual.
+ *   <li>On any part of a <b>receiver parameter</b> type (<a
+ *       href="https://docs.oracle.com/javase/specs/jls/se18/html/jls-8.html#jls-8.4">JLS 8.4</a>).
+ *   <li>If both {@code @Nullable} and {@code @NonNull} appear on the same type usage,
+ *       <i>neither</i> one is recognized.
+ * </ul>
+ *
+ * Whether the code is {@link NullMarked} also has no consequence in the above locations.
+ *
+ * <h2>Unannotated type usages</h2>
+ *
+ * <p>For a type usage where nullness annotations are <a href="#applicability">applicable</a> but
+ * not present, its nullness depends on whether it appears within {@linkplain NullMarked
+ * null-marked} code; see that class for details. Note in particular that nullness information from
+ * a superclass is never automatically "inherited".
+ */
+@Documented
+@Target(TYPE_USE)
+@Retention(RUNTIME)
+public @interface Nullable {}
diff --git a/third-party/java8-annotations/org/jspecify/annotations/NullnessUnspecified.java b/third-party/java8-annotations/org/jspecify/annotations/NullnessUnspecified.java
new file mode 100644
index 00000000000..0542dc79c91
--- /dev/null
+++ b/third-party/java8-annotations/org/jspecify/annotations/NullnessUnspecified.java
@@ -0,0 +1,39 @@
+/*
+ * Copyright 2018-2020 The JSpecify Authors.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package org.jspecify.annotations;
+
+import static java.lang.annotation.ElementType.TYPE_USE;
+import static java.lang.annotation.RetentionPolicy.RUNTIME;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.Retention;
+import java.lang.annotation.Target;
+
+/*
+
+
+        This is a fake annotation that does not exist in the JSpecify 
+        release, and with no expectation of being added!
+
+        Once Kotlin supports @NullUnmarked, the tests can be updated
+        and this should be removed.
+
+
+ */
+@Documented
+@Target(TYPE_USE)
+@Retention(RUNTIME)
+public @interface NullnessUnspecified {}
diff --git a/third-party/java9-annotations/module-info.java b/third-party/java9-annotations/module-info.java
index 77450ed8425..8e1110f355b 100644
--- a/third-party/java9-annotations/module-info.java
+++ b/third-party/java9-annotations/module-info.java
@@ -1,4 +1,5 @@
 module java9_annotations {
+    exports org.jspecify.annotations;
     exports org.jspecify.nullness;
     // add packages needed to export
-}
\ No newline at end of file
+}
diff --git a/third-party/java9-annotations/org/jspecify/annotations/NonNull.java b/third-party/java9-annotations/org/jspecify/annotations/NonNull.java
new file mode 100644
index 00000000000..771c769564c
--- /dev/null
+++ b/third-party/java9-annotations/org/jspecify/annotations/NonNull.java
@@ -0,0 +1,101 @@
+/*
+ * Copyright 2022 The JSpecify Authors.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package org.jspecify.annotations;
+
+import static java.lang.annotation.ElementType.TYPE_USE;
+import static java.lang.annotation.RetentionPolicy.RUNTIME;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.Retention;
+import java.lang.annotation.Target;
+
+/**
+ * Indicates that the annotated <a href="https://github.com/jspecify/jspecify/wiki/type-usages">type
+ * usage</a> (commonly a parameter type or return type) is considered to <i>exclude</i> {@code null}
+ * as a value; rarely needed within {@linkplain NullMarked null-marked} code.
+ *
+ * <p>This annotation serves two primary purposes:
+ *
+ * <ul>
+ *   <li>To mark any sporadic non-null type usages inside a scope that is not ready to be fully
+ *       {@link NullMarked} yet.
+ *   <li>To perform a <i>non-null projection</i> of a type variable, explained below.
+ * </ul>
+ *
+ * <p>For a comprehensive introduction to JSpecify, please see <a
+ * href="http://jspecify.org">jspecify.org</a>.
+ *
+ * <p><b>Warning:</b> These annotations are under development, and <b>any</b> aspect of their
+ * naming, locations, or design is subject to change until the JSpecify 1.0 release. Moreover,
+ * supporting analysis tools will be tracking the changes on varying schedules. Releasing a library
+ * using these annotations in its API is <b>strongly discouraged</b> at this time.
+ *
+ * <h2 id="projection">Non-null projection</h2>
+ *
+ * <p>In the following example, {@code MyOptional}'s type parameter {@code T} accepts only non-null
+ * type arguments, but {@code MyList}'s type parameter {@code E} will accept either a non-null or
+ * nullable type argument.
+ *
+ * <pre>{@code
+ * // All the below is null-marked code
+ *
+ * class MyOptional<T> { … }
+ *
+ * interface MyList<E extends @Nullable Object> {
+ *   // Returns the first non-null element, if such element exists.
+ *   MyOptional<E> firstNonNull() { … } // problem here!
+ * }
+ *
+ * MyList<@Nullable String> maybeNulls = …
+ * MyList<String> nonNulls = …
+ * }</pre>
+ *
+ * <p>Because {@code MyOptional} accepts only non-null type arguments, we need both {@code
+ * maybeNulls.firstNonNull()} and {@code nonNulls.firstNonNull()} to produce the same return type:
+ * {@code MyOptional!<String!>} (see <a
+ * href="https://github.com/jspecify/jspecify/wiki/notation#shorthand-notation">notation</a>).
+ * However, as specified above, they won't do that. In fact, there is a problem with the {@code
+ * firstNonNull} signature, since the type argument {@code String?} would not meet the requirements
+ * of {@code MyOptional}'s type parameter.
+ *
+ * <p>The solution is to <b>project</b> the type argument to its non-null counterpart:
+ *
+ * <pre>{@code
+ * // Returns the first non-null element, if such element exists.
+ * MyOptional<@NonNull E> firstNonNull() { … } // problem fixed!
+ * }</pre>
+ *
+ * <p>Here, {@code @NonNull E} selects the non-null form of the type argument, whether it was
+ * already non-null or not, which is just what we need in this scenario.
+ *
+ * <p>If {@code E} has a non-null upper bound, then the apparent projection {@code @NonNull E} is
+ * redundant but harmless.
+ *
+ * <p><a href="Nullable.html#projection">Nullable projection</a> serves the equivalent purpose in
+ * the opposite direction, and is far more commonly useful.
+ *
+ * <p>If a type variable has <i>all</i> its usages being projected in one direction or the other, it
+ * should be given a non-null upper bound, and any non-null projections can then be removed.
+ *
+ * <h2>Where it is not applicable</h2>
+ *
+ * <p>{@code @NonNull} is inapplicable in all the <a href="Nullable.html#applicability">same
+ * locations</a> as {@link Nullable}.
+ */
+@Documented
+@Target(TYPE_USE)
+@Retention(RUNTIME)
+public @interface NonNull {}
diff --git a/third-party/java9-annotations/org/jspecify/annotations/NullMarked.java b/third-party/java9-annotations/org/jspecify/annotations/NullMarked.java
new file mode 100644
index 00000000000..a8752e68945
--- /dev/null
+++ b/third-party/java9-annotations/org/jspecify/annotations/NullMarked.java
@@ -0,0 +1,117 @@
+/*
+ * Copyright 2018-2020 The JSpecify Authors.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package org.jspecify.annotations;
+
+import static java.lang.annotation.ElementType.CONSTRUCTOR;
+import static java.lang.annotation.ElementType.METHOD;
+import static java.lang.annotation.ElementType.MODULE;
+import static java.lang.annotation.ElementType.PACKAGE;
+import static java.lang.annotation.ElementType.TYPE;
+import static java.lang.annotation.RetentionPolicy.RUNTIME;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.Retention;
+import java.lang.annotation.Target;
+
+/**
+ * Indicates that the annotated element and the code transitively {@linkplain
+ * javax.lang.model.element.Element#getEnclosedElements() enclosed} within it are <b>null-marked
+ * code</b>: there, type usages are generally considered to exclude {@code null} as a value unless
+ * specified otherwise. Using this annotation avoids the need to write {@link NonNull @NonNull} many
+ * times throughout your code.
+ *
+ * <p>For a comprehensive introduction to JSpecify, please see <a
+ * href="http://jspecify.org">jspecify.org</a>.
+ *
+ * <p><b>Warning:</b> These annotations are under development, and <b>any</b> aspect of their
+ * naming, locations, or design is subject to change until the JSpecify 1.0 release. Moreover,
+ * supporting analysis tools will be tracking the changes on varying schedules. Releasing a library
+ * using these annotations in its API is <b>strongly discouraged</b> at this time.
+ *
+ * <h2 id="effects">Effects of being null-marked</h2>
+ *
+ * <p>Within null-marked code, as a <i>general</i> rule, a type usage is considered non-null (to
+ * exclude {@code null} as a value) unless explicitly annotated as {@link Nullable}. However, there
+ * are several special cases to address.
+ *
+ * <h3 id="effects-special-cases">Special cases</h3>
+ *
+ * <p>Within null-marked code:
+ *
+ * <ul>
+ *   <li>We might expect the type represented by a <b>wildcard</b> (like the {@code ?} in {@code
+ *       List<?>}) to be non-null, but it isn't necessarily. It's non-null only if it {@code
+ *       extends} a non-null type (like in {@code List<? extends String>}), or if the <i>class</i>
+ *       in use accepts only non-null type arguments (such as if {@code List} were declared as
+ *       {@code class List<E extends String>}). But if {@code List} does accept nullable type
+ *       arguments, then the wildcards seen in {@code List<?>} and {@code List<? super String>} must
+ *       include {@code null}, because they have no "upper bound". (<a
+ *       href="https://bit.ly/3ppb8ZC">Why?</a>)
+ *       <ul>
+ *         <li>Conversely, a <b>type parameter</b> is always considered to have an upper bound; when
+ *             none is given explicitly, {@code Object} is filled in by the compiler. The example
+ *             {@code class MyList<E>} is interpreted identically to {@code class MyList<E extends
+ *             Object>}: in both cases the type argument in {@code MyList<@Nullable Foo>} is
+ *             out-of-bounds, so the list elements are always non-null. (<a
+ *             href="https://bit.ly/3ppb8ZC">Why?</a>)
+ *       </ul>
+ *   <li>Otherwise, being null-marked has no consequence for any type usage where {@code @Nullable}
+ *       and {@code @NonNull} are <a href="Nullable.html#applicability"><b>not applicable</b></a>,
+ *       such as the root type of a local variable declaration.
+ *   <li>When a type variable has a nullable upper bound, such as the {@code E} in {@code class
+ *       Foo<E extends @Nullable Bar>}), an unannotated usage of this type variable is not
+ *       considered nullable, non-null, or even of "unspecified" nullness. Rather it has
+ *       <b>parametric nullness</b>. In order to support both nullable and non-null type arguments
+ *       safely, the {@code E} type itself must be handled <i>strictly</i>: as if nullable when
+ *       "read from", but as if non-null when "written to". (Contrast with {@code class Foo<E
+ *       extends Bar>}, where usages of {@code E} are simply non-null, just like usages of {@code
+ *       String} are.)
+ *   <li>By using {@link NullUnmarked}, an element within null-marked code can be excluded and made
+ *       null-unmarked, exactly as if there were no enclosing {@code @NullMarked} element at all.
+ * </ul>
+ *
+ * <h2 id="where">Where it can be used</h2>
+ *
+ * {@code @NullMarked} and {@link NullUnmarked @NullUnmarked} can be used on any package, class,
+ * method, or constructor declaration; {@code @NullMarked} can be used on a module declaration as
+ * well. Special considerations:
+ *
+ * <ul>
+ *   <li>To apply this annotation to an entire (single) <b>package</b>, create a <a
+ *       href="https://docs.oracle.com/javase/specs/jls/se19/html/jls-7.html#jls-7.4.1">{@code
+ *       package-info.java}</a> file there. This is recommended so that newly-created classes will
+ *       be null-marked by default. This annotation has no effect on "subpackages". <b>Warning</b>:
+ *       if the package does not belong to a module, be very careful: it can easily happen that
+ *       different versions of the package-info file are seen and used in different circumstances,
+ *       causing the same classes to be interpreted inconsistently. For example, a package-info file
+ *       from a {@code test} source path might hide the corresponding one from the {@code main}
+ *       source path, or generated code might be compiled without seeing a package-info file at all.
+ *   <li>Although Java permits it to be applied to a <b>record component</b> declaration (as in
+ *       {@code record Foo(@NullMarked String bar) {...}}), this annotation has no meaning when used
+ *       in that way.
+ *   <li>Applying this annotation to an instance <b>method</b> of a <i>generic</i> class is
+ *       acceptable, but is not recommended because it can lead to some confusing situations.
+ *   <li>An advantage of Java <b>modules</b> is that you can make a lot of code null-marked with
+ *       just a single annotation (before the {@code module} keyword). {@link NullUnmarked} is not
+ *       supported on modules, since it's already the default.
+ *   <li>If both {@code @NullMarked} and {@code @NullUnmarked} appear together on the same element,
+ *       <i>neither</i> one is recognized.
+ * </ul>
+ */
+@Documented
+@Target({MODULE, PACKAGE, TYPE, METHOD, CONSTRUCTOR})
+@Retention(RUNTIME)
+public @interface NullMarked {}
diff --git a/third-party/java9-annotations/org/jspecify/annotations/NullUnmarked.java b/third-party/java9-annotations/org/jspecify/annotations/NullUnmarked.java
new file mode 100644
index 00000000000..36d55de6509
--- /dev/null
+++ b/third-party/java9-annotations/org/jspecify/annotations/NullUnmarked.java
@@ -0,0 +1,87 @@
+/*
+ * Copyright 2022 The JSpecify Authors.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package org.jspecify.annotations;
+
+import static java.lang.annotation.ElementType.CONSTRUCTOR;
+import static java.lang.annotation.ElementType.METHOD;
+import static java.lang.annotation.ElementType.PACKAGE;
+import static java.lang.annotation.ElementType.TYPE;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+/**
+ * Indicates that the annotated element and the code transitively {@linkplain
+ * javax.lang.model.element.Element#getEnclosedElements() enclosed} within it is <b>null-unmarked
+ * code</b>: there, type usages generally have <b>unspecified nullness</b> unless explicitly
+ * annotated otherwise.
+ *
+ * <p>This annotation's purpose is to ease migration of a large existing codebase to null-marked
+ * status. It makes it possible to "flip the default" for new code added to a class or package even
+ * before that class or package has been fully migrated. Since new code is the most important code
+ * to analyze, this is strongly recommended as a temporary measure whenever necessary. However, once
+ * a codebase has been fully migrated it would be appropriate to ban use of this annotation.
+ *
+ * <p>For a comprehensive introduction to JSpecify, please see <a
+ * href="http://jspecify.org">jspecify.org</a>.
+ *
+ * <p><b>Warning:</b> These annotations are under development, and <b>any</b> aspect of their
+ * naming, locations, or design is subject to change until the JSpecify 1.0 release. Moreover,
+ * supporting analysis tools will track with these changes on varying schedules. Releasing a library
+ * using these annotations in its API is <b>strongly discouraged</b> at this time.
+ *
+ * <h2>Null-marked and null-unmarked code</h2>
+ *
+ * <p>{@link NullMarked} and this annotation work as a pair to include and exclude sections of code
+ * from null-marked status (respectively). Specifically, code is considered null-marked if the most
+ * narrowly enclosing element annotated with either of these two annotations exists and is annotated
+ * with {@code @NullMarked}.
+ *
+ * <p>Otherwise it is considered null-unmarked. This can happen in two ways: either it is more
+ * narrowly enclosed by a {@code @NullUnmarked}-annotated element than by any
+ * {@code @NullMarked}-annotated element, or neither annotation is present on any enclosing element.
+ * No distinction is made between these cases.
+ *
+ * <p>The effects of being null-marked are described in the <a
+ * href="NullMarked.html#effects">Effects</a> section of {@code NullMarked}.
+ *
+ * <h2>Unspecified nullness</h2>
+ *
+ * <p>Within null-unmarked code, a type usage with no nullness annotation has <b>unspecified
+ * nullness</b> (<a href="https://bit.ly/3ppb8ZC">Why?</a>). This means that, while there is always
+ * <i>some</i> correct way to annotate it for nullness, that information is missing: we <i>do not
+ * know</i> whether it includes or excludes {@code null} as a value. In such a case, tools can vary
+ * widely in how strict or lenient their enforcement is, or might make it configurable.
+ *
+ * <p>For more, please see this more <a
+ * href="https://github.com/jspecify/jspecify/wiki/nullness-unspecified">comprehensive
+ * discussion</a> of unspecified nullness.
+ *
+ * <p>There is no way for an individual type usage within null-marked code to have unspecified
+ * nullness. (<a href="https://bit.ly/3ppb8ZC">Why?</a>)
+ *
+ * <h2>Where it can be used</h2>
+ *
+ * The information in the <a href="NullMarked.html#where">Where it can be used</a> section of {@code
+ * NullMarked} applies as well to this annotation.
+ */
+// TODO(kevinb9n): word the middle section better with good words
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({PACKAGE, TYPE, METHOD, CONSTRUCTOR})
+public @interface NullUnmarked {}
diff --git a/third-party/java9-annotations/org/jspecify/annotations/Nullable.java b/third-party/java9-annotations/org/jspecify/annotations/Nullable.java
new file mode 100644
index 00000000000..8d07ca3a244
--- /dev/null
+++ b/third-party/java9-annotations/org/jspecify/annotations/Nullable.java
@@ -0,0 +1,144 @@
+/*
+ * Copyright 2018-2020 The JSpecify Authors.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package org.jspecify.annotations;
+
+import static java.lang.annotation.ElementType.TYPE_USE;
+import static java.lang.annotation.RetentionPolicy.RUNTIME;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.Retention;
+import java.lang.annotation.Target;
+
+/**
+ * Indicates that the annotated <a href="https://github.com/jspecify/jspecify/wiki/type-usages">type
+ * usage</a> (commonly a parameter type or return type) is considered to include {@code null} as a
+ * value.
+ *
+ * <p>Example usages:
+ *
+ * <pre>{@code
+ * @Nullable String field;
+ *
+ * @Nullable String getField() { return field; }
+ *
+ * void setField(@Nullable String value) { field = value; }
+ *
+ * List<@Nullable String> getList() { … }
+ * }</pre>
+ *
+ * <p>For a comprehensive introduction to JSpecify, please see <a
+ * href="http://jspecify.org">jspecify.org</a>.
+ *
+ * <p><b>Warning:</b> These annotations are under development, and <b>any</b> aspect of their
+ * naming, locations, or design is subject to change until the JSpecify 1.0 release. Moreover,
+ * supporting analysis tools will be tracking the changes on varying schedules. Releasing a library
+ * using these annotations in its API is <b>strongly discouraged</b> at this time.
+ *
+ * <h2>Meaning per each kind of type usage</h2>
+ *
+ * <p>The essential meaning of this annotation is always the same: the type it annotates is
+ * considered to include {@code null} as a value. But this may affect your code a little differently
+ * based on the kind of type usage involved.
+ *
+ * <ul>
+ *   <li>On a <b>parameter type</b>: The {@code setField} method (at top) permissively accepts a
+ *       "string-or-null", meaning that it is okay to pass an actual string, or to pass {@code
+ *       null}. (This doesn't guarantee that passing {@code null} won't produce an exception at
+ *       runtime, but it should be much less likely.) This also applies to the type of a lambda
+ *       expression parameter, if that type is given explicitly (otherwise its nullness must be
+ *       inferred from context).
+ *   <li>On a <b>method return type</b>: The {@code getField} method returns a "string-or-null", so
+ *       while the caller might get a string back, it should also address the possibility of getting
+ *       {@code null} instead. (This doesn't guarantee there is any circumstance in which {@code
+ *       null} <i>will</i> actually be returned.)
+ *   <li>On a <b>field type</b>: The {@code field} field has the type "string-or-null", so at times
+ *       it might hold a string, and at times it might hold {@code null}. (Of course, every field of
+ *       a reference type <i>originally</i> holds {@code null}, but as long as the class ensures
+ *       that its uninitialized states can't be observed, it's appropriate to overlook that fact.)
+ *   <li>On a <b>type argument</b>: A type usage of "nullable string" appears <i>within</i> the
+ *       compound type {@code List<@Nullable String>}. No matter how this type is used (return type,
+ *       etc.), this means the same thing: every appearance of {@code E} in {@code List}'s member
+ *       signatures will be considered nullable. For a list, this means it may contain null
+ *       <i>elements</i>. If the list reference itself might be null as well, we can write
+ *       {@code @Nullable List<@Nullable String>}, a "nullable list of nullable strings".
+ *   <li>On the upper bound of a <b>type parameter</b>: For example, as seen in {@code class List<E
+ *       extends @Nullable Object>}. This means that a <i>type argument</i> supplied for that type
+ *       parameter is permitted to be nullable if desired: {@code List<@Nullable String>}. (A
+ *       non-null type argument, as in {@code List<String>}, is permitted either way.)
+ *   <li>On a usage of a <b>type variable</b>: A type parameter, like the {@code E} in {@code
+ *       interface List<E>}, defines a "type variable" of the same name, usable only <i>within</i>
+ *       the scope of the declaring API element. In any example using {@code String} above, a type
+ *       variable like {@code E} might appear instead. {@code @Nullable} continues to mean "or null"
+ *       as always, but notably, this works without regard to whether the type argument is
+ *       <i>already</i> nullable. For example, suppose that {@code class Foo<E extends @Nullable
+ *       Object>} has a method {@code @Nullable E eOrNull()}. Then, whether {@code foo} is of type
+ *       {@code Foo<String>} or {@code Foo<@Nullable String>}, the expression {@code foo.eOrNull()}
+ *       is nullable either way. Using {@code @Nullable E} in this way is called "nullable
+ *       projection" (<a href="NonNull.html#projection">non-null projection</a> is likewise
+ *       supported, but less commonly useful).
+ *   <li>On a <b>nested type</b>: In most examples above, in place of {@code String} we might use a
+ *       nested type such as {@code Map.Entry}. The Java syntax for annotating such a type as
+ *       nullable looks like {@code Map.@Nullable Entry}.
+ *   <li>On a <b>record component</b>: As expected, {@code @Nullable} here applies equally to the
+ *       corresponding parameter type of the canonical constructor, and to the return type of a
+ *       generated accessor method as well. If an explicit accessor method is provided for this
+ *       record component, it must still be annotated explicitly. Any non-null components should be
+ *       checked (for example using {@link java.util.Objects#requireNonNull}) in a <a
+ *       href="https://docs.oracle.com/en/java/javase/19/language/records.html">compact
+ *       constructor</a>.
+ * </ul>
+ *
+ * <h2 id="applicability">Where it is applicable</h2>
+ *
+ * <p>This annotation and {@link NonNull} are applicable to any <a
+ * href="https://github.com/jspecify/jspecify/wiki/type-usages">type usage</a> <b>except</b> the
+ * following cases, where they have no defined meaning:
+ *
+ * <ul>
+ *   <li>On any<b> intrinsically non-null type usage</b>. Some type usages are incapable of
+ *       including {@code null} by the rules of the Java language. Examples include any usage of a
+ *       primitive type, the argument to {@code instanceof}, a method return type in an annotation
+ *       interface, or the type following {@code throws} or {@code catch}. In such locations, a
+ *       nullness annotation could only be contradictory ({@code @Nullable}) or redundant
+ *       ({@code @NonNull}).
+ *   <li>On the root type of a <b>local variable</b> declaration. The nullness of a local variable
+ *       itself is not a fixed declarative property of its <i>type</i>. Rather it should be inferred
+ *       from the nullness of each expression assigned to the variable, possibly changing over time.
+ *       (<a href="https://bit.ly/3ppb8ZC">Why?</a>). Subcomponents of the type (type arguments,
+ *       array component types) are annotatable as usual.
+ *   <li>On the root type in a <b>cast expression</b>. To inform an analyzer that an expression it
+ *       sees as nullable is truly non-null, use an assertion or a method like {@link
+ *       java.util.Objects#requireNonNull}. (<a href="https://bit.ly/3ppb8ZC">Why?</a>)
+ *       Subcomponents of the type (type arguments, array component types) are annotatable as usual.
+ *   <li>On any part of a <b>receiver parameter</b> type (<a
+ *       href="https://docs.oracle.com/javase/specs/jls/se18/html/jls-8.html#jls-8.4">JLS 8.4</a>).
+ *   <li>If both {@code @Nullable} and {@code @NonNull} appear on the same type usage,
+ *       <i>neither</i> one is recognized.
+ * </ul>
+ *
+ * Whether the code is {@link NullMarked} also has no consequence in the above locations.
+ *
+ * <h2>Unannotated type usages</h2>
+ *
+ * <p>For a type usage where nullness annotations are <a href="#applicability">applicable</a> but
+ * not present, its nullness depends on whether it appears within {@linkplain NullMarked
+ * null-marked} code; see that class for details. Note in particular that nullness information from
+ * a superclass is never automatically "inherited".
+ */
+@Documented
+@Target(TYPE_USE)
+@Retention(RUNTIME)
+public @interface Nullable {}
diff --git a/third-party/java9-annotations/org/jspecify/annotations/NullnessUnspecified.java b/third-party/java9-annotations/org/jspecify/annotations/NullnessUnspecified.java
new file mode 100644
index 00000000000..0542dc79c91
--- /dev/null
+++ b/third-party/java9-annotations/org/jspecify/annotations/NullnessUnspecified.java
@@ -0,0 +1,39 @@
+/*
+ * Copyright 2018-2020 The JSpecify Authors.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package org.jspecify.annotations;
+
+import static java.lang.annotation.ElementType.TYPE_USE;
+import static java.lang.annotation.RetentionPolicy.RUNTIME;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.Retention;
+import java.lang.annotation.Target;
+
+/*
+
+
+        This is a fake annotation that does not exist in the JSpecify 
+        release, and with no expectation of being added!
+
+        Once Kotlin supports @NullUnmarked, the tests can be updated
+        and this should be removed.
+
+
+ */
+@Documented
+@Target(TYPE_USE)
+@Retention(RUNTIME)
+public @interface NullnessUnspecified {}