impl Debug/Default for Tracked

[ziqiaozhou]

Add Debug and Default Trait for Tracked, so that a struct with derived Debug/Default can use Tracked field.

I have used some tracked variable in struct that implements Debug and Default. If I do not implement Debug and Default for Tracked, I will not be able to pass lifetime checker.

tracked struct P {
   no_copy: NoCopy,
}
#[derive(Debug, Default)]
struct X {
    x: [usize; 16],
    #[cfg(verus_keep_ghost_body)]
    y: Tracked<Map<int, P>>,
}

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[tjhance]

The Default implementation for Tracked<A> will allow the user to forge tracked tokens.

[ziqiaozhou]

The Default implementation for Tracked<A> will allow the user to forge tracked tokens.

Thanks for the comment. That is true. I removed the default. I think I can avoid using default trait.