CBMC: Add proof for aws_string_new_from_buf

[GeorgiaGriffin]

Issue #, and/or reason for changes (REQUIRED):
aws_string_new_from_buf did not have a proof for CBMC verification.

Description of changes:
Create a proof harness for aws_string_new_from_buf. The proof verifies that the function returns a valid string given preconditions.

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

[Copilot]

Pull request overview

This PR adds a CBMC proof harness for the aws_string_new_from_buf function, which previously lacked formal verification. The proof verifies that the function correctly creates a valid string from a byte buffer.

Key changes:

• Adds proof harness with preconditions ensuring valid allocator and byte buffer
• Verifies postconditions: correct length, null termination, matching bytes, and string validity

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated 4 comments.

File	Description
verification/cbmc/proofs/aws_string_new_from_buf/cbmc-proof.txt	Marker file indicating the directory contains a CBMC proof
verification/cbmc/proofs/aws_string_new_from_buf/aws_string_new_from_buf_harness.c	Proof harness that verifies aws_string_new_from_buf returns a valid string with correct properties
verification/cbmc/proofs/aws_string_new_from_buf/Makefile	Build configuration for the CBMC proof, including necessary source files and dependencies

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.