// Copyright 2021 Ian Jackson and contributors
// SPDX-License-Identifier: GPL-3.0-or-later
// There is NO WARRANTY.

// Safety and soundness argument.
//
// Interleaved comments, added by hand to output from input.rs.
// Original input.rs output is in blank.rs.  Utilities and helper:
//
//  * `argument/check` checks that the output hasn't changed.
//  * `argument/merge` attempts to merge the code with the comments,
//     so you can check things are still true after editing derive.rs,
//     and resolve syntactic/semantic conflicts.
//  * `argument/argument-to-blank` overwrites blank.rs with a comment-
//    stripped version of argument.rs, for updating blank.rs if you have
//    edited the code in argument.rs (and, probably, also in derive.rs).

/// Safety / soundness!
///
/// This is repr(C) and F_a is always a ZST (for all of our methods),
/// so this is always a ZST and all of its members have the same
/// address.
///
/// We prevent safe code from ever having an owned Partial.
/// This is possible because we prevent them from ever having an
/// owned F_a, so they cannot construct one.
///
/// We never actually construct this type, just references to it.
/// That is OK because it is a ZST so it cannot have a wrong
/// representation, and it cannot have any aliasing problems (in SB
/// terms, &[mut] ZST doesn't affect any memory location stacks).
///
/// Invariant:
///
/// An &[mut] Partial *must* have the same memory address as some
/// Struct, from which it must have been borrowed (borrowck pov).
///
/// Additionally, the struct's address have been exposed as an integer,
/// so that we can magic up references to it.
/// There are no requirements on the provenance.
///
/// Multiple &[mut] Partial may exist, for the same Struct, provided
/// that the Pa are compatible (field-wise).  Pa: IsRefOrNot`)
/// Field-wise Pa compatibility is orthogonal to whether we have &mut
/// Partial or &Partial.

/// Use of integer/pointer cases
///
/// We use pointer/integer casting because the Rust Strict Proenance
/// experiment does not currently provide a method to pass nonempty
/// provenance spans with ZST references.
///
/// This could be better if Rust had a way to access functionality
/// similar to `__attribute__((cheri_no_subobject_bounds))`
/// in CHERI C/C++.  See p16 of the CHERI TR
///   https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-947.pdf#page=16
///
/// Relevant discussion here in the Rust Zulip (sadly, login required):
///   https://rust-lang.zulipchat.com/#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/strict.20provenance.20and.20partial-borrow
#[allow(dead_code)]
#[allow(non_camel_case_types)]
#[repr(C)]
pub struct Partial<Pa> {
  a: Module::F_a<Pa, String, Struct>,
}

/// Not relevant to safety.
impl PartialBorrow for Struct {
  type All_No = Partial<No>;
  type All_Const = Partial<Const>;
  type All_Mut = Partial<Mut>;
  type Fields = Module::Fields;
  const FIELDS: Self::Fields = Module::FIELDS;
}

#[allow(non_camel_case_types)]
impl<P, T> Deref for Module::F_a<P, T, Struct>
where
  P: IsRef,
{
  /// Safety!
  ///
  /// F_a has the same pointer value as Struct (see above).  We
  /// calculate the address of Struct.a, and synthesize a reference.
  ///
  /// Representation and alignment: this is actually the field a.
  ///
  /// Provenance: we convert an integer to a previously-exposed *Struct.
  type Target = T;

  /// Safety!
  ///
  /// Our signature ends up borrowing F from the Partial, which is in
  /// turn borrowed from the Struct, just as a normal field lookup
  /// would borrow F from the Struct.
  ///
  /// For the lifetime of this returned reference, no-one can have any
  /// other references to `a` that are incompatible with `f` (ie,
  /// mutable references):
  ///
  /// To do that via our machinery, they would need an &mut Partial
  /// with mutable access to `a`, but such a thing cannot exist other
  /// than as the one we reborrowed.
  ///
  /// We can rule out the notion that someone else would let them do
  /// that, because that someone else would have to have put a
  /// SharedReadWrite in the stack after s.  But someone who does
  /// that, and allows that SharedReadWrite to be used, could also be
  /// exploited using only ordinary field access.
  fn deref(&self) -> &T
  where
    T: Sized,
  {
    unsafe {
      let p: *const Self = self;
      let p: *const Struct = p as usize as _; // ptr::from_exposed
      let offset = offset_of!(Struct, a); // calculae offset of a:
      let p: *const u8 = p as _;          // no retag on ptr manip (SB 2.1)
      let p = p.add(offset);   // no retag on ptr manip (SB 2.1)
      let p: *const T = p as _;           // no retag on ptr manip (SB 2.1)
      // p now has provenance over the whole of Struct but points to the field
      let p: &T = p.as_ref().unwrap(); // retag, reborrow
      p
    }
  }
}

