Conversation
Replace the global/block split (and the `block_wit` typeclass) in the
`is_send_across` subsystem with one generic, location-polymorphic weakening
instance per resource.
Background
----------
A kernel's `kpre`/`kpost` are `block_of` goals that mix global arrays (e.g.
`a |-> va`) with block/shared-memory arrays (e.g. an Array1 view of an shmem
cell). Resolving them previously relied on:
- per-resource `is_send_across_global_*` instances guarded by `{ is_global a }`,
- a `gpu_of -> block_of` lift instance, and
- a `block_wit` typeclass to make a separate block instance backtrack.
For a block array the lift was picked first, the global instance's `is_global`
refinement was deferred to SMT, and the proof failed with no backtracking. The
`block_wit` workaround functioned but duplicated every instance and forced
explicit `is_send_across_exists`/`star` assembly in the kernels.
New design
----------
Each resource now has exactly one instance
`is_send_across v (pts_to a)` for `v : visibility { vis_refines v (visibility_of (core a)) }`
that weakens the resource's home-visibility sendability to any finer `v`. This
subsumes the global case (`v = gpu_of`, reflexive), the block case
(`v = block_of`, reflexive for shmem arrays), and the old lift (`block_of`
refines `gpu_of`). Layers delegate down to the base
`is_send_pts_to_slice_weaken`; whole-array instances are just `solve`.
`Kuiper.Locs` gains `vis_refines` (kept abstract so it never unfolds into a
quantifier in unrelated contexts), its eliminator, and two narrow SMT-pattern
lemmas (`vis_refines_refl`, `vis_refines_block_gpu`) that fire only on
`vis_refines` terms. This avoids polluting arithmetic-heavy proofs (an earlier
broad `block_of` SMT pattern destabilized the tiled GEMM kernels).
The `gpu_of -> block_of` lift is no longer an instance: as an instance it is
greedily chosen ahead of the per-resource instances for concrete block arrays
and then fails. It survives as the explicit combinator `send_gpu_block`, used by
hand in `Kuiper.Kernel.Casts` (`pad_kn_sendable`, `kn_as_kmn`, `km1_as_kmn`,
`k11_as_k1n`) where the padded `kpre`/`kpost` are abstract slprops with no
per-resource instance to match.
Result
------
- `block_wit` and the duplicated global/block instances are removed.
- The four HReduce kernels' `kpre_sendable`/`kpost_sendable` are now plain
`solve` (no helpers, no explicit existential assembly).
- `gpu_ref` sendability is likewise generalized to any `v` refining `gpu_of`.
- Full `make verify` passes (275 modules).
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…tance
The base whole-array `pts_to` sendability in Kuiper.Array.Core was a magic()
stub ("Should extend Pulse.Lib.Array.PtsTo"), which forced every kernel whose
full_pre/kpre held a raw larray (or sparse matrix) to use magic() for its
sendable proof. This derives it for real and unblocks several of those sites.
Kuiper.Array.Core:
- is_send_across_pts_to_whole: prove `is_send_across (visibility_of_array x)
(pts_to x s)` by reinterpreting the whole array as a full pts_to_slice
(array_to_slice), moving that across locations (it is sendable), and
converting back (slice_to_array). Pulse only proves the *masked* pts_to at
visibility level, and the whole pts_to is `exists* s'. pts_to_mask s' full`,
so the slice route reuses the already-real masked sendability. Replaces the
magic() base instance.
- is_send_pts_to_raw (fsti): a single instance stated on the *named* raw
`A.pts_to` (not the `pts_to` typeclass method). The class method, the `frac`
wrapper (`x |-> Frac f v`) and the `lseq` wrapper are all pulse_unfold and
reduce to `A.pts_to`, so one instance serves array, larray, frac- and
lseq-keyed goals — the cases the per-type class instances missed because TC
does not unfold those wrappers. This is the analogue of how is_send_tensor /
is_send_array2 key on their named pts_to.
Kuiper.Sparse.Matrix:
- is_send_smatrix: a sparse matrix is the existential star of its three backing
larrays plus a placeless pure fact; with the raw instance above, solve now
assembles it (guards discharged via the vis_refines SMTPats for global
matrices).
Sendable proofs flipped from magic() to solve:
- DotProduct.Poly: full_pre_sendable / full_post_sendable (raw larray `live`).
- Sparse.GEMM: kpre_sendable / kpost_sendable (smatrix + array2 + cells).
SPMM's four sendables remain magic(): they additionally need is_global facts
for the block-level resources and run into shmem implicit-inference, which is a
separate concern. Full `make verify` is green.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Removes the last four magic() sendable stubs (block_pre/block_post/kpre/kpost
in the SPMM kernel descriptor), so no kernel descriptor in the repo carries a
magic() sendable anymore.
Kuiper.ForEvery:
- is_send_when__: sendability of a guarded resource [when__ p q]. It is [q ()]
when p holds and emp otherwise, so it is sendable whenever q is sendable under
the proof of p. This proof is also what types the guarded payload (e.g. an
in-bounds matrix-cell column index), which is why solving the SPMM block
predicates previously failed with "expected natlt cols, got int": without this
instance, solve unfolded when__ and re-elaborated the cell index outside the
guard.
Kuiper.Sparse.SPMM (+ Klas.SPMM.Inst):
- Thread an is_global_array refinement on row_indices through the kdesc, spmm
and inst signatures (.fst and .fsti), matching the existing is_global facts on
gA/gB/gC. It is needed to discharge vis_refines _ (visibility_of row_indices)
for the row-index array, which lives on the GPU like the other inputs.
- Extract the four sendable proofs into top-level helpers
(block_pre/post_sendable_pf, kpre/kpost_sendable_pf). Two reasons:
* Solving block_pre and block_post inline in the same record literal made the
shared [_ /. allthreads p] permission arithmetic ill-typed (each solves
fine in isolation); top-level definitions elaborate independently.
* kpre/kpost add the two shared-memory arrays as [exists* s. fst sh |-> Frac]
/ [live (fst sh)], which is definitionally [live_c_shmem (fst sh)]. solve
does not rewrite the existential form into live_c_shmem, so we apply the
dedicated is_send_across_live_c_shmem instance explicitly (it also handles
the c_shmem type reduction and block visibility from the c_shmems_inv
witness), and weaken block_pre/post to block_of via solve.
Full make verify is green.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This fixes the admitted proofs about sendability by tweaking the instance hierarchy. Needs review