cuda-oxide: preserve rustc reference attributes on kernels

cuda-oxide/crates/cuda-device/src/atomic.rs

@@ -201,8 +201,10 @@ macro_rules! define_integer_atomic {
             ///   atomic and non-atomic access to the same location is UB.
             /// * For block-scoped types, only threads in the same thread block
             ///   may access this memory.
-            /// * For system-scoped types, the memory must be reachable by both
-            ///   the GPU and the CPU (unified memory).
+            /// * The memory and concurrently accessing threads must support
+            ///   the chosen scope. System scope permits device memory accessed
+            ///   only by threads on one GPU; CPU or peer-GPU access must satisfy
+            ///   the [CUDA atomicity requirements](https://docs.nvidia.com/cuda/cuda-programming-guide/05-appendices/cuda-cpp-memory-model.html#atomicity).
             #[inline(always)]
             pub const unsafe fn from_ptr<'a>(ptr: *mut $ty) -> &'a Self {
                 // SAFETY: `Self` is `#[repr(transparent)]` over `UnsafeCell<$ty>`,
@@ -388,7 +390,9 @@ macro_rules! define_float_atomic {
             ///   the entire lifetime `'a`.
             /// * No non-atomic accesses to `*ptr` may occur during `'a`.
             /// * Block-scoped: only same-block threads may access.
-            ///   System-scoped: memory must be reachable by GPU and CPU.
+            /// * The memory and concurrently accessing threads must support
+            ///   the chosen scope, as described on the integer atomic types.
+            ///   System scope permits device memory accessed only by one GPU.
             #[inline(always)]
             pub const unsafe fn from_ptr<'a>(ptr: *mut $ty) -> &'a Self {
                 // SAFETY: `Self` is `#[repr(transparent)]` over `UnsafeCell<$ty>`,

cuda-oxide/crates/dialect-mir/src/attributes.rs

@@ -79,19 +79,31 @@ pub struct MutabilityAttr(pub bool);
 /// Proven validity facts for one Rust-reference kernel parameter.
 ///
 /// Presence of this attribute means the source argument is a Rust reference
-/// proven non-null by `rustc_public`. The payload is the pointee alignment in
-/// bytes; it must be a non-zero power of two. LLVM `align 1` is redundant and
+/// proven non-null by `rustc_public`. Pointee alignment is in bytes and must
+/// be a non-zero power of two. LLVM `align 1` is redundant and
 /// is omitted during export, but retaining `1` here keeps the proof complete.
 ///
 /// The attribute is stored on `mir.func` under a source-argument-indexed key.
-/// It intentionally carries no aliasing or dereferenceability promise.
-#[pliron_attr(
-    name = "mir.reference_param_validity",
-    format = "$0",
-    verifier = "succ"
-)]
+/// Additional promises are independently proven by the importer. A zero
+/// dereferenceable byte count records no dereferenceability promise.
+#[pliron_attr(name = "mir.reference_param_validity", format, verifier = "succ")]
 #[derive(PartialEq, Eq, Clone, Copy, Debug, Hash)]
-pub struct ReferenceParamValidityAttr(pub u64);
+pub struct ReferenceParamValidityAttr {
+    pub pointee_alignment: u64,
+    pub no_alias: bool,
+    pub dereferenceable_bytes: u64,
+}
+
+impl ReferenceParamValidityAttr {
+    /// Non-nullness and alignment, without additional reference promises.
+    pub const fn new(pointee_alignment: u64) -> Self {
+        Self {
+            pointee_alignment,
+            no_alias: false,
+            dereferenceable_bytes: 0,
+        }
+    }
+}
 
 /// Structural field index for aggregate access ops
 /// (`mir.extract_field`, `mir.insert_field`, `mir.field_addr`, `mir.enum_payload`).

cuda-oxide/crates/dialect-mir/src/ops/function.rs

@@ -66,7 +66,7 @@ fn reference_param_validity_key(index: usize) -> Identifier {
 /// |----------------|-----------|------------------------------------|
 /// | `sym_name`     | StringAttr| Function name (from SymbolOpInterface) |
 /// | `mir_func_type`| TypeAttr  | Function type (mir.func_type)      |
-/// | `reference_param_validity_N` | ReferenceParamValidityAttr | Proven nonnull/alignment for source argument `N` on a kernel entry |
+/// | `reference_param_validity_N` | ReferenceParamValidityAttr | Proven reference facts for source argument `N` on a kernel entry |
 /// ```
 ///
 /// # Verification
@@ -116,8 +116,9 @@ impl MirFuncOp {
 
     /// Record rustc-proven validity for one source-level kernel argument.
     ///
-    /// Presence proves `nonnull`; the payload carries the rustc ABI alignment
-    /// of the pointee. The source argument index is deliberately retained until
+    /// Presence proves `nonnull`; the payload carries the pointee alignment
+    /// and independently proven aliasing and size facts.
+    /// The source argument index is deliberately retained until
     /// kernel ABI lowering decides which physical LLVM parameter represents it.
     pub fn set_reference_param_validity(
         &self,
@@ -285,12 +286,12 @@ impl Verify for MirFuncOp {
                     key_text
                 );
             };
-            if validity.0 == 0 || !validity.0.is_power_of_two() {
+            if validity.pointee_alignment == 0 || !validity.pointee_alignment.is_power_of_two() {
                 return verify_err!(
                     op.loc(),
                     "MirFuncOp reference validity alignment on argument {} must be a non-zero power of two, found {}",
                     index,
-                    validity.0
+                    validity.pointee_alignment
                 );
             }
 

cuda-oxide/crates/dialect-mir/tests/ops_test/scalars_and_funcs.rs

@@ -510,43 +510,50 @@ fn test_mir_func_reference_param_validity_verify() {
     };
 
     let valid = make_func(&mut ctx, true);
-    valid.set_reference_param_validity(&mut ctx, 0, ReferenceParamValidityAttr(4));
-    valid.set_reference_param_validity(&mut ctx, 1, ReferenceParamValidityAttr(4));
+    valid.set_reference_param_validity(
+        &mut ctx,
+        0,
+        ReferenceParamValidityAttr {
+            dereferenceable_bytes: 4,
+            ..ReferenceParamValidityAttr::new(4)
+        },
+    );
+    valid.set_reference_param_validity(&mut ctx, 1, ReferenceParamValidityAttr::new(4));
     assert!(
         valid.verify(&ctx).is_ok(),
         "Rust reference facts on kernel source arguments are valid"
     );
 
     let non_kernel = make_func(&mut ctx, false);
-    non_kernel.set_reference_param_validity(&mut ctx, 0, ReferenceParamValidityAttr(4));
+    non_kernel.set_reference_param_validity(&mut ctx, 0, ReferenceParamValidityAttr::new(4));
     assert!(
         non_kernel.verify(&ctx).is_err(),
         "reference validity is kernel-entry-only"
     );
 
     let raw = make_func(&mut ctx, true);
-    raw.set_reference_param_validity(&mut ctx, 2, ReferenceParamValidityAttr(4));
+    raw.set_reference_param_validity(&mut ctx, 2, ReferenceParamValidityAttr::new(4));
     assert!(
         raw.verify(&ctx).is_err(),
         "raw pointers cannot carry Rust-reference validity"
     );
 
     let scalar = make_func(&mut ctx, true);
-    scalar.set_reference_param_validity(&mut ctx, 3, ReferenceParamValidityAttr(4));
+    scalar.set_reference_param_validity(&mut ctx, 3, ReferenceParamValidityAttr::new(4));
     assert!(
         scalar.verify(&ctx).is_err(),
         "non-pointer parameters cannot carry Rust-reference validity"
     );
 
     let bad_alignment = make_func(&mut ctx, true);
-    bad_alignment.set_reference_param_validity(&mut ctx, 0, ReferenceParamValidityAttr(3));
+    bad_alignment.set_reference_param_validity(&mut ctx, 0, ReferenceParamValidityAttr::new(3));
     assert!(
         bad_alignment.verify(&ctx).is_err(),
         "alignment must be a non-zero power of two"
     );
 
     let out_of_range = make_func(&mut ctx, true);
-    out_of_range.set_reference_param_validity(&mut ctx, 9, ReferenceParamValidityAttr(4));
+    out_of_range.set_reference_param_validity(&mut ctx, 9, ReferenceParamValidityAttr::new(4));
     assert!(
         out_of_range.verify(&ctx).is_err(),
         "source argument index must be in range"

cuda-oxide/crates/llvm-export/src/export/function.rs

@@ -61,6 +61,30 @@ fn sanitize_comment(text: &str) -> String {
         .collect()
 }
 
+/// Spell only the facts already proven at the import boundary. Shared by
+/// definitions and declarations, including the empty-region declaration path.
+fn export_reference_parameter_attrs(
+    validity: ops::KernelReferenceParamValidityAttr,
+    include_alignment: bool,
+    output: &mut String,
+) {
+    write!(output, " nonnull").unwrap();
+    if validity.pointee_alignment > 1 && include_alignment {
+        write!(output, " align {}", validity.pointee_alignment).unwrap();
+    }
+    if validity.no_alias {
+        write!(output, " noalias").unwrap();
+    }
+    if validity.dereferenceable_bytes > 0 {
+        write!(
+            output,
+            " dereferenceable({})",
+            validity.dereferenceable_bytes
+        )
+        .unwrap();
+    }
+}
+
 /// Final LLVM spelling of a pliron function symbol.
 ///
 /// Shared-global owner attributes carry the raw symbol, so the module prepass,
@@ -799,7 +823,7 @@ impl<'a> ModuleExportState<'a> {
                     "kernel `@{fixed_func_name}` reference validity parameter {index} is not an LLVM pointer"
                 ));
             }
-            reference_param_validities[index] = Some(validity.0);
+            reference_param_validities[index] = Some(validity);
         }
 
         let is_declaration = func.get_operation().deref(self.ctx).regions().count() == 0;
@@ -975,11 +999,8 @@ impl<'a> ModuleExportState<'a> {
                 let grid_constant = grid_constant_params
                     .iter()
                     .find(|parameter| parameter.index == i);
-                if let Some(alignment) = reference_param_validities[i] {
-                    write!(output, " nonnull").unwrap();
-                    if alignment > 1 && grid_constant.is_none() {
-                        write!(output, " align {alignment}").unwrap();
-                    }
+                if let Some(validity) = reference_param_validities[i] {
+                    export_reference_parameter_attrs(validity, grid_constant.is_none(), output);
                 }
                 if let Some(parameter) = grid_constant {
                     self.export_grid_constant_parameter_attrs(
@@ -1046,15 +1067,9 @@ impl<'a> ModuleExportState<'a> {
             let block = entry_block.deref(self.ctx);
             let args = block.arguments();
             let mut entry_prologue = String::new();
-            // Kernel Rust references may carry importer-proven `nonnull` and
-            // pointee `align N`. Every other parameter remains bare.
-            //
-            // In particular this deliberately does NOT infer `noalias`,
-            // `readonly`, `dereferenceable`, or any validity fact from LLVM
-            // pointer shape. `DisjointSlice` and raw pointers therefore retain
-            // the conservative behavior required by their unsafe construction
-            // contracts. Future alias attributes need their own audited proof
-            // source rather than extending this mechanical export step.
+            // Kernel Rust references carry only importer-proven facts.
+            // LLVM pointer shape alone grants no reference promises, so raw
+            // pointers, slice metadata, and other parameters remain bare.
             for (i, arg) in args.enumerate() {
                 if i > 0 {
                     write!(output, ", ").unwrap();
@@ -1064,11 +1079,8 @@ impl<'a> ModuleExportState<'a> {
                 let grid_constant = grid_constant_params
                     .iter()
                     .find(|parameter| parameter.index == i);
-                if let Some(alignment) = reference_param_validities[i] {
-                    write!(output, " nonnull").unwrap();
-                    if alignment > 1 && grid_constant.is_none() {
-                        write!(output, " align {alignment}").unwrap();
-                    }
+                if let Some(validity) = reference_param_validities[i] {
+                    export_reference_parameter_attrs(validity, grid_constant.is_none(), output);
                 }
                 if let Some(parameter) = grid_constant {
                     self.export_grid_constant_parameter_attrs(
@@ -1409,11 +1421,8 @@ impl<'a> ModuleExportState<'a> {
                 let grid_constant = grid_constant_params
                     .iter()
                     .find(|parameter| parameter.index == i);
-                if let Some(alignment) = reference_param_validities[i] {
-                    write!(output, " nonnull").unwrap();
-                    if alignment > 1 && grid_constant.is_none() {
-                        write!(output, " align {alignment}").unwrap();
-                    }
+                if let Some(validity) = reference_param_validities[i] {
+                    export_reference_parameter_attrs(validity, grid_constant.is_none(), output);
                 }
                 if let Some(parameter) = grid_constant {
                     self.export_grid_constant_parameter_attrs(

cuda-oxide/crates/llvm-export/src/lib.rs

@@ -210,16 +210,31 @@ pub mod ops {
 
     /// Kernel-entry parameter validity proven at the Rust MIR import boundary.
     ///
-    /// Presence proves `nonnull`; the payload is the rustc ABI alignment of
-    /// the pointee represented by this physical LLVM parameter. It deliberately
-    /// carries no aliasing, readonly, or dereferenceability promise.
+    /// Presence proves `nonnull`; each field transports an independently
+    /// proven promise for this physical LLVM parameter. A zero byte count
+    /// records no dereferenceability promise.
     #[pliron_attr(
         name = "llvm.kernel_reference_param_validity",
-        format = "$0",
+        format,
         verifier = "succ"
     )]
     #[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
-    pub struct KernelReferenceParamValidityAttr(pub u64);
+    pub struct KernelReferenceParamValidityAttr {
+        pub pointee_alignment: u64,
+        pub no_alias: bool,
+        pub dereferenceable_bytes: u64,
+    }
+
+    impl KernelReferenceParamValidityAttr {
+        /// Non-nullness and alignment, without additional reference promises.
+        pub const fn new(pointee_alignment: u64) -> Self {
+            Self {
+                pointee_alignment,
+                no_alias: false,
+                dereferenceable_bytes: 0,
+            }
+        }
+    }
 
     fn kernel_reference_param_validity_key(index: usize) -> Identifier {
         Identifier::try_new(reserved_oxide_symbols::kernel_reference_param_validity_key(
@@ -271,10 +286,10 @@ pub mod ops {
                     "kernel reference parameter validity attribute `{key_text}` has the wrong attribute type"
                 ));
             };
-            if validity.0 == 0 || !validity.0.is_power_of_two() {
+            if validity.pointee_alignment == 0 || !validity.pointee_alignment.is_power_of_two() {
                 return Err(format!(
                     "kernel reference parameter {index} alignment must be a non-zero power of two, found {}",
-                    validity.0
+                    validity.pointee_alignment
                 ));
             }
             result.push((index, validity));