#[allow(non_camel_case_types)]
impl<P, T> DerefMut for Module::F_a<P, T, Struct>
where
  P: IsMut,
{
  /// Safety!
  /// 
  /// As with `Deref`, lifetime soundness prevents using us (or the
  /// original `Struct` to create incompatible referencess to `a`.
  fn deref_mut(&mut self) -> &mut T
  where
    // If &self is fat, this would all go horribly wrong
    T: Sized,
  {
    unsafe {
      let p: *mut Self = self;
      let p: *mut Struct = p as usize as _; // ptr::from_exposed
      let offset = offset_of!(Struct, a); // calculae offset of a:
      let p: *mut u8 = p as _;           // no retag on ptr manip (SB 2.1)
      let p = p.add(offset);  // no retag on ptr arith (SB 2.1)
      let p: *mut T = p as _;            // no retag on ptr manip (SB 2.1)
      // p now has provenance over the whole of Struct but points to the field
      let p: &mut T = p.as_mut().unwrap(); // retag, reborrow
      p
    }
  }
}

#[allow(non_camel_case_types)]
impl<P, T> Debug for Module::F_a<P, T, Struct>
where
  T: Debug,
  P: IsRefOrNot,
{
  /// Safety!
  ///
  /// We transmute &F_a<_P,_T,Struct> to &F_a<Const,_T,Struct> but only
  /// if the unsafe IsrefOrNot trait's REF is Some, ie it's actually
  /// a downgrade.
  ///
  /// Both of these are ZSTs, so the retag is fine and there is no reborrow.
  /// The lifetime is stated explicitly.
  
  fn fmt<'r>(&'r self, f: &mut Formatter) -> fmt::Result {
    if let Some(Const) = <P as IsRefOrNot>::REF {
      let downgraded = unsafe {
        transmute::<
          &'r Module::F_a<P, T, Struct>,
          &'r Module::F_a<Const, T, Struct>,
        >(self)
      };
      Debug::fmt(&**downgraded, f)
    } else {
      Formatter::write_str(f, "_")
    }
  }
}

#[allow(non_camel_case_types)]
impl<Pa, N> Adjust<N, 0usize> for Partial<Pa> {
  type Adjusted = Partial<N>;
}

#[allow(non_camel_case_types)]
impl<Ra, Pa> AsRef<Partial<Ra>> for Partial<Pa>
where
  Ra: IsDowngradeFrom<Pa>,
{
  /// No safety implications - uses Downgrade.
  fn as_ref(&self) -> &Partial<Ra> {
    Downgrade::downgrade(self)
  }
}

#[allow(non_camel_case_types)]
impl<Ra, Pa> AsMut<Partial<Ra>> for Partial<Pa>
where
  Ra: IsDowngradeFrom<Pa>,
{
  /// No safety implications - uses Downgrade.
  fn as_mut(&mut self) -> &mut Partial<Ra> {
    Downgrade::downgrade_mut(self)
  }
}

