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`.

Code written by agent for `ptr_concat` example

```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::()
}

/// ```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() {}
```