net/http go1.26.5: Prove that `http.Client` rewrites a POST to GET when automatically following a 303 response.

The first `search_known_solution` call reported a local hit for slow-body timeout behavior in `http.Client` (`case:sha256:8a3b9795afd5fed47a451d4a013163fc7764b661cf0e78c579edb91221b7c212`), so this sample uses a different trap.
A model that expects a 303 redirect to preserve the original POST method/body will produce the wrong assertion, because the follow-up request is automatically rewritten to `GET` with an empty body.

{"case":{"believed":"A POST request that receives a 303 See Other keeps its method and body through automatic redirect following.","caseId":"case:sha256:9d3c51dbc95b202c0d4566a999ad7cde43d4fb24e1c65644df82deab266a4808","contract":["A default client must follow `StatusSeeOther` (`303`) by issuing the next request as `GET`, not as the original method.","The follow-up request body from that redirect must be empty."],"goal":"Prove that `http.Client` rewrites a POST to GET when automatically following a 303 response.","kind":"HOW","packages":["pkg:golang/net/http@go1.26.5"],"schemaVersion":1,"symbols":["Client.CheckRedirect"]},"contractCommand":["go","test","./..."],"environment":{"arch":"x64","ecosystem":"golang","executionContext":"go","language":"go","os":"linux","packageManager":"golang","runtime":"go","schemaVersion":1},"license":"MIT-0","packages":["pkg:golang/net/http@go1.26.5"],"schemaVersion":1,"symbols":["Client.CheckRedirect"],"verifierAdapter":"golang@1"}

module redirecttest

go 1.26

package redirecttest

import (
	"io"
	"net/http"
	"net/http/httptest"
	"strings"
	"testing"
)

func TestSeeOtherRedirectRewritesPostToGet(t *testing.T) {
	mux := http.NewServeMux()
	var startMethod string
	var followMethod string
	var followBody []byte

	mux.HandleFunc("/start", func(w http.ResponseWriter, r *http.Request) {
		startMethod = r.Method
		w.Header().Set("Location", "/follow")
		w.WriteHeader(http.StatusSeeOther)
	})

	mux.HandleFunc("/follow", func(w http.ResponseWriter, r *http.Request) {
		followMethod = r.Method
		followBody, _ = io.ReadAll(r.Body)
		_ = r.Body.Close()
		_, _ = w.Write([]byte("followed"))
	})

	server := httptest.NewServer(mux)
	defer server.Close()

	resp, err := http.Post(server.URL+"/start", "text/plain", strings.NewReader("payload"))
	if err != nil {
		t.Fatalf("unexpected request error: %v", err)
	}
	defer resp.Body.Close()
	_, _ = io.Copy(io.Discard, resp.Body)

	if got := resp.StatusCode; got != http.StatusOK {
		t.Fatalf("expected final status 200, got %d", got)
	}
	if got := startMethod; got != http.MethodPost {
		t.Fatalf("expected start handler to receive POST, got %s", got)
	}
	if got := followMethod; got != http.MethodGet {
		t.Fatalf("expected redirected request to be rewritten to GET, got %s", got)
	}
	if len(followBody) != 0 {
		t.Fatalf("expected redirected request body to be empty, got %q", string(followBody))
	}
}