#[allow(non_camel_case_types)]
impl<Ra, Pa> Downgrade<Partial<Ra>> for Partial<Pa>
where
  Ra: IsDowngradeFrom<Pa>,
{
  /// Safety!
  ///
  /// We just convert the reference.  We end up retagging multiple
  /// times.  But each time it's a ZST, so there is no reborrow, and the
  /// retag is legal.  We don't care about the provenance of the result.
  ///
  /// The exposed-as-integer condition is satisfied for the result,
  /// because it must have been satisfied for the input.
  ///
  /// Creating a Partial reference is only sound if it is
  /// borrowed from something appropriate.  That is what
  /// IsDowngradeFrom<Mut> does.
  ///
  /// We permit downgrading from and to &Partial<Mut>.  The existence
  /// of such a thing is not troublesome (since you can't deref_mut
  /// its fields) and you might well have one, and you should be able to
  /// give it to someone who wants &Partial<Const>.
  ///
  /// The output lifetime is auto-inferred by the compiler,
  /// because of the signature of `downgrade`: the return value has to
  /// be borrowed from the input.

  fn downgrade(input: &Self) -> &Partial<Ra> {
    unsafe {
      let input = input as *const _;
      (input as *const Partial<Ra>).as_ref().unwrap()
    }
  }

  fn downgrade_mut(input: &mut Self) -> &mut Partial<Ra> {
    unsafe {
      let input = input as *mut _;
      (input as *mut Partial<Ra>).as_mut().unwrap()
    }
  }
}

#[allow(non_camel_case_types)]
impl<Ra, Pa> SplitOff<Partial<Ra>> for Partial<Pa>
where
  Ra: IsDowngradeFrom<Pa>,
{
  /// Safety!  See downgrade[_mut].
  ///
  /// Here, we give the user back the other half too.
  /// <Output as IsDowngradeFrom<Input>>::Remaining
  /// is what you have left if you had an Input ref
  /// and take an Output borrow of it.
  ///
  /// The transmute output lifetimes is specified to be the same as the
  /// input's lifetime, `'r`.

  type Remaining = Partial<<Ra as IsDowngradeFrom<Pa>>::Remaining>;

  fn split_off<'r>(
    input: &'r Partial<Pa>,
  ) -> (&'r Partial<Ra>, &'r Self::Remaining) {
    unsafe {
      let input = input as *const _;
      (
        (input as *const Partial<Ra>).as_ref().unwrap(),
        (input as *const Self::Remaining).as_ref().unwrap(),
      )
    }
  }

  fn split_off_mut<'r>(
    input: &'r mut Partial<Pa>,
  ) -> (&'r mut Partial<Ra>, &'r mut Self::Remaining) {
    unsafe {
      let input = input as *mut _;
      (
        (input as *mut Partial<Ra>).as_mut().unwrap(),
        (input as *mut Self::Remaining).as_mut().unwrap(),
      )
    }
  }
}

#[allow(non_camel_case_types)]
impl<'r, Ra, Sa, Pa> From<&'r Partial<Pa>>
  for (&'r Partial<Ra>, &'r Partial<Sa>)
where
  Pa: CanSplitInto<Ra, Sa>,
{
  /// No safety implications: uses SplitInto::split_into.
  fn from(input: &'r Partial<Pa>) -> Self {
    SplitInto::split_into(input)
  }
}

#[allow(non_camel_case_types)]
impl<'r, Ra, Sa, Pa> From<&'r mut Partial<Pa>>
  for (&'r mut Partial<Ra>, &'r mut Partial<Sa>)
where
  Pa: CanSplitInto<Ra, Sa>,
{
  fn from(input: &'r mut Partial<Pa>) -> Self {
    SplitInto::split_into_mut(input)
  }
}

#[allow(non_camel_case_types)]
impl<Ra, Sa, Pa> SplitInto<Partial<Ra>, Partial<Sa>> for Partial<Pa>
where
  Pa: CanSplitInto<Ra, Sa>,
{
  /// Safety!  See above.
  ///
  /// This can simultaneously split and downgrade each half.
  /// The borrowck rules are enforced by perms::CanSplitInto.
  ///
  /// Again, the inputs and outputs are all ZSTs so there is no SB effect.
  /// (again, the lifetimes borrow from the input)

  fn split_into<'r>(
    input: &'r Partial<Pa>,
  ) -> (&'r Partial<Ra>, &'r Partial<Sa>) {
    unsafe {
      let input = input as *const _;
      (
        (input as *const Partial<Ra>).as_ref().unwrap(),
        (input as *const Partial<Sa>).as_ref().unwrap(),
      )
    }
  }

  fn split_into_mut<'r>(
    input: &'r mut Partial<Pa>,
  ) -> (&'r mut Partial<Ra>, &'r mut Partial<Sa>) {
    unsafe {
      let input = input as *mut _;
      (
        (input as *mut Partial<Ra>).as_mut().unwrap(),
        (input as *mut Partial<Sa>).as_mut().unwrap(),
      )
    }
  }
}

