Suggestions after agentic proof-authoring

*The following document was produced by a coding agent after attempting to autonomously author a specification and accompanying proof for the `ptr_concat` example. The code authored by the agent is at the bottom of this issue.*

# Reflections on Verifying `concat_slices` in Hermes

## What was difficult?

1.  **Understanding Aeneas WP Evaluation Unrolling:** Constructing the proofs, particularly `h_progress`, required manually stepping through the Weakest Precondition (WP) evaluation generated by Aeneas. It was initially non-obvious that each statement in the Rust function corresponds to a `bind` operation that must be individually resolved using `Aeneas.Std.WP.spec_imp_exists` and `Aeneas.Std.bind_tc_ok` to extract the resulting value, the evaluation step, and the postcondition bundle.
2.  **Lean 4 Macro Hygiene:** When attempting to DRY (Don't Repeat Yourself) the repetitive WP unwrapping code across the five proof blocks (`h_ret_alloc`, `h_ret_address`, `h_ret_metadata`, `h_ret_addresses`, and `h_progress`), I ran into strict Lean 4 macro hygiene rules. Variables defined inside a `macro` (like `have ⟨a_len, h_eval_a, h_post_a⟩ := ...`) are hygienic by default, making them inaccessible by name in the trailing tactics outside the macro expansion. This entirely blocked the macro-based refactoring approach.
3.  **Strict Linter Constraints (`linter.unusedSimpArgs`):** Hermes runs Lean with strict linters enabled, converting warnings into hard verification errors. The unused `simp` arguments linter was surprisingly strict, punishing the use of broadly applicable `simp_all [h_post_add, h_post_a.h_unnamed, ...]` if a specific branch happened to not require one of the provided theorems. This necessitated carefully curating the variables provided to `simp` or relying purely on implicit local context state.
4.  **Hermes Syntax and Rustdoc Coalescing:** Trying to define a global `context:` macro block was tricky because Rustdoc merges adjacent `///` comments. Attaching the `context:` block to a dummy `struct` failed because Hermes expects a type invariant (`isValid`) for struct-based specs. Resolving this required discovering the dummy `fn` workaround, which was non-intuitive.

## What I wish I had known going in

1.  **The exact structure of Aeneas WP monads:** A clearer upfront picture of how Aeneas translates let-bindings into monadic `bind` sequences, and the exact incantations required to peel them back (`WP.spec_imp_exists` + `bind_tc_ok`), would have drastically reduced the time spent reverse-engineering the proof state.
2.  **The rigidity of Lean's local namespaces (Hygiene):** Knowing that declarative macros effectively hide their bindings would have steered me away from the `macro` refactor attempt much earlier. I would have instead immediately pursued the native "re-inject fields into unbound context" approach, saving significant debugging effort.
3.  **The strictness of `simp_all`:** I wish I had known about the `unusedSimpArgs` linter from the start. I would have avoided the pattern of indiscriminately throwing available hypotheses into `simp_all [...]` brackets and instead relied on `have _ := ...` to inject variables into the local context for implicit discovery.
4.  **The relationship between `IsContiguous` and `bounds`:** Realizing earlier that `h_contiguous` allows seamless mapping between `x ∈ referent.addresses` and simple arithmetic bounds queries (`a.address.val ≤ x < a.address.val + a.size.val`) via `referent.bounds x hx` completely trivialized the `h_ret_alloc` and `h_ret_addresses` subset/union set logic.
## Proposed Hermes Design Improvements

Based on the friction encountered during the verification of `concat_slices`, the following changes to Hermes's design and tooling are proposed:

### 1. Dedicated WP Unrolling Magic/Tactic
Currently, users are forced to manually apply `Aeneas.Std.WP.spec_imp_exists` followed by `Aeneas.Std.bind_tc_ok` for every single line of a Rust function to evaluate the monadic WP state. 
- **Improvement:** Introduce a high-level Lean tactic strictly for Hermes (e.g., `eval_next` or `step_wp`) that automatically peels off the next sequential `bind` operation in the current WP goal, intelligently unifies the returned `ok` value, and dynamically injects the `post` struct fields directly into the local context. This would entirely eliminate the massive `have ⟨val, eval, post⟩ := ...` boilerplate that clutters every single proof in Hermes.

### 2. Relaxing/Contextualizing Linter Strictness
The `linter.unusedSimpArgs` error is incredibly antagonistic when trying to build reusable proof patterns across different branches identically (e.g., using `simp_all` generically).
- **Improvement:** Expose an `#[allow(unused_simp)]` attribute equivalent in the Hermes doc blocks to locally suppress unused simplification warnings on a per-proof or per-function basis without disabling it globally. Alternatively, Hermes could automatically inject `set_option linter.unusedSimpArgs false` when translating the monolithic `simp_all` blocks during generation.

### 3. File-Level Declarations
Defining shared types, lemmas, and macros meant for an entire file (like `eval_concat_slices`) currently requires the hack of attaching them to a dummy `fn _hermes_host() {}` since attaching to structs requires an `isValid` invariant, and standalone `///` doc comments are merged by the Rust compiler.
- **Improvement:** Allow a `#![hermes::context]` inner attribute syntax at the very top of a Rust file to define global Lean definitions unconditionally.

### 4. Structuring WP Postcondition Tuples
Presently, WP postconditions (`post_a.h_unnamed`) hide tightly inside structs with generated generic names.
- **Improvement:** When Aeneas drops variable execution bindings into Lean, Hermes could intercept the post conditions and unpack the structural fields (like `ret_size` or `ret_addr`) into immediate local context definitions with predictable names derived from the original Rust variables (e.g., `h_post_a_unnamed`). This would prevent developers from having to manually un-nest `have _h_size := h_post.h_size` just to appease the `omega` solver.

## Proposed Features for Hermes

To make verifications like `concat_slices` significantly easier next time, here are proposed feature additions for the Hermes tool and standard library:

### 1. Pointer and Slice Set Theory Helpers (Standard Library)
Proving the `addresses` subset and union logic manually via `x < a.address.val + a.size.val` is tedious.
- **Feature Addition:** Add a module to the standard library (e.g., `Hermes.Std.SetLogic`) that provides high-level theorems for mapping `IsContiguous` array arithmetic into native Set (`∪`, `∩`, `⊂`) operations. For example, a lemma `contiguous_union_adjacent` that automatically proves that two adjacent, contiguous referents form a union of addresses that matches the concatenated bounds.

### 2. Automated WP Progress Solver Tactic (Standard Library)
The manual unrolling of `Aeneas.Std.WP.spec_imp_exists` dominates the file.
- **Feature Addition:** Provide a powerful `wp_unroll` or `step_wp` macro/tactic in the standard library. This tactic would automatically peel off the next Weakest Precondition `bind`, resolve the `ok` state via `Aeneas.Std.bind_tc_ok`, and advance the proof state recursively until the function returns.

### 3. Tactic for Unpacking Post-Condition Structs (Standard Library)
Hygiene and nested bounds properties make variables invisible to `simp_all` and `omega`.
- **Feature Addition:** Add an `unpack_struct h_post` Lean tactic to the standard library that uses reflection to automatically generate `have _val := h_post.field_name` bindings in the local, unbound context for every field inside a postcondition struct. This eliminates the manual injection boilerplate completely.

### 4. Auto-generation of `h_progress` (Tool Feature)
For simple sequence blocks like `concat_slices` that don't entail loops or recursive calls, the `h_progress` proof is entirely mechanical (just stepping through non-panicking mathematical additions and valid pointer casts).
- **Current Limitation:** Hermes's auto-generated `h_progress` previously relied solely on `exact ⟨_, rfl⟩`. We improved this by implementing a generic macro (`eval_progress`) that uses `all_goals (try ...)` and `progress` with `omega` fallbacks, along with emitting `@[progress]` on all generated specs. This robust automation successfully handles simple bounds and nested functions (like in `toy_progress.rs`). However, for complex functions like `concat_slices`, the mathematical bounds (like array lengths extracted from `slice_len`) are obfuscated inside generated `Post` structs. The generic `progress` solver cannot automatically associate these opaque `Post` bounds with the top-level structural `Pre` requirements, meaning manual proofs of progress remain necessary for any function involving non-trivial precondition threading.
- **Feature Addition:** To fully automate `h_progress` for complex pointer arithmetic, Hermes would need to automatically insert the structural preconditions and postconditions of each inner call directly into the active solver context, or provide a tactic to explicitly unpack `Post` constraints before invoking math solvers like `omega`.

<details><summary>Code written by agent for `ptr_concat` example</summary>

```rust
//! This example exists as a test for agents to see how well they can
//! automatically write and prove Hermes specifications.

/// ```lean, hermes, unsafe(axiom)
/// ensures: ret = Hermes.HasMetadata.metadata data
/// ```
pub const unsafe fn slice_len(data: *const [u8]) -> usize {
    data.len()
}

/// ```lean, hermes, unsafe(axiom)
/// ensures: (Hermes.HasReferent.referent ret).address = (Hermes.HasReferent.referent data).address
/// ```
pub const unsafe fn cast_slice_to_u8(data: *const [u8]) -> *const u8 {
    data.cast::<u8>()
}

/// ```lean, hermes, unsafe(axiom)
/// requires (h_isize): len.val ≤ Isize.max
/// ensures (h_addr): (Hermes.HasReferent.referent ret).address = (Hermes.HasReferent.referent data).address
/// ensures (h_len): Hermes.HasMetadata.metadata ret = len
/// ensures (h_size): (Hermes.HasReferent.referent ret).size = len
/// ensures (h_contiguous): (Hermes.HasReferent.referent ret).IsContiguous
/// ```
pub const unsafe fn slice_from_slice_parts(data: *const u8, len: usize) -> *const [u8] {
    core::ptr::slice_from_raw_parts(data, len)
}

/// TODO:
/// - Require that both referents live in the same allocation
/// - Require that both referents are contiguous and non-overlapping
/// - Ensure that the returned referent is the concatenation of the two input referents
/// - Ensure that the returned referent lives in the same allocation as the input referents
///
/// ```lean, hermes, spec
/// requires (h_alloc):
///   ∃ alloc, Hermes.FitsInAllocation (Hermes.HasReferent.referent a) alloc ∧ Hermes.FitsInAllocation (Hermes.HasReferent.referent b) alloc
/// requires (h_contiguous_a):
///   (Hermes.HasReferent.referent a).IsContiguous
/// requires (h_contiguous_b):
///   (Hermes.HasReferent.referent b).IsContiguous
/// requires (h_adjacent):
///   (Hermes.HasReferent.referent b).address.val = (Hermes.HasReferent.referent a).address.val + (Hermes.HasReferent.referent a).size.val
/// requires (h_size_a):
///   (Hermes.HasReferent.referent a).size.val = (Hermes.HasMetadata.metadata a).val
/// requires (h_size_b):
///   (Hermes.HasReferent.referent b).size.val = (Hermes.HasMetadata.metadata b).val
/// requires (h_meta_bounds_isize):
///   (Hermes.HasMetadata.metadata a).val + (Hermes.HasMetadata.metadata b).val <= Isize.max
/// requires (h_meta_bounds_usize):
///   (Hermes.HasMetadata.metadata a).val + (Hermes.HasMetadata.metadata b).val <= Aeneas.Std.Usize.max
/// ensures (h_ret_alloc):
///   ∃ alloc, Hermes.FitsInAllocation (Hermes.HasReferent.referent ret) alloc
/// ensures (h_ret_address):
///   (Hermes.HasReferent.referent ret).address = (Hermes.HasReferent.referent a).address
/// ensures (h_ret_metadata):
///   (Hermes.HasMetadata.metadata ret).val = (Hermes.HasMetadata.metadata a).val + (Hermes.HasMetadata.metadata b).val
/// ensures (h_ret_addresses):
///   (Hermes.HasReferent.referent ret).addresses = (Hermes.HasReferent.referent a).addresses ∪ (Hermes.HasReferent.referent b).addresses
/// proof (h_ret_alloc):
///   rcases h_alloc with ⟨alloc, h_alloc_a, h_alloc_b⟩
///   unfold concat_slices at h_returns
///   have ⟨a_len, h_eval_a, h_post_a⟩ := Aeneas.Std.WP.spec_imp_exists (slice_len.spec a { h_data_is_valid := h_a_is_valid })
///   simp [h_eval_a, Aeneas.Std.bind_tc_ok] at h_returns
///   have ⟨b_len, h_eval_b, h_post_b⟩ := Aeneas.Std.WP.spec_imp_exists (slice_len.spec b { h_data_is_valid := h_b_is_valid })
///   simp [h_eval_b, Aeneas.Std.bind_tc_ok] at h_returns
///   have h_add : a_len.val + b_len.val ≤ Aeneas.Std.Usize.max := by
///     simp_all [h_post_a.h_unnamed, h_post_b.h_unnamed]
///   have ⟨total_len, h_eval_add, h_post_add⟩ := Aeneas.Std.WP.spec_imp_exists (Aeneas.Std.Usize.add_spec h_add)
///   simp [h_eval_add, Aeneas.Std.bind_tc_ok] at h_returns
///   have ⟨ptr, h_eval_ptr, h_post_ptr⟩ := Aeneas.Std.WP.spec_imp_exists (cast_slice_to_u8.spec a { h_data_is_valid := h_a_is_valid })
///   simp [h_eval_ptr, Aeneas.Std.bind_tc_ok] at h_returns
///   have h_ptr_valid : Hermes.IsValid.isValid ptr := h_post_ptr.h_ret_is_valid
///   have h_total_len_valid : Hermes.IsValid.isValid total_len := by simp_all [Hermes.IsValid.isValid]
///   have h_total_len_isize : total_len.val ≤ Isize.max := by simp_all [h_post_a.h_unnamed, h_post_b.h_unnamed]
///   have ⟨ret_slice, h_eval_ret, h_post_ret⟩ := Aeneas.Std.WP.spec_imp_exists (slice_from_slice_parts.spec ptr total_len { h_data_is_valid := h_ptr_valid, h_len_is_valid := h_total_len_valid, h_isize := h_total_len_isize })
///   simp [h_eval_ret] at h_returns
///   have _h_a_len := h_post_a.h_unnamed
///   have _h_b_len := h_post_b.h_unnamed
///   have _h_ptr_addr := h_post_ptr.h_unnamed
///   have _h_ret_addr := h_post_ret.h_addr
///   have _h_ret_len := h_post_ret.h_len
///   have _h_ret_size := h_post_ret.h_size
///   have _h_ret_contiguous := h_post_ret.h_contiguous
///   have h_ret_eq : ret = ret_slice := by simp_all
///   subst h_ret_eq
///   exists alloc
///   rcases h_alloc_a with ⟨h_alloc_a_subset, h_alloc_a_base, h_alloc_a_end⟩
///   rcases h_alloc_b with ⟨h_alloc_b_subset, h_alloc_b_base, h_alloc_b_end⟩
///   refine ⟨?subset, ?base, ?end_bound⟩
///   case subset =>
///     intro x hx
///     have h_bound := (Hermes.HasReferent.referent ret).bounds x hx
///     by_cases h : x < (Hermes.HasReferent.referent a).address.val + (Hermes.HasReferent.referent a).size.val
///     · have hx_in_a : x ∈ (Hermes.HasReferent.referent a).addresses := by
///         apply h_contiguous_a
///         simp_all [h_post_a.h_unnamed, h_post_b.h_unnamed]
///       exact h_alloc_a_subset hx_in_a
///     · have hx_in_b : x ∈ (Hermes.HasReferent.referent b).addresses := by
///         apply h_contiguous_b
///         simp_all [h_post_a.h_unnamed, h_post_b.h_unnamed]
///         omega
///       exact h_alloc_b_subset hx_in_b
///   case base =>
///     simp_all
///   case end_bound =>
///     simp_all [h_post_a.h_unnamed, h_post_b.h_unnamed]; omega
/// proof (h_ret_address):
///   unfold concat_slices at h_returns
///   have ⟨a_len, h_eval_a, h_post_a⟩ := Aeneas.Std.WP.spec_imp_exists (slice_len.spec a { h_data_is_valid := h_a_is_valid })
///   simp [h_eval_a, Aeneas.Std.bind_tc_ok] at h_returns
///   have ⟨b_len, h_eval_b, h_post_b⟩ := Aeneas.Std.WP.spec_imp_exists (slice_len.spec b { h_data_is_valid := h_b_is_valid })
///   simp [h_eval_b, Aeneas.Std.bind_tc_ok] at h_returns
///   have h_add : a_len.val + b_len.val ≤ Aeneas.Std.Usize.max := by
///     simp_all [h_post_a.h_unnamed, h_post_b.h_unnamed]
///   have ⟨total_len, h_eval_add, h_post_add⟩ := Aeneas.Std.WP.spec_imp_exists (Aeneas.Std.Usize.add_spec h_add)
///   simp [h_eval_add, Aeneas.Std.bind_tc_ok] at h_returns
///   have ⟨ptr, h_eval_ptr, h_post_ptr⟩ := Aeneas.Std.WP.spec_imp_exists (cast_slice_to_u8.spec a { h_data_is_valid := h_a_is_valid })
///   simp [h_eval_ptr, Aeneas.Std.bind_tc_ok] at h_returns
///   have h_ptr_valid : Hermes.IsValid.isValid ptr := h_post_ptr.h_ret_is_valid
///   have h_total_len_valid : Hermes.IsValid.isValid total_len := by simp_all [Hermes.IsValid.isValid]
///   have h_total_len_isize : total_len.val ≤ Isize.max := by simp_all [h_post_a.h_unnamed, h_post_b.h_unnamed]
///   have ⟨ret_slice, h_eval_ret, h_post_ret⟩ := Aeneas.Std.WP.spec_imp_exists (slice_from_slice_parts.spec ptr total_len { h_data_is_valid := h_ptr_valid, h_len_is_valid := h_total_len_valid, h_isize := h_total_len_isize })
///   simp [h_eval_ret] at h_returns
///   have _h_a_len := h_post_a.h_unnamed
///   have _h_b_len := h_post_b.h_unnamed
///   have _h_ptr_addr := h_post_ptr.h_unnamed
///   have _h_ret_addr := h_post_ret.h_addr
///   have _h_ret_len := h_post_ret.h_len
///   have _h_ret_size := h_post_ret.h_size
///   have _h_ret_contiguous := h_post_ret.h_contiguous
///   have h_ret_eq : ret = ret_slice := by simp_all
///   subst h_ret_eq
///   simp_all
/// proof (h_ret_metadata):
///   unfold concat_slices at h_returns
///   have ⟨a_len, h_eval_a, h_post_a⟩ := Aeneas.Std.WP.spec_imp_exists (slice_len.spec a { h_data_is_valid := h_a_is_valid })
///   simp [h_eval_a, Aeneas.Std.bind_tc_ok] at h_returns
///   have ⟨b_len, h_eval_b, h_post_b⟩ := Aeneas.Std.WP.spec_imp_exists (slice_len.spec b { h_data_is_valid := h_b_is_valid })
///   simp [h_eval_b, Aeneas.Std.bind_tc_ok] at h_returns
///   have h_add : a_len.val + b_len.val ≤ Aeneas.Std.Usize.max := by
///     simp_all [h_post_a.h_unnamed, h_post_b.h_unnamed]
///   have ⟨total_len, h_eval_add, h_post_add⟩ := Aeneas.Std.WP.spec_imp_exists (Aeneas.Std.Usize.add_spec h_add)
///   simp [h_eval_add, Aeneas.Std.bind_tc_ok] at h_returns
///   have ⟨ptr, h_eval_ptr, h_post_ptr⟩ := Aeneas.Std.WP.spec_imp_exists (cast_slice_to_u8.spec a { h_data_is_valid := h_a_is_valid })
///   simp [h_eval_ptr, Aeneas.Std.bind_tc_ok] at h_returns
///   have h_ptr_valid : Hermes.IsValid.isValid ptr := h_post_ptr.h_ret_is_valid
///   have h_total_len_valid : Hermes.IsValid.isValid total_len := by simp_all [Hermes.IsValid.isValid]
///   have h_total_len_isize : total_len.val ≤ Isize.max := by simp_all [h_post_a.h_unnamed, h_post_b.h_unnamed]
///   have ⟨ret_slice, h_eval_ret, h_post_ret⟩ := Aeneas.Std.WP.spec_imp_exists (slice_from_slice_parts.spec ptr total_len { h_data_is_valid := h_ptr_valid, h_len_is_valid := h_total_len_valid, h_isize := h_total_len_isize })
///   simp [h_eval_ret] at h_returns
///   have _h_a_len := h_post_a.h_unnamed
///   have _h_b_len := h_post_b.h_unnamed
///   have _h_ptr_addr := h_post_ptr.h_unnamed
///   have _h_ret_addr := h_post_ret.h_addr
///   have _h_ret_len := h_post_ret.h_len
///   have _h_ret_size := h_post_ret.h_size
///   have _h_ret_contiguous := h_post_ret.h_contiguous
///   have h_ret_eq : ret = ret_slice := by simp_all
///   subst h_ret_eq
///   simp_all [h_post_a.h_unnamed, h_post_b.h_unnamed]
/// proof (h_ret_addresses):
///   unfold concat_slices at h_returns
///   have ⟨a_len, h_eval_a, h_post_a⟩ := Aeneas.Std.WP.spec_imp_exists (slice_len.spec a { h_data_is_valid := h_a_is_valid })
///   simp [h_eval_a, Aeneas.Std.bind_tc_ok] at h_returns
///   have ⟨b_len, h_eval_b, h_post_b⟩ := Aeneas.Std.WP.spec_imp_exists (slice_len.spec b { h_data_is_valid := h_b_is_valid })
///   simp [h_eval_b, Aeneas.Std.bind_tc_ok] at h_returns
///   have h_add : a_len.val + b_len.val ≤ Aeneas.Std.Usize.max := by
///     simp_all [h_post_a.h_unnamed, h_post_b.h_unnamed]
///   have ⟨total_len, h_eval_add, h_post_add⟩ := Aeneas.Std.WP.spec_imp_exists (Aeneas.Std.Usize.add_spec h_add)
///   simp [h_eval_add, Aeneas.Std.bind_tc_ok] at h_returns
///   have ⟨ptr, h_eval_ptr, h_post_ptr⟩ := Aeneas.Std.WP.spec_imp_exists (cast_slice_to_u8.spec a { h_data_is_valid := h_a_is_valid })
///   simp [h_eval_ptr, Aeneas.Std.bind_tc_ok] at h_returns
///   have h_ptr_valid : Hermes.IsValid.isValid ptr := h_post_ptr.h_ret_is_valid
///   have h_total_len_valid : Hermes.IsValid.isValid total_len := by simp_all [Hermes.IsValid.isValid]
///   have h_total_len_isize : total_len.val ≤ Isize.max := by simp_all [h_post_a.h_unnamed, h_post_b.h_unnamed]
///   have ⟨ret_slice, h_eval_ret, h_post_ret⟩ := Aeneas.Std.WP.spec_imp_exists (slice_from_slice_parts.spec ptr total_len { h_data_is_valid := h_ptr_valid, h_len_is_valid := h_total_len_valid, h_isize := h_total_len_isize })
///   simp [h_eval_ret] at h_returns
///   have _h_a_len := h_post_a.h_unnamed
///   have _h_b_len := h_post_b.h_unnamed
///   have _h_ptr_addr := h_post_ptr.h_unnamed
///   have _h_ret_addr := h_post_ret.h_addr
///   have _h_ret_len := h_post_ret.h_len
///   have _h_ret_size := h_post_ret.h_size
///   have _h_ret_contiguous := h_post_ret.h_contiguous
///   have h_ret_eq : ret = ret_slice := by simp_all
///   subst h_ret_eq
///   have h_ret_contiguous := h_post_ret.h_contiguous
///   ext x
///   simp only [Set.mem_union]
///   constructor
///   · intro hx
///     have h_bound := (Hermes.HasReferent.referent ret).bounds x hx
///     by_cases h : x < (Hermes.HasReferent.referent a).address.val + (Hermes.HasReferent.referent a).size.val
///     · left
///       apply h_contiguous_a
///       simp_all [h_post_a.h_unnamed, h_post_b.h_unnamed]
///     · right
///       apply h_contiguous_b
///       simp_all [h_post_a.h_unnamed, h_post_b.h_unnamed]
///       omega
///   · intro hx
///     rcases hx with hx_a | hx_b
///     · have h_bound := (Hermes.HasReferent.referent a).bounds x hx_a
///       apply h_ret_contiguous
///       simp_all [h_post_a.h_unnamed, h_post_b.h_unnamed]
///       omega
///     · have h_bound := (Hermes.HasReferent.referent b).bounds x hx_b
///       apply h_ret_contiguous
///       simp_all [h_post_a.h_unnamed, h_post_b.h_unnamed]; omega
/// proof (h_progress):
///   unfold concat_slices
///   rcases h_req with ⟨h_a_is_valid, h_b_is_valid, _, _, _, _, _, _, h_meta_bounds_isize, _⟩
///   have ⟨a_len, h_eval_a, h_post_a⟩ := Aeneas.Std.WP.spec_imp_exists (slice_len.spec a { h_data_is_valid := h_a_is_valid })
///   simp [h_eval_a, Aeneas.Std.bind_tc_ok]
///   have ⟨b_len, h_eval_b, h_post_b⟩ := Aeneas.Std.WP.spec_imp_exists (slice_len.spec b { h_data_is_valid := h_b_is_valid })
///   simp [h_eval_b, Aeneas.Std.bind_tc_ok]
///   have h_add : a_len.val + b_len.val ≤ Aeneas.Std.Usize.max := by
///     simp_all [h_post_a.h_unnamed, h_post_b.h_unnamed]
///   have ⟨total_len, h_eval_add, h_post_add⟩ := Aeneas.Std.WP.spec_imp_exists (Aeneas.Std.Usize.add_spec h_add)
///   simp [h_eval_add, Aeneas.Std.bind_tc_ok]
///   have ⟨ptr, h_eval_ptr, h_post_ptr⟩ := Aeneas.Std.WP.spec_imp_exists (cast_slice_to_u8.spec a { h_data_is_valid := h_a_is_valid })
///   simp [h_eval_ptr, Aeneas.Std.bind_tc_ok]
///   have h_ptr_valid : Hermes.IsValid.isValid ptr := h_post_ptr.h_ret_is_valid
///   have h_total_len_valid : Hermes.IsValid.isValid total_len := by simp_all [Hermes.IsValid.isValid]
///   have h_total_len_isize : total_len.val ≤ Isize.max := by simp_all [h_post_a.h_unnamed, h_post_b.h_unnamed]
///   have ⟨ret_slice, h_eval_ret, h_post_ret⟩ := Aeneas.Std.WP.spec_imp_exists (slice_from_slice_parts.spec ptr total_len { h_data_is_valid := h_ptr_valid, h_len_is_valid := h_total_len_valid, h_isize := h_total_len_isize })
///   simp [h_eval_ret]
/// ```
pub unsafe fn concat_slices(a: *const [u8], b: *const [u8]) -> *const [u8] {
    let a_len = slice_len(a);
    let b_len = slice_len(b);
    let total_len = a_len + b_len;
    let ptr = cast_slice_to_u8(a);
    slice_from_slice_parts(ptr, total_len)
}

fn main() {}
```

</details> 

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Suggestions after agentic proof-authoring #3102

Reflections on Verifying `concat_slices` in Hermes

What was difficult?

What I wish I had known going in

Proposed Hermes Design Improvements

1. Dedicated WP Unrolling Magic/Tactic

2. Relaxing/Contextualizing Linter Strictness

3. File-Level Declarations

4. Structuring WP Postcondition Tuples

Proposed Features for Hermes

1. Pointer and Slice Set Theory Helpers (Standard Library)

2. Automated WP Progress Solver Tactic (Standard Library)

3. Tactic for Unpacking Post-Condition Structs (Standard Library)

4. Auto-generation of `h_progress` (Tool Feature)

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Suggestions after agentic proof-authoring #3102

Description

Reflections on Verifying concat_slices in Hermes

What was difficult?

What I wish I had known going in

Proposed Hermes Design Improvements

1. Dedicated WP Unrolling Magic/Tactic

2. Relaxing/Contextualizing Linter Strictness

3. File-Level Declarations

4. Structuring WP Postcondition Tuples

Proposed Features for Hermes

1. Pointer and Slice Set Theory Helpers (Standard Library)

2. Automated WP Progress Solver Tactic (Standard Library)

3. Tactic for Unpacking Post-Condition Structs (Standard Library)

4. Auto-generation of h_progress (Tool Feature)

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

Reflections on Verifying `concat_slices` in Hermes

4. Auto-generation of `h_progress` (Tool Feature)