#[allow(non_camel_case_types)]
impl<Ra> AsRef<Partial<Ra>> for Struct
where
  Ra: IsDowngradeFrom<Mut>,
{
  /// No safety implications.
  fn as_ref(&self) -> &Partial<Ra> {
    Downgrade::downgrade(self)
  }
}

#[allow(non_camel_case_types)]
impl<Ra> AsMut<Partial<Ra>> for Struct
where
  Ra: IsDowngradeFrom<Mut>,
{
  /// No safety implications.
  fn as_mut(&mut self) -> &mut Partial<Ra> {
    Downgrade::downgrade_mut(self)
  }
}

#[allow(non_camel_case_types)]
impl<Ra> Downgrade<Partial<Ra>> for Struct
where
  Ra: IsDowngradeFrom<Mut>,
{
  /// Safety!
  ///
  /// Calculating the address of the returned reference is straightforward
  /// and its provenance doesn't matter.  But we need to expose it.
  ///
  /// The partial borrowck soundness is straightforward; we require
  /// IsDowngradeFrom<Mut> since super::Struct is equivalent to
  /// Partial<Mut>.
  ///
  /// Aliasing: the output is a ZST, so this has no SB effect because
  /// we construct it directly.
  ///
  /// Lifetimes: the signature forces the output to be borrowed from
  /// the input, as before.

  fn downgrade(input: &Self) -> &Partial<Ra> {
    unsafe {
      let input = input as *const _ as usize; // expose
      (input as *const Partial<Ra>).as_ref().unwrap()
    }
  }

  fn downgrade_mut(input: &mut Self) -> &mut Partial<Ra> {
    unsafe {
      let input = input as *mut _ as usize; // expose
      (input as *mut Partial<Ra>).as_mut().unwrap()
    }
  }
}

#[allow(non_camel_case_types)]
impl<Ra> SplitOff<Partial<Ra>> for Struct
where
  Ra: IsDowngradeFrom<Mut>,
{
  /// Safety!
  ///
  /// See `Downgrade`.
  ///
  /// We return two references.  That the address is right is easy,
  /// and the provenance doesn't matter.  Both references
  /// must satisfy the addresses-exposed condition, but there's only
  /// one address to expose: the input address.
  ///
  /// Lifetimes: explicitly borrowed from the input, `'r` as before.

  type Remaining = Partial<<Ra as IsDowngradeFrom<Mut>>::Remaining>;

  fn split_off<'r>(
    input: &'r Struct,
  ) -> (&'r Partial<Ra>, &'r Self::Remaining) {
    unsafe {
      let input = input as *const _ as usize; // expose
      (
        (input as *const Partial<Ra>).as_ref().unwrap(),
        (input as *const Self::Remaining).as_ref().unwrap(),
      )
    }
  }

  /// Safety!  See above.
  fn split_off_mut<'r>(
    input: &'r mut Struct,
  ) -> (&'r mut Partial<Ra>, &'r mut Self::Remaining) {
    unsafe {
      let input = input as *mut _ as usize; // expose
      (
        (input as *mut Partial<Ra>).as_mut().unwrap(),
        (input as *mut Self::Remaining).as_mut().unwrap(),
      )
    }
  }
}

#[allow(non_camel_case_types)]
impl<'r, Ra, Sa> From<&'r Struct> for (&'r Partial<Ra>, &'r Partial<Sa>)
where
  Mut: CanSplitInto<Ra, Sa>,
{
  /// No safety implications.
  fn from(input: &'r Struct) -> Self {
    SplitInto::split_into(input)
  }
}

#[allow(non_camel_case_types)]
impl<'r, Ra, Sa> From<&'r mut Struct>
  for (&'r mut Partial<Ra>, &'r mut Partial<Sa>)
where
  Mut: CanSplitInto<Ra, Sa>,
{
  /// No safety implications.
  fn from(input: &'r mut Struct) -> Self {
    SplitInto::split_into_mut(input)
  }
}

#[allow(non_camel_case_types)]
impl<Ra, Sa> SplitInto<Partial<Ra>, Partial<Sa>> for Struct
where
  Mut: CanSplitInto<Ra, Sa>,
{
  /// Safety!
  ///
  /// This has the same SB and lifetime implications as the SplitOff impl.
  fn split_into<'r>(input: &'r Struct) -> (&'r Partial<Ra>, &'r Partial<Sa>) {
    unsafe {
      let input = input as *const _ as usize; // expose
      (
        (input as *const Partial<Ra>).as_ref().unwrap(),
        (input as *const Partial<Sa>).as_ref().unwrap(),
      )
    }
  }

  fn split_into_mut<'r>(
    input: &'r mut Struct,
  ) -> (&'r mut Partial<Ra>, &'r mut Partial<Sa>) {
    unsafe {
      let input = input as *mut _ as usize; // expose
      (
        (input as *mut Partial<Ra>).as_mut().unwrap(),
        (input as *mut Partial<Sa>).as_mut().unwrap(),
      )
    }
  }
}

#[allow(non_camel_case_types)]
impl<Pa> Deref for Partial<Pa>
where
  Pa: IsRef,
{
  type Target = Struct;

  /// Safety!
  ///
  /// This is similar to Deref from the SB soundness pov, and
  /// similar to Downgrade from a borrowck soundness pov.
  ///
  /// The lifetime is right: we do indeed borrow from the input.
  fn deref(&self) -> &Self::Target {
    unsafe {
      let p: *const Self = self as _;
      let p: *const Self::Target = p as usize as _; // ptr::from_exposed
      // p now has provenance over the whole of Struct
      let p = p.as_ref().unwrap();
      p
    }
  }
}

#[allow(non_camel_case_types)]
impl<Pa> Debug for Partial<Pa>
where
  Module::F_a<Pa, String, Struct>: Debug,
{
  /// No safety implications.
  fn fmt(&self, f: &mut Formatter) -> fmt::Result {
    let mut fields = Formatter::debug_struct(f, "Partial");
    fmt::DebugStruct::field(&mut fields, "a", &self.a);
    fields.finish()
  }
}

#[allow(dead_code)]
#[allow(non_camel_case_types)]
#[allow(non_snake_case)]
pub mod Module {
  use super::*;

  /// Safety / soundness!
  ///
  /// repr(C).  Must be a ZST.  This is enforced by all of our unsafe
  /// methods taking trait bounds which imply one of the unsafe traits
  /// in partial_borrow::perms, which are impl'd only for Mut Const No.
  /// (If you impl these unsafe traits yourself you get to keep the pieces.)
  ///
  /// Safe code can never have an owned F_a.  They cannot construct
  /// one, because the fields are all private.  The cannot clone one
  /// because it's not Clone (and they can't implement Clone manually
  /// because they'd have to construct one).
  ///
  /// In fact, an `F_a` is never constructed.  It only ever exists
  /// as a notion inside a Struct_Partial.  The compiler's struct
  /// projection will convert &[mut] Partial to &[mut] F_a.
  /// Those references are fine to construct because it's all ZST.
  ///
  /// So every &[mut] F_a has the same pointer value as its &[mut]
  /// Struct_Partial.  It is borrowed from that reference, which in
  /// turn has the same pointer and is borrowed from an original
  /// &[mut] Struct.
  ///
  /// The actual address has been exposed via pointer-to-integer
  /// cast, during initial conversion to a Partial.
  #[repr(C)]
  pub struct F_a<P, T, S> {
    p: P,
    t: PhantomData<T>,
    s: PhantomData<*const S>,
  }
  /// This is for partial!() and has no safety implications.
  pub struct Fields {
    pub a: usize,
  }
  pub const FIELDS: Fields = Fields { a: 0usize };
}